awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
g : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall f g x r
this : Metric.eball x r ∈ 𝓝 x
y : E
hy : y ∈ Metric.eball x r
⊢ ContinuousAt f y
have h : Metric.eball x r ∈ 𝓝 y
Tactic: apply hg.continuousOn.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
fa : AnalyticOnNhd 𝕜 f univ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
have rw : ContinuousOn f univ
Tactic: rw [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum (0 + y))
have rw : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst_5 : CompleteSpace F
⊢ ContinuousOn p.sum (Metric.eball 0 p.radius)
have inl : ∀ (h : p.radius = 0), ContinuousOn p.sum (Metric.eball 0 p.radius)
Tactic: rcases eq_zero_or_pos p.radius with h | h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst_5 : CompleteSpace F
inl : ∀ (h : p.radius = 0), ContinuousOn p.sum (Metric.eball 0 p.radius)
⊢ ContinuousOn p.sum (Metric.eball 0 p.radius)
have inr : ∀ (h : 0 < p.radius), ContinuousOn p.sum (Metric.eball 0 p.radius)
Tactic: rcases eq_zero_or_pos p.radius with h | h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
have refine : (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))) → HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
Tactic: refine ⟨fun ⟨r, _, r_pos, h⟩ =>
    eventually_of_mem (Metric.eball_mem_nhds 0 r_pos) fun _ => by simpa using h, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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))) → HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
have simp : (∃ ε > 0, ∀ ⦃y : 𝕜⦄, dist y 0 < ε → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))) →
  HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
Tactic: simp only [Metric.eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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))
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
have refine_1 : 0 < min (radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p) (↑r.toNNReal : ℝ≥0∞)
Tactic: refine ⟨p.radius ⊓ r.toNNReal, by simp, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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_1 : 0 < min (radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p) (↑r.toNNReal : ℝ≥0∞)
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
have refine_2 : ∀ {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: refine ⟨p.radius ⊓ r.toNNReal, by simp, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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))
⊢ 0 < min (radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p) (↑r.toNNReal : ℝ≥0∞)
have refine_1 : 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
Tactic: simp only [r_pos.lt, lt_inf_iff, ENNReal.coe_pos, Real.toNNReal_pos, and_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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))
⊢ 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
have refine_1 : ∀ (z : 𝕜) (z_pos : 0 < ‖z‖) (le_z : ‖z‖ < r), 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
Tactic: obtain ⟨z, z_pos, le_z⟩ := NormedField.exists_norm_lt 𝕜 r_pos.lt
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
have h₁ : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
Tactic: simp only [dist_zero_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
⊢ (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
have h₁ : Tendsto (fun (n : ℕ) ↦ ‖p n‖ * (↑‖z‖₊ : ℝ) ^ n) atTop (𝓝 (norm.{u_2} (E := E) 0))
Tactic: apply FormalMultilinearSeries.le_radius_of_tendsto
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
have this : (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
Tactic: have : (‖z‖₊ : ENNReal) ≤ p.radius := by
      simp only [dist_zero_right] at h
      apply FormalMultilinearSeries.le_radius_of_tendsto
      convert! tendsto_norm.comp (h le_z).summable.tendsto_atTop_zero
      simp [norm_smul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
have refine_1 : 0 < (↑‖z‖₊ : ℝ≥0∞)
Tactic: refine lt_of_lt_of_le ?_ this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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‖₊ : ℝ≥0∞)
have refine_1 : 0 < ‖z‖₊
Tactic: simp only [ENNReal.coe_pos]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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))
⊢ ∀ {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))
have 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))
Tactic: simp only [Metric.mem_eball, lt_inf_iff, edist_lt_coe, apply_eq_pow_smul_coeff, and_imp,
      dist_zero_right] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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))
have 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
Tactic: refine fun {y} _ hyr => h ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun (n : ℕ) ↦ (z - z₀) ^ n • p.coeff n) (f z)
have 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))
Tactic: rw [← map_add_left_nhds_zero, eventually_map, hasFPowerSeriesAt_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸) (binomialSeries 𝔸 a : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (FormalMultilinearSeries.compContinuousLinearMap
        (ordinaryHypergeometricSeries 𝔸 (-a) b b : FormalMultilinearSeries 𝕂 𝔸 𝔸) (-ContinuousLinearMap.id 𝕂 𝔸) :
      FormalMultilinearSeries 𝕂 𝔸 𝔸)
have 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 𝕂 𝔸 𝔸)
Tactic: simp only [binomialSeries, ordinaryHypergeometricSeries,
    FormalMultilinearSeries.ofScalars_comp_neg_id]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ 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 𝕂 𝔸 𝔸)
have h₁ : ∀ (n : ℕ), Ring.choose a n = HPow.hPow (α := 𝕂) (-1) n * ordinaryHypergeometricCoefficient (-a) b b n
Tactic: congr! with n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 b (ascPochhammer 𝕂 n) ≠ 0
have simp : ∀ x < n, ¬(↑x : 𝕂) = -b
Tactic: simp [ascPochhammer_eval_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 : ℕ
⊢ Ring.choose a n = HPow.hPow (α := 𝕂) (-1) n * ordinaryHypergeometricCoefficient (-a) b b n
have h₁ : Ring.choose a n = HPow.hPow (α := 𝕂) (-1) n * ((↑n ! : 𝕂)⁻¹ * Polynomial.eval (-a) (ascPochhammer 𝕂 n))
Tactic: rw [ordinaryHypergeometricCoefficient,
    mul_inv_cancel_right₀ (by simp [ascPochhammer_eval_eq_zero_iff]; grind)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 : ℕ
⊢ Ring.choose a n = HPow.hPow (α := 𝕂) (-1) n * ((↑n ! : 𝕂)⁻¹ * Polynomial.eval (-a) (ascPochhammer 𝕂 n))
have 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)))
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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 : ℕ
⊢ 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)))
have h₁ : Polynomial.eval (1 + a - (↑n : 𝕂)) (ascPochhammer 𝕂 n) * (↑n ! : 𝕂)⁻¹ =
  Polynomial.eval (1 + a - (↑n : 𝕂)) (ascPochhammer 𝕂 n) * (↑n ! : 𝕂)⁻¹ * HPow.hPow (α := 𝕂) (-1) (n * 2)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : ℕ
