awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
⊢ 0 < ‖z‖₊

Tactic:
zero_lt_iff.mpr (nnnorm_ne_zero_iff.mpr (norm_pos_iff.mp z_pos))

Premises used: Iff.mpr, norm_pos_iff, nnnorm_ne_zero_iff, Iff.mp, zero_lt_iff
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
⊢ 0 < ‖z‖₊

Tactic:
exact zero_lt_iff.mpr (nnnorm_ne_zero_iff.mpr (norm_pos_iff.mp z_pos))

Premises used: Iff.mpr, norm_pos_iff, nnnorm_ne_zero_iff, Iff.mp, zero_lt_iff
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
refine_2 :
  ∀ (h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))) {y : 𝕜},
    edist y 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p →
      nndist y 0 < r.toNNReal → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
⊢ ∀ {y : 𝕜},
    Membership.mem (γ := Set 𝕜)
        (Metric.eball 0 (min (radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p) (↑r.toNNReal : ℝ≥0∞))) y →
      HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ y) (f (z₀ + y))

Tactic:
simp only [Metric.mem_eball, lt_inf_iff, edist_lt_coe, apply_eq_pow_smul_coeff, and_imp,
      dist_zero_right] at h ⊢

Premises used: lt_inf_iff, and_imp, FormalMultilinearSeries.apply_eq_pow_smul_coeff, edist_lt_coe, dist_zero_right, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
⊢ ∀ {y : 𝕜},
    edist y 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p →
      nndist y 0 < r.toNNReal → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))

Tactic:
fun {y} _ hyr => h ?_
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
refine_2 :
  ∀ {y : 𝕜},
    edist y 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p → ∀ (hyr : nndist y 0 < r.toNNReal), ‖y‖ < r
⊢ ∀ {y : 𝕜},
    edist y 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p →
      nndist y 0 < r.toNNReal → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))

Tactic:
refine fun {y} _ hyr => h ?_
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
y : 𝕜
h_1 : edist y 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
hyr : nndist y 0 < r.toNNReal
⊢ ‖y‖ < r

Tactic:
simpa [nndist_eq_nnnorm, Real.lt_toNNReal_iff_coe_lt] using hyr

Premises used: nndist_eq_nnnorm, Real.lt_toNNReal_iff_coe_lt
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
rw :
  (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))) ↔
    ∀ᶠ (a : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ (z₀ + a - z₀) ^ n • p.coeff n) (f (z₀ + a))
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun (n : ℕ) ↦ (z - z₀) ^ n • p.coeff n) (f z)

Tactic:
rw [← map_add_left_nhds_zero, eventually_map, hasFPowerSeriesAt_iff]

Premises used: Filter.eventually_map, hasFPowerSeriesAt_iff, map_add_left_nhds_zero
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))) ↔
    ∀ᶠ (a : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ (z₀ + a - z₀) ^ n • p.coeff n) (f (z₀ + a))

Tactic:
simp_rw [add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
n : ℕ
⊢ (↑(Ring.choose a n) : ℂ) = Ring.choose (↑a : ℂ) n

Tactic:
Ring.map_choose (algebraMap ℝ ℂ) _ _

Premises used: Real, Algebra.algebraMap, Ring.choose, Ring.multichoose, Complex, Ring.map_choose
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a : 𝕂
n : ℕ
v : Fin n → 𝔸
⊢ (binomialSeries 𝔸 a n : (a : (i : Fin n) → 𝔸) → 𝔸) v = Ring.choose a n • (List.ofFn v).prod

Tactic:
simp [binomialSeries, FormalMultilinearSeries.ofScalars]

Premises used: binomialSeries, FormalMultilinearSeries.ofScalars
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), (↑k : 𝕂) ≠ -b
simp :
  Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (FormalMultilinearSeries.ofScalars 𝔸 fun (x : ℕ) ↦ Ring.choose a x : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (FormalMultilinearSeries.ofScalars 𝔸 fun (k : ℕ) ↦
        HPow.hPow (α := 𝕂) (-1) k * ordinaryHypergeometricCoefficient (-a) b b k :
      FormalMultilinearSeries 𝕂 𝔸 𝔸)
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸) (binomialSeries 𝔸 a : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (FormalMultilinearSeries.compContinuousLinearMap
        (ordinaryHypergeometricSeries 𝔸 (-a) b b : FormalMultilinearSeries 𝕂 𝔸 𝔸) (-ContinuousLinearMap.id 𝕂 𝔸) :
      FormalMultilinearSeries 𝕂 𝔸 𝔸)

Tactic:
simp only [binomialSeries, ordinaryHypergeometricSeries,
    FormalMultilinearSeries.ofScalars_comp_neg_id]

Premises used: binomialSeries, FormalMultilinearSeries.ofScalars_comp_neg_id, ordinaryHypergeometricSeries
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), (↑k : 𝕂) ≠ -b
h₁ : ∀ (n : ℕ), Ring.choose a n = HPow.hPow (α := 𝕂) (-1) n * ordinaryHypergeometricCoefficient (-a) b b n
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (FormalMultilinearSeries.ofScalars 𝔸 fun (x : ℕ) ↦ Ring.choose a x : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (FormalMultilinearSeries.ofScalars 𝔸 fun (k : ℕ) ↦
        HPow.hPow (α := 𝕂) (-1) k * ordinaryHypergeometricCoefficient (-a) b b k :
      FormalMultilinearSeries 𝕂 𝔸 𝔸)

Tactic:
congr! with n
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), (↑k : 𝕂) ≠ -b
n : ℕ
simp : ∀ x < n, ¬(↑x : 𝕂) = -b
⊢ Polynomial.eval b (ascPochhammer 𝕂 n) ≠ 0

