-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
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)
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
⊢ S = T

Tactic:
obtain ⟨⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩, _⟩ := S