awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
this :
  ∀ (a b : A),
    0 ≤ a →
      0 ≤ b →
        ‖a‖ < 1 →
          ‖b‖ < 1 →
            a ≤
              cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f
                (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
a : A
ha₁ : 0 ≤ a
ha₂ : Membership.mem (γ := Set A) (Metric.ball 0 1) a
b : A
hb₁ : 0 ≤ b
hb₂ : Membership.mem (γ := Set A) (Metric.ball 0 1) b
ha₃ : ‖a‖ < 1
⊢ ∃ (z : A),
    Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) z ∧
      (fun (x1 x2 : A) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : A) ↦ x1 ≤ x2) b z
have hb₃ : ‖b‖ < 1
Tactic: simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂
Cleared hypotheses: ha₂, hb₂
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
this :
  ∀ (a b : A),
    0 ≤ a →
      0 ≤ b →
        ‖a‖ < 1 →
          ‖b‖ < 1 →
            a ≤
              cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f
                (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ ∃ (z : A),
    Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) z ∧
      (fun (x1 x2 : A) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : A) ↦ x1 ≤ x2) b z
have refine_1 : Membership.mem (γ := Set A) (Metric.ball 0 1)
  (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b))
Tactic: refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
this :
  ∀ (a b : A),
    0 ≤ a →
      0 ≤ b →
        ‖a‖ < 1 →
          ‖b‖ < 1 →
            a ≤
              cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f
                (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
refine_1 :
  Membership.mem (γ := Set A) (Metric.ball 0 1)
    (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b))
⊢ ∃ (z : A),
    Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) z ∧
      (fun (x1 x2 : A) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : A) ↦ x1 ≤ x2) b z
have refine_2 : (fun (x1 x2 : A) ↦ x1 ≤ x2) a
  (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b))
Tactic: refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
this :
  ∀ (a b : A),
    0 ≤ a →
      0 ≤ b →
        ‖a‖ < 1 →
          ‖b‖ < 1 →
            a ≤
              cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f
                (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
refine_1 :
  Membership.mem (γ := Set A) (Metric.ball 0 1)
    (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b))
refine_2 :
  (fun (x1 x2 : A) ↦ x1 ≤ x2) a
    (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b))
⊢ ∃ (z : A),
    Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) z ∧
      (fun (x1 x2 : A) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : A) ↦ x1 ≤ x2) b z
have refine_3 : (fun (x1 x2 : A) ↦ x1 ≤ x2) b
  (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b))
Tactic: refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
⊢ DirectedOn (fun (x1 x2 : A) ↦ x1 ≤ x2) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1)
have suffices : ∀ (a b : A),
  0 ≤ a →
    0 ≤ b →
      ‖a‖ < 1 →
        ‖b‖ < 1 →
          a ≤
            cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f
              (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
Tactic: suffices ∀ a b : A, 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 →
      a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) by
    rintro a ⟨(ha₁ : 0 ≤ a), ha₂⟩ b ⟨(hb₁ : 0 ≤ b), hb₂⟩
    simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂
    refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
    · simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _
    · exact this a b ha₁ hb₁ ha₂ hb₂
    · exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
| a
have rw : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a
Tactic: rw [← cfcₙ_id ℝ≥0 a]
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a
have conv_lhs : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a
Tactic: conv_lhs => rw [← cfcₙ_id ℝ≥0 a]
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a
have refine : ∀ (x : ℝ≥0) (hx : x ∈ σₙ ℝ≥0 a), Membership.mem (γ := Set ℝ≥0) {x : ℝ≥0 | x < 1} x
Tactic: refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a)
have rw : ContinuousOn f (g '' σₙ ℝ≥0 a)
Tactic: rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
rw : ContinuousOn f (g '' σₙ ℝ≥0 a)
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a)
have rw₁ : ContinuousOn g (σₙ ℝ≥0 a)
Tactic: rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ ContinuousOn f (g '' σₙ ℝ≥0 a)
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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
⊢ ContinuousOn f (g '' σₙ ℝ≥0 a)
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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
funProp₁ : ∀ (x : ℝ≥0), x ≠ 0
⊢ ContinuousOn f (g '' σₙ ℝ≥0 a)
have funProp₂ : ∀ x ∈ g '' σₙ ℝ≥0 a, 1 + 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ 1 - x ≠ 0
have refine : x < 1
Tactic: refine tsub_pos_of_lt ?_ |>.ne'
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ ContinuousOn g (σₙ ℝ≥0 a)
have this : ∀ (x : ℝ≥0) (hx : x ∈ σₙ ℝ≥0 a), 1 - x ≠ 0
Tactic: have (x) (hx : x ∈ σₙ ℝ≥0 a) : 1 - x ≠ 0 := by
          refine tsub_pos_of_lt ?_ |>.ne'
          exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
