awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : IsStarNormal a
x : ℝ
⊢ Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
have h : NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) =
  (↑(expUnitary
        (x •
          HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
            (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A)))) :
    A)
Tactic: convert! (selfAdjoint.expUnitary (x • (2 : ℝ) • ℑ a)).2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : IsStarNormal a
x : ℝ
⊢ NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) =
    (↑(expUnitary
          (x •
            HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A)))) :
      A)
have hcomm : Commute (x • a) (-x • star a)
Tactic: have hcomm := star_comm_self (x := a) |>.symm.smul_left x |>.smul_right (-x)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : IsStarNormal a
x : ℝ
hcomm : Commute (x • a) (-x • star a)
⊢ NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a) =
    (↑(expUnitary
          (x •
            HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A)))) :
      A)
have h : NormedSpace.exp (x • a + -x • star a) =
  (↑(expUnitary
        (x •
          HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
            (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A)))) :
    A)
Tactic: rw [← exp_add_of_commute hcomm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : 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))
x : ℝ
u : ↥(unitary A) :=
  Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (unitary A) x)
    (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a)) ⋯
⊢ NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a)
have h : NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = (↑(star u) : A)
Tactic: convert! congr(($(Unitary.star_eq_inv u) : A))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : 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))
x : ℝ
u : ↥(unitary A) :=
  Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (unitary A) x)
    (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a)) ⋯
h : NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = (↑(star u) : A)
⊢ NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a)
have h₁ : NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = (↑u⁻¹ : A)
Tactic: convert! congr(($(Unitary.star_eq_inv u) : A))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : 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))
x : ℝ
u : ↥(unitary A) :=
  Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (unitary A) x)
    (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a)) ⋯
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = (↑u⁻¹ : A)
have h : NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a)) *
    (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a))) =
  1
Tactic: simp_rw [u, ← Unitary.val_inv_toUnits_apply, neg_smul, ← Units.mul_eq_one_iff_eq_inv,
          Unitary.val_toUnits_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : 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))
x : ℝ
u : ↥(unitary A) :=
  Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (unitary A) x)
    (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a)) ⋯
x_2 : (x : A) → Invertible (NormedSpace.exp x) := invertibleExp
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a)) *
      (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a))) =
    1
have h : NormedSpace.exp (x • star a) *
    (NormedSpace.exp (-(x • a)) * (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a)))) =
  1
Tactic: rw [mul_assoc]
-- 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))
⊢ IsStarNormal a
have key : ∀ (x : ℝ),
  NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a)
Tactic: have key : ∀ x : ℝ, exp (- x • a) * exp (x • star a) = exp (x • star a) * exp (- x • a) := by
      intro x
      let u : unitary A := ⟨_, ha x⟩
      convert! congr(($(Unitary.star_eq_inv u) : A))
      · simp [u, star_exp]
      · simp_rw [u, ← Unitary.val_inv_toUnits_apply, neg_smul, ← Units.mul_eq_one_iff_eq_inv,
          Unitary.val_toUnits_apply]
        let _ := invertibleExp (𝔸 := A)
        rw [mul_assoc]
        simp [← invOf_exp]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a_1 : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha :
  ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a_1) * NormedSpace.exp (-x • star a_1))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a_1) * NormedSpace.exp (x • star a_1) =
      NormedSpace.exp (x • star a_1) * NormedSpace.exp (-x • a_1)
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)
have rw : deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
  NormedSpace.exp (y • a) * a * c * NormedSpace.exp (y • b) +
    NormedSpace.exp (y • a) * c * (b * NormedSpace.exp (y • b))