Tactic:
simp [ascPochhammer_eval_eq_zero_iff]

Premises used: ascPochhammer_eval_eq_zero_iff
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), (↑k : 𝕂) ≠ -b
n : ℕ
⊢ ∀ x < n, ¬(↑x : 𝕂) = -b

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), (↑k : 𝕂) ≠ -b
n : ℕ
h₁ : Ring.choose a n = HPow.hPow (α := 𝕂) (-1) n * ((↑n ! : 𝕂)⁻¹ * Polynomial.eval (-a) (ascPochhammer 𝕂 n))
⊢ Ring.choose a n = HPow.hPow (α := 𝕂) (-1) n * ordinaryHypergeometricCoefficient (-a) b b n

Tactic:
rw [ordinaryHypergeometricCoefficient,
    mul_inv_cancel_right₀ (by simp [ascPochhammer_eval_eq_zero_iff]; grind)]

Premises used: mul_inv_cancel_right₀, ordinaryHypergeometricCoefficient
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), (↑k : 𝕂) ≠ -b
n : ℕ
h₁ :
  HSMul.hSMul (α := 𝕂) (↑n ! : 𝕂)⁻¹ (Polynomial.eval (a - (↑n : 𝕂) + 1) (ascPochhammer 𝕂 n)) =
    HPow.hPow (α := 𝕂) (-1) n *
      ((↑n ! : 𝕂)⁻¹ * (HPow.hPow (α := 𝕂) (-1) n * Polynomial.eval (a - (↑n : 𝕂) + 1) (ascPochhammer 𝕂 n)))
⊢ Ring.choose a n = HPow.hPow (α := 𝕂) (-1) n * ((↑n ! : 𝕂)⁻¹ * Polynomial.eval (-a) (ascPochhammer 𝕂 n))

Tactic:
simp only [Ring.choose_eq_smul, Polynomial.descPochhammer_smeval_eq_ascPochhammer,
    Polynomial.ascPochhammer_smeval_cast, Polynomial.ascPochhammer_smeval_eq_eval,
    ascPochhammer_eval_neg_eq_descPochhammer, descPochhammer_eval_eq_ascPochhammer]

Premises used: Ring.choose_eq_smul, Polynomial.ascPochhammer_smeval_cast, descPochhammer_eval_eq_ascPochhammer, Polynomial.ascPochhammer_smeval_eq_eval, Polynomial.descPochhammer_smeval_eq_ascPochhammer, ascPochhammer_eval_neg_eq_descPochhammer
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), (↑k : 𝕂) ≠ -b
n : ℕ
h₁ :
  Polynomial.eval (1 + a - (↑n : 𝕂)) (ascPochhammer 𝕂 n) * (↑n ! : 𝕂)⁻¹ =
    Polynomial.eval (1 + a - (↑n : 𝕂)) (ascPochhammer 𝕂 n) * (↑n ! : 𝕂)⁻¹ * HPow.hPow (α := 𝕂) (-1) (n * 2)