this : ∀ (x : ℝ≥0) (hx : x ∈ σₙ ℝ≥0 a), 1 - x ≠ 0
⊢ ContinuousOn g (σₙ ℝ≥0 a)
have funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
Tactic: 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
this : ∀ (x : ℝ≥0) (hx : x ∈ σₙ ℝ≥0 a), 1 - x ≠ 0
funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
⊢ ContinuousOn g (σₙ ℝ≥0 a)
have funProp₁ : ∀ (x : ℝ≥0), x ≠ 0
Tactic: fun_prop
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a) ≤
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
have hab' : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a ≤ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b
Tactic: have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ a ≤ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
have a₁ : a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a
Tactic: calc
    a = cfcₙ (f ∘ g) a := by
      conv_lhs => rw [← cfcₙ_id ℝ≥0 a]
      refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)
      exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
    _ = cfcₙ f (cfcₙ g a) := by
      rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
      · fun_prop (disch := intro _ _; positivity)
      · have (x) (hx : x ∈ σₙ ℝ≥0 a) : 1 - x ≠ 0 := by
          refine tsub_pos_of_lt ?_ |>.ne'
          exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
        fun_prop
    _ ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) := by
      have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
      exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
        (cfcₙ_nonneg_of_predicate.trans hab') hab'
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
a₁ : a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a
⊢ a ≤ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
have a₂ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a)
Tactic: calc
    a = cfcₙ (f ∘ g) a := by
      conv_lhs => rw [← cfcₙ_id ℝ≥0 a]
      refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)
      exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
    _ = cfcₙ f (cfcₙ g a) := by
      rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
      · fun_prop (disch := intro _ _; positivity)
      · have (x) (hx : x ∈ σₙ ℝ≥0 a) : 1 - x ≠ 0 := by
          refine tsub_pos_of_lt ?_ |>.ne'
          exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
        fun_prop
    _ ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) := by
      have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
      exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
        (cfcₙ_nonneg_of_predicate.trans hab') hab'
-- 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
f : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
a₁ : a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a
a₂ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a)
⊢ a ≤ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
have a₃ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a) ≤
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
Tactic: calc
    a = cfcₙ (f ∘ g) a := by
      conv_lhs => rw [← cfcₙ_id ℝ≥0 a]
      refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)
      exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
    _ = cfcₙ f (cfcₙ g a) := by
      rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
      · fun_prop (disch := intro _ _; positivity)
      · have (x) (hx : x ∈ σₙ ℝ≥0 a) : 1 - x ≠ 0 := by
          refine tsub_pos_of_lt ?_ |>.ne'
          exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
        fun_prop
    _ ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) := by
      have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
      exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
        (cfcₙ_nonneg_of_predicate.trans hab') hab'
-- 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
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
have obtain : ∀ (n : ℕ) (c : Fin n → ℂ) (x : Fin n → (↑({x : A | 0 ≤ x} ∩ ball 0 1) : Type u_1)),
  Tendsto (β := A) (fun (x_1 : A) ↦ x_1 * ∑ i : Fin n, c i • (↑(x i) : A)) l (𝓝 (∑ i : Fin n, c i • (↑(x i) : A)))
Tactic: obtain ⟨n, c, x, rfl⟩ := mem_span_set'.mp <| by
    change m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)
    simp [span_nonneg_inter_unitBall]
Cleared hypotheses: 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
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → (↑({x : A | 0 ≤ x} ∩ ball 0 1) : Type u_1)
⊢ Tendsto (β := A) (fun (x_1 : A) ↦ x_1 * ∑ i : Fin n, c i • (↑(x i) : A)) l (𝓝 (∑ i : Fin n, c i • (↑(x i) : A)))
have simp_rw : Tendsto (β := A) (fun (x_1 : A) ↦ ∑ i : Fin n, x_1 * c i • (↑(x i) : A)) l (𝓝 (∑ i : Fin n, c i • (↑(x i) : A)))
Tactic: simp_rw [Finset.mul_sum]
-- 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
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → (↑({x : A | 0 ≤ x} ∩ ball 0 1) : Type u_1)
⊢ Tendsto (β := A) (fun (x_1 : A) ↦ ∑ i : Fin n, x_1 * c i • (↑(x i) : A)) l (𝓝 (∑ i : Fin n, c i • (↑(x i) : A)))
have refine : ∀ (i : Fin n),
  Membership.mem (γ := Finset (Fin n)) Finset.univ i →
    Tendsto (fun (x_2 : A) ↦ x_2 * c i • (↑(x i) : A)) l (𝓝 (c i • (↑(x i) : A)))
