-- 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
S T : VonNeumannAlgebra H
h :
  Eq.{u + 1} (α := Set (H →L[ℂ] H)) ((fun (S : VonNeumannAlgebra H) ↦ S.carrier) S)
    ((fun (S : VonNeumannAlgebra H) ↦ S.carrier) T)
⊢ S = T
have obtain : ∀ (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
Tactic: obtain ⟨⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩, _⟩ := S
Cleared hypotheses: S, h