-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp', map_sdiff' := map_sdiff' :
      BiheytingHom α β } =
    g
have 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 }
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
Cleared hypotheses: g, h