α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
⊢ IsCoatom (u b)
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
⊢ IsCoatom (u b) ↔ IsCoatom b
refine' ⟨fun hb => gi.isCoatom_of_image hb, fun hb => _⟩
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
⊢ IsCoatom (u b)
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
⊢ IsCoatom (u b)
obtain ⟨a, ha, hab⟩ :=
  (eq_top_or_exists_le_coatom (u b)).resolve_left fun h =>
    hb.1 <| (gi.gc.u_top ▸ gi.l_u_eq ⊤ : l ⊤ = ⊤) ▸ gi.l_u_eq b ▸ congr_arg l h
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
this : l a = b
⊢ IsCoatom (u b)
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
⊢ IsCoatom (u b)
have : l a = b :=
  (hb.le_iff.mp (gi.l_u_eq b ▸ gi.gc.monotone_l hab : b ≤ l a)).resolve_left fun hla =>
    ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)
no goals
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
this : l a = b
⊢ IsCoatom (u b)
exact this ▸ (h_coatom a ha).symm ▸ ha