awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ (x_1 : ℕ) (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
⊢ ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0
have neg : ∀ (zi : ℕ) (hzi : zi ≥ ti) (z : c zi = 0),
  ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0
Tactic: obtain ⟨zi, hzi, z⟩ := h ti
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ (x_1 : ℕ) (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
⊢ ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0
have neg : ∀ (n : ℕ) (hmn : zi ≤ n) (a : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0),
  Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) 0
Tactic: refine ⟨zi, Nat.le_induction (ofScalars_eq_zero_of_scalar_zero E z) fun n hmn a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ (x_1 : ℕ) (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) 0
have a₁ : Nontrivial E
Tactic: nontriviality E
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ (x_1 : ℕ) (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
h_1 : Nontrivial E
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) 0
have simp : ∀ (a : c n = 0), c (n + 1) = 0
Tactic: simp only [ofScalars_eq_zero] at a ⊢
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ (x_1 : ℕ) (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
n : ℕ
hmn : zi ≤ n
h_1 : Nontrivial E
a : c n = 0
⊢ c (n + 1) = 0
have contrapose! : ∀ (hti : c (n + 1) ≠ 0), ∃ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ = ∞
Tactic: contrapose! hti
Cleared hypotheses: hti
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = ∞
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have inr : ∀ (hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)),
  radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = 0
Tactic: simp_rw [hr, inv_top] at hc' ⊢
Cleared hypotheses: hc'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = 0
have apply : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c (n + 1).succ‖ / ‖c (n + 1)‖) atTop atTop
Tactic: apply ofScalars_radius_eq_zero_of_tendsto E c ((tendsto_add_atTop_iff_nat 1).mp ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c (n + 1).succ‖ / ‖c (n + 1)‖) atTop atTop
have refine : EventuallyEq (β := ℝ≥0∞) atTop (fun (n : ℕ) ↦ ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖)
  fun (x : ℕ) ↦ ENNReal.ofReal (‖c (x + 1).succ‖ / ‖c (x + 1)‖)
Tactic: refine tendsto_ofReal_nhds_top.mp (Tendsto.congr' ?_ ((tendsto_add_atTop_iff_nat 1).mpr hc'))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
⊢ EventuallyEq (β := ℝ≥0∞) atTop (fun (n : ℕ) ↦ ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖)
    fun (x : ℕ) ↦ ENNReal.ofReal (‖c (x + 1).succ‖ / ‖c (x + 1)‖)
have h : ∀ (n : ℕ) (hn : ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖ ≠ 0),
  ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖ = ENNReal.ofReal (‖c (n + 1).succ‖ / ‖c (n + 1)‖)
Tactic: filter_upwards [hc'.eventually_ne top_ne_zero] with n hn
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
n : ℕ
hn : ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖ ≠ 0
⊢ ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖ = ENNReal.ofReal (‖c (n + 1).succ‖ / ‖c (n + 1)‖)
have apply : ‖c (n + 1)‖ ≠ 0
Tactic: apply (ofReal_div_of_pos (Ne.lt_of_le (Ne.symm ?_) (norm_nonneg _))).symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have hr' : r ≠ 0 ∧ r ≠ ∞
Tactic: have hr' := toReal_ne_zero.mp hr.ne.symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
hr' : r ≠ 0 ∧ r ≠ ∞
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have hr'' : r.toNNReal ≠ 0
Tactic: have hr'' := toNNReal_ne_zero.mpr hr'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
hr' : r ≠ 0 ∧ r ≠ ∞
hr'' : r.toNNReal ≠ 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have h : r⁻¹ = (↑r.toNNReal⁻¹ : ℝ≥0∞)
Tactic: convert! ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
hr' : r ≠ 0 ∧ r ≠ ∞
hr'' : r.toNNReal ≠ 0
h : r⁻¹ = (↑r.toNNReal⁻¹ : ℝ≥0∞)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have inr : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r.toNNReal : ℝ))
Tactic: convert! ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
hr' : r ≠ 0 ∧ r ≠ ∞
hr'' : r.toNNReal ≠ 0
⊢ Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r.toReal)
have inr : (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun (n : ℕ) ↦
  ‖c n.succ‖ / ‖c n‖
Tactic: refine Tendsto.congr' ?_ <| (tendsto_toReal hr'.2).comp hc'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
hr' : r ≠ 0 ∧ r ≠ ∞
hr'' : r.toNNReal ≠ 0
⊢ (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun (n : ℕ) ↦
    ‖c n.succ‖ / ‖c n‖
have h : ∀ (a : ℕ),
  ENNReal.ofReal ‖c a.succ‖ / ENNReal.ofReal ‖c a‖ ≠ 0 →
    ENNReal.ofReal ‖c a.succ‖ / ENNReal.ofReal ‖c a‖ ≠ ∞ →
      (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) a = ‖c a.succ‖ / ‖c a‖
Tactic: filter_upwards [hc'.eventually_ne hr'.1, hc'.eventually_ne hr'.2]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf :
  Eq (α := ℕ∞)
    (if hf : AnalyticAt 𝕜 f z₀ then
      if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
      else
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞)
    else 0)
    ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
