awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • 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
⊢ 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

Tactic:
simp only [smul_neg, even_two, Even.neg_pow, neg_smul] at h₃ h₄ key

Premises used: neg_smul, even_two, Even.neg_pow, smul_neg
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • 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
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
⊢ 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

Tactic:
simp only [smul_neg, even_two, Even.neg_pow, neg_smul] at h₃ h₄ key

Premises used: neg_smul, even_two, Even.neg_pow, smul_neg
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • 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
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
⊢ ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))

Tactic:
simp only [smul_neg, even_two, Even.neg_pow, neg_smul] at h₃ h₄ key

Premises used: neg_smul, even_two, Even.neg_pow, smul_neg
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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))
⊢ 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₃
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
⊢ 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₄
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
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
⊢ ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))

Tactic:
rw [h₃] at h₄
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
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))
⊢ 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:
rw [h₃] at h₄
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
refine_2 : star a * a = a * star a
⊢ IsStarNormal a

Tactic:
rw [isStarNormal_iff, commute_iff_eq]

Premises used: isStarNormal_iff, commute_iff_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
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))
⊢ star a * a = a * star a

Tactic:
apply nsmul_right_injective two_ne_zero

Premises used: two_ne_zero, nsmul_right_injective
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
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
⊢ 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:
rw [← sub_eq_zero] at h₄ ⊢

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
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)
⊢ 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 [← h₄]
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
refine_2 refine_2₁ refine_2₂ 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)
⊢ 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:
noncomm_ring
-- 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
a : A
ha : a ∈ I
simp_rw : Set.Nonempty.some (s := {0}) ⋯ = 0
⊢ Set.Nonempty.some (s := spectrum ℂ (A := A ⧸ I) ((Quotient.mk I : (a : A) → A ⧸ I) a : A ⧸ I)) ⋯ = 0

Tactic:
simp_rw [Quotient.eq_zero_iff_mem.mpr ha, spectrum.zero_eq]

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem, spectrum.zero_eq
-- 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
a : A
ha : a ∈ I
⊢ Set.Nonempty.some (s := {0}) ⋯ = 0

Tactic:
Set.eq_of_mem_singleton (Set.singleton_nonempty (0 : ℂ)).some_mem

Premises used: Set.singleton_nonempty, Set.eq_of_mem_singleton, Set.Nonempty.some_mem, OfNat.ofNat
-- 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
a : A
ha : a ∈ I
⊢ Set.Nonempty.some (s := {0}) ⋯ = 0

Tactic:
exact Set.eq_of_mem_singleton (Set.singleton_nonempty (0 : ℂ)).some_mem

Premises used: Set.singleton_nonempty, Set.eq_of_mem_singleton, Set.Nonempty.some_mem, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
ha : ¬IsUnit a
obtain :
  ∀ (M : Ideal A) (hM : M.IsMaximal) (haM : span {a} ≤ M),
    ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), Eq (α := ℂ) ((f : (a : A) → ℂ) a : ℂ) (0 : ℂ)
⊢ ∃ (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)

Premises used: Ideal.exists_le_maximal, Ideal.span, Ideal.span_singleton_ne_top, Singleton.singleton
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Goal:
A : Type u_1
inst : NormedCommRing A
inst_1 : NormedAlgebra ℂ A
inst_2 : CompleteSpace A
a : A
ha : ¬IsUnit a
M : Ideal A
hM : M.IsMaximal
haM : span {a} ≤ M
⊢ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), Eq (α := ℂ) ((f : (a : A) → ℂ) a : ℂ) (0 : ℂ)

Tactic:
⟨M.toCharacterSpace,
      M.toCharacterSpace_apply_eq_zero_of_mem
        (haM (mem_span_singleton.mpr ⟨1, (mul_one a).symm⟩))⟩

Premises used: Iff.mpr, Ideal.toCharacterSpace_apply_eq_zero_of_mem, Ideal.toCharacterSpace, Exists.intro, mul_one, Ideal.mem_span_singleton, OfNat.ofNat, 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
ha : ¬IsUnit a
M : Ideal A
hM : M.IsMaximal
haM : span {a} ≤ M
⊢ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), Eq (α := ℂ) ((f : (a : A) → ℂ) a : ℂ) (0 : ℂ)

Tactic:
exact
    ⟨M.toCharacterSpace,
      M.toCharacterSpace_apply_eq_zero_of_mem
        (haM (mem_span_singleton.mpr ⟨1, (mul_one a).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 : ℂ
⊢ z ∈ spectrum ℂ a ↔ ∃ (f : (↑(characterSpace ℂ A) : Type u_1)), (f : (a : A) → ℂ) a = z

Tactic:
⟨fun hz => ?_, ?_⟩

Premises used: Iff.intro