[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝¹ : IsPreorder α r
inst✝ : Inhabited α
⊢ Inhabited (Antisymmetrization α r)
[PROOFSTEP]
unfold Antisymmetrization
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝¹ : IsPreorder α r
inst✝ : Inhabited α
⊢ Inhabited (Quotient (AntisymmRel.setoid α r))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
⊢ Relation.Fibration (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (toAntisymmetrization fun x x_1 => x ≤ x_1)
[PROOFSTEP]
rintro a ⟨b⟩ h
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ b✝¹ a : α
b✝ : Antisymmetrization α fun x x_1 => x ≤ x_1
b : α
h : Quot.mk Setoid.r b < toAntisymmetrization (fun x x_1 => x ≤ x_1) a
⊢ ∃ a', (fun x x_1 => x < x_1) a' a ∧ toAntisymmetrization (fun x x_1 => x ≤ x_1) a' = Quot.mk Setoid.r b
[PROOFSTEP]
exact ⟨b, h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝¹ b : α
a✝ : (Antisymmetrization α fun x x_1 => x ≤ x_1)ᵒᵈ
a : α
⊢ Quotient.map' id
      (_ :
        ∀ (x x_1 : αᵒᵈ),
          (fun x x_2 => x ≤ x_2) x x_1 ∧ (fun x x_2 => x ≤ x_2) x_1 x →
            (fun x x_2 => x ≤ x_2) x_1 x ∧ (fun x x_2 => x ≤ x_2) x x_1)
      (Quotient.map' id
        (_ :
          ∀ (x x_1 : α),
            (fun x x_2 => x ≤ x_2) x x_1 ∧ (fun x x_2 => x ≤ x_2) x_1 x →
              (fun x x_2 => x ≤ x_2) x_1 x ∧ (fun x x_2 => x ≤ x_2) x x_1)
        (Quotient.mk'' a)) =
    Quotient.mk'' a
[PROOFSTEP]
simp_rw [Quotient.map'_mk'', id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝¹ b : α
a✝ : Antisymmetrization αᵒᵈ fun x x_1 => x ≤ x_1
a : αᵒᵈ
⊢ Quotient.map' id
      (_ :
        ∀ (x x_1 : α),
          (fun x x_2 => x ≤ x_2) x x_1 ∧ (fun x x_2 => x ≤ x_2) x_1 x →
            (fun x x_2 => x ≤ x_2) x_1 x ∧ (fun x x_2 => x ≤ x_2) x x_1)
      (Quotient.map' id
        (_ :
          ∀ (x x_1 : αᵒᵈ),
            (fun x x_2 => x ≤ x_2) x x_1 ∧ (fun x x_2 => x ≤ x_2) x_1 x →
              (fun x x_2 => x ≤ x_2) x_1 x ∧ (fun x x_2 => x ≤ x_2) x x_1)
        (Quotient.mk'' a)) =
    Quotient.mk'' a
[PROOFSTEP]
simp_rw [Quotient.map'_mk'', id]
