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

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 (cfcₙ g a) ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)

Tactic:
have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate

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
hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b
⊢ cfcₙ f (cfcₙ g a) ≤ 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
hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b
⊢ cfcₙ f (cfcₙ g a) ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)

Tactic:
exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
  (cfcₙ_nonneg_of_predicate.trans hab') hab'

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
⊢ g 0 = 0

Tactic:
simp [g]

Result:
no goals

Proof state:
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))

Tactic:
exact this a b ha₁ hb₁ ha₂ hb₂

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)⁻¹
⊢ DirectedOn (fun x1 x2 => x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)

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

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)⁻¹
⊢ DirectedOn (fun x1 x2 => x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)

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ₙ id a = cfcₙ (f ∘ g) a

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

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
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ x ∈ {x | x < 1}

Proof state:
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))

Tactic:
exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂

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
⊢ ContinuousOn f (g '' σₙ ℝ≥0 a)

Tactic:
fun_prop (disch := intro _ _; positivity)

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
⊢ 1 - x ≠ 0

Tactic:
refine tsub_pos_of_lt ?_ |>.ne'

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
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ x < 1

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

Tactic:
exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂

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
⊢ ContinuousOn g (σₙ ℝ≥0 a)

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₂

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
this : ∀ x ∈ σₙ ℝ≥0 a, 1 - x ≠ 0
⊢ ContinuousOn g (σₙ ℝ≥0 a)

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)
⊢ DirectedOn (fun x1 x2 => x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)

Tactic:
rintro a ⟨(ha₁ : 0 ≤ a), ha₂⟩ b ⟨(hb₁ : 0 ≤ b), 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
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

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), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)

Tactic:
rintro a b ha₁ - 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
⊢ a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)