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
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
c : Unitization ℂ A
hc : 0 ≤ c
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
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
c : Unitization ℂ A
hc : 0 ≤ c
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
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
c : Unitization ℂ A
hc : 0 ≤ c
x : ℝ≥0
funProp : x ∈ σ ℝ≥0 c → 1 + x ≠ 0
⊢ x ∈ σ ℝ≥0 c → 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
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
c : Unitization ℂ A
hc : 0 ≤ c
x : ℝ≥0
h : x ∈ σ ℝ≥0 c
⊢ 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
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
c : Unitization ℂ A
hc : 0 ≤ c
funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
funProp₁ : ∀ (x : ℝ≥0), x ≠ 0
funProp₂ : ∀ x ∈ σ ℝ≥0 c, 1 + x ≠ 0
⊢ ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ (1 + x)⁻¹) (σ ℝ≥0 c)

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
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
c : Unitization ℂ A
hc : 0 ≤ c
rw : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x⁻¹) ((fun (x : ℝ≥0) ↦ 1 + x) '' σ ℝ≥0 c)
⊢ cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) c =
    1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹) (1 + c)

Tactic:
rw [cfc_tsub _ _ _ (fun x _ ↦ by simp) (hg := by fun_prop (disch := intro _ _; positivity)),
      cfc_const_one ℝ≥0 c, cfc_comp' (·⁻¹) (1 + ·) c ?_, cfc_add .., cfc_const_one ℝ≥0 c,
      cfc_id' ℝ≥0 c]

Premises used: cfc_const_one, cfc_id', cfc_comp', NNReal, Inv.inv, HAdd.hAdd, cfc_tsub, OfNat.ofNat, cfc_add
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
c : Unitization ℂ A
hc : 0 ≤ c
⊢ ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x⁻¹) ((fun (x : ℝ≥0) ↦ 1 + x) '' σ ℝ≥0 c)

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

Premises used: Iff.mpr, ContinuousOn.inv₀, continuousOn_id, Set.forall_mem_image
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
⊢ ∀ (c : Unitization ℂ A) (hc : autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_5),
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) c =
      1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹) (1 + c)

Tactic:
have h_cfc_one_sub (c : A⁺¹) (hc : 0 ≤ c := by cfc_tac) :
      cfc (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (·⁻¹ : ℝ≥0 → ℝ≥0) (1 + c) := by
    rw [cfc_tsub _ _ _ (fun x _ ↦ by simp) (hg := by fun_prop (disch := intro _ _; positivity)),
      cfc_const_one ℝ≥0 c, cfc_comp' (·⁻¹) (1 + ·) c ?_, cfc_add .., cfc_const_one ℝ≥0 c,
      cfc_id' ℝ≥0 c]
    exact continuousOn_id.inv₀ (Set.forall_mem_image.mpr fun x _ ↦ by dsimp only [id]; positivity)
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A) (hc : autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_5),
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) c =
      1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹) (1 + c)
rw :
  1 -
      cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹)
        (HAdd.hAdd (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A)) ≤
    1 -
      cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹)
        (HAdd.hAdd (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A))
⊢ cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) (↑a : Unitization ℂ A) ≤
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) (↑b : Unitization ℂ A)

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

Premises used: Unitization.inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A) (hc : autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_5),
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) c =
      1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹) (1 + c)
h :
  cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹)
      (HAdd.hAdd (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A)) ≤
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹)
      (HAdd.hAdd (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A))
⊢ 1 -
      cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹)
        (HAdd.hAdd (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A)) ≤
    1 -
      cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹)
        (HAdd.hAdd (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A))

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A) (hc : autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_5),
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) c =
      1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹) (1 + c)
h :
  HPow.hPow (β := ℝ) (HAdd.hAdd (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A)) (-1) ≤
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A)) (-1)
⊢ cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹)
      (HAdd.hAdd (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A)) ≤
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹)
      (HAdd.hAdd (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A))

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

Premises used: CFC.rpow_neg_one_eq_cfc_inv
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A) (hc : autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_5),
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) c =
      1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹) (1 + c)
⊢ HAdd.hAdd (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A) ≤ HAdd.hAdd (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A)

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A) (hc : autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_5),
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) c =
      1 - cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹) (1 + c)
⊢ HPow.hPow (β := ℝ) (HAdd.hAdd (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A)) (-1) ≤
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A)) (-1)

Tactic:
exact rpow_neg_one_le_rpow_neg_one (by gcongr)

Premises used: CStarAlgebra.rpow_neg_one_le_rpow_neg_one
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
this :
  ∀ (ha : 0 ≤ a) ⦃b : A⦄,
    Membership.mem (γ := Set A) (Set.Ici 0) b →
      a ≤ b →
        cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a ≤
          cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b
⊢ Membership.mem (γ := Set A) (Set.Ici 0) a →
    ∀ ⦃b : A⦄,
      Membership.mem (γ := Set A) (Set.Ici 0) b →
        a ≤ b →
          cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a ≤
            cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b