⊢ HSMul.hSMul (α := 𝕂) (↑n ! : 𝕂)⁻¹ (Polynomial.eval (a - (↑n : 𝕂) + 1) (ascPochhammer 𝕂 n)) =
    HPow.hPow (α := 𝕂) (-1) n *
      ((↑n ! : 𝕂)⁻¹ * (HPow.hPow (α := 𝕂) (-1) n * Polynomial.eval (a - (↑n : 𝕂) + 1) (ascPochhammer 𝕂 n)))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u
inst : Field 𝕂
inst_1 : CharZero 𝕂
𝔸 : Type v
inst_2 : Ring 𝔸
inst_3 : Algebra 𝕂 𝔸
inst_4 : TopologicalSpace 𝔸
inst_5 : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), (↑k : 𝕂) ≠ -b
n : ℕ
⊢ Polynomial.eval (1 + a - (↑n : 𝕂)) (ascPochhammer 𝕂 n) * (↑n ! : 𝕂)⁻¹ =
    Polynomial.eval (1 + a - (↑n : 𝕂)) (ascPochhammer 𝕂 n) * (↑n ! : 𝕂)⁻¹ * HPow.hPow (α := 𝕂) (-1) (n * 2)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : ℕ
norm_cast : ∀ (k : ℕ), ¬False
⊢ ∀ (k : ℕ), Ne.{v + 1} (α := 𝕂) (↑k : 𝕂) (-1)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : ℕ
⊢ ∀ (k : ℕ), ¬False

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : ℕ
⊢ FormalMultilinearSeries.radius.{v, u, u} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 (↑a : 𝕂)) = ⊤

Tactic:
simp [binomialSeries_eq_ordinaryHypergeometricSeries (b := (1 : 𝕂)) (by norm_cast; simp),
    ordinaryHypergeometric_radius_top_of_neg_nat₁]

Premises used: binomialSeries_eq_ordinaryHypergeometricSeries, ordinaryHypergeometric_radius_top_of_neg_nat₁
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
norm_cast : ∀ (k : ℕ), ¬False
⊢ ∀ (k : ℕ), Ne.{v + 1} (α := 𝕂) (↑k : 𝕂) (-1)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
⊢ ∀ (k : ℕ), ¬False

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
simp : FormalMultilinearSeries.radius.{v, u, u} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-a) 1 1) = 1
⊢ FormalMultilinearSeries.radius.{v, u, u} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a) = 1

Tactic:
simp only [binomialSeries_eq_ordinaryHypergeometricSeries (b := (1 : 𝕂)) (by norm_cast; simp),
    FormalMultilinearSeries.radius_compNeg]

Premises used: binomialSeries_eq_ordinaryHypergeometricSeries, FormalMultilinearSeries.radius_compNeg
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
ext : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
| ∀ (k : ℕ), a ≠ (↑k : 𝕂)

Tactic:
ext
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
k : ℕ
rw : (↑k : 𝕂) ≠ a
| a ≠ (↑k : 𝕂)

Tactic:
rw [ne_comm]

Premises used: ne_comm
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
rw : ∀ (k : ℕ), (↑k : 𝕂) ≠ a
| ∀ (k : ℕ), a ≠ (↑k : 𝕂)

Tactic:
ext; rw [ne_comm]

Premises used: ne_comm
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
⊢ ∀ (k : ℕ), (↑k : 𝕂) ≠ a

Tactic:
conv at ha => ext; rw [ne_comm]

Premises used: ne_comm
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), (↑k : 𝕂) ≠ a
norm_cast : ∀ (kn : ℕ), ¬(↑kn : 𝕂) = - -a ∧ ¬False ∧ ¬False
⊢ ∀ (kn : ℕ), (↑kn : 𝕂) ≠ - -a ∧ Ne.{v + 1} (α := 𝕂) (↑kn : 𝕂) (-1) ∧ Ne.{v + 1} (α := 𝕂) (↑kn : 𝕂) (-1)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), (↑k : 𝕂) ≠ a
⊢ ∀ (kn : ℕ), ¬(↑kn : 𝕂) = - -a ∧ ¬False ∧ ¬False

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), (↑k : 𝕂) ≠ a
⊢ FormalMultilinearSeries.radius.{v, u, u} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-a) 1 1) = 1

Tactic:
exact ordinaryHypergeometricSeries_radius_eq_one _ _ _ _ (by norm_cast; grind)

Premises used: ordinaryHypergeometricSeries_radius_eq_one
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
pos :
  ∀ (ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)),
    1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
neg :
  ∀ (ha : ¬∀ (k : ℕ), a ≠ (↑k : 𝕂)),
    1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)

