awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
⊢ ∑ k : Fin (n + 1),
      HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑(k/ₙ) : ℝ)) 2)
        ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)
have h : ∑ k : Fin (n + 1),
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑(k/ₙ) : ℝ)) 2)
      ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
  HDiv.hDiv (α := ℝ)
    ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ)
        (∑ ν ∈ Finset.range (n + 1),
          HPow.hPow (β := ℕ) (HSMul.hSMul (β := Polynomial ℝ) n Polynomial.X - (↑ν : Polynomial ℝ)) 2 *
            bernsteinPolynomial ℝ n ν) :
      ℝ)
    (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
Tactic: convert! congr(Polynomial.aeval (x : ℝ) $(bernsteinPolynomial.variance ℝ n) / n ^ 2) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
h :
  ∑ k : Fin (n + 1),
      HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑(k/ₙ) : ℝ)) 2)
        ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    HDiv.hDiv (α := ℝ)
      ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ)
          (∑ ν ∈ Finset.range (n + 1),
            HPow.hPow (β := ℕ) (HSMul.hSMul (β := Polynomial ℝ) n Polynomial.X - (↑ν : Polynomial ℝ)) 2 *
              bernsteinPolynomial ℝ n ν) :
        ℝ)
      (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
⊢ ∑ k : Fin (n + 1),
      HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑(k/ₙ) : ℝ)) 2)
        ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)
have h₁ : (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) =
  HDiv.hDiv (α := ℝ)
    ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ)
        (HSMul.hSMul (β := Polynomial ℝ) n Polynomial.X * HSub.hSub (α := Polynomial ℝ) 1 Polynomial.X) :
      ℝ)
    (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
Tactic: convert! congr(Polynomial.aeval (x : ℝ) $(bernsteinPolynomial.variance ℝ n) / n ^ 2) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
⊢ ∑ k : Fin (n + 1),
      HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑(k/ₙ) : ℝ)) 2)
        ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    HDiv.hDiv (α := ℝ)
      ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ)
          (∑ ν ∈ Finset.range (n + 1),
            HPow.hPow (β := ℕ) (HSMul.hSMul (β := Polynomial ℝ) n Polynomial.X - (↑ν : Polynomial ℝ)) 2 *
              bernsteinPolynomial ℝ n ν) :
        ℝ)
      (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
have h : ∑ x_1 : Fin (n + 1),
    HPow.hPow (β := ℕ) ((↑x : ℝ) - HDiv.hDiv (α := ℝ) (↑(↑x_1 : ℕ) : ℝ) (↑n : ℝ)) 2 *
      ((↑(n.choose (↑x_1 : ℕ)) : ℝ) * (↑x : ℝ) ^ (↑x_1 : ℕ) * (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ))) =
  (∑ x_1 : Fin (n + 1),
      HPow.hPow (β := ℕ) ((↑n : ℝ) * (↑x : ℝ) - (↑(↑x_1 : ℕ) : ℝ)) 2 *
        ((↑(n.choose (↑x_1 : ℕ)) : ℝ) * (↑x : ℝ) ^ (↑x_1 : ℕ) * (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ)))) /
    HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
Tactic: simp only [z, bernstein_apply, nsmul_eq_mul, bernsteinPolynomial, Finset.sum_range, map_sum,
      Polynomial.coe_aeval_eq_eval, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_sub,
      Polynomial.eval_natCast, Polynomial.eval_X, Polynomial.eval_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
⊢ ∑ x_1 : Fin (n + 1),
      HPow.hPow (β := ℕ) ((↑x : ℝ) - HDiv.hDiv (α := ℝ) (↑(↑x_1 : ℕ) : ℝ) (↑n : ℝ)) 2 *
        ((↑(n.choose (↑x_1 : ℕ)) : ℝ) * (↑x : ℝ) ^ (↑x_1 : ℕ) * (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ))) =
    (∑ x_1 : Fin (n + 1),
        HPow.hPow (β := ℕ) ((↑n : ℝ) * (↑x : ℝ) - (↑(↑x_1 : ℕ) : ℝ)) 2 *
          ((↑(n.choose (↑x_1 : ℕ)) : ℝ) * (↑x : ℝ) ^ (↑x_1 : ℕ) * (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ)))) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
