awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (hypothesis)
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
⊢ IsStarProjection e
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)
⊢ IsStarProjection e
have refine_2 : ‖e * e‖ ≤ 1
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⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ IsStarProjection e
have refine_2₁ : ‖HSMul.hSMul (α := ℝ) 2 e - e * e‖ ≤ 1
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⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)
⊢ ‖e * e‖ ≤ 1
have refine_2 : ‖e‖ * ‖e‖ ≤ 1
Tactic: grw [norm_mul_le, h2, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ ‖e * e‖ ≤ 1
have refine_2₁ : HMul.hMul (α := ℝ) 1 1 ≤ 1
Tactic: grw [norm_mul_le, h2, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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
⊢ ‖e * e‖ ≤ 1
have refine_2₂ : LE.le (α := ℝ) 1 1
Tactic: grw [norm_mul_le, h2, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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)
⊢ ‖HSMul.hSMul (α := ℝ) 2 e - e * e‖ ≤ 1
have refine_2 : 0 ≤ HSub.hSub (α := Unitization ℂ A) 1 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
Tactic: rw [← norm_inr (𝕜 := ℂ), norm_le_one_iff_of_nonneg _ this, ← sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Extreme (goal)
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 ≤ HSub.hSub (α := Unitization ℂ A) 1 (↑(HSMul.hSMul (α := ℝ) 2 e - e * e) : Unitization ℂ A)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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
⊢ 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)
have 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)
Tactic: nth_rw 1 [expMulMulExp, ← (h.smul_right (star z)).exp_neg_mul_mul_exp_eq_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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 (-(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)
have 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)
Tactic: simp_rw [← mul_assoc, mul_assoc (_ * _ * x)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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 (-(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)
have 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)
Tactic: congr!
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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)
⊢ 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)
have 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)
Tactic: congr!
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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 (-(star z • b)) =
    (↑(expUnitary
          (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
            (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
      A)
have 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)
Tactic: simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_smul I I, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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 (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)
have 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))
Tactic: simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_smul I I, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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)
have unfold : Differentiable.{0, 0, u_1} ℂ (F := A) fun (z : ℂ) ↦ NormedSpace.exp (z • star b) * x * NormedSpace.exp (z • star (-a))
Tactic: unfold expMulMulExp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (hypothesis)
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 : ℂ
⊢ expMulMulExp a b x z = x
have hf : Differentiable ℂ (expMulMulExp a b x)
Tactic: have hf : Differentiable ℂ (expMulMulExp a b x : ℂ → A) := by unfold expMulMulExp; fun_prop
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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))
have apply : Set.range (expMulMulExp a b x) ⊆ Metric.sphere 0 ‖x‖
Tactic: apply Metric.isBounded_sphere (x := (0 : A)) (r := ‖x‖) |>.subset
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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 : ℂ
⊢ Membership.mem (γ := Set A) (Metric.sphere 0 ‖x‖) (expMulMulExp a b x z)
have rw : ‖expMulMulExp a b x z - 0‖ = ‖x‖
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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‖
⊢ Membership.mem (γ := Set A) (Metric.sphere 0 ‖x‖) (expMulMulExp a b x z)
have rw₁ : ‖expMulMulExp a b x z‖ = ‖x‖
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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‖
⊢ Membership.mem (γ := Set A) (Metric.sphere 0 ‖x‖) (expMulMulExp a b x z)
have 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‖
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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‖
⊢ Membership.mem (γ := Set A) (Metric.sphere 0 ‖x‖) (expMulMulExp a b x z)
have rw₃ : ‖(↑(expUnitary
            (HSMul.hSMul (α := ℝ) (β := ↥(selfAdjoint A)) 2
              (((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) (z • star b) : ↥(selfAdjoint A)))) :
        A) *
      x‖ =
  ‖x‖
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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‖
⊢ Membership.mem (γ := Set A) (Metric.sphere 0 ‖x‖) (expMulMulExp a b x z)
have rw₄ : ‖x‖ = ‖x‖
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (hypothesis)
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)
⊢ expMulMulExp a b x z = x
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (hypothesis)
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
⊢ SemiconjBy x (star a) (star b)
have this : ∀ (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 : ℂ)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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
⊢ SemiconjBy x (star a) (star b)
have apply : HasDerivAt (fun (y : ℂ) ↦ x * NormedSpace.exp (y • star a)) (star b * x) 0
Tactic: apply (this (star a)).const_mul x |>.unique
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
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
⊢ SemiconjBy x (star a) (star b)
have suffices : ∀ (z : ℂ), x * NormedSpace.exp (z • star a) = NormedSpace.exp (z • star b) * x
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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
⊢ SemiconjBy x (star a) (star b)
have a₁ : Eq (α := Unitization ℂ A) (↑(x * star a) : Unitization ℂ A) (↑(star b * x) : Unitization ℂ A)
Tactic: apply Unitization.inr_injective (R := ℂ)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
⊢ Eq (α := Unitization ℂ A) (↑(x * star a) : Unitization ℂ A) (↑(star b * x) : Unitization ℂ A)
have a₁ : HMul.hMul (α := Unitization ℂ A) (↑x : Unitization ℂ A) (star (↑a : Unitization ℂ A)) =
  HMul.hMul (α := Unitization ℂ A) (star (↑b : Unitization ℂ A)) (↑x : Unitization ℂ A)
Tactic: simp only [Unitization.inr_mul, Unitization.inr_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
⊢ HMul.hMul (α := Unitization ℂ A) (↑x : Unitization ℂ A) (star (↑a : Unitization ℂ A)) =
    HMul.hMul (α := Unitization ℂ A) (star (↑b : Unitization ℂ A)) (↑x : Unitization ℂ A)
have a₁ : SemiconjBy (M := Unitization ℂ A) (↑x : Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
Tactic: apply SemiconjBy.star_right_of_unital
-- 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
⊢ IsStarNormal a ↔
    ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
have this : IsAddTorsionFree A
Tactic: have : IsAddTorsionFree A := IsAddTorsionFree.of_module_rat A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
⊢ IsStarNormal a ↔
    ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
have refine_1 : ∀ (ha : 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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Fuglede (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
x : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
refine_1 :
  ∀ (ha : IsStarNormal a) (x : ℝ),
    Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
⊢ IsStarNormal a ↔
    ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))
have refine_2 : ∀
  (ha :
    ∀ (x : ℝ), Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a))),
  IsStarNormal a
Tactic: refine ⟨fun ha x ↦ ?_, fun ha ↦ ?_⟩