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

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