Tactic:
by_cases ha : ∀ (k : ℕ), a ≠ k
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
pos pos₁ : LE.le (α := ENNReal) 1 1
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)

Tactic:
rw [binomialSeries_radius_eq_one ha]

Premises used: binomialSeries_radius_eq_one
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ¬∀ (k : ℕ), a ≠ (↑k : 𝕂)
⊢ ∃ (k : ℕ), a = (↑k : 𝕂)

Tactic:
push Not at ha

Premises used: Not
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∃ (k : ℕ), a = (↑k : 𝕂)
neg :
  ∀ (k : ℕ), 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 (↑k : 𝕂))
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)

Tactic:
rcases ha with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
k : ℕ
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 (↑k : 𝕂))

Tactic:
simp [binomialSeries_radius_eq_top_of_nat]

Premises used: binomialSeries_radius_eq_top_of_nat
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ (1 + x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
      HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ))
    0 1

Tactic:
AnalyticOn.hasFPowerSeriesOnSubball _ _ _

Premises used: AnalyticOn.hasFPowerSeriesOnSubball
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
convert_6 : LT.lt (α := ENNReal) 0 1
convert_7 : AnalyticOn ℂ (F := ℂ) (fun (x : ℂ) ↦ (1 + x) ^ a) (Metric.eball 0 1)
convert_8 :
  1 ≤
    FormalMultilinearSeries.radius (𝕜 := ℂ) (E := ℂ) (F := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ))
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0 1

Tactic:
convert! AnalyticOn.hasFPowerSeriesOnSubball _ _ _

Premises used: AnalyticOn.hasFPowerSeriesOnSubball
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
⊢ LT.lt (α := ENNReal) 0 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
convert_7 :
  ∀ (z : ℂ),
    Membership.mem (γ := Set ℂ) (Metric.eball 0 1) z →
      HAdd.hAdd (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (x : ℂ) ↦ 1) (fun (x : ℂ) ↦ x) z ∈ slitPlane
⊢ AnalyticOn ℂ (F := ℂ) (fun (x : ℂ) ↦ (1 + x) ^ a) (Metric.eball 0 1)

Tactic:
apply AnalyticOn.cpow (analyticOn_const.add analyticOn_id) analyticOn_const

Premises used: AnalyticOn.cpow, analyticOn_id, AnalyticOn.add, analyticOn_const
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.eball 0 1) z
convert_7 : norm (E := ℂ) ((fun (x : ℂ) ↦ x) z) < 1
⊢ HAdd.hAdd (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (x : ℂ) ↦ 1) (fun (x : ℂ) ↦ x) z ∈ slitPlane

Tactic:
apply Complex.mem_slitPlane_of_norm_lt_one

Premises used: Complex.mem_slitPlane_of_norm_lt_one
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.eball 0 1) z
⊢ Membership.mem (γ := Set ℂ) (Metric.ball 0 1) z

Tactic:
rw [← ENNReal.ofReal_one, Metric.eball_ofReal] at hz

Premises used: Metric.eball_ofReal, ENNReal.ofReal_one
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) z
⊢ norm (E := ℂ) ((fun (x : ℂ) ↦ x) z) < 1

Tactic:
simpa using hz
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
convert_8 : 1 ≤ FormalMultilinearSeries.radius (binomialSeries ℂ a)
⊢ 1 ≤
    FormalMultilinearSeries.radius (𝕜 := ℂ) (E := ℂ) (F := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ))

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
⊢ 1 ≤ FormalMultilinearSeries.radius (binomialSeries ℂ a)

Tactic:
binomialSeries_radius_ge_one

Premises used: binomialSeries_radius_ge_one
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
⊢ 1 ≤ FormalMultilinearSeries.radius (binomialSeries ℂ a)

Tactic:
exact binomialSeries_radius_ge_one

Premises used: binomialSeries_radius_ge_one
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
suffices :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0 1

Tactic:
suffices (binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ
      fun n ↦ iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0 / n !) by
    convert! AnalyticOn.hasFPowerSeriesOnSubball _ _ _
    · norm_num
    · -- TODO: use `fun_prop` for this subgoal
      apply AnalyticOn.cpow (analyticOn_const.add analyticOn_id) analyticOn_const
      intro z hz
      apply Complex.mem_slitPlane_of_norm_lt_one
      rw [← ENNReal.ofReal_one, Metric.eball_ofReal] at hz
      simpa using hz
    · rw [← this]
      exact binomialSeries_radius_ge_one