Module: Mathlib.Order.Closure

Goal state before:
pp: α : 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✝¹ : α → Prop
isClosed_iff✝¹ : ∀ {x : α}, IsClosed✝¹ x ↔ toOrderHom✝.toFun x = x
IsClosed✝ : α → Prop
le_closure'✝ :
  ∀ (x : α),
    x ≤
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        x
idempotent'✝ :
  ∀ (x : α),
    { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        ({ toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹,
              IsClosed := IsClosed✝¹, isClosed_iff := isClosed_iff✝¹ }.toFun
          x) =
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        x
isClosed_iff✝ :
  ∀ {x : α},
    IsClosed✝ x ↔
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
              isClosed_iff := isClosed_iff✝¹ }.toFun
          x =
        x
h :
  (fun c ↦ ⇑c.toOrderHom)
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
        isClosed_iff := isClosed_iff✝¹ } =
    (fun c ↦ ⇑c.toOrderHom)
      {
        toOrderHom :=
          { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹,
              IsClosed := IsClosed✝¹, isClosed_iff := isClosed_iff✝¹ }.toOrderHom,
        le_closure' := le_closure'✝, idempotent' := idempotent'✝, IsClosed := IsClosed✝, isClosed_iff := isClosed_iff✝ }
⊢ { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
      isClosed_iff := isClosed_iff✝¹ } =
    {
      toOrderHom :=
        { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toOrderHom,
      le_closure' := le_closure'✝, idempotent' := idempotent'✝, IsClosed := IsClosed✝, isClosed_iff := isClosed_iff✝ }

Tactic:
congr with x

Goal state after:
case e_IsClosed
α : 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✝¹ : α → Prop
isClosed_iff✝¹ : ∀ {x : α}, IsClosed✝¹ x ↔ toOrderHom✝.toFun x = x
IsClosed✝ : α → Prop
le_closure'✝ :
  ∀ (x : α),
    x ≤
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        x
idempotent'✝ :
  ∀ (x : α),
    { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        ({ toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹,
              IsClosed := IsClosed✝¹, isClosed_iff := isClosed_iff✝¹ }.toFun
          x) =
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        x
isClosed_iff✝ :
  ∀ {x : α},
    IsClosed✝ x ↔
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
              isClosed_iff := isClosed_iff✝¹ }.toFun
          x =
        x
h :
  (fun c ↦ ⇑c.toOrderHom)
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
        isClosed_iff := isClosed_iff✝¹ } =
    (fun c ↦ ⇑c.toOrderHom)
      {
        toOrderHom :=
          { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹,
              IsClosed := IsClosed✝¹, isClosed_iff := isClosed_iff✝¹ }.toOrderHom,
        le_closure' := le_closure'✝, idempotent' := idempotent'✝, IsClosed := IsClosed✝, isClosed_iff := isClosed_iff✝ }
x : α
⊢ IsClosed✝¹ x ↔ IsClosed✝ x