Tactic: rw [mul_add, add_mul, ← mul_assoc _ a, ← mul_assoc _ c b, mul_assoc _ b]
-- 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))
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 : ∀ (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)
Tactic: have h_deriv (a b c : A) (y : ℝ) :
        deriv (fun x : ℝ ↦ exp (x • a) * c * exp (x • b)) y =
          exp (y • a) * (a * c + c * b) * exp (y • b) := by
      rw [mul_add, add_mul, ← mul_assoc _ a, ← mul_assoc _ c b, mul_assoc _ b]
      exact (hasDerivAt_exp_smul_const a y).mul_const c |>.mul
        (hasDerivAt_exp_smul_const' b y) |>.deriv
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a_1 : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha :
  ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a_1) * NormedSpace.exp (-x • star a_1))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a_1) * NormedSpace.exp (x • star a_1) =
      NormedSpace.exp (x • star a_1) * NormedSpace.exp (-x • a_1)
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)
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
have h : ∀ (y x : ℝ), NormedSpace.exp (x • a)
Tactic: enter [1, 1, y, 1, x, 1]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a_1 : A
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha :
  ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a_1) * NormedSpace.exp (-x • star a_1))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a_1) * NormedSpace.exp (x • star a_1) =
      NormedSpace.exp (x • star a_1) * NormedSpace.exp (-x • a_1)
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)
a b : A
y x : ℝ
| NormedSpace.exp (x • a)
have h : NormedSpace.exp (x • a) * 1
Tactic: rw [← mul_one (exp (x • a))]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a_1 : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha :
  ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a_1) * NormedSpace.exp (-x • star a_1))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a_1) * NormedSpace.exp (x • star a_1) =
      NormedSpace.exp (x • star a_1) * NormedSpace.exp (-x • a_1)
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)
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
have h : ∀ (y x : ℝ), NormedSpace.exp (x • a) * 1
Tactic: enter [1, 1, y, 1, x, 1]; rw [← mul_one (exp (x • a))]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a_1 : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha :
  ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a_1) * NormedSpace.exp (-x • star a_1))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a_1) * NormedSpace.exp (x • star a_1) =
      NormedSpace.exp (x • star a_1) * NormedSpace.exp (-x • a_1)
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)
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
have conv : deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * 1 * NormedSpace.exp (x • b)) y) 0 =
  HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
Tactic: conv => enter [1, 1, y, 1, x, 1]; rw [← mul_one (exp (x • a))]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a_1 : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha :
  ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a_1) * NormedSpace.exp (-x • star a_1))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a_1) * NormedSpace.exp (x • star a_1) =
      NormedSpace.exp (x • star a_1) * NormedSpace.exp (-x • a_1)
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)
a b : A
⊢ deriv (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ NormedSpace.exp (x • a) * 1 * NormedSpace.exp (x • b)) y) 0 =
    HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
have simp_rw : a * (a + b) + (a + b) * b = HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
Tactic: simp_rw [h_deriv, zero_smul, NormedSpace.exp_zero, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a_1 : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha :
  ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a_1) * NormedSpace.exp (-x • star a_1))
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a_1) * NormedSpace.exp (x • star a_1) =
      NormedSpace.exp (x • star a_1) * NormedSpace.exp (-x • a_1)
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)
a b : A
⊢ a * (a + b) + (a + b) * b = HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
have noncomm_ring : a * a + a * b + (a * b + b * b) = a * a + HSMul.hSMul (α := ℕ) 2 (a * b) + b * b
Tactic: noncomm_ring
-- 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))
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)
⊢ IsStarNormal a
have 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
Tactic: have h_deriv₂ (a b : A) :
        deriv (fun y ↦ deriv (fun x : ℝ ↦ exp (x • a) * exp (x • b)) y) 0 =
          a ^ 2 + 2 • (a * b) + b ^ 2 := by
      conv => enter [1, 1, y, 1, x, 1]; rw [← mul_one (exp (x • a))]
      simp_rw [h_deriv, zero_smul, NormedSpace.exp_zero, mul_one, one_mul]
      noncomm_ring
-- 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))
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
⊢ IsStarNormal a
have 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
Tactic: have h₃ := h_deriv₂ (-a) (star a)
-- 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))
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
⊢ IsStarNormal a
have 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
Tactic: have h₄ := h_deriv₂ (star a) (-a)
-- 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))
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
⊢ IsStarNormal a
have 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
Tactic: simp only [smul_neg, even_two, Even.neg_pow, neg_smul] at h₃ h₄ key
Cleared hypotheses: key, h₃, 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))
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
⊢ IsStarNormal a
have 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
Tactic: simp only [smul_neg, even_two, Even.neg_pow, neg_smul] at h₃ h₄ key
Cleared hypotheses: key, h₃, 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))
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
⊢ IsStarNormal a
have key₁ : ∀ (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
Cleared hypotheses: key, h₃, h₄