case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y

case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y
constructor
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y
rintro rfl x
no goals
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y
exact (gc x y).symm
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z
intro H
no goals
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.12736
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z
exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)