awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a x : A
ha : IsStarNormal a
h : Commute x a
⊢ Commute x (star a)

Tactic:
h.semiconjBy.star_right ha ha

Premises used: Commute.semiconjBy, Commute, SemiconjBy.star_right
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a x : A
ha : IsStarNormal a
h : Commute a x
⊢ Commute (star a) x

Tactic:
ha.commute_star_right h.symm |>.symm

Premises used: IsStarNormal.commute_star_right, Commute.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ IsAddTorsionFree A

Tactic:
have : IsAddTorsionFree A := IsAddTorsionFree.of_module_rat A
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
⊢ IsStarNormal a ↔
    ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))

Tactic:
⟨fun ha x ↦ ?_, fun ha ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
refine_1 :
  ∀ (ha : IsStarNormal a) (x : ℝ),
    Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
refine_2 :
  ∀
    (ha :
      ∀ (x : ℝ),
        Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))),
    IsStarNormal a
⊢ IsStarNormal a ↔
    ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))

Tactic:
refine ⟨fun ha x ↦ ?_, fun ha ↦ ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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)
    (↑(expUnitary
          (x •
            HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A)))) :
      A)

Tactic:
(selfAdjoint.expUnitary (x • (2 : ℝ) • ℑ a)).2

Premises used: selfAdjoint.expUnitary, imaginaryPart, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : IsStarNormal a
x : ℝ
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)
⊢ Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))

Tactic:
convert! (selfAdjoint.expUnitary (x • (2 : ℝ) • ℑ a)).2

Premises used: selfAdjoint.expUnitary, imaginaryPart, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : IsStarNormal a
x : ℝ
⊢ Commute (x • a) (-x • star a)

Tactic:
have hcomm := star_comm_self (x := a) |>.symm.smul_left x |>.smul_right (-x)
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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)
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)
⊢ 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:
rw [← exp_add_of_commute hcomm]

Premises used: NormedSpace.exp_add_of_commute
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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 + -x • star a) =
    (↑(expUnitary
          (x •
            HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a : ↥(selfAdjoint A)))) :
      A)

Tactic:
simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_comm x I, smul_smul I I, smul_add x,
      sub_eq_add_neg]

Premises used: sub_eq_add_neg, smul_smul, imaginaryPart_apply_coe, SMulCommClass.smul_comm, OfNat.ofNat, smul_add, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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)) ⋯
⊢ (↑(star u) : A) = (↑u⁻¹ : A)

Tactic:
congr(($(Unitary.star_eq_inv u) : A))

Premises used: congrArg, id, Unitary.star_eq_inv, Subtype.val
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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)
h₁ : NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = (↑u⁻¹ : A)
⊢ NormedSpace.exp (-x • a) * NormedSpace.exp (x • star a) = NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a)

Tactic:
convert! congr(($(Unitary.star_eq_inv u) : A))
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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) = (↑(star u) : A)

Tactic:
simp [u, star_exp]

Premises used: NormedSpace.star_exp
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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 • star a) * NormedSpace.exp (-(x • a)) *
      (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a))) =
    1
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = (↑u⁻¹ : A)

Tactic:
simp_rw [u, ← Unitary.val_inv_toUnits_apply, neg_smul, ← Units.mul_eq_one_iff_eq_inv,
          Unitary.val_toUnits_apply]

Premises used: neg_smul, Units.mul_eq_one_iff_eq_inv, Unitary.val_toUnits_apply, Unitary.val_inv_toUnits_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
h :
  NormedSpace.exp (x • star a) *
      (NormedSpace.exp (-(x • a)) * (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a)))) =
    1
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a)) *
      (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a))) =
    1

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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

Tactic:
simp [← invOf_exp]

Premises used: NormedSpace.invOf_exp
-- 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))
⊢ ∀ (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]
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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 : ℝ
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))
⊢ 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:
rw [mul_add, add_mul, ← mul_assoc _ a, ← mul_assoc _ c b, mul_assoc _ b]

Premises used: add_mul, mul_assoc, mul_add
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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 * NormedSpace.exp (y • b) +
      NormedSpace.exp (y • a) * c * (b * NormedSpace.exp (y • b))

Tactic:
(hasDerivAt_exp_smul_const a y).mul_const c |>.mul
        (hasDerivAt_exp_smul_const' b y) |>.deriv

Premises used: HasDerivAt.deriv, hasDerivAt_exp_smul_const, HasDerivAt.mul, hasDerivAt_exp_smul_const', HasDerivAt.mul_const
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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 * NormedSpace.exp (y • b) +
      NormedSpace.exp (y • a) * c * (b * NormedSpace.exp (y • b))

Tactic:
exact (hasDerivAt_exp_smul_const a y).mul_const c |>.mul
        (hasDerivAt_exp_smul_const' b y) |>.deriv

Premises used: HasDerivAt.deriv, hasDerivAt_exp_smul_const, HasDerivAt.mul, hasDerivAt_exp_smul_const', HasDerivAt.mul_const
-- 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)
⊢ ∀ (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
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
h : ∀ (y x : ℝ), NormedSpace.exp (x • 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:
enter [1, 1, y, 1, x, 1]
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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 : ℝ
h : NormedSpace.exp (x • a) * 1
| NormedSpace.exp (x • a)

Tactic:
rw [← mul_one (exp (x • a))]

Premises used: NormedSpace.exp, HSMul.hSMul, mul_one
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
h : ∀ (y x : ℝ), NormedSpace.exp (x • a) * 1
| 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:
enter [1, 1, y, 1, x, 1]; rw [← mul_one (exp (x • a))]
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
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
⊢ 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:
conv => enter [1, 1, y, 1, x, 1]; rw [← mul_one (exp (x • a))]
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
simp_rw : a * (a + b) + (a + b) * b = HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2
⊢ 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:
simp_rw [h_deriv, zero_smul, NormedSpace.exp_zero, mul_one, one_mul]

Premises used: NormedSpace.exp_zero, zero_smul, mul_one, one_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
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
noncomm_ring noncomm_ring₁ noncomm_ring₂ noncomm_ring₃ :
  a * a + a * b + (a * b + b * b) = a * a + HSMul.hSMul (α := ℕ) 2 (a * b) + b * b
⊢ a * (a + b) + (a + b) * b = HPow.hPow (β := ℕ) a 2 + HSMul.hSMul (α := ℕ) 2 (a * b) + HPow.hPow (β := ℕ) b 2

Tactic:
noncomm_ring
-- 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)
⊢ ∀ (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
-- 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
⊢ 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)
-- 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
⊢ 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)