Module: Mathlib.Order.Hom.BoundedLattice

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

Tactic:
;

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