-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
lemma CStarAlgebra.directedOn_nonneg_ball :
    DirectedOn (· ≤ ·) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1)

Proof state:
case intro.intro.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ cfcₙ f (cfcₙ g a + cfcₙ g b) ∈ Metric.ball 0 1

Tactic:
simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ x ∈ {x | x < 1}

Tactic:
exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂

Result:
no goals

Proof state:
case intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
ha₂ : a ∈ Metric.ball 0 1
b : A
hb₁ : 0 ≤ b
hb₂ : b ∈ Metric.ball 0 1
⊢ ∃ z ∈ {x | 0 ≤ x} ∩ Metric.ball 0 1, (fun x1 x2 => x1 ≤ x2) a z ∧ (fun x1 x2 => x1 ≤ x2) b z

Tactic:
simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂

Result:
case intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ ∃ z ∈ {x | 0 ≤ x} ∩ Metric.ball 0 1, (fun x1 x2 => x1 ≤ x2) a z ∧ (fun x1 x2 => x1 ≤ x2) b z

Proof state:
case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
this : ∀ x ∈ σₙ ℝ≥0 a, 1 - x ≠ 0
⊢ ∀ x ∈ σₙ ℝ≥0 a, 1 - x ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ a = cfcₙ (f ∘ g) a

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

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ cfcₙ id a = cfcₙ (f ∘ g) a

Proof state:
case intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ ∃ z ∈ {x | 0 ≤ x} ∩ Metric.ball 0 1, (fun x1 x2 => x1 ≤ x2) a z ∧ (fun x1 x2 => x1 ≤ x2) b z

Tactic:
refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩

Result:
case intro.intro.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ cfcₙ f (cfcₙ g a + cfcₙ g b) ∈ Metric.ball 0 1

case intro.intro.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ (fun x1 x2 => x1 ≤ x2) a (cfcₙ f (cfcₙ g a + cfcₙ g b))

case intro.intro.refine_3
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ (fun x1 x2 => x1 ≤ x2) b (cfcₙ f (cfcₙ g a + cfcₙ g b))

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ f 0 = 0

Tactic:
simp [f, tsub_self]

Result:
no goals

Proof state:
case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ ∀ x ∈ g '' σₙ ℝ≥0 a, 1 + x ≠ 0

Tactic:
intro _ _

Result:
case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
x✝ : ℝ≥0
a✝ : x✝ ∈ g '' σₙ ℝ≥0 a
⊢ 1 + x✝ ≠ 0

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
this : ∀ x ∈ σₙ ℝ≥0 a, 1 - x ≠ 0
⊢ ContinuousOn g (σₙ ℝ≥0 a)

Tactic:
fun_prop (disch := assumption)

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ cfcₙ f (cfcₙ g a + cfcₙ g b) ∈ {x | 0 ≤ x}

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ cfcₙ (f ∘ g) a = cfcₙ f (cfcₙ g a)

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

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ ContinuousOn f (g '' σₙ ℝ≥0 a)

A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
⊢ ContinuousOn g (σₙ ℝ≥0 a)

Proof state:
case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
x✝ : ℝ≥0
a✝ : x✝ ∈ g '' σₙ ℝ≥0 a
⊢ 1 + x✝ ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ DirectedOn (fun x1 x2 => x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)

Tactic:
let f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
⊢ DirectedOn (fun x1 x2 => x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)