Tactic: refine tendsto_finsetSum _ fun i _ ↦ ?_
-- 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
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → (↑({x : A | 0 ≤ x} ∩ ball 0 1) : Type u_1)
i : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
⊢ Tendsto (fun (x_1 : A) ↦ x_1 * c i • (↑(x i) : A)) l (𝓝 (c i • (↑(x i) : A)))
have simp_rw : Tendsto (fun (x_1 : A) ↦ c i • (x_1 * (↑(x i) : A))) l (𝓝 (c i • (↑(x i) : A)))
Tactic: simp_rw [mul_smul_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
⊢ (∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)) ↔ ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
have refine_1 : ∀ (h : ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)) (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
Tactic: refine ⟨fun h m ↦ ?_, fun h m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
refine_1 : ∀ (h : ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)) (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
⊢ (∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)) ↔ ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
have refine_2 : ∀ (h : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)) (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)
Tactic: refine ⟨fun h m ↦ ?_, fun h m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)
m : A
⊢ Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
have refine_1 : l.EventuallyEq (β := A) (star ∘ fun (x : A) ↦ star m * x) fun (x : A) ↦ x * m
Tactic: apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)
m : A
⊢ l.EventuallyEq (β := A) (star ∘ fun (x : A) ↦ star m * x) fun (x : A) ↦ x * m
have h₁ : ∀ (x : A) (hx : IsSelfAdjoint x), (star ∘ fun (x : A) ↦ star m * x) x = x * m
Tactic: filter_upwards [hl] with x hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun (x : A) ↦ m * x) l (𝓝 m)
have refine_2 : l.EventuallyEq (β := A) (star ∘ fun (x : A) ↦ x * star m) fun (x : A) ↦ m * x
Tactic: apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)
m : A
⊢ l.EventuallyEq (β := A) (star ∘ fun (x : A) ↦ x * star m) fun (x : A) ↦ m * x
have h₁ : ∀ (x : A) (hx : IsSelfAdjoint x), (star ∘ fun (x : A) ↦ x * star m) x = m * x
Tactic: filter_upwards [hl] with x 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
x y : A
hx : 0 ≤ x ∧ ‖x‖ < 1
hy : 0 ≤ y ∧ ‖y‖ < 1
⊢ ∃ (k : A), (0 ≤ k ∧ ‖k‖ < 1) ∧ Subset.{u_1} (α := Set A) {x : A | k ≤ x} ({x_1 : A | x ≤ x_1} ∩ {x : A | y ≤ x})
have h : ∀ (z : A)
  (hz :
    Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ ball 0 1) z ∧
      (fun (x1 x2 : A) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : A) ↦ x1 ≤ x2) y z),
  (0 ≤ z ∧ ‖z‖ < 1) ∧ Subset.{u_1} (α := Set A) {x : A | z ≤ x} ({x_1 : A | x ≤ x_1} ∩ {x : A | y ≤ x})
Tactic: peel directedOn_nonneg_ball x (by simpa) y (by simpa) with z hz
-- 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
⊢ ‖z - y * z‖₊ ≤ c
have nth_rw : ‖1 * z - y * z‖₊ ≤ c
Tactic: nth_rw 1 [← one_mul z]
-- 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
⊢ ‖1 * z - y * z‖₊ ≤ c
have rw : ‖star ((1 - y) * z) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2
Tactic: rw [← sqrt_sq c, le_sqrt_iff_sq_le, ← sub_mul, sq, ← CStarRing.nnnorm_star_mul_self]
-- 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
⊢ ‖star ((1 - y) * z) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2
have simp : ‖star z * (1 - star y) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2
Tactic: simp only [star_mul, star_sub, star_one]
-- 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
⊢ ‖star z * (1 - star y) * ((1 - y) * z)‖₊ ≤ HPow.hPow (β := ℕ) c 2
have hy₀ : Membership.mem (γ := Set A) (Set.Icc 0 1) y
Tactic: have hy₀ : y ∈ Set.Icc 0 1 := ⟨hx₀.trans hy.1, hy.2⟩