Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun (a ⊓ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun a ⊓ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun b
map_himp'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun (a ⇨ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun a ⇨
        { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun b
map_sdiff'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun (a \ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun a \
        { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_himp'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a ⇨ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a ⇨
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
map_sdiff'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a \ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a \
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_himp' := map_himp'✝¹,
        map_sdiff' := map_sdiff'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
        map_sdiff' := map_sdiff'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_himp' := map_himp'✝¹,
      map_sdiff' := map_sdiff'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
      map_sdiff' := map_sdiff'✝ }

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun (a ⊓ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun a ⊓ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun b
map_himp'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun (a ⇨ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun a ⇨
        { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun b
map_sdiff'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun (a \ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun a \
        { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_himp'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a ⇨ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a ⇨
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
map_sdiff'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a \ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a \
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_himp' := map_himp'✝¹,
        map_sdiff' := map_sdiff'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
        map_sdiff' := map_sdiff'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_himp' := map_himp'✝¹,
      map_sdiff' := map_sdiff'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
      map_sdiff' := map_sdiff'✝ }