awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
⊢ ‖star z * (1 - star y) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2
have hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
Tactic: have hy' : 1 - y ∈ Set.Icc 0 1 := Set.sub_mem_Icc_zero_iff_right.mpr hy₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ ‖star z * (1 - star y) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2
have rw : ‖star z * HPow.hPow (β := ℕ) (1 - y) 2 * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
Tactic: rw [hy₀.1.star_eq, ← mul_assoc, mul_assoc (star _), ← sq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ ‖star z * HPow.hPow (β := ℕ) (1 - y) 2 * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
have refine : star z * HPow.hPow (β := ℕ) (1 - y) 2 * z ≤ star z * (1 - x) * z
Tactic: refine nnnorm_le_nnnorm_of_nonneg_of_le (star_left_conjugate_nonneg (pow_nonneg hy'.1 2) _) ?_
    |>.trans h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ star z * HPow.hPow (β := ℕ) (1 - y) 2 * z ≤ star z * (1 - x) * z
have refine : HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - x
Tactic: refine star_left_conjugate_le_conjugate ?_ _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - x
have trans : HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - y
Tactic: trans (1 - y)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
trans : HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - y
⊢ HPow.hPow (β := ℕ) (1 - y) 2 ≤ 1 - x
have trans₁ : 1 - y ≤ 1 - x
Tactic: trans (1 - y)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ HPow.hPow (β := ℕ) c 2
hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set A) (Set.Icc 0 1) (1 - y)
⊢ 1 - y ≤ 1 - x
have h₁ : x ≤ y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
⊢ ‖z - y * z‖ ≤ c
have rw : ‖(↑z : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑z : Unitization ℂ A)‖ ≤ c
Tactic: rw [← norm_inr (𝕜 := ℂ), inr_sub, inr_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
⊢ ‖(↑z : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑z : Unitization ℂ A)‖ ≤ c
have refine_1 : LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A)
Tactic: refine norm_sub_mul_self_le _ ?_ ?_ hc h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
refine_1 : LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A)
⊢ ‖(↑z : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑z : Unitization ℂ A)‖ ≤ c
have refine_2 : Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc (↑x : Unitization ℂ A) 1) (↑y : Unitization ℂ A)
Tactic: refine norm_sub_mul_self_le _ ?_ ?_ hc h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc (↑x : Unitization ℂ A) 1) (↑y : Unitization ℂ A)
have hy : 0 ≤ y
Tactic: have hy := hx₀.trans hxy
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h :
  ‖star (↑z : Unitization ℂ A) * HSub.hSub (α := Unitization ℂ A) 1 (↑x : Unitization ℂ A) * (↑z : Unitization ℂ A)‖ ≤
    HPow.hPow (β := ℕ) c 2
hy : 0 ≤ y
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc (↑x : Unitization ℂ A) 1) (↑y : Unitization ℂ A)
have refine_2 : x ≤ y ∧ ‖y‖ ≤ 1
Tactic: rw [Set.mem_Icc, inr_le_iff _ _ hx₀.isSelfAdjoint hy.isSelfAdjoint,
      ← norm_le_one_iff_of_nonneg _, norm_inr]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : A
⊢ Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)
have refine : ∀ (m : A) (hm₁ : 0 ≤ m) (hm₂ : ‖m‖ < 1), Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)
Tactic: refine tendsto_mul_right_of_forall_nonneg_tendsto (fun m hm₁ hm₂ ↦ ?_) m
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
⊢ Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)
have rw : ∀ (ib : ℝ),
  0 < ib →
    ∃ (ia : A),
      (0 ≤ ia ∧ ‖ia‖ < 1) ∧
        ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m ib
Tactic: rw [(hasBasis_approximateUnit A).tendsto_iff nhds_basis_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ
hε : 0 < ε
⊢ ∃ (ia : A),
    (0 ≤ ia ∧ ‖ia‖ < 1) ∧
      ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m ε
have lift : ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ)),
  ∃ (ia : A),
    (0 ≤ ia ∧ ‖ia‖ < 1) ∧
      ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m (↑ε : ℝ)
Tactic: lift ε to ℝ≥0 using hε.le
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
⊢ ∃ (ia : A),
    (0 ≤ ia ∧ ‖ia‖ < 1) ∧
      ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m (↑ε : ℝ)
have hε₁ : 0 < ε
Tactic: rw [coe_pos] at hε
Cleared hypotheses: hε
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ (ia : A),
    (0 ≤ ia ∧ ‖ia‖ < 1) ∧
      ∀ (x : A), Membership.mem (γ := Set A) ({x : A | ia ≤ x} ∩ closedBall 0 1) x → x * m ∈ closedBall m (↑ε : ℝ)
