case mk
α : Type u_1
β : Type ?u.3549
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
α : Type u_1
β : Type ?u.3549
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)
rintro a ⟨b⟩ h
no goals
case mk
α : Type u_1
β : Type ?u.3549
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
exact ⟨b, h, rfl⟩