awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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 < ε
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 (↑ε : ℝ)
⊢ ∃ (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:
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)⟩, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
simp : ∀ (hx₂ : ‖x‖ ≤ 1), ‖m - x * m‖ ≤ (↑ε : ℝ)
⊢ x * m ∈ closedBall m (↑ε : ℝ)

Tactic:
simp only [mem_closedBall, dist_eq_norm', zero_sub, norm_neg] at hx₂ ⊢

Premises used: dist_eq_norm', norm_neg, Metric.mem_closedBall, zero_sub
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
rw : ‖m - x * m‖₊ ≤ ε
⊢ ‖m - x * m‖ ≤ (↑ε : ℝ)

Tactic:
rw [← coe_nnnorm, coe_le_coe]

Premises used: coe_nnnorm, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ 0 ≤ x

Tactic:
have hx₀ : 0 ≤ x := cfcₙ_nonneg_of_predicate.trans hx₁
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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₁ :
  LE.le (α := Unitization ℂ A)
    (↑(cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹) (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) :
      Unitization ℂ A)
    (↑x : Unitization ℂ A)
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
⊢ 1 - (HAdd.hAdd (α := ℝ≥0) 1 0)⁻¹ = 0

Tactic:
simp [tsub_self]

Premises used: tsub_self
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ 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₁

Premises used: Unitization.inr_le_iff, Unitization.inr_smul, IsSelfAdjoint.of_nonneg, Unitization.nnreal_cfcₙ_eq_cfc_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
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)
⊢ ‖x‖ ≤ 1

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₁

Premises used: Unitization.inr_le_iff, Unitization.inr_smul, IsSelfAdjoint.of_nonneg, Unitization.nnreal_cfcₙ_eq_cfc_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
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
⊢ 0 ≤ x

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₁

Premises used: Unitization.inr_le_iff, Unitization.inr_smul, IsSelfAdjoint.of_nonneg, Unitization.nnreal_cfcₙ_eq_cfc_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
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‖₊ ≤ ε
⊢ ‖m - x * m‖₊ ≤ ε

Tactic:
rw [← norm_inr (𝕜 := ℂ)] at hm₂ hx₂

Premises used: Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
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‖₊ ≤ ε
⊢ ‖m - x * m‖₊ ≤ ε

Tactic:
rw [← inr_nonneg_iff] at hx₀ hm₁

Premises used: Unitization.inr_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)
rw : ‖(↑m : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑m : Unitization ℂ A)‖₊ ≤ ε
⊢ ‖m - x * m‖₊ ≤ ε

Tactic:
rw [← nnnorm_inr (𝕜 := ℂ), inr_sub, inr_mul]

Premises used: Unitization.inr_sub, Unitization.inr_mul, Unitization.nnnorm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)
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‖₊ ≤ ε
⊢ ‖(↑m : Unitization ℂ A) - HMul.hMul (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑m : Unitization ℂ A)‖₊ ≤ ε

Tactic:
generalize (x : A⁺¹) = x, (m : A⁺¹) = m at *

Premises used: Unitization.inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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₁ : 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
⊢ let g : ℝ≥0 → ℝ≥0 := fun (y : ℝ≥0) ↦ 1 - (1 + y)⁻¹;
  cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) ≤ x

Tactic:
set g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹

Premises used: HSub.hSub, Inv.inv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
rw : ContinuousOn g Set.univ
⊢ Continuous g

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
x_2 : ℝ≥0
funProp : x_2 ∈ σ ℝ≥0 (↑?a : ?A) → x_2 ≠ 0
⊢ x_2 ∈ σ ℝ≥0 (↑?a : ?A) → x_2 ≠ 0

Tactic:
_
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
x_2 : ℝ≥0
funProp : x_2 = 0 → False
⊢ x_2 ≠ 0

Tactic:
_
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
x_2 : ℝ≥0
funProp : Membership.mem (γ := Set ℝ≥0) Set.univ x_2 → 1 + x_2 ≠ 0
⊢ Membership.mem (γ := Set ℝ≥0) Set.univ x_2 → 1 + x_2 ≠ 0

Tactic:
_
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
x_2 : ℝ≥0
h : Membership.mem (γ := Set ℝ≥0) Set.univ x_2
⊢ 1 + x_2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
funProp₂ : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) Set.univ x → 1 + x ≠ 0
⊢ ContinuousOn g Set.univ

Tactic:
fun_prop (disch := intro _ _; positivity)
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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

Tactic:
have hg : Continuous g := by
    rw [← continuousOn_univ]
    fun_prop (disch := intro _ _; positivity)
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ ContinuousOn (Y := ℝ≥0) (fun (y : ℝ≥0) ↦ 1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y) (σ ℝ≥0 m)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
x_2 : ℝ≥0
h : x_2 ∈ σ ℝ≥0 m
⊢ 1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • x_2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)
⊢ 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₂⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ 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⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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‖₊ ≤ ε

Tactic:
nnnorm_sub_mul_self_le m cfc_nonneg_of_predicate hx' ?_

Premises used: CStarAlgebra.nnnorm_sub_mul_self_le, cfc_nonneg_of_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
refine :
  ‖star m * (1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) * m‖₊ ≤
    HPow.hPow (β := ℕ) ε 2
⊢ ‖m - x * m‖₊ ≤ ε

Tactic:
refine nnnorm_sub_mul_self_le m cfc_nonneg_of_predicate hx' ?_

Premises used: CStarAlgebra.nnnorm_sub_mul_self_le, cfc_nonneg_of_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
rw :
  ‖cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y) m‖₊ ≤
    HPow.hPow (β := ℕ) ε 2
⊢ ‖star m * (1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) * m‖₊ ≤
    HPow.hPow (β := ℕ) ε 2

Tactic:
rw [this]
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ ‖cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y) m‖₊ ≤
    HPow.hPow (β := ℕ) ε 2

Tactic:
nnnorm_cfc_nnreal_le fun y hy ↦ ?_

Premises used: Unitization.inl, nnnorm_cfc_nnreal_le, Unitization.inlRingHom
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
refine : ∀ (y : ℝ≥0) (hy : y ∈ σ ℝ≥0 m), y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y ≤ HPow.hPow (β := ℕ) ε 2
⊢ ‖cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y) m‖₊ ≤
    HPow.hPow (β := ℕ) ε 2

Tactic:
refine nnnorm_cfc_nnreal_le fun y hy ↦ ?_

Premises used: nnnorm_cfc_nnreal_le
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y = y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y))

Tactic:
simp [field]