have refine : ∀ (x : A),
  Membership.mem (γ := Set A)
      ({x : A | cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹) (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x} ∩
        closedBall 0 1)
      x →
    x * m ∈ closedBall m (↑ε : ℝ)
Tactic: refine ⟨cfcₙ (fun y : ℝ≥0 ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • m),
    ⟨cfcₙ_nonneg_of_predicate, norm_cfcₙ_one_sub_one_add_inv_lt_one (ε⁻¹ ^ 2 • m)⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹) (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hx₂ : Membership.mem (γ := Set A) (closedBall 0 1) x
⊢ x * m ∈ closedBall m (↑ε : ℝ)
have simp : ∀ (hx₂ : ‖x‖ ≤ 1), ‖m - x * m‖ ≤ (↑ε : ℝ)
Tactic: simp only [mem_closedBall, dist_eq_norm', zero_sub, norm_neg] at hx₂ ⊢
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹) (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hx₂ : ‖x‖ ≤ 1
⊢ ‖m - x * m‖ ≤ (↑ε : ℝ)
have rw : ‖m - x * m‖₊ ≤ ε
Tactic: rw [← coe_nnnorm, coe_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹) (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hx₂ : ‖x‖ ≤ 1
⊢ ‖m - x * m‖₊ ≤ ε
have hx₀ : 0 ≤ x
Tactic: have hx₀ : 0 ≤ x := cfcₙ_nonneg_of_predicate.trans hx₁
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹) (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
⊢ ‖m - x * m‖₊ ≤ ε
have hx₃ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹)
    (HSMul.hSMul (β := Unitization ℂ A) (HPow.hPow (β := ℕ) ε⁻¹ 2) (↑m : Unitization ℂ A)) ≤
  (↑x : Unitization ℂ A)
Tactic: rw [← inr_le_iff _ _ (.of_nonneg cfcₙ_nonneg_of_predicate) (.of_nonneg hx₀),
    nnreal_cfcₙ_eq_cfc_inr _ _ (by simp [tsub_self]), inr_smul] at hx₁
Cleared hypotheses: hx₁, hx₂, hx₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ :
  cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹)
      (HSMul.hSMul (β := Unitization ℂ A) (HPow.hPow (β := ℕ) ε⁻¹ 2) (↑m : Unitization ℂ A)) ≤
    (↑x : Unitization ℂ A)
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
⊢ ‖m - x * m‖₊ ≤ ε
have rw : ∀ (hm₂ : norm (E := Unitization ℂ A) (↑m : Unitization ℂ A) < 1) (ε : ℝ≥0) (hε : 0 < ε) (x : A)
  (hx₁ :
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹)
        (HSMul.hSMul (β := Unitization ℂ A) (HPow.hPow (β := ℕ) ε⁻¹ 2) (↑m : Unitization ℂ A)) ≤
      (↑x : Unitization ℂ A))
  (hx₂ : norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1) (hx₀ : 0 ≤ x), ‖m - x * m‖₊ ≤ ε
Tactic: rw [← norm_inr (𝕜 := ℂ)] at hm₂ hx₂
Cleared hypotheses: hm₂, ε, hε, x, hx₁, hx₂, hx₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : 0 ≤ m
hm₂ : norm (E := Unitization ℂ A) (↑m : Unitization ℂ A) < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ :
  cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹)
      (HSMul.hSMul (β := Unitization ℂ A) (HPow.hPow (β := ℕ) ε⁻¹ 2) (↑m : Unitization ℂ A)) ≤
    (↑x : Unitization ℂ A)
hx₂ : norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1
hx₀ : 0 ≤ x
⊢ ‖m - x * m‖₊ ≤ ε
have rw : ∀ (hm₁ : LE.le (α := Unitization ℂ A) 0 (↑m : Unitization ℂ A))
  (hm₂ : norm (E := Unitization ℂ A) (↑m : Unitization ℂ A) < 1) (ε : ℝ≥0) (hε : 0 < ε) (x : A)
  (hx₁ :
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹)
        (HSMul.hSMul (β := Unitization ℂ A) (HPow.hPow (β := ℕ) ε⁻¹ 2) (↑m : Unitization ℂ A)) ≤
      (↑x : Unitization ℂ A))
  (hx₂ : norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1)
  (hx₀ : LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A)), ‖m - x * m‖₊ ≤ ε
