awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) (↑e : Unitization ℂ A) 1
⊢ Commute (↑e : Unitization ℂ A) (HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A))

Tactic:
simp [commute_iff_eq, mul_sub, sub_mul, mul_two, two_mul]

Premises used: mul_sub, commute_iff_eq, two_mul, sub_mul, mul_two
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
⊢ (↑e : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 2 (↑e : Unitization ℂ A) =
    (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)

Tactic:
simp [mul_sub, two_smul, mul_two]

Premises used: mul_sub, two_smul, mul_two
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
⊢ LE.le (α := Unitization ℂ A) 0 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)

Tactic:
have := calc
      0 ≤ (e : A⁺¹) * (2 - e) := by
        have : (e : A⁺¹) ≤ 1 := norm_le_one_iff_of_nonneg _ (by simpa) |>.mp (by simpa [norm_inr])
        apply Commute.mul_nonneg (by simpa) (by grw [sub_nonneg, this, one_le_two])
        simp [commute_iff_eq, mul_sub, sub_mul, mul_two, two_mul]
      _ = (((2 : ℝ) • e - e * e : A) : A⁺¹) := by simp [mul_sub, two_smul, mul_two]
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) 0 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
⊢ LT.lt (α := ℝ) 0 2⁻¹ ∧
    LT.lt (α := ℝ) 0 2⁻¹ ∧
      HAdd.hAdd (α := ℝ) 2⁻¹ 2⁻¹ = 1 ∧
        HSMul.hSMul (α := ℝ) 2⁻¹ (e * e) + HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) 2 e - e * e) = e

Tactic:
simp [smul_sub, ← one_div, smul_smul]

Premises used: smul_smul, smul_sub, one_div
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) 0 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
refine_2 : ‖e * e‖ ≤ 1
refine_2₁ : ‖HSMul.hSMul (α := ℝ) 2 e - e * e‖ ≤ 1
⊢ IsStarProjection e

Tactic:
refine ⟨h3 _ (Commute.mul_nonneg h1 h1 rfl) ?_ ((2 : ℝ) • e - e * e) this.of_inr ?_
      ⟨2⁻¹, 2⁻¹, by simp [smul_sub, ← one_div, smul_smul]⟩, h1.isSelfAdjoint⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) 0 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
refine_2 : ‖e‖ * ‖e‖ ≤ 1
refine_2₁ : HMul.hMul (α := ℝ) 1 1 ≤ 1
refine_2₂ refine_2₃ : LE.le (α := ℝ) 1 1
⊢ ‖e * e‖ ≤ 1

Tactic:
grw [norm_mul_le, h2, one_mul]

Premises used: norm_mul_le, one_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) 0 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
refine_2 : 0 ≤ HSub.hSub (α := Unitization ℂ A) 1 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
⊢ ‖HSMul.hSMul (α := ℝ) 2 e - e * e‖ ≤ 1

Tactic:
rw [← norm_inr (𝕜 := ℂ), norm_le_one_iff_of_nonneg _ this, ← sub_nonneg]

Premises used: CStarAlgebra.norm_le_one_iff_of_nonneg, sub_nonneg, Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) 0 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
⊢ 0 ≤
    star (HSub.hSub (α := Unitization ℂ A) 1 (↑e : Unitization ℂ A)) *
      HSub.hSub (α := Unitization ℂ A) 1 (↑e : Unitization ℂ A)

Tactic:
star_mul_self_nonneg _

Premises used: star_mul_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) 0 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
⊢ star (HSub.hSub (α := Unitization ℂ A) 1 (↑e : Unitization ℂ A)) *
      HSub.hSub (α := Unitization ℂ A) 1 (↑e : Unitization ℂ A) =
    HSub.hSub (α := Unitization ℂ A) 1 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)

Tactic:
simp [LE.le.star_eq, h1, mul_sub, sub_mul, two_smul, sub_sub, add_sub]

Premises used: LE.le.star_eq, mul_sub, add_sub, two_smul, sub_mul, sub_sub
-- Module: Mathlib.Analysis.CStarAlgebra.Extreme
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
e : A
h : (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : LE.le (α := Unitization ℂ A) 0 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
calc :
  star (HSub.hSub (α := Unitization ℂ A) 1 (↑e : Unitization ℂ A)) *
      HSub.hSub (α := Unitization ℂ A) 1 (↑e : Unitization ℂ A) =
    HSub.hSub (α := Unitization ℂ A) 1 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
⊢ 0 ≤ HSub.hSub (α := Unitization ℂ A) 1 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)

