[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S T : VonNeumannAlgebra H
h : (fun S => S.carrier) S = (fun S => S.carrier) T
⊢ S = T
[PROOFSTEP]
obtain ⟨⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩, _⟩ := S
[GOAL]
case mk.mk.mk.mk.mk.mk
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : 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'✝ }.carrier
add_mem'✝ :
  ∀ {a b : H →L[ℂ] H},
    a ∈
        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
              one_mem' := one_mem'✝ }.toSubsemigroup.carrier →
      b ∈
          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                one_mem' := one_mem'✝ }.toSubsemigroup.carrier →
        a + b ∈
          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                one_mem' := one_mem'✝ }.toSubsemigroup.carrier
zero_mem'✝ :
  0 ∈ { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ }.toSubsemigroup.carrier
algebraMap_mem'✝ :
  ∀ (r : ℂ),
    ↑(algebraMap ℂ (H →L[ℂ] H)) r ∈
      { toSubmonoid := { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
              add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }.toSubmonoid.toSubsemigroup.carrier
star_mem'✝ :
  ∀ {a : H →L[ℂ] H},
    a ∈
        {
                  toSubsemiring :=
                    {
                      toSubmonoid :=
                        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                      add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      star a ∈
        {
                  toSubsemiring :=
                    {
                      toSubmonoid :=
                        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                      add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
centralizer_centralizer'✝ :
  Set.centralizer
      (Set.centralizer
        {
                    toSubalgebra :=
                      {
                        toSubsemiring :=
                          {
                            toSubmonoid :=
                              { toSubsemigroup := { 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'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) =
    {
                toSubalgebra :=
                  {
                    toSubsemiring :=
                      {
                        toSubmonoid :=
                          { toSubsemigroup := { 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'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
h :
  (fun S => S.carrier)
      {
        toStarSubalgebra :=
          {
            toSubalgebra :=
              {
                toSubsemiring :=
                  {
                    toSubmonoid :=
                      { toSubsemigroup := { 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 => S.carrier) T
⊢ {
      toStarSubalgebra :=
        {
          toSubalgebra :=
            {
              toSubsemiring :=
                {
                  toSubmonoid :=
                    { toSubsemigroup := { 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'✝ } =
    T
[PROOFSTEP]
cases T
[GOAL]
case mk.mk.mk.mk.mk.mk.mk
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace 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'✝ }.carrier
add_mem'✝ :
  ∀ {a b : H →L[ℂ] H},
    a ∈
        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
              one_mem' := one_mem'✝ }.toSubsemigroup.carrier →
      b ∈
          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                one_mem' := one_mem'✝ }.toSubsemigroup.carrier →
        a + b ∈
          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                one_mem' := one_mem'✝ }.toSubsemigroup.carrier
zero_mem'✝ :
  0 ∈ { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ }.toSubsemigroup.carrier
algebraMap_mem'✝ :
  ∀ (r : ℂ),
    ↑(algebraMap ℂ (H →L[ℂ] H)) r ∈
      { toSubmonoid := { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
              add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }.toSubmonoid.toSubsemigroup.carrier
star_mem'✝ :
  ∀ {a : H →L[ℂ] H},
    a ∈
        {
                  toSubsemiring :=
                    {
                      toSubmonoid :=
                        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                      add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      star a ∈
        {
                  toSubsemiring :=
                    {
                      toSubmonoid :=
                        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                      add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
centralizer_centralizer'✝¹ :
  Set.centralizer
      (Set.centralizer
        {
                    toSubalgebra :=
                      {
                        toSubsemiring :=
                          {
                            toSubmonoid :=
                              { toSubsemigroup := { 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'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) =
    {
                toSubalgebra :=
                  {
                    toSubsemiring :=
                      {
                        toSubmonoid :=
                          { toSubsemigroup := { 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'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
toStarSubalgebra✝ : StarSubalgebra ℂ (H →L[ℂ] H)
centralizer_centralizer'✝ : Set.centralizer (Set.centralizer toStarSubalgebra✝.carrier) = toStarSubalgebra✝.carrier
h :
  (fun S => S.carrier)
      {
        toStarSubalgebra :=
          {
            toSubalgebra :=
              {
                toSubsemiring :=
                  {
                    toSubmonoid :=
                      { toSubsemigroup := { 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 => S.carrier)
      { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }
⊢ {
      toStarSubalgebra :=
        {
          toSubalgebra :=
            {
              toSubsemiring :=
                {
                  toSubmonoid :=
                    { toSubsemigroup := { 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'✝¹ } =
    { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }
[PROOFSTEP]
congr
  -- porting note: `StarMemClass` should be in `Prop`?
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ Set.centralizer
      (Set.centralizer
        (StarSubalgebra.centralizer ℂ ↑S).toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) =
    (StarSubalgebra.centralizer ℂ ↑S).toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
simp
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ ↑(commutant S) = Set.centralizer ↑S
[PROOFSTEP]
simp [commutant]
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ commutant S ↔ ∀ (g : H →L[ℂ] H), g ∈ S → g * z = z * g
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_commutant]
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ Set.centralizer ↑S ↔ ∀ (g : H →L[ℂ] H), g ∈ S → g * z = z * g
[PROOFSTEP]
rfl
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ ↑(commutant (commutant S)) = ↑S
[PROOFSTEP]
simp
