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✝³ : 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 : α),
    { 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_top'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
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_top' := map_top'✝,
        map_sdiff' := map_sdiff'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ } =
    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✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
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_top'✝¹ : { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun ⊤ = ⊤
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_top'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
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_top' := map_top'✝¹,
        map_sdiff' := map_sdiff'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝,
        map_sdiff' := map_sdiff'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹,
      map_sdiff' := map_sdiff'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ }