awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ‖cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (y : ℝ≥0) ↦ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y) m‖₊ ≤
    HPow.hPow (β := ℕ) ε 2
have refine : ∀ (y : ℝ≥0) (hy : y ∈ σ ℝ≥0 m), y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y ≤ HPow.hPow (β := ℕ) ε 2
Tactic: refine nnnorm_cfc_nnreal_le fun y hy ↦ ?_
-- 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
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y)) ≤ HPow.hPow (β := ℕ) ε 2 * 1
have h₁ : y * HPow.hPow (β := ℕ) ε 2 ≤ HPow.hPow (β := ℕ) ε 2
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
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
⊢ y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y)) ≤ HPow.hPow (β := ℕ) ε 2 * 1
have h₂ : y / (HPow.hPow (β := ℕ) ε 2 + y) ≤ 1
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
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 ≤ HPow.hPow (β := ℕ) ε 2
have h₁ : y ≤ 1
Tactic: apply mul_le_of_le_one_left'
-- 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
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
have hm' : ‖m‖ ≤ 1
Tactic: have hm' := hm₂.le
-- 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
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
⊢ y ≤ 1
have hm'₁ : ∀ 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'
Cleared hypotheses: hm'
-- 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
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y ≤ HPow.hPow (β := ℕ) ε 2
have y₁ : y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y = y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y))
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 _
-- 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
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
y₁ : y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y = y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y))
⊢ y * (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹ * y ≤ HPow.hPow (β := ℕ) ε 2
have y₂ : y * HPow.hPow (β := ℕ) ε 2 * (y / (HPow.hPow (β := ℕ) ε 2 + y)) ≤ HPow.hPow (β := ℕ) ε 2 * 1
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 _
-- 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
⊢ ‖star m * (1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) g (HPow.hPow (β := ℕ) ε⁻¹ 2 • m)) * m‖₊ ≤
    HPow.hPow (β := ℕ) ε 2
have 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
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 _
-- 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
⊢ 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
have 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
Tactic: rw [cfc_mul _ _ m (continuousOn_id' _ |>.fun_mul hg') (continuousOn_id' _),
    cfc_mul _ _ m (continuousOn_id' _) hg', cfc_id' .., hm₁.star_eq]
-- 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 * (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
have 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
Tactic: congr
-- 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
⊢ 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
have 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
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)]
-- 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
⊢ 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
have e_a : ∀ y ∈ σ ℝ≥0 m, 1 y - g (HPow.hPow (β := ℕ) ε⁻¹ 2 • y) = (1 + HPow.hPow (β := ℕ) ε⁻¹ 2 • y)⁻¹
Tactic: refine cfc_congr (fun y _ ↦ ?_)
-- 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) ↦ m * x) (approximateUnit A) (𝓝 m)
have rw : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)
Tactic: rw [tendsto_mul_left_iff_tendsto_mul_right]
-- 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
rw : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) (approximateUnit A) (𝓝 m)
⊢ ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) (approximateUnit A) (𝓝 m)
have rw₁ : ∀ᶠ (x : A) in approximateUnit A, IsSelfAdjoint x
Tactic: rw [tendsto_mul_left_iff_tendsto_mul_right]
-- 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 : A) in approximateUnit A, IsSelfAdjoint x
have rw : ∃ (i : A),
  (0 ≤ i ∧ ‖i‖ < 1) ∧ ∀ ⦃x : A⦄, Membership.mem (γ := Set A) ({x : A | i ≤ x} ∩ closedBall 0 1) x → IsSelfAdjoint x
Tactic: rw [(hasBasis_approximateUnit A).eventually_iff]
-- 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
⊢ ∃ (i : A),
    (0 ≤ i ∧ ‖i‖ < 1) ∧ ∀ ⦃x : A⦄, Membership.mem (γ := Set A) ({x : A | i ≤ x} ∩ closedBall 0 1) x → IsSelfAdjoint x
have 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
Tactic: peel (hasBasis_approximateUnit A).ex_mem with x hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
⊢ ‖x⋆‖ ≤ ‖x‖
have inl : ∀ (hx : x⋆ = 0), ‖x⋆‖ ≤ ‖x‖
Tactic: obtain (hx | hx) := eq_zero_or_norm_pos x⋆
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
inl : ∀ (hx : x⋆ = 0), ‖x⋆‖ ≤ ‖x‖
⊢ ‖x⋆‖ ≤ ‖x‖
have inr : ∀ (hx : 0 < ‖x⋆‖), ‖x⋆‖ ≤ ‖x‖
Tactic: obtain (hx | hx) := eq_zero_or_norm_pos x⋆
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖
have inr : ‖x⋆‖ * ‖x⋆‖ ≤ ‖x‖ * ‖x⋆‖
Tactic: refine le_of_mul_le_mul_right ?_ hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x⋆‖ ≤ ‖x‖
have inl : ∀ (hx : x⋆ = 0), ‖x⋆‖ ≤ ‖x‖
Tactic: obtain (hx | hx) := eq_zero_or_norm_pos x⋆
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
inl : ∀ (hx : x⋆ = 0), ‖x⋆‖ ≤ ‖x‖
⊢ ‖x⋆‖ ≤ ‖x‖
have inr : ∀ (hx : 0 < ‖x⋆‖), ‖x⋆‖ ≤ ‖x‖
Tactic: obtain (hx | hx) := eq_zero_or_norm_pos x⋆
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖
have inr : ‖x⋆‖ * ‖x⋆‖ ≤ ‖x‖ * ‖x⋆‖
Tactic: refine le_of_mul_le_mul_right ?_ hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x⋆‖ * ‖x‖ ≤ ‖x‖ * ‖x‖
have rw : ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖
Tactic: rw [norm_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x * x⋆‖ = ‖x‖ * ‖x‖
have nth_rw : ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖
Tactic: nth_rw 1 [← star_star x]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖
have rw : ‖x‖ * ‖x‖ = ‖x⋆‖ * ‖x‖
Tactic: rw [norm_star_mul_self, norm_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
rw : ‖x‖ * ‖x‖ = ‖x⋆‖ * ‖x‖
⊢ ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖
have rw₁ : ‖x‖ * ‖x‖ = ‖x‖ * ‖x‖
Tactic: rw [norm_star_mul_self, norm_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
⊢ x⋆ * x = 0 ↔ x = 0
have rw : ‖x‖ * ‖x‖ = 0 ↔ x = 0
Tactic: rw [← norm_eq_zero, norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
⊢ max ‖x.1‖ ‖x.2‖ * max ‖x.1‖ ‖x.2‖ ≤ max ‖(x⋆ * x).1‖ ‖(x⋆ * x).2‖
have simp : HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ max (HPow.hPow (β := ℕ) ‖x.1‖ 2) (HPow.hPow (β := ℕ) ‖x.2‖ 2)
Tactic: simp only [Prod.fst_mul, Prod.fst_star, Prod.snd_mul, Prod.snd_star, norm_star_mul_self, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
⊢ HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ max (HPow.hPow (β := ℕ) ‖x.1‖ 2) (HPow.hPow (β := ℕ) ‖x.2‖ 2)
have rw : HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
  HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
Tactic: rw [le_sup_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
⊢ HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
have inl : ∀ (h : ‖x.1‖ ≤ ‖x.2‖),
  HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
Tactic: rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h)