have pos : ∀ (h : AnalyticAt 𝕜 f z₀), (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) → ∀ (hf : Eq (α := ℕ∞) ⊤ ⊤), ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
Tactic: split_ifs at hf with h
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf :
  Eq (α := ℕ∞)
    (if hf : AnalyticAt 𝕜 f z₀ then
      if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
      else
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞)
    else 0)
    ⊤
pos : ∀ (h : AnalyticAt 𝕜 f z₀), (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) → ∀ (hf : Eq (α := ℕ∞) ⊤ ⊤), ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
have neg : ∀ (h : AnalyticAt 𝕜 f z₀) (h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0)
  (hf :
    Eq (α := ℕ∞)
      (↑(sorry.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞)
      ⊤),
  ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
Tactic: split_ifs at hf with h
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf :
  Eq (α := ℕ∞)
    (if hf : AnalyticAt 𝕜 f z₀ then
      if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
      else
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞)
    else 0)
    ⊤
pos : ∀ (h : AnalyticAt 𝕜 f z₀), (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) → ∀ (hf : Eq (α := ℕ∞) ⊤ ⊤), ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
neg :
  ∀ (h : AnalyticAt 𝕜 f z₀) (h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0)
    (hf :
      Eq (α := ℕ∞)
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞)
        ⊤),
    ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
have neg₁ : ∀ (h : ¬AnalyticAt 𝕜 f z₀) (hf : Eq (α := ℕ∞) 0 ⊤), ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
Tactic: split_ifs at hf with h
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ Eq (α := ℕ∞)
      (if hf : AnalyticAt 𝕜 f z₀ then
        if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
        else
          (↑(⋯.choose (p := fun (n : ℕ) ↦
                ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
            ℕ∞)
      else 0)
      (↑n : ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
have pos : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0),
  Eq (α := ℕ∞) ⊤ (↑n : ℕ∞) ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
pos :
  ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0),
    Eq (α := ℕ∞) ⊤ (↑n : ℕ∞) ↔
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ Eq (α := ℕ∞)
      (if hf : AnalyticAt 𝕜 f z₀ then
        if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
        else
          (↑(⋯.choose (p := fun (n : ℕ) ↦
                ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
            ℕ∞)
      else 0)
      (↑n : ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
have neg : ∀ (h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0),
  Eq (α := ℕ∞)
      (↑(sorry.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞)
      (↑n : ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ Eq (α := ℕ∞) ⊤ (↑n : ℕ∞) ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
have pos : ¬∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Tactic: simp only [ENat.top_ne_coe, false_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ¬∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
have pos : ∀ (h : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z),
  ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
have pos : ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Tactic: rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ Eq (α := ℕ∞)
      (↑(⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞)
      (↑n : ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
have h₁ : ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Tactic: rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff] at h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
h : ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ Eq (α := ℕ∞)
      (↑(⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞)
      (↑n : ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
have neg : ∀ (h' : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z),
  Eq (α := ℕ∞)
    (↑(sorry.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
      ℕ∞)
    (↑n : ℕ∞)
Tactic: refine ⟨fun hn ↦ (WithTop.coe_inj.mp hn : h.choose = n) ▸ h.choose_spec, fun h' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
h : ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h' : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ Eq (α := ℕ∞)
    (↑(⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
      ℕ∞)
    (↑n : ℕ∞)
have neg : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
Tactic: rw [AnalyticAt.unique_eventuallyEq_pow_smul_nonzero h.choose_spec h']
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
have pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
Tactic: by_cases hf : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
⊢ analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
have neg : ∀ (hf : ¬AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
Tactic: by_cases hf : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
have pos : (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z) ↔
  ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
Tactic: rw [← ENat.coe_zero, hf.analyticOrderAt_eq_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z) ↔
    ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
have pos : (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z) →
  ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
pos :
  (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z) →
    ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
⊢ (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z) ↔
    ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
have pos₁ : ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0 →
  ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
⊢ f z₀ = 0
have pos : ∀ (hf' : AnalyticAt 𝕜 f z₀), f z₀ = 0
Tactic: by_cases hf' : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
pos : ∀ (hf' : AnalyticAt 𝕜 f z₀), f z₀ = 0
⊢ f z₀ = 0
have neg : ∀ (hf' : ¬AnalyticAt 𝕜 f z₀), f z₀ = 0
Tactic: by_cases hf' : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
⊢ f z₀ = 0
have pos : ∀ (hf' : AnalyticAt 𝕜 f z₀), f z₀ = 0
Tactic: by_cases hf' : AnalyticAt 𝕜 f z₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
pos : ∀ (hf' : AnalyticAt 𝕜 f z₀), f z₀ = 0
⊢ f z₀ = 0
have neg : ∀ (hf' : ¬AnalyticAt 𝕜 f z₀), f z₀ = 0
Tactic: by_cases hf' : AnalyticAt 𝕜 f z₀