Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: case 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 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
        a + b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
zero_mem'✝ : 0 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
algebraMap_mem'✝ :
  ∀ (r : ℂ),
    (algebraMap ℂ (H →L[ℂ] H)) r ∈
      { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
          zero_mem' := zero_mem'✝ }.carrier
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'✝ }.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'✝ }.carrier
centralizer_centralizer'✝¹ :
  { 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'✝ }.carrier.centralizer.centralizer =
    { 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'✝ }.carrier
toStarSubalgebra✝ : StarSubalgebra ℂ (H →L[ℂ] H)
centralizer_centralizer'✝ : toStarSubalgebra✝.carrier.centralizer.centralizer = toStarSubalgebra✝.carrier
h :
  (fun S ↦ 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 ↦ S.carrier) { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }
⊢ { 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'✝ }

Tactic:
;

Goal state after:
case 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 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
        a + b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
zero_mem'✝ : 0 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
algebraMap_mem'✝ :
  ∀ (r : ℂ),
    (algebraMap ℂ (H →L[ℂ] H)) r ∈
      { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
          zero_mem' := zero_mem'✝ }.carrier
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'✝ }.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'✝ }.carrier
centralizer_centralizer'✝¹ :
  { 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'✝ }.carrier.centralizer.centralizer =
    { 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'✝ }.carrier
toStarSubalgebra✝ : StarSubalgebra ℂ (H →L[ℂ] H)
centralizer_centralizer'✝ : toStarSubalgebra✝.carrier.centralizer.centralizer = toStarSubalgebra✝.carrier
h :
  (fun S ↦ 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 ↦ S.carrier) { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }
⊢ { 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'✝ }