Tactic: rw [← inr_nonneg_iff] at hx₀ hm₁
Cleared hypotheses: hm₁, hm₂, ε, hε, x, hx₁, hx₂, hx₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : LE.le (α := Unitization ℂ A) 0 (↑m : Unitization ℂ A)
hm₂ : norm (E := Unitization ℂ A) (↑m : Unitization ℂ A) < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ :
  cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹)
      (HSMul.hSMul (β := Unitization ℂ A) (HPow.hPow (β := ℕ) ε⁻¹ 2) (↑m : Unitization ℂ A)) ≤
    (↑x : Unitization ℂ A)
hx₂ : norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1
hx₀ : LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A)
⊢ ‖m - x * m‖₊ ≤ ε
have rw : ‖(↑m : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑m : Unitization ℂ A)‖₊ ≤ ε
Tactic: rw [← nnnorm_inr (𝕜 := ℂ), inr_sub, inr_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m : A
hm₁ : LE.le (α := Unitization ℂ A) 0 (↑m : Unitization ℂ A)
hm₂ : norm (E := Unitization ℂ A) (↑m : Unitization ℂ A) < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ :
  cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹)
      (HSMul.hSMul (β := Unitization ℂ A) (HPow.hPow (β := ℕ) ε⁻¹ 2) (↑m : Unitization ℂ A)) ≤
    (↑x : Unitization ℂ A)
hx₂ : norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1
hx₀ : LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A)
⊢ ‖(↑m : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑m : Unitization ℂ A)‖₊ ≤ ε
have generalize : ∀ (x m : Unitization ℂ A) (hm₁ : 0 ≤ m) (hm₂ : ‖m‖ < 1)
  (hx₁ :
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹) (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x)
  (hx₂ : ‖x‖ ≤ 1) (hx₀ : 0 ≤ x), ‖m - x * m‖₊ ≤ ε
Tactic: generalize (x : A⁺¹) = x, (m : A⁺¹) = m at *
Cleared hypotheses: hm₁, hm₂, hx₁, hx₂, hx₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
⊢ Continuous g
have rw : ContinuousOn g Set.univ
Tactic: rw [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
⊢ ContinuousOn g Set.univ
have funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
Tactic: fun_prop (disch := intro _ _; positivity)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
⊢ ContinuousOn g Set.univ
have funProp₁ : ∀ (x : ℝ≥0), x ≠ 0
Tactic: fun_prop (disch := intro _ _; positivity)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
funProp₁ : ∀ (x : ℝ≥0), x ≠ 0
⊢ ContinuousOn g Set.univ
have funProp₂ : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) Set.univ x → 1 + x ≠ 0
Tactic: fun_prop (disch := intro _ _; positivity)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
⊢ ‖m - x * m‖₊ ≤ ε
have hg : Continuous g
Tactic: have hg : Continuous g := by
    rw [← continuousOn_univ]
    fun_prop (disch := intro _ _; positivity)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hg : Continuous g
⊢ ‖m - x * m‖₊ ≤ ε
have hg' : ContinuousOn (Y := ℝ≥0) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) (σ ℝ≥0 m)
Tactic: have hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (spectrum ℝ≥0 m) :=
    ContinuousOn.inv₀ (by fun_prop) fun _ _ ↦ by positivity
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (Y := ℝ≥0) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) (σ ℝ≥0 m)
⊢ ‖m - x * m‖₊ ≤ ε
have hx : Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc 0 1) x
Tactic: have hx : x ∈ Set.Icc 0 1 := mem_Icc_iff_norm_le_one.mpr ⟨hx₀, hx₂⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (Y := ℝ≥0) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc 0 1) x
⊢ ‖m - x * m‖₊ ≤ ε
have hx' : x ∈ Set.Icc (cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) 1
Tactic: have hx' : x ∈ Set.Icc _ 1 := ⟨hx₁, hx.2⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (Y := ℝ≥0) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc 0 1) x
hx' : x ∈ Set.Icc (cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) 1
⊢ ‖m - x * m‖₊ ≤ ε
have refine : ‖star m * (1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) * m‖₊ ≤
  HPow.hPow (β := ℕ) ε 2
Tactic: refine nnnorm_sub_mul_self_le m cfc_nonneg_of_predicate hx' ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m_1 m_2 : A
ε : ℝ≥0
hε : 0 < ε
x_1 : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹
hx₁ : cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (Y := ℝ≥0) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : Membership.mem (γ := Set (Unitization ℂ A)) (Set.Icc 0 1) x
hx' : x ∈ Set.Icc (cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) 1
this :
  star m * (1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) * m =
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y) m
⊢ ‖star m * (1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) * m‖₊ ≤
    HPow.hPow (β := ℕ) ε 2
have rw : ‖cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y) m‖₊ ≤
  HPow.hPow (β := ℕ) ε 2
Tactic: rw [this]