-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : BiheytingAlgebra α
inst_2 : BiheytingAlgebra β
inst_3 : BiheytingAlgebra γ
inst_4 : BiheytingAlgebra δ
g : BiheytingHom α β
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
map_inf' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun (a ⊓ b) =
      { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun a ⊓
        { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun b
map_himp' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun (a ⇨ b) =
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun a ⇨
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun b
map_sdiff' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun (a \ b) =
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun a \
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun b
h :
  Eq (α := (a : α) → β)
    ((fun (f : BiheytingHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp', map_sdiff' := map_sdiff' })
    ((fun (f : BiheytingHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b)
    (map_inf'_1 :
      ∀ (a b : α),
        { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun (a ⊓ b) =
          { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun a ⊓
            { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun b)
    (map_himp'_1 :
      ∀ (a b : α),
        { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun (a ⇨ b) =
          { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun a ⇨
            { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun b)
    (map_sdiff'_1 :
      ∀ (a b : α),
        { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun (a \ b) =
          { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun a \
            { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : BiheytingHom α β) ↦ f.toFun)
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp',
            map_sdiff' := map_sdiff' })
        ((fun (f : BiheytingHom α β) ↦ f.toFun)
          { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_himp' := map_himp'_1,
            map_sdiff' := map_sdiff'_1 })),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp', map_sdiff' := map_sdiff' :
        BiheytingHom α β } =
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_himp' := map_himp'_1,
        map_sdiff' := map_sdiff'_1 }
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp', map_sdiff' := map_sdiff' :
      BiheytingHom α β } =
    g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g