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_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
h₁ : y * HPow.hPow (β := ℕ) ε 2 ≤ HPow.hPow (β := ℕ) ε 2
h₂ : y / (HPow.hPow (β := ℕ) ε 2 + y) ≤ 1
⊢ y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y)) ≤ HPow.hPow (β := ℕ) ε 2 * 1

Tactic:
gcongr
-- 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
h₁ : y ≤ 1
⊢ y * HPow.hPow (β := ℕ) ε 2 ≤ HPow.hPow (β := ℕ) ε 2

Tactic:
apply mul_le_of_le_one_left'

Premises used: mul_le_of_le_one_left'
-- 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
⊢ ‖m‖ ≤ 1

Tactic:
have hm' := hm₂.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
hm' : ‖m‖ ≤ 1
⊢ ∀ x ∈ σ ℝ≥0 m, x ≤ 1 x

Tactic:
rw [norm_le_one_iff_of_nonneg m hm₁, ← cfc_id' ℝ≥0 m, ← cfc_one (R := ℝ≥0) m,
            cfc_nnreal_le_iff _ _ _ (QuasispectrumRestricts.nnreal_of_nonneg hm₁)] at hm'

Premises used: cfc_id', NNReal, cfc_nnreal_le_iff, cfc_one, QuasispectrumRestricts.nnreal_of_nonneg, CStarAlgebra.norm_le_one_iff_of_nonneg
-- 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
hm' : ∀ x ∈ σ ℝ≥0 m, x ≤ 1 x
⊢ y ≤ 1

Tactic:
hm' y hy
-- 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
hm' : ∀ x ∈ σ ℝ≥0 m, x ≤ 1 x
⊢ y ≤ 1

Tactic:
exact hm' y hy
-- 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
⊢ 0 < HPow.hPow (β := ℕ) ε 2 + y

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
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 / (HPow.hPow (β := ℕ) ε 2 + y) ≤ 1

Tactic:
exact div_le_one (by positivity) |>.mpr le_add_self

Premises used: Iff.mpr, div_le_one, le_add_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_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
⊢ HPow.hPow (β := ℕ) ε 2 * 1 = HPow.hPow (β := ℕ) ε 2

Tactic:
mul_one _

Premises used: mul_one
-- 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₁ : y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y = y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y))
y₂ : y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y)) ≤ HPow.hPow (β := ℕ) ε 2 * 1
⊢ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y ≤ HPow.hPow (β := ℕ) ε 2

Tactic:
calc
      y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y = y * ε ^ 2 * (y / (ε ^ 2 + y)) := by simp [field]
      _ ≤ ε ^ 2 * 1 := by
        gcongr
        · apply mul_le_of_le_one_left'
          have hm' := hm₂.le
          rw [norm_le_one_iff_of_nonneg m hm₁, ← cfc_id' ℝ≥0 m, ← cfc_one (R := ℝ≥0) m,
            cfc_nnreal_le_iff _ _ _ (QuasispectrumRestricts.nnreal_of_nonneg hm₁)] at hm'
          exact hm' y hy
        · exact div_le_one (by positivity) |>.mpr le_add_self
      _ = ε ^ 2 := mul_one _

Premises used: HDiv.hDiv, Inv.inv, HPow.hPow, HAdd.hAdd, HSMul.hSMul, mul_one, 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
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
suffices :
  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

Tactic:
suffices star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m =
      cfc (fun y : ℝ≥0 ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m by
    rw [this]
    refine nnnorm_cfc_nnreal_le fun y hy ↦ ?_
    calc
      y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y = y * ε ^ 2 * (y / (ε ^ 2 + y)) := by simp [field]
      _ ≤ ε ^ 2 * 1 := by
        gcongr
        · apply mul_le_of_le_one_left'
          have hm' := hm₂.le
          rw [norm_le_one_iff_of_nonneg m hm₁, ← cfc_id' ℝ≥0 m, ← cfc_one (R := ℝ≥0) m,
            cfc_nnreal_le_iff _ _ _ (QuasispectrumRestricts.nnreal_of_nonneg hm₁)] at hm'
          exact hm' y hy
        · exact div_le_one (by positivity) |>.mpr le_add_self
      _ = ε ^ 2 := mul_one _
-- 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
rw :
  m * (1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) * m =
    m * cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) m * m
⊢ 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

