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
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
⊢ Membership.mem (γ := Set A) {x : A | 0 ≤ x}
    (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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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))
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))
⊢ ∃ (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

Tactic:
refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ 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:
simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _

Premises used: Metric.mem_ball, norm_cfcₙ_one_sub_one_add_inv_lt_one, dist_zero_right
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ (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:
this a b ha₁ hb₁ ha₂ hb₂
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ (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:
exact this a b ha₁ hb₁ ha₂ hb₂
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ (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:
add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂

Premises used: cfcₙ, Eq.rec, add_comm, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ (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:
exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)⁻¹
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)
⊢ DirectedOn (fun (x1 x2 : A) ↦ x1 ≤ x2) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1)

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₂
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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 : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a
| a

Tactic:
rw [← cfcₙ_id ℝ≥0 a]

Premises used: NNReal, cfcₙ_id
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
conv_lhs : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a
⊢ a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a

Tactic:
conv_lhs => rw [← cfcₙ_id ℝ≥0 a]

Premises used: NNReal, cfcₙ_id
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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

Tactic:
cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)

Premises used: Set.LeftInvOn.eqOn, Set.InvOn.one_sub_one_add_inv, cfcₙ_congr, And.left, Set.EqOn.symm, Set.EqOn.mono
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
refine : ∀ (x : ℝ≥0) (hx : x ∈ σₙ ℝ≥0 a), Membership.mem (γ := Set ℝ≥0) {x : ℝ≥0 | x < 1} x
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (f ∘ g) a

Tactic:
refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)

Premises used: Set.LeftInvOn.eqOn, Set.InvOn.one_sub_one_add_inv, cfcₙ_congr, And.left, Set.EqOn.symm, Set.EqOn.mono
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ Membership.mem (γ := Set ℝ≥0) {x : ℝ≥0 | x < 1} x

Tactic:
lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂

Premises used: lt_of_le_of_lt, Set.Mem, setOf, CStarAlgebra.le_nnnorm_of_mem_quasispectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ Membership.mem (γ := Set ℝ≥0) {x : ℝ≥0 | x < 1} x

Tactic:
exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂

Premises used: lt_of_le_of_lt, CStarAlgebra.le_nnnorm_of_mem_quasispectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ f 0 = 0

Tactic:
simp [f, 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
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
⊢ g 0 = 0

Tactic:
simp [g]
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)
rw₁ : ContinuousOn 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)

Tactic:
rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]

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

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

Tactic:
_
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
funProp : x ∈ g '' σₙ ℝ≥0 a → 1 + x ≠ 0
⊢ x ∈ g '' σₙ ℝ≥0 a → 1 + x ≠ 0

Tactic:
_
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
h : x ∈ g '' σₙ ℝ≥0 a
⊢ 1 + x ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
funProp₂ : ∀ x ∈ g '' σₙ ℝ≥0 a, 1 + x ≠ 0
⊢ ContinuousOn f (g '' σₙ ℝ≥0 a)

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
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

Tactic:
tsub_pos_of_lt ?_ |>.ne'

Premises used: LT.lt.ne', tsub_pos_of_lt
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
refine : x < 1
⊢ 1 - x ≠ 0

Tactic:
refine tsub_pos_of_lt ?_ |>.ne'

Premises used: LT.lt.ne', tsub_pos_of_lt
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ x < 1

Tactic:
lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂

Premises used: lt_of_le_of_lt, CStarAlgebra.le_nnnorm_of_mem_quasispectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ x < 1

Tactic:
exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂

Premises used: lt_of_le_of_lt, CStarAlgebra.le_nnnorm_of_mem_quasispectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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

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₂
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
funProp₁ : ∀ (x : ℝ≥0), x ≠ 0
funProp₂ : ∀ x ∈ σₙ ℝ≥0 a, 1 - x ≠ 0
⊢ ContinuousOn g (σₙ ℝ≥0 a)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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) 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
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
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
⊢ 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:
CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
        (cfcₙ_nonneg_of_predicate.trans hab') hab'

Premises used: CFC.monotoneOn_one_sub_one_add_inv, LE.le.trans, 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
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
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
⊢ 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:
exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
        (cfcₙ_nonneg_of_predicate.trans hab') hab'

Premises used: CFC.monotoneOn_one_sub_one_add_inv, LE.le.trans, 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
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) f (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a + cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g b)
⊢ 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'

Premises used: cfcₙ, Function.comp, HAdd.hAdd
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
l : Filter A
hl : l.IsIncreasingApproximateUnit
⊢ ∀ᶠ (x : A) in l, ‖x‖₊ ≤ 1

Tactic:
hl.eventually_norm

Premises used: Filter.IsIncreasingApproximateUnit.eventually_norm
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
l : Filter A
hl : l.IsIncreasingApproximateUnit
⊢ ∀ᶠ (x : A) in l, IsSelfAdjoint x

Tactic:
hl.eventually_nonneg.mp <| .of_forall fun _ ↦ IsSelfAdjoint.of_nonneg

Premises used: Filter.IsIncreasingApproximateUnit.eventually_nonneg, Filter.Eventually.of_forall, IsSelfAdjoint.of_nonneg, Filter.Eventually.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
l : Filter A
hl : l.IsIncreasingApproximateUnit
⊢ ∀ᶠ (x : A) in l, star x = x

Tactic:
hl.eventually_isSelfAdjoint.mp <| .of_forall fun _ ↦ IsSelfAdjoint.star_eq

Premises used: Filter.Eventually.of_forall, Filter.IsIncreasingApproximateUnit.eventually_isSelfAdjoint, Filter.Eventually.mp, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ ({x : A | 0 ≤ x} ∩ ball 0 1)) m

Tactic:
simp [span_nonneg_inter_unitBall]

Premises used: CStarAlgebra.span_nonneg_inter_unitBall
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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
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)))
⊢ Tendsto (fun (x : A) ↦ x * m) l (𝓝 m)

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]

Premises used: Iff.mp, Submodule.mem_span_set', rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)
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)))
⊢ 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:
simp_rw [Finset.mul_sum]

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

Tactic:
tendsto_finsetSum _ fun i _ ↦ ?_

Premises used: tendsto_finsetSum
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
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)
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)))
⊢ 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:
refine tendsto_finsetSum _ fun i _ ↦ ?_

Premises used: tendsto_finsetSum