awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ 0 < x

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 0) x
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 0) x
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 0) x
rw : x < 0
⊢ artanh x < 0

Tactic:
rw [← artanh_zero, artanh_lt_artanh_iff (by grind) (by grind)]

Premises used: Real.artanh_zero, Real.artanh_lt_artanh_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 0) x
⊢ x < 0

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 0) x
⊢ x < 0

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
by_cases : x < 1 → 0 ≤ artanh x
by_cases₁ : ¬x < 1 → 0 ≤ artanh x
⊢ 0 ≤ artanh x

Tactic:
by_cases x < 1
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
h : x < 1
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
h : x < 1
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
h : x < 1
rw : 0 ≤ x
⊢ 0 ≤ artanh x

Tactic:
rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]

Premises used: Real.artanh_zero, Real.artanh_le_artanh_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
h : x < 1
⊢ 0 ≤ x

Tactic:
hx
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
h : x < 1
⊢ 0 ≤ x

Tactic:
exact hx
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
h : x < 1
⊢ 0 ≤ artanh x

Tactic:
case pos =>
    rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]
    exact hx

Premises used: Real.artanh_zero, Real.artanh_le_artanh_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
h : ¬x < 1
⊢ 0 ≤ artanh x

Tactic:
grind [artanh_eq_zero_iff]

Premises used: Real.artanh_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : 0 ≤ x
h : ¬x < 1
⊢ 0 ≤ artanh x

Tactic:
case neg => grind [artanh_eq_zero_iff]

Premises used: Real.artanh_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
by_cases : -1 < x → artanh x ≤ 0
by_cases₁ : ¬-1 < x → artanh x ≤ 0
⊢ artanh x ≤ 0

Tactic:
by_cases -1 < x
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
h : -1 < x
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
h : -1 < x
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
h : -1 < x
rw : x ≤ 0
⊢ artanh x ≤ 0

Tactic:
rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]

Premises used: Real.artanh_zero, Real.artanh_le_artanh_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
h : -1 < x
⊢ x ≤ 0

Tactic:
hx
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
h : -1 < x
⊢ x ≤ 0

Tactic:
exact hx
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
h : -1 < x
⊢ artanh x ≤ 0

Tactic:
case pos =>
    rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]
    exact hx

Premises used: Real.artanh_zero, Real.artanh_le_artanh_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
h : ¬-1 < x
⊢ artanh x ≤ 0

Tactic:
grind [artanh_eq_zero_iff]

Premises used: Real.artanh_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : x ≤ 0
h : ¬-1 < x
⊢ artanh x ≤ 0

Tactic:
case neg => grind [artanh_eq_zero_iff]

Premises used: Real.artanh_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
⊢ BijOn tanh univ (Ioo (-1) 1)

Tactic:
tanhPartialEquiv.bijOn

Premises used: Real.tanh, Set.univ, setOf, PartialEquiv.bijOn, Real.tanhPartialEquiv, Set.Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
⊢ Injective tanh

Tactic:
fun _ _ ↦ tanhPartialEquiv.injOn trivial trivial

Premises used: trivial, Real.tanh, PartialEquiv.injOn, Real.tanhPartialEquiv, Function.Injective
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
⊢ SurjOn tanh univ (Ioo (-1) 1)

Tactic:
tanhPartialEquiv.surjOn

Premises used: Real.tanh, Set.univ, setOf, Real.tanhPartialEquiv, PartialEquiv.surjOn, Set.Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
⊢ BijOn artanh (Ioo (-1) 1) univ

Tactic:
tanhPartialEquiv.symm.bijOn

Premises used: Set.univ, setOf, PartialEquiv.bijOn, PartialEquiv.symm, Real.log, dite, Real.tanhPartialEquiv, Real.artanh, Set.Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
⊢ InjOn artanh (Ioo (-1) 1)

Tactic:
tanhPartialEquiv.symm.injOn

Premises used: PartialEquiv.injOn, setOf, PartialEquiv.symm, Real.log, dite, Real.tanhPartialEquiv, Real.artanh, Set.Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
⊢ SurjOn artanh (Ioo (-1) 1) univ

