awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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)
⊢ (∀ (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:
exact fun h => Subtype.ext (ContinuousLinearMap.ext fun a =>
    h (gelfandTransform ℂ A a) ⟨gelfandTransform ℂ A a, ⟨a, rfl⟩, rfl⟩)

Premises used: ContinuousLinearMap.ext, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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)
⊢ Isometry f

Tactic:
have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ f 0 = 0

Tactic:
simp [f]
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ f (a + b) = f a + f b

Tactic:
simp [f]
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
simp_rw : ‖f a + f b‖ = max ‖f a‖ ‖f b‖
⊢ ‖a + b‖ = max ‖a‖ ‖b‖

Tactic:
simp_rw [← hf.norm_map_of_map_zero (by simp [f]), show f (a + b) = f a + f b by simp [f]]

Premises used: Isometry.norm_map_of_map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ f a * f b = 0

Tactic:
simpa [f] using congr(f $h)
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ ‖f a + f b‖ = max ‖f a‖ ‖f b‖

Tactic:
exact ContinuousMap.norm_add_eq_max <| by simpa [f] using congr(f $h)

Premises used: ContinuousMap.norm_add_eq_max
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
⊢ ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊

Tactic:
NNReal.eq <| norm_add_eq_max h

Premises used: NNReal.eq, CommCStarAlgebra.norm_add_eq_max
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
⊢ a * -b = 0

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
⊢ ‖a - b‖ = max ‖a‖ ‖b‖

Tactic:
simpa [sub_eq_add_neg] using norm_add_eq_max (a := a) (b := -b) (by simpa)

Premises used: sub_eq_add_neg, CommCStarAlgebra.norm_add_eq_max
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
⊢ ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊

Tactic:
NNReal.eq <| norm_sub_eq_max h

Premises used: NNReal.eq, CommCStarAlgebra.norm_sub_eq_max
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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‖₊
this : f j * ∑ i ∈ s, f i = 0
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
simp_all [nnnorm_add_eq_max this]

Premises used: CommCStarAlgebra.nnnorm_add_eq_max
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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‖₊
insert : f j * ∑ i ∈ s, f i = 0
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ Insert.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
suffices f j * ∑ i ∈ s, f i = 0 by simp_all [nnnorm_add_eq_max this]
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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‖₊
i : ι
hi : i ∈ s
⊢ j ≠ i

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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‖₊
⊢ f j * ∑ i ∈ s, f i = 0

Tactic:
simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

Premises used: Finset.mul_sum, Finset.sum_eq_zero
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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‖₊
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.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = 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)

Premises used: Finset.mul_sum, Finset.sum_eq_zero, Insert.insert
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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‖₊
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.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ s, f i) = 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)

Premises used: Finset.mul_sum, Finset.sum_eq_zero, Insert.insert
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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})
⊢ IsClosed (↑S : Set A)

Tactic:
have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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)
⊢ Commute (star a) b

Tactic:
have hcomm₁ := ha.commute_star_left hcomm
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ Commute a (star b)

Tactic:
have hcomm₂ := hb.commute_star_right hcomm
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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)
⊢ ∀ (x : A), Membership.mem (γ := Set A) {a, b} x → ∀ (y : A), Membership.mem (γ := Set A) {a, b} y → x * y = y * x

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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_1 : A),
    Membership.mem (γ := Set A) {a, b} a_1 →
      ∀ (b_1 : A), Membership.mem (γ := Set A) {a, b} b_1 → a_1 * star b_1 = star b_1 * a_1

Tactic:
grind [commute_star_comm]

Premises used: commute_star_comm
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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)
⊢ 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])
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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₁ :
  (↑(HMul.hMul (α := ↥S) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) a ⋯) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) b ⋯)) : A) =
    (↑0 : A)
⊢ HMul.hMul (α := ↥S) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) a ⋯) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) b ⋯) = 0

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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 ⋯)) : A) =
    (↑0 : A)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
refine_2 : b ∈ S
⊢ ‖a + b‖ = max ‖a‖ ‖b‖

Tactic:
refine CommCStarAlgebra.norm_add_eq_max (A := S) (a := ⟨a, ?_⟩) (b := ⟨b, ?_⟩) (by ext; simpa)

Premises used: CommCStarAlgebra.norm_add_eq_max
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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 : Membership.mem (γ := NonUnitalStarSubalgebra ℂ A) (adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A) a
⊢ a ∈ S

Tactic:
apply le_topologicalClosure

Premises used: NonUnitalStarSubalgebra.le_topologicalClosure
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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 := ⋯ }
⊢ Membership.mem (γ := NonUnitalStarSubalgebra ℂ A) (adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A) a

Tactic:
aesop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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_2 : Membership.mem (γ := NonUnitalStarSubalgebra ℂ A) (adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A) b
⊢ b ∈ S

Tactic:
apply le_topologicalClosure

Premises used: NonUnitalStarSubalgebra.le_topologicalClosure
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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 := ⋯ }
⊢ Membership.mem (γ := NonUnitalStarSubalgebra ℂ A) (adjoin ℂ (A := A) {a, b} : NonUnitalStarSubalgebra ℂ A) b

Tactic:
aesop
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊

Tactic:
NNReal.eq <| ha.norm_add_eq_max hb hcomm hab

Premises used: IsStarNormal.norm_add_eq_max, NNReal.eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ a * -b = 0

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ ‖a - b‖ = max ‖a‖ ‖b‖

Tactic:
simpa [sub_eq_add_neg] using
    ha.norm_add_eq_max hb.neg hcomm.neg_right (by simpa)

Premises used: IsStarNormal.norm_add_eq_max, sub_eq_add_neg, IsStarNormal.neg, Commute.neg_right
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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
⊢ ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊

Tactic:
NNReal.eq <| ha.norm_sub_eq_max hb hcomm hab

Premises used: IsStarNormal.norm_sub_eq_max, NNReal.eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ Commute a b

Tactic:
grind [commute_of_mul_eq_zero]

Premises used: IsSelfAdjoint.commute_of_mul_eq_zero
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊

Tactic:
NNReal.eq <| ha.norm_add_eq_max hb hab

Premises used: NNReal.eq, IsSelfAdjoint.norm_add_eq_max
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ a * -b = 0

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ ‖a - b‖ = max ‖a‖ ‖b‖

Tactic:
simpa [sub_eq_add_neg] using ha.norm_add_eq_max hb.neg (by simpa)

Premises used: sub_eq_add_neg, IsSelfAdjoint.neg, IsSelfAdjoint.norm_add_eq_max
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊

Tactic:
NNReal.eq <| ha.norm_sub_eq_max hb hab

Premises used: IsSelfAdjoint.norm_sub_eq_max, NNReal.eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun (x1 x2 : A) ↦ x1 * x2 = 0) on f)
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSelfAdjoint (f i)
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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)
this : f j * ∑ i ∈ s, f i = 0
⊢ j ∈ insert j s

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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)
this : f j * ∑ i ∈ s, f i = 0
⊢ IsSelfAdjoint.{u_1} (R := A) (∑ i ∈ s, f i)

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
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)
this : f j * ∑ i ∈ s, f i = 0
⊢ nnnorm.{u_1} (E := A) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]

Premises used: IsSelfAdjoint.nnnorm_add_eq_max