awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 =
      HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
h₃ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a)) y) 0 =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2
h₄ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
⊢ IsStarNormal a
have h₅ : deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
  HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2
Tactic: simp_rw [key] at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 =
      HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
h₄ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2
⊢ IsStarNormal a
have h₅ : HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 =
  HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2
Tactic: rw [h₃] at h₄
Cleared hypotheses: h₄, key, h₃
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 =
      HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
h₄ :
  HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 =
    HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2
⊢ IsStarNormal a
have refine_2 : star a * a = a * star a
Tactic: rw [isStarNormal_iff, commute_iff_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 =
      HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
h₄ :
  HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 =
    HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2
⊢ star a * a = a * star a
have refine_2 : Eq.{u_1 + 1} (α := A) ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (star a * a))
  ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (a * star a))
Tactic: apply nsmul_right_injective two_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 =
      HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
h₄ :
  HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 =
    HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2
⊢ Eq.{u_1 + 1} (α := A) ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (star a * a))
    ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (a * star a))
have refine_2 : ∀
  (h₄ :
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 -
        (HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2) =
      0)
  (key :
    ∀ (x : ℝ),
      NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
        NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a)))
  (h₃ :
    deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
      HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2),
  HSub.hSub (α := A) ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (star a * a))
      ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (a * star a)) =
    0
Tactic: rw [← sub_eq_zero] at h₄ ⊢
Cleared hypotheses: h₄, key, h₃
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 =
      HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
h₄ :
  HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 -
      (HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2) =
    0
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2
⊢ HSub.hSub (α := A) ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (star a * a))
      ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (a * star a)) =
    0
have refine_2 : HSub.hSub (α := A) ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (star a * a))
    ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (a * star a)) =
  HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 -
    (HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2)
Tactic: rw [← h₄]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 =
      HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
h₄ :
  HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 -
      (HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2) =
    0
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2
⊢ HSub.hSub (α := A) ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (star a * a))
      ((fun (a : A) ↦ HSMul.hSMul (α := ℕ) 2 a) (a * star a)) =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (-a * star a) + HPow.hPow (β := ℕ) (star a) 2 -
      (HPow.hPow (β := ℕ) (star a) 2 + HSMul.hSMul (α := ℕ) 2 (star a * -a) + HPow.hPow (β := ℕ) a 2)
have refine_2 : HSMul.hSMul (α := ℕ) 2 (star a * a) + -HSMul.hSMul (α := ℕ) 2 (a * star a) =
  a * a + HSMul.hSMul (α := ℕ) 2 (-(a * star a)) + star a * star a +
    -(star a * star a + HSMul.hSMul (α := ℕ) 2 (-(star a * a)) + a * a)
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
I : Ideal A
inst_3 : I.IsMaximal
a : A
ha : a ∈ I
⊢ Set.Nonempty.some (s := spectrum ℂ (A := A ⧸ I) ((Quotient.mk I : (a : A) → A ⧸ I) a : A ⧸ I)) ⋯ = 0
have simp_rw : Set.Nonempty.some (s := {0}) sorry = 0
Tactic: simp_rw [Quotient.eq_zero_iff_mem.mpr ha, spectrum.zero_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
ha : ¬IsUnit a
⊢ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), Eq (α := ℂ) ((f : (a : A) → ℂ) a : ℂ) (0 : ℂ)
have obtain : ∀ (M : Ideal A) (hM : M.IsMaximal) (haM : span {a} ≤ M),
  ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), Eq (α := ℂ) ((f : (a : A) → ℂ) a : ℂ) (0 : ℂ)
Tactic: obtain ⟨M, hM, haM⟩ := (span {a}).exists_le_maximal (span_singleton_ne_top ha)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ spectrum ℂ a ↔ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z
have refine_1 : ∀ (hz : z ∈ spectrum ℂ a), ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z
Tactic: refine ⟨fun hz => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
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
⊢ z ∈ spectrum ℂ a ↔ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z
have refine_2 : (∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z) → z ∈ spectrum ℂ a
Tactic: refine ⟨fun hz => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
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)), (f : (a : A) → ℂ) a = z
have 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
Tactic: obtain ⟨f, hf⟩ := WeakDual.CharacterSpace.exists_apply_eq_zero hz
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
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 : ℂ)
⊢ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z
have hf₁ : Eq (α := ℂ) ((algebraMap ℂ ℂ : (a : ℂ) → ℂ) z : ℂ) ((f : (a : A) → ℂ) a : ℂ)
Tactic: simp only [map_sub, sub_eq_zero, AlgHomClass.commutes] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : 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
have 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
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace 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
have 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
Tactic: rw [ContinuousMap.spectrum_eq_range, WeakDual.CharacterSpace.mem_spectrum_iff_exists]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
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), ℂ))
have 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‖
Tactic: refine AddMonoidHomClass.isometry_of_norm (gelfandTransform ℂ A) fun a => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
Goal:
A : Type u_1
inst : CommCStarAlgebra A
a : A
⊢ 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))
have rw : Eq (α := ENNReal) (⨆ k ∈ spectrum ℂ (star a * a), (↑‖k‖₊ : ENNReal)) (⨆ k ∈ spectrum ℂ (star a * a), (↑‖k‖₊ : ENNReal))
Tactic: rw [spectrum.gelfandTransform_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
Goal:
A : Type u_1
inst : CommCStarAlgebra A
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‖
have 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)
Tactic: have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by
    unfold spectralRadius; rw [spectrum.gelfandTransform_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
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)
⊢ 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‖
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (hypothesis)
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)
⊢ 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‖
have 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
Tactic: simp only [ENNReal.coe_inj, CStarRing.nnnorm_star_mul_self, ← sq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.GelfandDuality (goal)
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), ℂ))
have 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), ℂ))
Tactic: refine ⟨(gelfandTransform_isometry A).injective, ?_⟩