Tactic:
rw [cfc_mul _ _ m (continuousOn_id' _ |>.fun_mul hg') (continuousOn_id' _),
    cfc_mul _ _ m (continuousOn_id' _) hg', cfc_id' .., hm₁.star_eq]

Premises used: ContinuousOn.fun_mul, LE.le.star_eq, cfc_id', cfc_mul, continuousOn_id'
-- 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
e_a :
  1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) =
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) m
⊢ m * (1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) * m =
    m * cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) m * m

Tactic:
congr
-- 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
⊢ ∀ x ∈ σ ℝ≥0 m, g (HPow.hPow (β := ℕ) ε⁻¹ 2 • x) ≤ 1 x

Tactic:
simp [g]
-- 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
⊢ ContinuousOn (Y := ℝ≥0) 1 (σ ℝ≥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
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
⊢ Continuous (Y := ℝ≥0) fun (x : ℝ≥0) ↦ g (HPow.hPow (β := ℕ) ε⁻¹ 2 • x)

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
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
e_a :
  cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 x - g (HPow.hPow (β := ℕ) ε⁻¹ 2 • x)) m =
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) m
⊢ 1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m) =
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) m

Tactic:
rw [← cfc_one (R := ℝ≥0) m, ← cfc_comp_smul _ _ _ hg.continuousOn hm₁,
    ← cfc_tsub _ _ m (by simp [g]) hm₁ (by fun_prop) (Continuous.continuousOn <| by fun_prop)]

Premises used: Continuous.continuousOn, cfc_comp_smul, NNReal, cfc_one, cfc_tsub
-- 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
⊢ cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 x - g (HPow.hPow (β := ℕ) ε⁻¹ 2 • x)) m =
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) m

Tactic:
cfc_congr (fun y _ ↦ ?_)

Premises used: cfc_congr
-- 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
e_a : ∀ y ∈ σ ℝ≥0 m, 1 y - g (HPow.hPow (β := ℕ) ε⁻¹ 2 • y) = (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹
⊢ cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 x - g (HPow.hPow (β := ℕ) ε⁻¹ 2 • x)) m =
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹) m

Tactic:
refine cfc_congr (fun y _ ↦ ?_)

Premises used: cfc_congr
-- 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
y : ℝ≥0
h : y ∈ σ ℝ≥0 m
⊢ 1 y - g (HPow.hPow (β := ℕ) ε⁻¹ 2 • y) = (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹

Tactic:
simp [g, tsub_tsub_cancel_of_le]

Premises used: tsub_tsub_cancel_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
rw : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)
rw₁ : ∀ᶠ (x : A) in approximateUnit A, IsSelfAdjoint x
⊢ ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) (approximateUnit A) (𝓝 m)

Tactic:
rw [tendsto_mul_left_iff_tendsto_mul_right]

Premises used: CStarAlgebra.tendsto_mul_left_iff_tendsto_mul_right
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)

Tactic:
tendsto_mul_right_approximateUnit

Premises used: _private.0.CStarAlgebra.tendsto_mul_right_approximateUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)

Tactic:
exact tendsto_mul_right_approximateUnit

Premises used: _private.0.CStarAlgebra.tendsto_mul_right_approximateUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
rw :
  ∃ (i : A),
    (0 ≤ i ∧ ‖i‖ < 1) ∧ ∀ ⦃x : A⦄, Membership.mem (γ := Set A) ({x : A | i ≤ x} ∩ closedBall 0 1) x → IsSelfAdjoint x
⊢ ∀ᶠ (x : A) in approximateUnit A, IsSelfAdjoint x

Tactic:
rw [(hasBasis_approximateUnit A).eventually_iff]

Premises used: Filter.HasBasis.eventually_iff, CStarAlgebra.hasBasis_approximateUnit
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
h :
  ∀ (x : A) (hx : 0 ≤ x ∧ ‖x‖ < 1),
    (0 ≤ x ∧ ‖x‖ < 1) ∧
      ∀ ⦃x_1 : A⦄, Membership.mem (γ := Set A) ({x_2 : A | x ≤ x_2} ∩ closedBall 0 1) x_1 → IsSelfAdjoint x_1
⊢ ∃ (i : A),
    (0 ≤ i ∧ ‖i‖ < 1) ∧ ∀ ⦃x : A⦄, Membership.mem (γ := Set A) ({x : A | i ≤ x} ∩ closedBall 0 1) x → IsSelfAdjoint x

Tactic:
peel (hasBasis_approximateUnit A).ex_mem with x hx

Premises used: Filter.HasBasis.ex_mem, CStarAlgebra.hasBasis_approximateUnit