Tactic:
(ha : 0 ≤ a)
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
this :
  ∀ (hb : 0 ≤ b),
    a ≤ b →
      cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a ≤
        cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b
⊢ Membership.mem (γ := Set A) (Set.Ici 0) b →
    a ≤ b →
      cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a ≤
        cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b

Tactic:
(hb : 0 ≤ b)
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
rw :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) a

Tactic:
rw [cfcₙ_nnreal_eq_real _ _ ha]

Premises used: cfcₙ_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) a

Tactic:
cfcₙ_congr ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
refine : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) (σₙ ℝ a)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) a

Tactic:
refine cfcₙ_congr ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ 0 ≤ x

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ 0 ≤ x

Tactic:
have hx' : 0 ≤ x := by grind
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
hx : x ∈ σₙ ℝ a
hx' : 0 ≤ x
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) x) ((fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) x)

Tactic:
simp [hx']
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) a ≤
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) b

Tactic:
CFC.monotoneOn_one_sub_one_add_inv ha hb hab

Premises used: CFC.monotoneOn_one_sub_one_add_inv
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
rw :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) b =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) b =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b

Tactic:
rw [cfcₙ_nnreal_eq_real _ _ hb]

Premises used: cfcₙ_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) b =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b

Tactic:
cfcₙ_congr ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
refine : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (σₙ ℝ b)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) b =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b

Tactic:
refine cfcₙ_congr ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
hx : x ∈ σₙ ℝ b
⊢ 0 ≤ x

Tactic:
grind
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
hx : x ∈ σₙ ℝ b
⊢ 0 ≤ x

Tactic:
have hx' : 0 ≤ x := by grind
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
hx : x ∈ σₙ ℝ b
hx' : 0 ≤ x
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) x) ((fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) x)

Tactic:
simp [hx']
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
calc :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) a
calc₁ :
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) b =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b

Tactic:
calc _ = cfcₙ (fun x : ℝ≥0 => 1 - (1 + x)⁻¹) a := by
          rw [cfcₙ_nnreal_eq_real _ _ ha]
          refine cfcₙ_congr ?_
          intro x hx
          have hx' : 0 ≤ x := by grind
          simp [hx']
    _ ≤ cfcₙ (fun x : ℝ≥0 => 1 - (1 + x)⁻¹) b :=
          CFC.monotoneOn_one_sub_one_add_inv ha hb hab
    _ = cfcₙ (fun x : ℝ => 1 - (1 + x)⁻¹) b := by
          rw [cfcₙ_nnreal_eq_real _ _ hb]
          refine cfcₙ_congr ?_
          intro x hx
          have hx' : 0 ≤ x := by grind
          simp [hx']

Premises used: cfcₙ, CFC.monotoneOn_one_sub_one_add_inv, HSub.hSub, Inv.inv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
h : ∀ (x : ℝ≥0), x * (1 + x)⁻¹ = 1 - (1 + x)⁻¹
⊢ Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹

Tactic:
ext x : 1
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
x : ℝ≥0
⊢ x * (1 + x)⁻¹ = 1 - (1 + x)⁻¹

Tactic:
simp [field, mul_tsub]

Premises used: mul_tsub
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
⊢ Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹

Tactic:
have : (fun x : ℝ≥0 ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹ := by
    ext x : 1
    simp [field, mul_tsub]
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
rw : InvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}
⊢ InvOn (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
left : LeftInvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1}
right : RightInvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1}
⊢ InvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
left : ∀ (hx : x < 1), (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) x) = x
⊢ Membership.mem (γ := Set ℝ≥0) {x : ℝ≥0 | x < 1} x →
    (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) x) = x

Tactic:
(hx : x < 1)
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
right : ∀ (hx : x < 1), (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) x) = x
⊢ Membership.mem (γ := Set ℝ≥0) {x : ℝ≥0 | x < 1} x →
    (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) x) = x

Tactic:
(hx : x < 1)
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ 0 < 1 - x

Tactic:
have : 0 < 1 - x := tsub_pos_of_lt hx
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this_1 : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
this : 0 < 1 - x
⊢ (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) x) = x

Tactic:
simp [field, tsub_add_cancel_of_le hx.le]

Premises used: tsub_add_cancel_of_le, LT.lt.le
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
right : x * (1 + x - (1 + x) * (x * (1 + x)⁻¹))⁻¹ = x
⊢ (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) x) = x

Tactic:
simp [mul_assoc, ← mul_inv, mul_tsub]

Premises used: mul_inv, mul_assoc, mul_tsub
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
right : x = x * (1 + x - x)
⊢ x * (1 + x - (1 + x) * (x * (1 + x)⁻¹))⁻¹ = x

Tactic:
field_simp
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ x = x * (1 + x - x)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
x : ℝ≥0
h : x ∈ σₙ ℝ≥0 a
⊢ 0 < (1 + x)⁻¹

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)⁻¹
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
⊢ ‖a‖ < 1

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

Premises used: Metric.mem_ball, 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
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
⊢ ‖b‖ < 1

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

Premises used: Metric.mem_ball, dist_zero_right