-- 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 (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
k₁ :
  ∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    C * ∑ k ∈ Sᶜ, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
k₂ :
  C * ∑ k ∈ Sᶜ, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x ≤
    C *
      ∑ k ∈ Sᶜ,
        HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
          ((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₃ : C *
    ∑ k ∈ Sᶜ,
      HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
        ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) ≤
  C *
    ∑ k : Fin (n + 1),
      HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
        ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
Tactic: calc
      ∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ Sᶜ, C * bernstein n k x := by
        simp only [mul_comm (bernstein n _ x)]
        gcongr
        apply hC
      _ = C * ∑ k ∈ Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
      _ ≤ C * ∑ k ∈ Sᶜ, ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr with k hk
        conv_lhs => rw [← one_mul (bernstein _ _ _)]
        gcongr
        simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)]
          using hk
      -- Again enlarging the sum from `Sᶜ` to all of `Fin (n+1)`
      _ ≤ C * ∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr; exact Sᶜ.subset_univ
      _ = C * (∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x) / δ ^ 2 := by
        simp only [← mul_div_right_comm, ← mul_div_assoc, ← Finset.sum_div]
      -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
      _ = C / δ ^ 2 * x * (1 - x) / n := by rw [variance hn₀]; ring
      _ ≤ C / δ ^ 2 * 1 * 1 / n := by gcongr <;> unit_interval
      _ < 1 / 2 := by simpa only [mul_one]