Tactic:
calc 0 ≤ star (1 - e : A⁺¹) * (1 - e) := star_mul_self_nonneg _
        _ = _ := by simp [LE.le.star_eq, h1, mul_sub, sub_mul, two_smul, sub_sub, add_sub]

Premises used: HSub.hSub, Unitization.inr, star_mul_self_nonneg, OfNat.ofNat, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
nth_rw :
  NormedSpace.exp (z • star b) * (NormedSpace.exp (-(star z • b)) * x * NormedSpace.exp (star z • a)) *
      NormedSpace.exp (z • star (-a)) =
    (↑(expUnitary
              (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
                (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
          A) *
        x *
      (↑(expUnitary
            (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (star z • a) : ↥(selfAdjoint A)))) :
        A)
⊢ expMulMulExp a b x z =
    (↑(expUnitary
              (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
                (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
          A) *
        x *
      (↑(expUnitary
            (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (star z • a) : ↥(selfAdjoint A)))) :
        A)

Tactic:
nth_rw 1 [expMulMulExp, ← (h.smul_right (star z)).exp_neg_mul_mul_exp_eq_self]

Premises used: _private.0.expMulMulExp, SemiconjBy.smul_right, SemiconjBy.exp_neg_mul_mul_exp_eq_self, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
simp_rw :
  NormedSpace.exp (z • star b) * NormedSpace.exp (-(star z • b)) * x *
      (NormedSpace.exp (star z • a) * NormedSpace.exp (z • star (-a))) =
    (↑(expUnitary
              (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
                (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
          A) *
        x *
      (↑(expUnitary
            (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (star z • a) : ↥(selfAdjoint A)))) :
        A)
⊢ NormedSpace.exp (z • star b) * (NormedSpace.exp (-(star z • b)) * x * NormedSpace.exp (star z • a)) *
      NormedSpace.exp (z • star (-a)) =
    (↑(expUnitary
              (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
                (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
          A) *
        x *
      (↑(expUnitary
            (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (star z • a) : ↥(selfAdjoint A)))) :
        A)

Tactic:
simp_rw [← mul_assoc, mul_assoc (_ * _ * x)]

Premises used: HMul.hMul, mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
h₁ :
  NormedSpace.exp (z • star b) * NormedSpace.exp (-(star z • b)) =
    (↑(expUnitary
          (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
            (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
      A)
h₂ :
  NormedSpace.exp (star z • a) * NormedSpace.exp (z • star (-a)) =
    (↑(expUnitary
          (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
            (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (star z • a) : ↥(selfAdjoint A)))) :
      A)
⊢ NormedSpace.exp (z • star b) * NormedSpace.exp (-(star z • b)) * x *
      (NormedSpace.exp (star z • a) * NormedSpace.exp (z • star (-a))) =
    (↑(expUnitary
              (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
                (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
          A) *
        x *
      (↑(expUnitary
            (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (star z • a) : ↥(selfAdjoint A)))) :
        A)

Tactic:
congr!
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
h₁ :
  NormedSpace.exp (z • star b) * NormedSpace.exp (-HSMul.hSMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) b) =
    NormedSpace.exp (z • star b + -HSMul.hSMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) b)
⊢ NormedSpace.exp (z • star b) * NormedSpace.exp (-(star z • b)) =
    (↑(expUnitary
          (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
            (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
      A)

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

Premises used: sub_eq_add_neg, smul_smul, imaginaryPart_apply_coe, SMulCommClass.smul_comm, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * NormedSpace.exp (-HSMul.hSMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) b) =
    NormedSpace.exp (z • star b + -HSMul.hSMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) b)

Tactic:
grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]

Premises used: Commute.smul_right, Commute.neg_right, NormedSpace.exp_add_of_commute
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
h₁ :
  NormedSpace.exp (HSMul.hSMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) a) * NormedSpace.exp (-(z • star a)) =
    NormedSpace.exp (HSMul.hSMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) a + -(z • star a))
⊢ NormedSpace.exp (star z • a) * NormedSpace.exp (z • star (-a)) =
    (↑(expUnitary
          (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
            (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (star z • a) : ↥(selfAdjoint A)))) :
      A)

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

Premises used: sub_eq_add_neg, smul_smul, imaginaryPart_apply_coe, SMulCommClass.smul_comm, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (HSMul.hSMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) a) * NormedSpace.exp (-(z • star a)) =
    NormedSpace.exp (HSMul.hSMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) a + -(z • star a))

Tactic:
grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]

Premises used: Commute.smul_right, Commute.neg_right, NormedSpace.exp_add_of_commute
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
unfold :
  Differentiable.{0, 0, u_1} ℂ (F := A) fun (z : ℂ) ↦ NormedSpace.exp (z • star b) * x * NormedSpace.exp (z • star (-a))
⊢ Differentiable ℂ (expMulMulExp a b x)

Tactic:
unfold expMulMulExp

Premises used: _private.0.expMulMulExp
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
⊢ Differentiable.{0, 0, u_1} ℂ (F := A) fun (z : ℂ) ↦ NormedSpace.exp (z • star b) * x * NormedSpace.exp (z • star (-a))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
⊢ Differentiable ℂ (expMulMulExp a b x)

Tactic:
have hf : Differentiable ℂ (expMulMulExp a b x : ℂ → A) := by unfold expMulMulExp; fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
apply : Set.range (expMulMulExp a b x) ⊆ Metric.sphere 0 ‖x‖
⊢ IsBounded (Set.range (expMulMulExp a b x))

Tactic:
apply Metric.isBounded_sphere (x := (0 : A)) (r := ‖x‖) |>.subset

Premises used: Bornology.IsBounded.subset, Metric.isBounded_sphere
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z_1 : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
z : ℂ
rw : ‖expMulMulExp a b x z - 0‖ = ‖x‖
rw₁ : ‖expMulMulExp a b x z‖ = ‖x‖
rw₂ :
  ‖(↑(expUnitary
                (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
                  (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
            A) *
          x *
        (↑(expUnitary
              (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
                (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (star z • a) : ↥(selfAdjoint A)))) :
          A)‖ =
    ‖x‖
rw₃ :
  ‖(↑(expUnitary
              (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
                (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
          A) *
        x‖ =
    ‖x‖
rw₄ rw₅ : ‖x‖ = ‖x‖
⊢ Membership.mem (γ := Set A) (Metric.sphere 0 ‖x‖) (expMulMulExp a b x z)

Tactic:
rw [mem_sphere_iff_norm, sub_zero, expMulMulExp_eq_expUnitary_mul_mul_expUnitary h z,
      CStarRing.norm_mul_coe_unitary, CStarRing.norm_coe_unitary_mul]

Premises used: CStarRing.norm_mul_coe_unitary, sub_zero, _private.0.expMulMulExp_eq_expUnitary_mul_mul_expUnitary, mem_sphere_iff_norm, CStarRing.norm_coe_unitary_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
⊢ IsBounded (Set.range (expMulMulExp a b x))

Tactic:
have : IsBounded (Set.range (expMulMulExp a b x)) := by
    apply Metric.isBounded_sphere (x := (0 : A)) (r := ‖x‖) |>.subset
    rintro - ⟨z, hz, rfl⟩
    rw [mem_sphere_iff_norm, sub_zero, expMulMulExp_eq_expUnitary_mul_mul_expUnitary h z,
      CStarRing.norm_mul_coe_unitary, CStarRing.norm_coe_unitary_mul]
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
this : IsBounded (Set.range (expMulMulExp a b x))
⊢ expMulMulExp a b x z = x

Tactic:
simpa [expMulMulExp] using hf.apply_eq_apply_of_bounded this z 0

Premises used: _private.0.expMulMulExp, Differentiable.apply_eq_apply_of_bounded, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a_1 b x : A
inst_1 : IsStarNormal a_1
inst_2 : IsStarNormal b
h : SemiconjBy x a_1 b
key : ∀ (z : ℂ), x * NormedSpace.exp (z • star a_1) = NormedSpace.exp (z • star b) * x
a : A
⊢ HasDerivAt (fun (z : ℂ) ↦ NormedSpace.exp (z • a)) a 0

Tactic:
simpa using hasDerivAt_exp_smul_const a (0 : ℂ)

Premises used: hasDerivAt_exp_smul_const, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
key : ∀ (z : ℂ), x * NormedSpace.exp (z • star a) = NormedSpace.exp (z • star b) * x
⊢ ∀ (a : A), HasDerivAt (fun (z : ℂ) ↦ NormedSpace.exp (z • a)) a 0

Tactic:
have (a : A) : HasDerivAt (fun z : ℂ ↦ exp (z • a)) a 0 := by
      simpa using hasDerivAt_exp_smul_const a (0 : ℂ)
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
key : ∀ (z : ℂ), x * NormedSpace.exp (z • star a) = NormedSpace.exp (z • star b) * x
this : ∀ (a : A), HasDerivAt (fun (z : ℂ) ↦ NormedSpace.exp (z • a)) a 0
apply : HasDerivAt (fun (y : ℂ) ↦ x * NormedSpace.exp (y • star a)) (star b * x) 0
⊢ SemiconjBy x (star a) (star b)

Tactic:
apply (this (star a)).const_mul x |>.unique

Premises used: HasDerivAt.unique, HasDerivAt.const_mul, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
key : ∀ (z : ℂ), x * NormedSpace.exp (z • star a) = NormedSpace.exp (z • star b) * x
this : ∀ (a : A), HasDerivAt (fun (z : ℂ) ↦ NormedSpace.exp (z • a)) a 0
⊢ HasDerivAt (fun (y : ℂ) ↦ x * NormedSpace.exp (y • star a)) (star b * x) 0

Tactic:
simpa [key] using (this (star b)).mul_const x

Premises used: Star.star, HasDerivAt.mul_const
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
suffices : ∀ (z : ℂ), x * NormedSpace.exp (z • star a) = NormedSpace.exp (z • star b) * x
⊢ SemiconjBy x (star a) (star b)

Tactic:
suffices key : ∀ z : ℂ, x * exp (z • star a) = exp (z • star b) * x by
    have (a : A) : HasDerivAt (fun z : ℂ ↦ exp (z • a)) a 0 := by
      simpa using hasDerivAt_exp_smul_const a (0 : ℂ)
    apply (this (star a)).const_mul x |>.unique
    simpa [key] using (this (star b)).mul_const x
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_1
inst : CStarAlgebra A
a b x : A
inst_1 : IsStarNormal a
inst_2 : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x_1 : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
x_2 : Invertible (NormedSpace.exp (z • star a)) := invertibleExp (z • star a)
⊢ x * NormedSpace.exp (z • star a) = NormedSpace.exp (z • star b) * x

Tactic:
simpa [← mul_assoc, ← invOf_exp, expMulMulExp] using
    congr($(expMulMulExp_const h z) * exp (z • star a)).symm

Premises used: HMul.hMul, _private.0.expMulMulExp, congrArg, NormedSpace.exp, mul_assoc, id, _private.0.expMulMulExp_const, NormedSpace.invOf_exp, HSMul.hSMul, Eq.symm, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
a₁ : Eq (α := Unitization ℂ A) (↑(x * star a) : Unitization ℂ A) (↑(star b * x) : Unitization ℂ A)
⊢ SemiconjBy x (star a) (star b)

Tactic:
apply Unitization.inr_injective (R := ℂ)

Premises used: Unitization.inr_injective
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
a₁ :
  HMul.hMul (α := Unitization ℂ A) (↑x : Unitization ℂ A) (star (↑a : Unitization ℂ A)) =
    HMul.hMul (α := Unitization ℂ A) (star (↑b : Unitization ℂ A)) (↑x : Unitization ℂ A)
⊢ Eq (α := Unitization ℂ A) (↑(x * star a) : Unitization ℂ A) (↑(star b * x) : Unitization ℂ A)

Tactic:
simp only [Unitization.inr_mul, Unitization.inr_star]

Premises used: Unitization.inr_star, Unitization.inr_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
a₁ : SemiconjBy (M := Unitization ℂ A) (↑x : Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
⊢ HMul.hMul (α := Unitization ℂ A) (↑x : Unitization ℂ A) (star (↑a : Unitization ℂ A)) =
    HMul.hMul (α := Unitization ℂ A) (star (↑b : Unitization ℂ A)) (↑x : Unitization ℂ A)

Tactic:
apply SemiconjBy.star_right_of_unital

Premises used: _private.0.SemiconjBy.star_right_of_unital
-- Module: Mathlib.Analysis.CStarAlgebra.Fuglede
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
⊢ SemiconjBy (M := Unitization ℂ A) (↑x : Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)

Tactic:
simpa [SemiconjBy] using mod_cast h.eq

Premises used: SemiconjBy, SemiconjBy.eq