[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ ↑f a = ⊤ ↔ a = ⊤
[PROOFSTEP]
letI : TopHomClass F α β := OrderIsoClass.toTopHomClass
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : TopHomClass F α β := OrderIsoClass.toTopHomClass
⊢ ↑f a = ⊤ ↔ a = ⊤
[PROOFSTEP]
rw [← map_top f, (EquivLike.injective f).eq_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ ↑f a = ⊥ ↔ a = ⊥
[PROOFSTEP]
letI : BotHomClass F α β := OrderIsoClass.toBotHomClass
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : BotHomClass F α β := OrderIsoClass.toBotHomClass
⊢ ↑f a = ⊥ ↔ a = ⊥
[PROOFSTEP]
rw [← map_bot f, (EquivLike.injective f).eq_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f g : TopHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
g : TopHom α β
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝, map_top' := map_top'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_top' := map_top'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
toFun✝¹ : α → β
map_top'✝¹ : toFun✝¹ ⊤ = ⊤
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝¹, map_top' := map_top'✝¹ }.toFun = { toFun := toFun✝, map_top' := map_top'✝ }.toFun
⊢ { toFun := toFun✝¹, map_top' := map_top'✝¹ } = { toFun := toFun✝, map_top' := map_top'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f : TopHom β γ
g : TopHom α β
⊢ (↑f ∘ ↑g) ⊤ = ⊤
[PROOFSTEP]
rw [comp_apply, map_top, map_top]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← TopHom.comp_apply, h, TopHom.comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Top α
inst✝¹ : SemilatticeInf β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (↑f ⊓ ↑g) ⊤ = ⊤
[PROOFSTEP]
rw [Pi.inf_apply, map_top, map_top, inf_top_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (↑f ⊔ ↑g) ⊤ = ⊤
[PROOFSTEP]
rw [Pi.sup_apply, map_top, map_top, sup_top_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
f g : BotHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
g : BotHom α β
toFun✝ : α → β
map_bot'✝ : toFun✝ ⊥ = ⊥
h : { toFun := toFun✝, map_bot' := map_bot'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_bot' := map_bot'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
toFun✝¹ : α → β
map_bot'✝¹ : toFun✝¹ ⊥ = ⊥
toFun✝ : α → β
map_bot'✝ : toFun✝ ⊥ = ⊥
h : { toFun := toFun✝¹, map_bot' := map_bot'✝¹ }.toFun = { toFun := toFun✝, map_bot' := map_bot'✝ }.toFun
⊢ { toFun := toFun✝¹, map_bot' := map_bot'✝¹ } = { toFun := toFun✝, map_bot' := map_bot'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
f : BotHom β γ
g : BotHom α β
⊢ (↑f ∘ ↑g) ⊥ = ⊥
[PROOFSTEP]
rw [comp_apply, map_bot, map_bot]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bot α
inst✝² : Bot β
inst✝¹ : Bot γ
inst✝ : Bot δ
g : BotHom β γ
f₁ f₂ : BotHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← BotHom.comp_apply, h, BotHom.comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Bot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
f✝ g✝ f g : BotHom α β
⊢ (↑f ⊓ ↑g) ⊥ = ⊥
[PROOFSTEP]
rw [Pi.inf_apply, map_bot, map_bot, inf_bot_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Bot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f✝ g✝ f g : BotHom α β
⊢ (↑f ⊔ ↑g) ⊥ = ⊥
[PROOFSTEP]
rw [Pi.sup_apply, map_bot, map_bot, sup_bot_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
f g : BoundedOrderHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedOrderHom α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } ⊤ = ⊤
map_bot'✝ : OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } ⊥ = ⊥
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    (fun f => f.toFun) g
⊢ { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, map_top' := map_top'✝, map_bot' := map_bot'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_top'✝¹ : OrderHom.toFun { toFun := toFun✝¹, monotone' := monotone'✝¹ } ⊤ = ⊤
map_bot'✝¹ : OrderHom.toFun { toFun := toFun✝¹, monotone' := monotone'✝¹ } ⊥ = ⊥
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } ⊤ = ⊤
map_bot'✝ : OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } ⊥ = ⊥
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, map_top' := map_top'✝, map_bot' := map_bot'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply]
