[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
src✝ : SupHomClass F α β := inst✝
f : F
a b : α
h : a ≤ b
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
inst✝ : InfHomClass F α β
src✝ : InfHomClass F α β := inst✝
f : F
a b : α
h : a ≤ b
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
rw [← inf_eq_left, ← map_inf, inf_eq_left.2 h]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : OrderIsoClass F α β
src✝ : OrderHomClass F α β :=
  let_fun this := inferInstance;
  this
f : F
a b : α
c : (fun x => β) (a ⊔ b)
⊢ ↑f (a ⊔ b) ≤ c ↔ ↑f a ⊔ ↑f b ≤ c
[PROOFSTEP]
simp only [← le_map_inv_iff, sup_le_iff]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
inst✝ : OrderIsoClass F α β
src✝ : OrderHomClass F α β :=
  let_fun this := inferInstance;
  this
f : F
a b : α
c : (fun x => β) (a ⊓ b)
⊢ c ≤ ↑f (a ⊓ b) ↔ c ≤ ↑f a ⊓ ↑f b
[PROOFSTEP]
simp only [← map_inv_le_iff, le_inf_iff]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : Lattice β
inst✝¹ : BoundedOrder β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
h : Disjoint a b
⊢ Disjoint (↑f a) (↑f b)
[PROOFSTEP]
rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : Lattice β
inst✝¹ : BoundedOrder β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
h : Codisjoint a b
⊢ Codisjoint (↑f a) (↑f b)
[PROOFSTEP]
rw [codisjoint_iff, ← map_sup, h.eq_top, map_top]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ ↑f (a \ b) = ↑f a \ ↑f b
[PROOFSTEP]
rw [sdiff_eq, sdiff_eq, map_inf, map_compl']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ ↑f (a ∆ b) = ↑f a ∆ ↑f b
[PROOFSTEP]
rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
f g : SupHom α β
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
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
g : SupHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sup' := map_sup'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun = { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } = { toFun := toFun✝, map_sup' := map_sup'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ (↑f ∘ ↑g) (a ⊔ b) = (↑f ∘ ↑g) a ⊔ (↑f ∘ ↑g) b
[PROOFSTEP]
rw [comp_apply, map_sup, map_sup]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ ↑f (↑g a) ⊔ ↑f (↑g b) = (↑f ∘ ↑g) a ⊔ (↑f ∘ ↑g) b
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← SupHom.comp_apply, h, SupHom.comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ (↑f ⊔ ↑g) (a ⊔ b) = (↑f ⊔ ↑g) a ⊔ (↑f ⊔ ↑g) b
[PROOFSTEP]
rw [Pi.sup_apply, map_sup, map_sup]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ ↑f a ⊔ ↑f b ⊔ (↑g a ⊔ ↑g b) = (↑f ⊔ ↑g) a ⊔ (↑f ⊔ ↑g) b
[PROOFSTEP]
exact sup_sup_sup_comm _ _ _ _
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
f g : InfHom α β
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
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
g : InfHom α β
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
h : { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_inf' := map_inf'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
toFun✝¹ : α → β
map_inf'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊓ b) = toFun✝¹ a ⊓ toFun✝¹ b
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
h : { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }.toFun = { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun
⊢ { toFun := toFun✝¹, map_inf' := map_inf'✝¹ } = { toFun := toFun✝, map_inf' := map_inf'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
f : InfHom β γ
g : InfHom α β
a b : α
⊢ (↑f ∘ ↑g) (a ⊓ b) = (↑f ∘ ↑g) a ⊓ (↑f ∘ ↑g) b
[PROOFSTEP]
rw [comp_apply, map_inf, map_inf]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
f : InfHom β γ
g : InfHom α β
a b : α
⊢ ↑f (↑g a) ⊓ ↑f (↑g b) = (↑f ∘ ↑g) a ⊓ (↑f ∘ ↑g) b
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Inf α
inst✝² : Inf β
inst✝¹ : Inf γ
inst✝ : Inf δ
g : InfHom β γ
f₁ f₂ : InfHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← InfHom.comp_apply, h, InfHom.comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f g : InfHom α β
a b : α
⊢ (↑f ⊓ ↑g) (a ⊓ b) = (↑f ⊓ ↑g) a ⊓ (↑f ⊓ ↑g) b
[PROOFSTEP]
rw [Pi.inf_apply, map_inf, map_inf]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f g : InfHom α β
a b : α
⊢ ↑f a ⊓ ↑f b ⊓ (↑g a ⊓ ↑g b) = (↑f ⊓ ↑g) a ⊓ (↑f ⊓ ↑g) b
[PROOFSTEP]
exact inf_inf_inf_comm _ _ _ _
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Sup α
inst✝⁶ : Bot α
inst✝⁵ : Sup β
inst✝⁴ : Bot β
inst✝³ : Sup γ
inst✝² : Bot γ
inst✝¹ : Sup δ
inst✝ : Bot δ
f g : SupBotHom α β
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
δ : Type u_6
inst✝⁷ : Sup α
inst✝⁶ : Bot α
inst✝⁵ : Sup β
inst✝⁴ : Bot β
inst✝³ : Sup γ
inst✝² : Bot γ
inst✝¹ : Sup δ
inst✝ : Bot δ
g : SupBotHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_bot'✝ : SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } ⊥ = ⊥
h :
  (fun f => f.toFun) { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_bot' := map_bot'✝ } =
    (fun f => f.toFun) g
⊢ { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, 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
δ : Type u_6
inst✝⁷ : Sup α
inst✝⁶ : Bot α
inst✝⁵ : Sup β
inst✝⁴ : Bot β
inst✝³ : Sup γ
inst✝² : Bot γ
inst✝¹ : Sup δ
inst✝ : Bot δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_bot'✝¹ : SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } ⊥ = ⊥
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_bot'✝ : SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } ⊥ = ⊥
h :
  (fun f => f.toFun) { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_bot' := map_bot'✝¹ } =
    (fun f => f.toFun) { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_bot' := map_bot'✝ }
⊢ { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_bot' := map_bot'✝¹ } =
    { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_bot' := map_bot'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Sup α
inst✝⁶ : Bot α
inst✝⁵ : Sup β
inst✝⁴ : Bot β
inst✝³ : Sup γ
inst✝² : Bot γ
inst✝¹ : Sup δ
inst✝ : Bot δ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Inf α
inst✝⁶ : Top α
inst✝⁵ : Inf β
inst✝⁴ : Top β
inst✝³ : Inf γ
inst✝² : Top γ
inst✝¹ : Inf δ
inst✝ : Top δ
f g : InfTopHom α β
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
δ : Type u_6
inst✝⁷ : Inf α
inst✝⁶ : Top α
inst✝⁵ : Inf β
inst✝⁴ : Top β
inst✝³ : Inf γ
inst✝² : Top γ
inst✝¹ : Inf δ
inst✝ : Top δ
g : InfTopHom α β
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : InfHom.toFun { toFun := toFun✝, map_inf' := map_inf'✝ } ⊤ = ⊤
h :
  (fun f => f.toFun) { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ } =
    (fun f => f.toFun) g
⊢ { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ } = 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
δ : Type u_6
inst✝⁷ : Inf α
inst✝⁶ : Top α
inst✝⁵ : Inf β
inst✝⁴ : Top β
inst✝³ : Inf γ
inst✝² : Top γ
inst✝¹ : Inf δ
inst✝ : Top δ
toFun✝¹ : α → β
map_inf'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊓ b) = toFun✝¹ a ⊓ toFun✝¹ b
map_top'✝¹ : InfHom.toFun { toFun := toFun✝¹, map_inf' := map_inf'✝¹ } ⊤ = ⊤
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : InfHom.toFun { toFun := toFun✝, map_inf' := map_inf'✝ } ⊤ = ⊤
h :
  (fun f => f.toFun) { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ } =
    (fun f => f.toFun) { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }
⊢ { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ } =
    { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Inf α
inst✝⁶ : Top α
inst✝⁵ : Inf β
inst✝⁴ : Top β
inst✝³ : Inf γ
inst✝² : Top γ
inst✝¹ : Inf δ
inst✝ : Top δ
g : InfTopHom β γ
f₁ f₂ : InfTopHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
f g : LatticeHom α β
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
δ : Type u_6
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
g : LatticeHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
h :
  (fun f => f.toFun) { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ } =
    (fun f => f.toFun) g
⊢ { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ } = 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
δ : Type u_6
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } a ⊓
        SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
h :
  (fun f => f.toFun) { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ } =
    (fun f => f.toFun) { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }
⊢ { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ } =
    { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
[PROOFSTEP]
obtain h | h := le_total a b
[GOAL]
case inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
h : a ≤ b
⊢ ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
[PROOFSTEP]
rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]
[GOAL]
case inr
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
h : b ≤ a
⊢ ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
[PROOFSTEP]
rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
[PROOFSTEP]
obtain h | h := le_total a b
[GOAL]
case inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
h : a ≤ b
⊢ ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
[PROOFSTEP]
rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]
[GOAL]
case inr
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
src✝ : OrderHomClass F α β := inst✝
f : F
a b : α
h : b ≤ a
⊢ ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
[PROOFSTEP]
rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
f g : BoundedLatticeHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedLatticeHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_top'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊤ = ⊤
map_bot'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊥ = ⊥
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    (fun f => f.toFun) g
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } a ⊓
        SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } b
map_top'✝¹ :
  SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom ⊤ = ⊤
map_bot'✝¹ :
  SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom ⊥ = ⊥
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_top'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊤ = ⊤
map_bot'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊥ = ⊥
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
        map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
      map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      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
δ : Type u_6
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
⊢ (fun f => ↑f) (withTopWithBot (LatticeHom.id α)) = (fun f => ↑f) (BoundedLatticeHom.id (WithTop (WithBot α)))
[PROOFSTEP]
refine' (congr_arg Option.map _).trans Option.map_id
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
⊢ (fun x => ↑(LatticeHom.withBot (LatticeHom.id α)).toSupHom x) = id
[PROOFSTEP]
rw [withBot_id]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
⊢ (fun x => ↑(LatticeHom.id (WithBot α)).toSupHom x) = id
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ withTopWithBot (comp f g) = BoundedLatticeHom.comp (withTopWithBot f) (withTopWithBot g)
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a✝ : WithTop (WithBot α)
⊢ ↑(withTopWithBot (comp f g)) a✝ = ↑(BoundedLatticeHom.comp (withTopWithBot f) (withTopWithBot g)) a✝
[PROOFSTEP]
simp