have h : HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 *
    ∑ x_1 : Fin (n + 1),
      HPow.hPow (β := ℕ) ((↑x : ℝ) * (↑n : ℝ) - (↑(↑x_1 : ℕ) : ℝ)) 2 * (↑(n.choose (↑x_1 : ℕ)) : ℝ) *
            (↑x : ℝ) ^ (↑x_1 : ℕ) *
          (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ)) /
        HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 =
  ∑ x_1 : Fin (n + 1),
    HPow.hPow (β := ℕ) ((↑x : ℝ) * (↑n : ℝ) - (↑(↑x_1 : ℕ) : ℝ)) 2 * (↑(n.choose (↑x_1 : ℕ)) : ℝ) *
        (↑x : ℝ) ^ (↑x_1 : ℕ) *
      (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 *
      ∑ x_1 : Fin (n + 1),
        HPow.hPow (β := ℕ) ((↑x : ℝ) * (↑n : ℝ) - (↑(↑x_1 : ℕ) : ℝ)) 2 * (↑(n.choose (↑x_1 : ℕ)) : ℝ) *
              (↑x : ℝ) ^ (↑x_1 : ℕ) *
            (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ)) /
          HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 =
    ∑ x_1 : Fin (n + 1),
      HPow.hPow (β := ℕ) ((↑x : ℝ) * (↑n : ℝ) - (↑(↑x_1 : ℕ) : ℝ)) 2 * (↑(n.choose (↑x_1 : ℕ)) : ℝ) *
          (↑x : ℝ) ^ (↑x_1 : ℕ) *
        (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ))
have h : HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 *
    ((∑ i : Fin (n + 1),
        HPow.hPow (β := ℕ) ((↑x : ℝ) * (↑n : ℝ) - (↑(↑i : ℕ) : ℝ)) 2 * (↑(n.choose (↑i : ℕ)) : ℝ) *
            (↑x : ℝ) ^ (↑i : ℕ) *
          (1 - (↑x : ℝ)) ^ (n - (↑i : ℕ))) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) =
  ∑ x_1 : Fin (n + 1),
    HPow.hPow (β := ℕ) ((↑x : ℝ) * (↑n : ℝ) - (↑(↑x_1 : ℕ) : ℝ)) 2 * (↑(n.choose (↑x_1 : ℕ)) : ℝ) *
        (↑x : ℝ) ^ (↑x_1 : ℕ) *
      (1 - (↑x : ℝ)) ^ (n - (↑x_1 : ℕ))
Tactic: rw [← Finset.sum_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
⊢ (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) =
    HDiv.hDiv (α := ℝ)
      ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ)
          (HSMul.hSMul (β := Polynomial ℝ) n Polynomial.X * HSub.hSub (α := Polynomial ℝ) 1 Polynomial.X) :
        ℝ)
      (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
have h : (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) = (↑n : ℝ) * (↑x : ℝ) * (1 - (↑x : ℝ)) / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
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 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ Tendsto (fun (n : ℕ) ↦ bernsteinApproximation n f) atTop (𝓝 f)
have this₁ : IsUniformAddGroup E
Tactic: have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
-- 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_2 : IsUniformAddGroup E
this :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      Convex ℝ U →
        ∀ᶠ (n : ℕ) in atTop,
          ∀ (x : (↑I : Type)),
            gauge U
                (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
                  ((f : (a : (↑I : Type)) → E) x : E)) <
              1
⊢ Tendsto (fun (n : ℕ) ↦ bernsteinApproximation n f) atTop (𝓝 f)
have rw : ∀ (i : Set E),
  Membership.mem (γ := Filter E) (𝓝 0) i ∧ Convex ℝ i →
    ∀ᶠ (x : ℕ) in atTop,
      Membership.mem (γ := Set C((↑I : Type), E))
        {y : C((↑I : Type), E) |
          Membership.mem (γ := SetRel C((↑I : Type), E) C((↑I : Type), E))
            {fg : C((↑I : Type), E) × C((↑I : Type), E) |
              ∀ (x : (↑I : Type)),
                Membership.mem (α := E × E) (γ := Set (E × E)) {x : E × E | x.1 - x.2 ∈ id i}
                  (((fg.1 : (a : (↑I : Type)) → E) x, (fg.2 : (a : (↑I : Type)) → E) x) : E × E)}
            (y, f)}
        (bernsteinApproximation x f)
Tactic: rw [(LocallyConvexSpace.convex_basis_zero ℝ E).uniformity_of_nhds_zero_swapped
      |>.compactConvergenceUniformity_of_compact |> nhds_basis_uniformity |>.tendsto_right_iff]
-- 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_2 : IsUniformAddGroup E
this :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      Convex ℝ U →
        ∀ᶠ (n : ℕ) in atTop,
          ∀ (x : (↑I : Type)),
            gauge U
                (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
                  ((f : (a : (↑I : Type)) → E) x : E)) <
              1
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hcU : Convex ℝ U
⊢ ∀ᶠ (x : ℕ) in atTop,
    Membership.mem (γ := Set C((↑I : Type), E))
      {y : C((↑I : Type), E) |
        Membership.mem (γ := SetRel C((↑I : Type), E) C((↑I : Type), E))
          {fg : C((↑I : Type), E) × C((↑I : Type), E) |
            ∀ (x : (↑I : Type)),
              Membership.mem (α := E × E) (γ := Set (E × E)) {x : E × E | x.1 - x.2 ∈ id U}
                (((fg.1 : (a : (↑I : Type)) → E) x, (fg.2 : (a : (↑I : Type)) → E) x) : E × E)}
          (y, f)}
      (bernsteinApproximation x f)
have h : ∀ (n : ℕ)
  (hn :
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1)
  (x : (↑I : Type)),
  HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
      ((f : (a : (↑I : Type)) → E) x : E) ∈
    id U
Tactic: filter_upwards [this U hU₀ hcU] with n hn x
-- 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
⊢ Tendsto (fun (n : ℕ) ↦ bernsteinApproximation n f) atTop (𝓝 f)
have suffices : ∀ (U : Set E),
  Membership.mem (γ := Filter E) (𝓝 0) U →
    Convex ℝ U →
      ∀ᶠ (n : ℕ) in atTop,
        ∀ (x : (↑I : Type)),
          gauge U
              (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
                ((f : (a : (↑I : Type)) → E) x : E)) <
            1
Tactic: suffices ∀ U ∈ 𝓝 (0 : E), Convex ℝ U →
      ∀ᶠ n in atTop, ∀ x : I, gauge U (bernsteinApproximation n f x - f x) < 1 by
    rw [(LocallyConvexSpace.convex_basis_zero ℝ E).uniformity_of_nhds_zero_swapped
      |>.compactConvergenceUniformity_of_compact |> nhds_basis_uniformity |>.tendsto_right_iff]
    rintro U ⟨hU₀, hcU⟩
    filter_upwards [this U hU₀ hcU] with n hn x
    exact gauge_lt_one_subset_self hcU (mem_of_mem_nhds hU₀) (absorbent_nhds_zero hU₀) (hn x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
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 : ℝ),
    ∀ (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
have this₁ : Continuous (Y := ℝ) fun (x : (↑I : Type) × (↑I : Type)) ↦
  match (motive := (↑I : Type) × (↑I : Type) → ℝ) x with
  | (x, y) =>
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E))
Tactic: have : Continuous fun (x, y) ↦ gauge U (f x - f y) := by fun_prop
-- 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
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1
have obtain : ∀ (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),
  ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1
