-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : Preorder α
toOrderHom : α →o α
le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x
idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x
IsClosed : (x : α) → Prop
isClosed_iff : ∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x
toOrderHom_1 : α →o α
le_closure'_1 : ∀ (x : α), x ≤ toOrderHom_1.toFun x
idempotent'_1 : ∀ (x : α), toOrderHom_1.toFun (toOrderHom_1.toFun x) = toOrderHom_1.toFun x
IsClosed_1 : (x : α) → Prop
isClosed_iff_1 : ∀ {x : α}, IsClosed_1 x ↔ toOrderHom_1.toFun x = x
h :
  Eq.{u_1 + 1} (α := (a : α) → α)
    ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
        isClosed_iff := @isClosed_iff })
    ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
      { toOrderHom := toOrderHom_1, le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
        isClosed_iff := @isClosed_iff_1 })
⊢ { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
      isClosed_iff := @isClosed_iff : ClosureOperator α } =
    { toOrderHom := toOrderHom_1, le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
      isClosed_iff := @isClosed_iff_1 }
have obtain : ∀
  (le_closure'_2 :
    ∀ (x : α),
      x ≤
        { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          x)
  (idempotent'_2 :
    ∀ (x : α),
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          ({ toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
                isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
            x) =
        { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          x)
  (isClosed_iff_2 :
    ∀ {x : α},
      IsClosed_1 x ↔
        { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
                isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
            x =
          x)
  (h :
    Eq.{u_1 + 1} (α := (a : α) → α)
      ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
        { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
          isClosed_iff := @isClosed_iff })
      ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
        {
          toOrderHom :=
            { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
                isClosed_iff := @isClosed_iff }.toOrderHom,
          le_closure' := le_closure'_2, idempotent' := idempotent'_2, IsClosed := IsClosed_1,
          isClosed_iff := @isClosed_iff_2 })),
  { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
      isClosed_iff := @isClosed_iff : ClosureOperator α } =
    {
      toOrderHom :=
        { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff }.toOrderHom,
      le_closure' := le_closure'_2, idempotent' := idempotent'_2, IsClosed := IsClosed_1,
      isClosed_iff := @isClosed_iff_2 }
Tactic: obtain rfl := DFunLike.ext' h
Cleared hypotheses: toOrderHom_1, le_closure'_1, idempotent'_1, isClosed_iff_1, h