Tactic:
tanhPartialEquiv.symm.surjOn

Premises used: Set.univ, setOf, PartialEquiv.symm, Real.log, dite, Real.tanhPartialEquiv, Real.artanh, PartialEquiv.surjOn, Set.Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n ν : ℕ
x : (↑I : Type)
⊢ Polynomial.eval (↑x : ℝ)
      ((↑(n.choose ν) : Polynomial ℝ) * HPow.hPow (α := Polynomial ℝ) Polynomial.X ν *
        HSub.hSub (α := Polynomial ℝ) 1 Polynomial.X ^ (n - ν)) =
    (↑(n.choose ν) : ℝ) * (↑x : ℝ) ^ ν * (1 - (↑x : ℝ)) ^ (n - ν)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n ν : ℕ
x : (↑I : Type)
simp : 0 ≤ (↑(n.choose ν) : ℝ) * (↑x : ℝ) ^ ν * (1 - (↑x : ℝ)) ^ (n - ν)
⊢ LE.le (α := ℝ) (0 : ℝ) ((bernstein n ν : (a : (↑I : Type)) → ℝ) x : ℝ)

Tactic:
simp only [bernstein_apply]

Premises used: bernstein_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n ν : ℕ
x : (↑I : Type)
⊢ 0 ≤ (↑x : ℝ)

Tactic:
unit_interval
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n ν : ℕ
x : (↑I : Type)
⊢ 0 ≤ (↑x : ℝ)

Tactic:
have h₁ : (0 : ℝ) ≤ x := by unit_interval
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n ν : ℕ
x : (↑I : Type)
h₁ : 0 ≤ (↑x : ℝ)
⊢ 0 ≤ 1 - (↑x : ℝ)

Tactic:
unit_interval
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n ν : ℕ
x : (↑I : Type)
h₁ : 0 ≤ (↑x : ℝ)
⊢ 0 ≤ 1 - (↑x : ℝ)

Tactic:
have h₂ : (0 : ℝ) ≤ 1 - x := by unit_interval
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n ν : ℕ
x : (↑I : Type)
h₁ : 0 ≤ (↑x : ℝ)
h₂ : 0 ≤ 1 - (↑x : ℝ)
⊢ 0 ≤ (↑(n.choose ν) : ℝ) * (↑x : ℝ) ^ ν * (1 - (↑x : ℝ)) ^ (n - ν)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
k : Fin (n + 1)
⊢ HDiv.hDiv (α := ℝ) (↑(↑k : ℕ) : ℝ) (↑n : ℝ) ∈ I

Tactic:
simp [div_nonneg, div_le_one_of_le₀, k.is_le]

Premises used: div_le_one_of_le₀, Fin.is_le, div_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
⊢ z (n := n) 0 = 0

Tactic:
simp [z]

Premises used: bernstein.z
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
hn : n ≠ 0
⊢ Fin.last n/ₙ = 1

Tactic:
simp [z, hn]

Premises used: bernstein.z
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
x : (↑I : Type)
⊢ Eq (α := Polynomial ℝ) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) 1

Tactic:
have := bernsteinPolynomial.sum ℝ n
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
x : (↑I : Type)
this : Eq (α := Polynomial ℝ) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) 1
⊢ Eq (α := ℝ)
    ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) : ℝ)
    ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ) 1 : ℝ)

Tactic:
apply_fun fun p => Polynomial.aeval (x : ℝ) p at this

Premises used: Polynomial.aeval, Subtype.val, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
x : (↑I : Type)
this :
  Eq (α := ℝ)
    ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) : ℝ)
    ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ) 1 : ℝ)
⊢ Eq (α := ℝ) (∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x) 1

Tactic:
simpa [Finset.sum_range]

Premises used: Finset.sum_range
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
⊢ 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) =
    HDiv.hDiv (α := ℝ)
      ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ)
          (HSMul.hSMul (β := Polynomial ℝ) n Polynomial.X * HSub.hSub (α := Polynomial ℝ) 1 Polynomial.X) :
        ℝ)
      (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)

Tactic:
congr(Polynomial.aeval (x : ℝ) $(bernsteinPolynomial.variance ℝ n) / n ^ 2)