Tactic: obtain ⟨C, hC⟩ : ∃ C, ∀ x y, gauge U (f x - f y) ≤ C := by
    have : Continuous fun (x, y) ↦ gauge U (f x - f y) := by fun_prop
    simpa only [BddAbove, Set.Nonempty, mem_upperBounds, Set.forall_mem_range, Prod.forall]
      using isCompact_range this |>.bddAbove
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
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
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1
have hC₀ : 0 ≤ C
Tactic: have hC₀ : 0 ≤ C := le_trans (gauge_nonneg _) (hC 0 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
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
⊢ ∃ δ > 0,
    ∀ (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
have this₁ : UniformContinuous (α := (↑I : Type)) (β := E) (⇑f : (a : (↑I : Type)) → E)
Tactic: have := CompactSpace.uniformContinuous_of_continuous (map_continuous f)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
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_2 : 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
this : UniformContinuous (α := (↑I : Type)) (β := E) (⇑f : (a : (↑I : Type)) → E)
⊢ ∃ δ > 0,
    ∀ (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
have this₁ : ∀ (i : Set E),
  Membership.mem (γ := Filter E) (𝓝 0) i →
    ∃ (j : ℝ),
      0 < j ∧
        ∀ (x y : (↑I : Type)),
          Membership.mem (γ := SetRel (↑I : Type) (↑I : Type)) {p : (↑I : Type) × (↑I : Type) | dist p.1 p.2 < j}
              (x, y) →
            Membership.mem (α := E × E) (γ := Set (E × E)) {x : E × E | x.1 - x.2 ∈ id i}
              (((f : (a : (↑I : Type)) → E) x, (f : (a : (↑I : Type)) → E) y) : E × E)
Tactic: rw [Metric.uniformity_basis_dist.uniformContinuous_iff
      (basis_sets _).uniformity_of_nhds_zero_swapped] at this
Cleared hypotheses: this
-- 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
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1
have obtain : ∀ (δ : ℝ) (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),
  ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1
Tactic: obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0, ∀ x y : I, dist x y < δ → gauge U (f x - f y) < 1 / 2 := by
    have := CompactSpace.uniformContinuous_of_continuous (map_continuous f)
    rw [Metric.uniformity_basis_dist.uniformContinuous_iff
      (basis_sets _).uniformity_of_nhds_zero_swapped] at this
    exact this {z | gauge U z < 1 / 2} <| tendsto_gauge_nhds_zero hU₀
      |>.eventually_lt_const <| by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
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
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1
have nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
Tactic: have nhds_zero := tendsto_const_div_atTop_nhds_zero_nat (C / δ ^ 2)
-- 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 : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      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 : ∀ (n : ℕ) (nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2) (hn₀ : n ≠ 0) (x : (↑I : Type)),
  gauge U
      (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
        ((f : (a : (↑I : Type)) → E) x : E)) <
    1
Tactic: filter_upwards [nhds_zero.eventually_lt_const (half_pos one_pos), eventually_ne_atTop 0]
    with n nh hn₀ x
-- 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 < δ}
⊢ 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