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✝³ : 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 : α),
    { 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_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊥ = ⊥
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
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝,
        map_himp' := map_himp'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝, map_himp' := map_himp'✝ } = g

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

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
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_bot'✝¹ : { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun ⊥ = ⊥
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
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_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊥ = ⊥
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
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_bot' := map_bot'✝¹,
        map_himp' := map_himp'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝, map_himp' := map_himp'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_bot' := map_bot'✝¹,
      map_himp' := map_himp'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝, map_himp' := map_himp'✝ }