-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
lemma CFC.monotoneOn_one_sub_one_add_inv :
    MonotoneOn (cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹)) (Set.Ici (0 : A))

Proof state:
case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
⊢ ∀ x ∈ σ ℝ≥0 c, 1 + x ≠ 0

Tactic:
intro _ _

Result:
case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
x✝ : ℝ≥0
a✝ : x✝ ∈ σ ℝ≥0 c
⊢ 1 + x✝ ≠ 0

Proof state:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A), autoParam (0 ≤ c) _auto✝ → cfc (fun x => 1 - (1 + x)⁻¹) c = 1 - cfc (fun x => x⁻¹) (1 + c)
⊢ cfc (fun x => x⁻¹) (1 + ↑b) ≤ cfc (fun x => x⁻¹) (1 + ↑a)

Tactic:
rw [← CFC.rpow_neg_one_eq_cfc_inv, ← CFC.rpow_neg_one_eq_cfc_inv]

Result:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A), autoParam (0 ≤ c) _auto✝ → cfc (fun x => 1 - (1 + x)⁻¹) c = 1 - cfc (fun x => x⁻¹) (1 + c)
⊢ (1 + ↑b) ^ (-1) ≤ (1 + ↑a) ^ (-1)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
x : ℝ≥0
x✝ : x ∈ σ ℝ≥0 c
⊢ 1 + x ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
x : ℝ≥0
x✝ : x ∈ σ ℝ≥0 c
⊢ (1 + x)⁻¹ ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A), autoParam (0 ≤ c) _auto✝ → cfc (fun x => 1 - (1 + x)⁻¹) c = 1 - cfc (fun x => x⁻¹) (1 + c)
⊢ (1 + ↑b) ^ (-1) ≤ (1 + ↑a) ^ (-1)

Tactic:
exact rpow_neg_one_le_rpow_neg_one (add_nonneg zero_le_one ha) (by gcongr) <|
  isUnit_of_le isUnit_one zero_le_one <| le_add_of_nonneg_right ha

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A), autoParam (0 ≤ c) _auto✝ → cfc (fun x => 1 - (1 + x)⁻¹) c = 1 - cfc (fun x => x⁻¹) (1 + c)
⊢ 1 - cfc (fun x => x⁻¹) (1 + ↑a) ≤ 1 - cfc (fun x => x⁻¹) (1 + ↑b)

Tactic:
gcongr

Result:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A), autoParam (0 ≤ c) _auto✝ → cfc (fun x => 1 - (1 + x)⁻¹) c = 1 - cfc (fun x => x⁻¹) (1 + c)
⊢ cfc (fun x => x⁻¹) (1 + ↑b) ≤ cfc (fun x => x⁻¹) (1 + ↑a)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
⊢ ContinuousOn (fun x => (1 + x)⁻¹) (σ ℝ≥0 c)

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

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfc (fun x => 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x => 1 - (1 + x)⁻¹) ↑b

Tactic:
rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfc (fun x => 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x => 1 - (1 + x)⁻¹) ↑b

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A), autoParam (0 ≤ c) _auto✝ → cfc (fun x => 1 - (1 + x)⁻¹) c = 1 - cfc (fun x => x⁻¹) (1 + c)
⊢ cfc (fun x => 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x => 1 - (1 + x)⁻¹) ↑b

Tactic:
rw [h_cfc_one_sub (a : A⁺¹), h_cfc_one_sub (b : A⁺¹)]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A), autoParam (0 ≤ c) _auto✝ → cfc (fun x => 1 - (1 + x)⁻¹) c = 1 - cfc (fun x => x⁻¹) (1 + c)
⊢ 1 - cfc (fun x => x⁻¹) (1 + ↑a) ≤ 1 - cfc (fun x => x⁻¹) (1 + ↑b)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ Set.Ici 0
b : A
hb : b ∈ Set.Ici 0
hab : a ≤ b
⊢ cfcₙ (fun x => 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x => 1 - (1 + x)⁻¹) b

Tactic:
simp only [Set.mem_Ici] at ha hb

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfcₙ (fun x => 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x => 1 - (1 + x)⁻¹) b

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A), autoParam (0 ≤ c) _auto✝ → cfc (fun x => 1 - (1 + x)⁻¹) c = 1 - cfc (fun x => x⁻¹) (1 + c)
⊢ 1 + ↑a ≤ 1 + ↑b

Tactic:
gcongr

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfc (fun x => 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x => 1 - (1 + x)⁻¹) ↑b

Tactic:
rw [← inr_nonneg_iff] at ha hb

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
⊢ cfc (fun x => 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x => 1 - (1 + x)⁻¹) ↑b

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfcₙ (fun x => 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x => 1 - (1 + x)⁻¹) b

Tactic:
rw [← inr_le_iff .., nnreal_cfcₙ_eq_cfc_inr a _, nnreal_cfcₙ_eq_cfc_inr b _]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfc (fun x => 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x => 1 - (1 + x)⁻¹) ↑b

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
⊢ ContinuousOn (fun x => x⁻¹) ((fun x => 1 + x) '' σ ℝ≥0 c)

Tactic:
exact continuousOn_id.inv₀ (Set.forall_mem_image.mpr fun x _ ↦ by dsimp only [id]; positivity)

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ MonotoneOn (cfcₙ fun x => 1 - (1 + x)⁻¹) (Set.Ici 0)

Tactic:
intro a ha b hb hab

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ Set.Ici 0
b : A
hb : b ∈ Set.Ici 0
hab : a ≤ b
⊢ cfcₙ (fun x => 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x => 1 - (1 + x)⁻¹) b