⊢ ∀ (k : ℕ), Ne.{v + 1} (α := 𝕂) (↑k : 𝕂) (-1)
have norm_cast : ∀ (k : ℕ), ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
⊢ ∀ (k : ℕ), Ne.{v + 1} (α := 𝕂) (↑k : 𝕂) (-1)
have norm_cast : ∀ (k : ℕ), ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
⊢ FormalMultilinearSeries.radius.{v, u, u} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a) = 1
have simp : FormalMultilinearSeries.radius.{v, u, u} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-a) 1 1) = 1
Tactic: simp only [binomialSeries_eq_ordinaryHypergeometricSeries (b := (1 : 𝕂)) (by norm_cast; simp),
    FormalMultilinearSeries.radius_compNeg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
| ∀ (k : ℕ), a ≠ (↑k : 𝕂)
have ext : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
k : ℕ
| a ≠ (↑k : 𝕂)
have rw : (↑k : 𝕂) ≠ a
Tactic: rw [ne_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
| ∀ (k : ℕ), a ≠ (↑k : 𝕂)
have rw : ∀ (k : ℕ), (↑k : 𝕂) ≠ a
Tactic: ext; rw [ne_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
⊢ FormalMultilinearSeries.radius.{v, u, u} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (ordinaryHypergeometricSeries 𝔸 (-a) 1 1) = 1
have ha₁ : ∀ (k : ℕ), (↑k : 𝕂) ≠ a
Tactic: conv at ha => ext; rw [ne_comm]
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type v
inst : RCLike 𝕂
𝔸 : Type u
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), (↑k : 𝕂) ≠ a
⊢ ∀ (kn : ℕ), (↑kn : 𝕂) ≠ - -a ∧ Ne.{v + 1} (α := 𝕂) (↑kn : 𝕂) (-1) ∧ Ne.{v + 1} (α := 𝕂) (↑kn : 𝕂) (-1)
have norm_cast : ∀ (kn : ℕ), ¬(↑kn : 𝕂) = - -a ∧ ¬False ∧ ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
have pos : ∀ (ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)),
  1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
Tactic: by_cases ha : ∀ (k : ℕ), a ≠ k
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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)
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
have neg : ∀ (ha : ¬∀ (k : ℕ), a ≠ (↑k : 𝕂)),
  1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
Tactic: by_cases ha : ∀ (k : ℕ), a ≠ k
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ (↑k : 𝕂)
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
have pos : LE.le (α := ENNReal) 1 1
Tactic: rw [binomialSeries_radius_eq_one ha]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ¬∀ (k : ℕ), a ≠ (↑k : 𝕂)
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
have ha₁ : ∃ (k : ℕ), a = (↑k : 𝕂)
Tactic: push Not at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
𝔸 : Type u_2
inst_1 : NormedDivisionRing 𝔸
inst_2 : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∃ (k : ℕ), a = (↑k : 𝕂)
⊢ 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 a)
have neg : ∀ (k : ℕ), 1 ≤ FormalMultilinearSeries.radius.{u_1, u_2, u_2} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (binomialSeries 𝔸 (↑k : 𝕂))
Tactic: rcases ha with ⟨k, rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 (fun (x : ℂ) ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0 1
have convert_6 : LT.lt (α := ENNReal) 0 1
Tactic: convert! AnalyticOn.hasFPowerSeriesOnSubball _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0 1
have convert_7 : AnalyticOn ℂ (F := ℂ) (fun (x : ℂ) ↦ (1 + x) ^ a) (Metric.eball 0 1)
Tactic: convert! AnalyticOn.hasFPowerSeriesOnSubball _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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)
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0 1
have convert_8 : 1 ≤
  FormalMultilinearSeries.radius (𝕜 := ℂ) (E := ℂ) (F := ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
      HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ))
Tactic: convert! AnalyticOn.hasFPowerSeriesOnSubball _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
⊢ AnalyticOn ℂ (F := ℂ) (fun (x : ℂ) ↦ (1 + x) ^ a) (Metric.eball 0 1)
have convert_7 : ∀ (z : ℂ),
  Membership.mem (γ := Set ℂ) (Metric.eball 0 1) z →
    HAdd.hAdd (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (x : ℂ) ↦ 1) (fun (x : ℂ) ↦ x) z ∈ slitPlane
Tactic: apply AnalyticOn.cpow (analyticOn_const.add analyticOn_id) analyticOn_const
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ HAdd.hAdd (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (x : ℂ) ↦ 1) (fun (x : ℂ) ↦ x) z ∈ slitPlane
have convert_7 : norm (E := ℂ) ((fun (x : ℂ) ↦ x) z) < 1
Tactic: apply Complex.mem_slitPlane_of_norm_lt_one