awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
⊢ Membership.mem (α := C((↑(characterSpace ℂ A) : Type u_1), ℂ)) (γ := Set C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (Subsemigroup.carrier
        (Submonoid.toSubsemigroup
            (Subsemiring.toSubmonoid
              (Subalgebra.toSubsemiring
                (AlgHom.range (gelfandTransform ℂ A) : Subalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ)))) :
          Subsemigroup C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
      Set C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (star
        (((AlgHom.toRingHom (gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
              A →+* C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          a) :
      C((↑(characterSpace ℂ A) : Type u_1), ℂ))
have h : Eq (α := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
  (((AlgHom.toRingHom (gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
          A →+* C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
        (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
      (star a) :
    C((↑(characterSpace ℂ A) : Type u_1), ℂ))
  (star
      (((AlgHom.toRingHom (gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            A →+* C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
          (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
        a) :
    C((↑(characterSpace ℂ A) : Type u_1), ℂ))
Tactic: use star a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
⊢ Eq (α := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (((AlgHom.toRingHom (gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            A →+* C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
          (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
        (star a) :
      C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (star
        (((AlgHom.toRingHom (gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
              A →+* C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          a) :
      C((↑(characterSpace ℂ A) : Type u_1), ℂ))
have h : ∀ (φ : (↑(characterSpace ℂ A) : Type u_1)),
  Eq (α := ℂ)
    (((((AlgHom.toRingHom (gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                  A →+* C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
              (star a) :
            C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
          (a : (↑(characterSpace ℂ A) : Type u_1)) → ℂ)
        φ :
      ℂ)
    (((star
              (((AlgHom.toRingHom (gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                    A →+* C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                  (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
                a) :
            C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
          (a : (↑(characterSpace ℂ A) : Type u_1)) → ℂ)
        φ :
      ℂ)
Tactic: ext1 φ
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : CommCStarAlgebra A
rng : StarSubalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ) :=
  let __Subalgebra : Subalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ) := AlgHom.range (gelfandTransform ℂ A);
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
⊢ Function.Surjective (α := A) (β := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (⇑(gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
      (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
have suffices : rng = ⊤
Tactic: suffices rng = ⊤ from
    fun x => show x ∈ rng from this.symm ▸ StarSubalgebra.mem_top
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
Goal:
A : Type u_1
inst : CommCStarAlgebra A
rng : StarSubalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ) :=
  let __Subalgebra : Subalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ) := AlgHom.range (gelfandTransform ℂ A);
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
⊢ rng = ⊤
have h : rng.topologicalClosure = rng
Tactic: have h : rng.topologicalClosure = rng := le_antisymm
    (StarSubalgebra.topologicalClosure_minimal le_rfl
      (gelfandTransform_isometry A).isClosedEmbedding.isClosed_range)
    (StarSubalgebra.le_topologicalClosure _)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : CommCStarAlgebra A
rng : StarSubalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ) :=
  let __Subalgebra : Subalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ) := AlgHom.range (gelfandTransform ℂ A);
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
⊢ rng = ⊤
have refine : ∀ (x x_1 : (↑(characterSpace ℂ A) : Type u_1)),
  x ≠ x_1 →
    ∃ (f : (↑(characterSpace ℂ A) : Type u_1) → ℂ),
      Membership.mem (γ := Set ((↑(characterSpace ℂ A) : Type u_1) → ℂ))
          ((fun (f : C((↑(characterSpace ℂ A) : Type u_1), ℂ)) ↦ (⇑f : (a : (↑(characterSpace ℂ A) : Type u_1)) → ℂ)) ''
            (↑rng.toSubalgebra : Set C((↑(characterSpace ℂ A) : Type u_1), ℂ)))
          f ∧
        f x ≠ f x_1
Tactic: refine h ▸ ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
    _ (fun _ _ => ?_)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : CommCStarAlgebra A
rng : StarSubalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ) :=
  let __Subalgebra : Subalgebra ℂ C((↑(characterSpace ℂ A) : Type u_1), ℂ) := AlgHom.range (gelfandTransform ℂ A);
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
x x_1 : (↑(characterSpace ℂ A) : Type u_1)
⊢ x ≠ x_1 →
    ∃ (f : (↑(characterSpace ℂ A) : Type u_1) → ℂ),
      Membership.mem (γ := Set ((↑(characterSpace ℂ A) : Type u_1) → ℂ))
          ((fun (f : C((↑(characterSpace ℂ A) : Type u_1), ℂ)) ↦ (⇑f : (a : (↑(characterSpace ℂ A) : Type u_1)) → ℂ)) ''
            (↑rng.toSubalgebra : Set C((↑(characterSpace ℂ A) : Type u_1), ℂ)))
          f ∧
        f x ≠ f x_1
have contrapose! : (∀ (f : (↑(characterSpace ℂ A) : Type u_1) → ℂ)
    (_ :
      Membership.mem (γ := Set ((↑(characterSpace ℂ A) : Type u_1) → ℂ))
        ((fun (f : C((↑(characterSpace ℂ A) : Type u_1), ℂ)) ↦ (⇑f : (a : (↑(characterSpace ℂ A) : Type u_1)) → ℂ)) ''
          (↑rng.toSubalgebra : Set C((↑(characterSpace ℂ A) : Type u_1), ℂ)))
        f),
    f x = f x_1) →
  x = x_1
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
f : A → C((↑(characterSpace ℂ (Unitization ℂ A)) : Type u_1), ℂ) :=
  Function.comp (β := Unitization ℂ A)
    (⇑(gelfandStarTransform (Unitization ℂ A)) :
      (a : Unitization ℂ A) → C((↑(characterSpace ℂ (Unitization ℂ A)) : Type u_1), ℂ))
    (⇑(inrNonUnitalAlgHom ℂ A) : (a : A) → Unitization ℂ A)
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
have hf : Isometry f
Tactic: have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
f : A → C((↑(characterSpace ℂ (Unitization ℂ A)) : Type u_1), ℂ) :=
  Function.comp (β := Unitization ℂ A)
    (⇑(gelfandStarTransform (Unitization ℂ A)) :
      (a : Unitization ℂ A) → C((↑(characterSpace ℂ (Unitization ℂ A)) : Type u_1), ℂ))
    (⇑(inrNonUnitalAlgHom ℂ A) : (a : A) → Unitization ℂ A)
hf : Isometry f
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
have simp_rw : ‖f a + f b‖ = max ‖f a‖ ‖f b‖
Tactic: simp_rw [← hf.norm_map_of_map_zero (by simp [f]), show f (a + b) = f a + f b by simp [f]]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
have insert : f j * ∑ i ∈ s, f i = 0
Tactic: suffices f j * ∑ i ∈ s, f i = 0 by simp_all [nnnorm_add_eq_max this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have empty : nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simp_all [nnnorm_add_eq_max this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
empty : nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have insert : ∀ (j : ι) (s : Finset ι) (hj : j ∉ s) (ih : nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊),
  nnnorm.{u_1} (E := A) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simp_all [nnnorm_add_eq_max this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have empty : nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simp_all [nnnorm_add_eq_max this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
empty : nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have insert : ∀ (j : ι) (s : Finset ι) (hj : j ∉ s) (ih : nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊),
  nnnorm.{u_1} (E := A) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simp_all [nnnorm_add_eq_max this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
have hS : IsClosed (↑S : Set A)
Tactic: have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
hS : IsClosed (↑S : Set A)
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
have hcomm₁ : Commute (star a) b
Tactic: have hcomm₁ := ha.commute_star_left hcomm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
hS : IsClosed (↑S : Set A)
hcomm₁ : Commute (star a) b
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
have hcomm₂ : Commute a (star b)
Tactic: have hcomm₂ := hb.commute_star_right hcomm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
hS : IsClosed (↑S : Set A)
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
have this : IsMulCommutative.{u_1} ↥(adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A)
Tactic: have : IsMulCommutative (adjoin ℂ {a, b}) :=
    isMulCommutative_adjoin ℂ (by grind) (by grind [commute_star_comm])
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
hS : IsClosed (↑S : Set A)
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative.{u_1} ↥(adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A)
x : NonUnitalCommRing ↥S := nonUnitalCommRingTopologicalClosure (adjoin ℂ (A := A) {a, b}) ⋯
x_1 : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ HMul.hMul (α := ↥S) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) a ⋯) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) b ⋯) = 0
have a₁ : (↑(HMul.hMul (α := ↥S) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) a sorry) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) b sorry)) : A) =
  (↑0 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
hS : IsClosed (↑S : Set A)
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative.{u_1} ↥(adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A)
x : NonUnitalCommRing ↥S := nonUnitalCommRingTopologicalClosure (adjoin ℂ (A := A) {a, b}) ⋯
x_1 : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
have refine_1 : a ∈ S
Tactic: refine CommCStarAlgebra.norm_add_eq_max (A := S) (a := ⟨a, ?_⟩) (b := ⟨b, ?_⟩) (by ext; simpa)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
hS : IsClosed (↑S : Set A)
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative.{u_1} ↥(adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A)
x : NonUnitalCommRing ↥S := nonUnitalCommRingTopologicalClosure (adjoin ℂ (A := A) {a, b}) ⋯
x_1 : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
refine_1 : a ∈ S
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
have refine_2 : b ∈ S
Tactic: refine CommCStarAlgebra.norm_add_eq_max (A := S) (a := ⟨a, ?_⟩) (b := ⟨b, ?_⟩) (by ext; simpa)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
hS : IsClosed (↑S : Set A)
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative.{u_1} ↥(adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A)
x : NonUnitalCommRing ↥S := nonUnitalCommRingTopologicalClosure (adjoin ℂ (A := A) {a, b}) ⋯
x_1 : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ a ∈ S
have refine_1 : Membership.mem (γ := NonUnitalStarSubalgebra ℂ A) (adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A) a
Tactic: apply le_topologicalClosure
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := topologicalClosure (A := A) (adjoin ℂ (A := A) {a, b})
hS : IsClosed (↑S : Set A)
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative.{u_1} ↥(adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A)
x : NonUnitalCommRing ↥S := nonUnitalCommRingTopologicalClosure (adjoin ℂ (A := A) {a, b}) ⋯
x_1 : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ b ∈ S
have refine_2 : Membership.mem (γ := NonUnitalStarSubalgebra ℂ A) (adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A) b
Tactic: apply le_topologicalClosure
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (h : ∀ i ∈ s, IsSelfAdjoint (f i)), nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
have insert : f j * ∑ i ∈ s, f i = 0
Tactic: suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSelfAdjoint (f i)),
  nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSelfAdjoint (f i)),
    nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have insert : ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
  (ih : ∀ (h : ∀ i ∈ s, IsSelfAdjoint (f i)), nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊)
  (h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)),
  nnnorm.{u_1} (E := A) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSelfAdjoint (f i)),
  nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSelfAdjoint (f i)),
    nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have insert : ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
  (ih : ∀ (h : ∀ i ∈ s, IsSelfAdjoint (f i)), nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊)
  (h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)),
  nnnorm.{u_1} (E := A) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
Cleared hypotheses: s, h