awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
refine_2 :
  Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))
⊢ Tendsto
    (fun (b : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈b⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        b ^ card ι)
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * HPow.hPow (α := ℝ) 1 (card ι)))
have refine_2₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (↑⌈x⌉₊ : ℝ) / x) atTop (𝓝 1)
Tactic: refine Tendsto.congr' (tendsto_card_div_pow₆ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := Set A) (Set.Ici 0) a
b : A
hb : Membership.mem (γ := Set A) (Set.Ici 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
have ha₁ : 0 ≤ a
Tactic: simp only [Set.mem_Ici] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := Set A) (Set.Ici 0) a
b : A
hb : Membership.mem (γ := Set A) (Set.Ici 0) b
hab : a ≤ b
ha₁ : 0 ≤ a
⊢ 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
have hb₁ : 0 ≤ b
Tactic: simp only [Set.mem_Ici] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ 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
have rw : 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 [← inr_le_iff .., nnreal_cfcₙ_eq_cfc_inr a _, nnreal_cfcₙ_eq_cfc_inr b _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 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)
have hab₁ : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
Tactic: rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab
Cleared hypotheses: hab, ha, hb
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
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 : 0 ≤ a
hb : 0 ≤ b
⊢ 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)
have ha₁ : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
Tactic: rw [← inr_nonneg_iff] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
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 : 0 ≤ a
hb : 0 ≤ b
ha₁ : LE.le (α := Unitization ℂ A) 0 (↑a : 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)
have hb₁ : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
Tactic: rw [← inr_nonneg_iff] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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) ↦ (1 + x)⁻¹) (σ ℝ≥0 c)
have funProp : ∀ x ∈ σ ℝ≥0 (↑?a : ?A), x ≠ 0
Tactic: fun_prop (disch := intro _ _; positivity)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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
⊢ ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ (1 + x)⁻¹) (σ ℝ≥0 c)
have funProp₁ : ∀ (x : ℝ≥0), x ≠ 0
Tactic: fun_prop (disch := intro _ _; positivity)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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
⊢ ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ (1 + x)⁻¹) (σ ℝ≥0 c)
have funProp₂ : ∀ x ∈ σ ℝ≥0 c, 1 + x ≠ 0
Tactic: fun_prop (disch := intro _ _; positivity)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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
⊢ 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)
have rw : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x⁻¹) ((fun (x : ℝ≥0) ↦ 1 + x) '' σ ℝ≥0 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
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)
⊢ 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)
have 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)
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)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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)
⊢ 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)
have 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))
Tactic: rw [h_cfc_one_sub (a : A⁺¹), h_cfc_one_sub (b : A⁺¹)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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)
⊢ 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))
have 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))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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)
⊢ 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))
have h : HPow.hPow (β := ℝ) (HAdd.hAdd (α := Unitization ℂ A) 1 (↑b : Unitization ℂ A)) (-1) ≤
  HPow.hPow (β := ℝ) (HAdd.hAdd (α := Unitization ℂ A) 1 (↑a : Unitization ℂ A)) (-1)
Tactic: rw [← CFC.rpow_neg_one_eq_cfc_inv, ← CFC.rpow_neg_one_eq_cfc_inv]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ 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
have 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
Tactic: (ha : 0 ≤ a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
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
have this : ∀ (hb : 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)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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 := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) a
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a =
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) a
Tactic: rw [cfcₙ_nnreal_eq_real _ _ ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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
have refine : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) (σₙ ℝ a)
Tactic: refine cfcₙ_congr ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
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
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) x) ((fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) x)
have hx' : 0 ≤ x
Tactic: have hx' : 0 ≤ x := by grind
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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)⁻¹) b =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) b =
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b
Tactic: rw [cfcₙ_nnreal_eq_real _ _ hb]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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
have refine : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) (σₙ ℝ b)
Tactic: refine cfcₙ_congr ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
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
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ (↑(1 - (1 + x.toNNReal)⁻¹) : ℝ)) x) ((fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) x)
have hx' : 0 ≤ x
Tactic: have hx' : 0 ≤ x := by grind
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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)⁻¹) b
have calc : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a =
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) a
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']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1 - (1 + x)⁻¹) b
have calc₁ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) b =
  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']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
⊢ Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
have h : ∀ (x : ℝ≥0), x * (1 + x)⁻¹ = 1 - (1 + x)⁻¹
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
⊢ InvOn (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
⊢ InvOn (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}
have rw : InvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
⊢ InvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}
have left : LeftInvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
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}
⊢ InvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1}
have right : RightInvOn (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
⊢ Membership.mem (γ := Set ℝ≥0) {x : ℝ≥0 | x < 1} x →
    (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) x) = x
have left : ∀ (hx : x < 1), (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) x) = x
Tactic: (hx : x < 1)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
⊢ Membership.mem (γ := Set ℝ≥0) {x : ℝ≥0 | x < 1} x →
    (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) x) = x
have right : ∀ (hx : x < 1), (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) x) = x
Tactic: (hx : x < 1)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) x) = x
have this₁ : 0 < 1 - x
Tactic: have : 0 < 1 - x := tsub_pos_of_lt hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun (x : ℝ≥0) ↦ x * (1 - x)⁻¹) ((fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) x) = x
have right : x * (1 + x - (1 + x) * (x * (1 + x)⁻¹))⁻¹ = x
Tactic: simp [mul_assoc, ← mul_inv, mul_tsub]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (goal)
Goal:
this : Eq (α := (x : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0) ↦ x * (1 + x)⁻¹) fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ x * (1 + x - (1 + x) * (x * (1 + x)⁻¹))⁻¹ = x
have right : x = x * (1 + x - x)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ApproximateUnit (hypothesis)
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
⊢ ∃ (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
have ha₃ : ‖a‖ < 1
Tactic: simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂
Cleared hypotheses: ha₂, hb₂