awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
refine_1 : ∀ (hz : z ∈ spectrum ℂ a), ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z
refine_2 : (∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z) → z ∈ spectrum ℂ a
⊢ z ∈ spectrum ℂ a ↔ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z

Tactic:
refine ⟨fun hz => ?_, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
refine_1 :
  ∀ (f : (↑(characterSpace ℂ A) : Type u_1))
    (hf : Eq (α := ℂ) ((f : (a : A) → ℂ) (HSub.hSub (α := A) ((algebraMap ℂ A : (a : ℂ) → A) z : A) a) : ℂ) (0 : ℂ)),
    ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z
⊢ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z

Tactic:
obtain ⟨f, hf⟩ := WeakDual.CharacterSpace.exists_apply_eq_zero hz

Premises used: WeakDual.CharacterSpace.exists_apply_eq_zero
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : (↑(characterSpace ℂ A) : Type u_1)
hf : Eq (α := ℂ) ((f : (a : A) → ℂ) (HSub.hSub (α := A) ((algebraMap ℂ A : (a : ℂ) → A) z : A) a) : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((algebraMap ℂ ℂ : (a : ℂ) → ℂ) z : ℂ) ((f : (a : A) → ℂ) a : ℂ)

Tactic:
simp only [map_sub, sub_eq_zero, AlgHomClass.commutes] at hf

Premises used: map_sub, sub_eq_zero, AlgHomClass.commutes
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : (↑(characterSpace ℂ A) : Type u_1)
hf : Eq (α := ℂ) ((algebraMap ℂ ℂ : (a : ℂ) → ℂ) z : ℂ) ((f : (a : A) → ℂ) a : ℂ)
⊢ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z

Tactic:
⟨_, hf.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : (↑(characterSpace ℂ A) : Type u_1)
hf : Eq (α := ℂ) ((algebraMap ℂ ℂ : (a : ℂ) → ℂ) z : ℂ) ((f : (a : A) → ℂ) a : ℂ)
⊢ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z

Tactic:
exact ⟨_, hf.symm⟩
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
f : (↑(characterSpace ℂ A) : Type u_1)
⊢ Membership.mem (α := ℂ) (spectrum ℂ a) ((f : (a : A) → ℂ) a : ℂ)

Tactic:
AlgHom.apply_mem_spectrum f a

Premises used: AlgHom.apply_mem_spectrum, Set.Mem
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
f : (↑(characterSpace ℂ A) : Type u_1)
⊢ Membership.mem (α := ℂ) (spectrum ℂ a) ((f : (a : A) → ℂ) a : ℂ)

Tactic:
exact AlgHom.apply_mem_spectrum f a

Premises used: AlgHom.apply_mem_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
h :
  ∀ (z : ℂ),
    z ∈
        spectrum ℂ (A := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
              a :
            C((↑(characterSpace ℂ A) : Type u_1), ℂ)) ↔
      z ∈ spectrum ℂ a
⊢ spectrum ℂ (A := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
      (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          a :
        C((↑(characterSpace ℂ A) : Type u_1), ℂ)) =
    spectrum ℂ a

Tactic:
ext z
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
h :
  Membership.mem (γ := Set ℂ)
      (Set.range (ι := (↑(characterSpace ℂ A) : Type u_1))
        (⇑(((gelfandTransform ℂ A : 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)) → ℂ))
      z ↔
    ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z
⊢ z ∈
      spectrum ℂ (A := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
        (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
              (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
            a :
          C((↑(characterSpace ℂ A) : Type u_1), ℂ)) ↔
    z ∈ spectrum ℂ a

Tactic:
rw [ContinuousMap.spectrum_eq_range, WeakDual.CharacterSpace.mem_spectrum_iff_exists]

Premises used: ContinuousMap.spectrum_eq_range, WeakDual.CharacterSpace.mem_spectrum_iff_exists
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
⊢ Membership.mem (γ := Set ℂ)
      (Set.range (ι := (↑(characterSpace ℂ A) : Type u_1))
        (⇑(((gelfandTransform ℂ A : 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)) → ℂ))
      z ↔
    ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
⊢ Membership.mem (γ := Set ℂ)
      (Set.range (ι := (↑(characterSpace ℂ A) : Type u_1))
        (⇑(((gelfandTransform ℂ A : 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)) → ℂ))
      z ↔
    ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
I : Ideal A
inst_3 : I.IsMaximal
inst_4 : Nontrivial A
⊢ Nonempty.{u_1 + 1} (↑(characterSpace ℂ A) : Type u_1)

Tactic:
⟨Classical.choose <|
      WeakDual.CharacterSpace.exists_apply_eq_zero <| zero_mem_nonunits.2 zero_ne_one⟩

Premises used: Iff.mpr, zero_ne_one, Nonempty.intro, zero_mem_nonunits, Classical.choose, WeakDual.CharacterSpace.exists_apply_eq_zero
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
⊢ Eq (α := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
          (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
        (star a) :
      C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (star
        (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          a) :
      C((↑(characterSpace ℂ A) : Type u_1), ℂ))

Tactic:
ContinuousMap.ext fun φ => map_star φ a

Premises used: StarHomClass.map_star, ContinuousMap.ext
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
⊢ Isometry (α := A) (β := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (⇑(gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
      (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))

Tactic:
AddMonoidHomClass.isometry_of_norm (gelfandTransform ℂ A) fun a => ?_

Premises used: AddMonoidHomClass.isometry_of_norm, Set.Mem, setOf, Complex, WeakDual.gelfandTransform
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
refine :
  ∀ (a : A),
    norm (E := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
        (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
              (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
            a :
          C((↑(characterSpace ℂ A) : Type u_1), ℂ)) =
      ‖a‖
⊢ Isometry (α := A) (β := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (⇑(gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
      (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))

Tactic:
refine AddMonoidHomClass.isometry_of_norm (gelfandTransform ℂ A) fun a => ?_

Premises used: AddMonoidHomClass.isometry_of_norm, Complex, WeakDual.gelfandTransform
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
rw rw₁ :
  Eq (α := ENNReal) (⨆ k ∈ spectrum ℂ (star a * a), (↑‖k‖₊ : ENNReal))
    (⨆ k ∈ spectrum ℂ (star a * a), (↑‖k‖₊ : ENNReal))
⊢ Eq (α := ENNReal)
    (⨆
      k ∈
        spectrum ℂ (A := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
              (star a * a) :
            C((↑(characterSpace ℂ A) : Type u_1), ℂ)),
      (↑‖k‖₊ : ENNReal))
    (⨆ k ∈ spectrum ℂ (star a * a), (↑‖k‖₊ : ENNReal))

Tactic:
rw [spectrum.gelfandTransform_eq]

Premises used: spectrum.gelfandTransform_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
⊢ spectralRadius ℂ (A := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
      (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          (star a * a) :
        C((↑(characterSpace ℂ A) : Type u_1), ℂ)) =
    spectralRadius ℂ (star a * a)

Tactic:
have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by
    unfold spectralRadius; rw [spectrum.gelfandTransform_eq]
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
this :
  spectralRadius ℂ (A := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
      (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          (star a * a) :
        C((↑(characterSpace ℂ A) : Type u_1), ℂ)) =
    spectralRadius ℂ (star a * a)
⊢ (↑‖HMul.hMul (α := C((↑(characterSpace ℂ A) : Type u_1), ℂ)) (β := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
            (star
                (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                    (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
                  a) :
              C((↑(characterSpace ℂ A) : Type u_1), ℂ))
            (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                  (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
                a :
              C((↑(characterSpace ℂ A) : Type u_1), ℂ))‖₊ :
      ENNReal) =
    (↑‖star a * a‖₊ : ENNReal)

Tactic:
rw [map_mul, (IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
    (IsSelfAdjoint.star_mul_self (gelfandTransform ℂ A a)).spectralRadius_eq_nnnorm] at this

Premises used: IsSelfAdjoint.star_mul_self, gelfandTransform_map_star, map_mul, IsSelfAdjoint.spectralRadius_eq_nnnorm, Complex, DFunLike.coe, WeakDual.gelfandTransform
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
this :
  (↑‖HMul.hMul (α := C((↑(characterSpace ℂ A) : Type u_1), ℂ)) (β := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
            (star
                (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                    (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
                  a) :
              C((↑(characterSpace ℂ A) : Type u_1), ℂ))
            (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
                  (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
                a :
              C((↑(characterSpace ℂ A) : Type u_1), ℂ))‖₊ :
      ENNReal) =
    (↑‖star a * a‖₊ : ENNReal)
⊢ HPow.hPow (β := ℕ)
      (nnnorm (E := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
        (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
              (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
            a :
          C((↑(characterSpace ℂ A) : Type u_1), ℂ)))
      2 =
    HPow.hPow (β := ℕ) ‖a‖₊ 2

Tactic:
simp only [ENNReal.coe_inj, CStarRing.nnnorm_star_mul_self, ← sq] at this

Premises used: ENNReal.coe_inj, sq, CStarRing.nnnorm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
this :
  HPow.hPow (β := ℕ)
      (nnnorm (E := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
        (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
              (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
            a :
          C((↑(characterSpace ℂ A) : Type u_1), ℂ)))
      2 =
    HPow.hPow (β := ℕ) ‖a‖₊ 2
⊢ norm (E := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
      (((gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
            (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))
          a :
        C((↑(characterSpace ℂ A) : Type u_1), ℂ)) =
    ‖a‖

Tactic:
simpa only [Function.comp_apply, NNReal.sqrt_sq] using
    congr_arg (((↑) : ℝ≥0 → ℝ) ∘ ⇑NNReal.sqrt) this

Premises used: NNReal.sqrt_sq, Function.comp, congr_arg, NNReal.sqrt, Function.comp_apply, DFunLike.coe, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
⊢ Function.Bijective (α := A) (β := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (⇑(gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
      (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))

Tactic:
⟨(gelfandTransform_isometry A).injective, ?_⟩

Premises used: Isometry.injective, And.intro, Function.Bijective, gelfandTransform_isometry
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
refine :
  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), ℂ))
⊢ Function.Bijective (α := A) (β := C((↑(characterSpace ℂ A) : Type u_1), ℂ))
    (⇑(gelfandTransform ℂ A : A →ₐ[ℂ] C((↑(characterSpace ℂ A) : Type u_1), ℂ)) :
      (a : A) → C((↑(characterSpace ℂ A) : Type u_1), ℂ))

Tactic:
refine ⟨(gelfandTransform_isometry A).injective, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
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), ℂ))
⊢ 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), ℂ))

Tactic:
use star a

Premises used: Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
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)) → ℂ)
          φ :
        ℂ)
⊢ 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:
ext1 φ
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
φ : (↑(characterSpace ℂ A) : Type u_1)
⊢ Eq (α := ℂ) ((φ : (a : A) → ℂ) (star a) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : A) → ℂ) a : ℂ) : ℂ)

Tactic:
simp only [map_star, RCLike.star_def]

Premises used: RCLike.star_def, StarHomClass.map_star
-- 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' := ⋯ }
suffices : rng = ⊤
⊢ 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), ℂ))

Tactic:
suffices rng = ⊤ from
    fun x => show x ∈ rng from this.symm ▸ StarSubalgebra.mem_top
-- 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' := ⋯ }
⊢ 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 _)
-- 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
⊢ rng = ⊤

Tactic:
h ▸ ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
    _ (fun _ _ => ?_)

Premises used: Eq.rec, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
-- 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
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
⊢ rng = ⊤

Tactic:
refine h ▸ ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
    _ (fun _ _ => ?_)
-- 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)
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
⊢ 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:
contrapose!
-- 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:
fun h => Subtype.ext (ContinuousLinearMap.ext fun a =>
    h (gelfandTransform ℂ A a) ⟨gelfandTransform ℂ A a, ⟨a, rfl⟩, rfl⟩)

Premises used: And.intro, Exists.intro, Complex, DFunLike.coe, ContinuousLinearMap.ext, rfl, WeakDual.gelfandTransform, Subtype.ext