-- Module: Mathlib.Order.Closure
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 })
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 }
⊢ { 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 }

Tactic:
obtain rfl := DFunLike.ext' h

Premises used: DFunLike.ext', rfl