[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
src✝ : HeytingHomClass F α β := inst✝
f : F
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
src✝ : CoheytingHomClass F α β := inst✝
f : F
⊢ ↑f ⊥ = ⊥
[PROOFSTEP]
rw [← @sdiff_self α _ ⊤, ← sdiff_self, map_sdiff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
src✝ : BiheytingHomClass F α β := inst✝
f : F
⊢ ↑f ⊥ = ⊥
[PROOFSTEP]
rw [← @sdiff_self α _ ⊤, ← sdiff_self, BiheytingHomClass.map_sdiff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
src✝ : BiheytingHomClass F α β := inst✝
f : F
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
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_himp_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ ↑f a) ≤ b
[PROOFSTEP]
rw [← OrderIsoClass.map_le_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ ↑f (EquivLike.inv f c ⊓ a) ≤ ↑f b ↔ EquivLike.inv f (c ⊓ ↑f a) ≤ b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
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, sdiff_le_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv f (↑f b ⊔ c)
[PROOFSTEP]
rw [← OrderIsoClass.map_le_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ ↑f a ≤ ↑f (b ⊔ EquivLike.inv f c) ↔ a ≤ EquivLike.inv f (↑f b ⊔ c)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
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_himp_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ ↑f a) ≤ b
[PROOFSTEP]
rw [← OrderIsoClass.map_le_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ ↑f (EquivLike.inv f c ⊓ a) ≤ ↑f b ↔ EquivLike.inv f (c ⊓ ↑f a) ≤ b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
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, sdiff_le_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv f (↑f b ⊔ c)
[PROOFSTEP]
rw [← OrderIsoClass.map_le_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ ↑f a ≤ ↑f (b ⊔ EquivLike.inv f c) ↔ a ≤ EquivLike.inv f (↑f b ⊔ c)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
src✝ : BoundedLatticeHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⇨ b) = ↑f a ⇨ ↑f b
[PROOFSTEP]
rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
src✝ : BoundedLatticeHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a \ b) = ↑f a \ ↑f b
[PROOFSTEP]
rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ ↑f aᶜ = (↑f a)ᶜ
[PROOFSTEP]
rw [← himp_bot, ← himp_bot, map_himp, map_bot]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a b : α
⊢ ↑f (a ⇔ b) = ↑f a ⇔ ↑f b
[PROOFSTEP]
simp_rw [bihimp, map_inf, map_himp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a : α
⊢ ↑f (￢a) = ￢↑f a
[PROOFSTEP]
rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ ↑f (a ∆ b) = ↑f a ∆ ↑f b
[PROOFSTEP]
simp_rw [symmDiff, map_sup, map_sdiff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f g : HeytingHom α β
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
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
g : HeytingHom α β
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_bot'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊥ = ⊥
map_himp'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_bot' := map_bot'✝, map_himp' := map_himp'✝ } =
    (fun f => f.toFun) g
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_bot' := map_bot'✝, map_himp' := map_himp'✝ } =
    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
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
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_bot'✝¹ :
  SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom ⊥ = ⊥
map_himp'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom 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
map_bot'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊥ = ⊥
map_himp'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
        map_bot' := map_bot'✝¹, map_himp' := map_himp'✝¹ } =
    (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_bot' := map_bot'✝, map_himp' := map_himp'✝ }
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
      map_bot' := map_bot'✝¹, map_himp' := map_himp'✝¹ } =
    { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_bot' := map_bot'✝, map_himp' := map_himp'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b
[PROOFSTEP]
simpa only [h] using map_sup f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b
[PROOFSTEP]
simpa only [h] using map_inf f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ↑f
⊢ SupHom.toFun
      { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b) }.toSupHom
      ⊥ =
    ⊥
[PROOFSTEP]
simpa only [h] using map_bot f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun
        { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                        b) }.toSupHom
        (a ⇨ b) =
      SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          a ⇨
        SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          b
[PROOFSTEP]
simpa only [h] using map_himp f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom β γ
g : HeytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      ⊥ =
    ⊥
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom β γ
g : HeytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
a b : α
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      (a ⇨ b) =
    SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        a ⇨
      SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f f₁ f₂ : HeytingHom α β
g g₁ g₂ : HeytingHom β γ
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
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f g : CoheytingHom α β
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
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
g : CoheytingHom α β
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_sdiff'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ } =
    (fun f => f.toFun) g
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ } =
    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
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
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_sdiff'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom 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
map_top'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊤ = ⊤
map_sdiff'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
        map_top' := map_top'✝¹, map_sdiff' := map_sdiff'✝¹ } =
    (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ }
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
      map_top' := map_top'✝¹, map_sdiff' := map_sdiff'✝¹ } =
    { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b
[PROOFSTEP]
simpa only [h] using map_sup f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b
[PROOFSTEP]
simpa only [h] using map_inf f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ↑f
⊢ SupHom.toFun
      { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b) }.toSupHom
      ⊤ =
    ⊤
[PROOFSTEP]
simpa only [h] using map_top f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun
        { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                        b) }.toSupHom
        (a \ b) =
      SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          a \
        SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          b
[PROOFSTEP]
simpa only [h] using map_sdiff f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      ⊤ =
    ⊤
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
a b : α
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      (a \ b) =
    SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        a \
      SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f f₁ f₂ : CoheytingHom α β
g g₁ g₂ : CoheytingHom β γ
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
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f g : BiheytingHom α β
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
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
g : BiheytingHom α β
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_himp'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
map_sdiff'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_himp' := map_himp'✝, map_sdiff' := map_sdiff'✝ } =
    (fun f => f.toFun) g
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_himp' := map_himp'✝, map_sdiff' := map_sdiff'✝ } =
    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
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
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_himp'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom b
map_sdiff'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom 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
map_himp'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
map_sdiff'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
        map_himp' := map_himp'✝¹, map_sdiff' := map_sdiff'✝¹ } =
    (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_himp' := map_himp'✝, map_sdiff' := map_sdiff'✝ }
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
      map_himp' := map_himp'✝¹, map_sdiff' := map_sdiff'✝¹ } =
    { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_himp' := map_himp'✝, map_sdiff' := map_sdiff'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b
[PROOFSTEP]
simpa only [h] using map_sup f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b
[PROOFSTEP]
simpa only [h] using map_inf f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun
        { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                        b) }.toSupHom
        (a ⇨ b) =
      SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          a ⇨
        SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          b
[PROOFSTEP]
simpa only [h] using map_himp f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun
        { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                        b) }.toSupHom
        (a \ b) =
      SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          a \
        SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          b
[PROOFSTEP]
simpa only [h] using map_sdiff f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom β γ
g : BiheytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
a b : α
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      (a ⇨ b) =
    SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        a ⇨
      SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom β γ
g : BiheytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
a b : α
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      (a \ b) =
    SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        a \
      SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f f₁ f₂ : BiheytingHom α β
g g₁ g₂ : BiheytingHom β γ
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