Premises used: Real, congrArg, id, HDiv.hDiv, bernsteinPolynomial.variance, Nat.cast, HPow.hPow, Polynomial.aeval, OfNat.ofNat, Subtype.val, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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)
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)
⊢ ∑ k : Fin (n + 1),
      HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑(k/ₙ) : ℝ)) 2)
        ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)

Tactic:
convert! congr(Polynomial.aeval (x : ℝ) $(bernsteinPolynomial.variance ℝ n) / n ^ 2) using 1
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
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
⊢ ∑ 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:
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]

Premises used: Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_natCast, bernstein_apply, Polynomial.eval_mul, map_sum, bernsteinPolynomial, Finset.sum_range, Polynomial.eval_one, nsmul_eq_mul, Polynomial.coe_aeval_eq_eval, Polynomial.eval_sub, bernstein.z
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
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 : ℕ))
⊢ ∑ 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:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
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 : ℕ))
⊢ 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:
rw [← Finset.sum_div]

Premises used: Finset.sum_div
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
⊢ 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:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
h : (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) = (↑n : ℝ) * (↑x : ℝ) * (1 - (↑x : ℝ)) / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
⊢ (↑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:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
n : ℕ
hn : n ≠ 0
x : (↑I : Type)
⊢ (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) = (↑n : ℝ) * (↑x : ℝ) * (1 - (↑x : ℝ)) / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
n : ℕ
f : C((↑I : Type), E)
x : (↑I : Type)
⊢ Eq (α := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
    (∑ k : Fin (n + 1),
        HSMul.hSMul (α := ℝ) (β := E) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
          ((f : (a : (↑I : Type)) → E) k/ₙ : E) :
      E)

Tactic:
simp [bernsteinApproximation]

Premises used: bernsteinApproximation
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
n : ℕ
f : C((↑I : Type), E)
⊢ Eq (α := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) 0 : E) ((f : (a : (↑I : Type)) → E) 0 : E)

Tactic:
simp [apply, Fin.sum_univ_succ, bernstein_apply, z]

Premises used: bernstein_apply, Fin.sum_univ_succ, bernsteinApproximation.apply, bernstein.z
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
n : ℕ
hn : n ≠ 0
f : C((↑I : Type), E)
⊢ Eq (α := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) 1 : E) ((f : (a : (↑I : Type)) → E) 1 : E)

Tactic:
simp [apply, Fin.sum_univ_castSucc, bernstein_apply, hn, Nat.sub_eq_zero_iff_le]

Premises used: Fin.sum_univ_castSucc, Nat.sub_eq_zero_iff_le, bernstein_apply, bernsteinApproximation.apply
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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
⊢ IsUniformAddGroup E

Tactic:
have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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
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)
⊢ Tendsto (fun (n : ℕ) ↦ bernsteinApproximation n f) atTop (𝓝 f)

Tactic:
rw [(LocallyConvexSpace.convex_basis_zero ℝ E).uniformity_of_nhds_zero_swapped
      |>.compactConvergenceUniformity_of_compact |> nhds_basis_uniformity |>.tendsto_right_iff]

Premises used: Real, LocallyConvexSpace.convex_basis_zero, Filter.HasBasis.compactConvergenceUniformity_of_compact, Filter.HasBasis.tendsto_right_iff, nhds_basis_uniformity, Filter.HasBasis.uniformity_of_nhds_zero_swapped
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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
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
⊢ ∀ᶠ (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)

Tactic:
filter_upwards [this U hU₀ hcU] with n hn x
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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
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:
gauge_lt_one_subset_self hcU (mem_of_mem_nhds hU₀) (absorbent_nhds_zero hU₀) (hn x)

Premises used: Set.Mem, absorbent_nhds_zero, mem_of_mem_nhds, gauge_lt_one_subset_self
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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
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:
exact gauge_lt_one_subset_self hcU (mem_of_mem_nhds hU₀) (absorbent_nhds_zero hU₀) (hn x)

Premises used: absorbent_nhds_zero, mem_of_mem_nhds, gauge_lt_one_subset_self