-- Lean 4 proof step from Mathlib.Analysis.VonNeumannAlgebra.Basic (goal)
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
T : VonNeumannAlgebra H
carrier : Set (H →L[ℂ] H)
mul_mem' : ∀ {a b : H →L[ℂ] H}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
one_mem' : 1 ∈ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup (H →L[ℂ] H) }.carrier
add_mem' :
  ∀ {a b : H →L[ℂ] H},
    a ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid (H →L[ℂ] H) }.carrier →
      b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid (H →L[ℂ] H) }.carrier →
        a + b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid (H →L[ℂ] H) }.carrier
zero_mem' : 0 ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid (H →L[ℂ] H) }.carrier
algebraMap_mem' :
  ∀ (r : ℂ),
    Membership.mem (α := H →L[ℂ] H)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem' :
          Subsemiring (H →L[ℂ] H) }.carrier
      ((algebraMap ℂ (H →L[ℂ] H) : (a : ℂ) → H →L[ℂ] H) r : H →L[ℂ] H)
star_mem' :
  ∀ {a : H →L[ℂ] H},
    a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra ℂ (H →L[ℂ] H) }.carrier →
      star a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra ℂ (H →L[ℂ] H) }.carrier
centralizer_centralizer' :
  (StarSubalgebra.toSubalgebra
            { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
              zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' :
              StarSubalgebra ℂ (H →L[ℂ] H) }).carrier.centralizer.centralizer =
    (StarSubalgebra.toSubalgebra
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
          zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' :
          StarSubalgebra ℂ (H →L[ℂ] H) }).carrier
h :
  Eq.{u + 1} (α := Set (H →L[ℂ] H))
    ((fun (S : VonNeumannAlgebra H) ↦ S.carrier)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
        algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem',
        centralizer_centralizer' := centralizer_centralizer' })
    ((fun (S : VonNeumannAlgebra H) ↦ S.carrier) T)
⊢ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem',
      centralizer_centralizer' := centralizer_centralizer' : VonNeumannAlgebra H } =
    T
have mk : ∀ (toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H))
  (centralizer_centralizer'_1 : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier)
  (h :
    Eq.{u + 1} (α := Set (H →L[ℂ] H))
      ((fun (S : VonNeumannAlgebra H) ↦ S.carrier)
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
          zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem',
          centralizer_centralizer' := centralizer_centralizer' })
      ((fun (S : VonNeumannAlgebra H) ↦ S.carrier)
        { toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer'_1 })),
  { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem',
      centralizer_centralizer' := centralizer_centralizer' : VonNeumannAlgebra H } =
    { toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer'_1 }
Tactic: cases T
Cleared hypotheses: T, h