awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
h :
  ∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) ≤
    1 / 2
⊢ gauge U
      (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
        ((f : (a : (↑I : Type)) → E) x : E)) <
    1
have h₁ : ∑ k ∈ Sᶜ,
    HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
      (gauge U
        (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) <
  1 / 2
Tactic: calc
    gauge U (bernsteinApproximation n f x - f x)
      = gauge U (∑ k : Fin (n + 1), bernstein n k x • (f k/ₙ - f x)) := by
      simp [bernsteinApproximation.apply, smul_sub, ← Finset.sum_smul]
    _ ≤ ∑ k : Fin (n + 1), gauge U (bernstein n k x • (f k/ₙ - f x)) :=
      gauge_sum_le hUc (absorbent_nhds_zero hU₀) _ _
    _ = ∑ k : Fin (n + 1), bernstein n k x * gauge U (f k/ₙ - f x) := by
      simp only [gauge_smul_of_nonneg, bernstein_nonneg, smul_eq_mul]
    _ = (∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x)) +
          ∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) :=
      (S.sum_add_sum_compl _).symm
    -- We'll now deal with the terms in `S` and the terms in `Sᶜ` in separate calc blocks.
    _ < 1 / 2 + 1 / 2 := add_lt_add_of_le_of_lt ?_ ?_
    _ = 1 := add_halves 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ LE.le (α := ℝ)
    (∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
    (∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2))
have h : ∀ (k : Fin (n + 1)) (hk : k ∈ S),
  gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E)) ≤
    1 / 2
Tactic: gcongr with k hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k : Fin (n + 1)
hk : k ∈ S
⊢ gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E)) ≤
    1 / 2
have h : dist k/ₙ x < δ
Tactic: refine (hδ _ _ ?_).le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ ∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2) =
    1 / 2 * ∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
have rw : ∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2) =
  (∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x) * (1 / 2)
Tactic: rw [mul_comm, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
rw :
  ∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2) =
    (∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x) * (1 / 2)
⊢ ∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2) =
    1 / 2 * ∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
have rw₁ : Eq (α := ℝ) (∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2))
  (∑ i ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑i : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2))
Tactic: rw [mul_comm, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ 1 / 2 * ∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x ≤
    1 / 2 * ∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
have hbc : S ⊆ Finset.univ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ 1 / 2 * ∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x = 1 / 2
have rw : 1 / 2 * 1 = 1 / 2
Tactic: rw [bernstein.probability, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
rw : 1 / 2 * 1 = 1 / 2
⊢ 1 / 2 * ∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x = 1 / 2
have rw₁ : 1 / 2 = 1 / 2
Tactic: rw [bernstein.probability, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ ∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) ≤
    1 / 2
have k : LE.le (α := ℝ)
  (∑ k ∈ S,
    HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
      (gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
  (∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2))
Tactic: calc
      ∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ S, bernstein n k x * (1 / 2) := by
        gcongr with k hk
        refine (hδ _ _ ?_).le
        simpa [S] using hk
      _ = 1 / 2 * ∑ k ∈ S, bernstein n k x := by rw [mul_comm, Finset.sum_mul]
      -- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
      -- so that we can use `bernstein.probability`.
      _ ≤ 1 / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
      _ = 1 / 2 := by rw [bernstein.probability, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k :
  LE.le (α := ℝ)
    (∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
    (∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2))
⊢ ∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) ≤
    1 / 2
have k₁ : ∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2) =
  1 / 2 * ∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
Tactic: calc
      ∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ S, bernstein n k x * (1 / 2) := by
        gcongr with k hk
        refine (hδ _ _ ?_).le
        simpa [S] using hk
      _ = 1 / 2 * ∑ k ∈ S, bernstein n k x := by rw [mul_comm, Finset.sum_mul]
      -- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
      -- so that we can use `bernstein.probability`.
      _ ≤ 1 / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
      _ = 1 / 2 := by rw [bernstein.probability, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k :
  LE.le (α := ℝ)
    (∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
    (∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2))
k₁ :
  ∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2) =
    1 / 2 * ∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
⊢ ∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) ≤
    1 / 2
have k₂ : 1 / 2 * ∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x ≤
  1 / 2 * ∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
Tactic: calc
      ∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ S, bernstein n k x * (1 / 2) := by
        gcongr with k hk
        refine (hδ _ _ ?_).le
        simpa [S] using hk
      _ = 1 / 2 * ∑ k ∈ S, bernstein n k x := by rw [mul_comm, Finset.sum_mul]
      -- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
      -- so that we can use `bernstein.probability`.
      _ ≤ 1 / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
      _ = 1 / 2 := by rw [bernstein.probability, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k :
  LE.le (α := ℝ)
    (∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
    (∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2))
k₁ :
  ∑ k ∈ S, HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) (1 / 2) =
    1 / 2 * ∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
k₂ :
  1 / 2 * ∑ k ∈ S, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x ≤
    1 / 2 * ∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
⊢ ∑ k ∈ S,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) ≤
    1 / 2
have k₃ : 1 / 2 * ∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x = 1 / 2
Tactic: calc
      ∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ S, bernstein n k x * (1 / 2) := by
        gcongr with k hk
        refine (hδ _ _ ?_).le
        simpa [S] using hk
      _ = 1 / 2 * ∑ k ∈ S, bernstein n k x := by rw [mul_comm, Finset.sum_mul]
      -- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
      -- so that we can use `bernstein.probability`.
      _ ≤ 1 / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
      _ = 1 / 2 := by rw [bernstein.probability, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ LE.le (α := ℝ)
    (∑ k ∈ Sᶜ,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
    (∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
have simp : LE.le (α := ℝ)
  (∑ x_1 ∈ Sᶜ,
    HMul.hMul (β := ℝ)
      (gauge U
        (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x_1/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E)))
      ((bernstein n (↑x_1 : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
  (∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
Tactic: simp only [mul_comm (bernstein n _ x)]