awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ ∃ (g_1 : 𝕜 → E),
    AnalyticAt 𝕜 g_1 z₀ ∧
      g_1 z₀ ≠ 0 ∧
        ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • g_1 z
have neg : (f' • g') z₀ ≠ 0
Tactic: refine ⟨f' • g', h₁f'.smul h₁g', ?_, ?_⟩
-- 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
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
neg : (f' • g') z₀ ≠ 0
⊢ ∃ (g_1 : 𝕜 → E),
    AnalyticAt 𝕜 g_1 z₀ ∧
      g_1 z₀ ≠ 0 ∧
        ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • g_1 z
have neg₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') z
Tactic: refine ⟨f' • g', h₁f'.smul h₁g', ?_, ?_⟩
-- 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
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ (f' • g') z₀ ≠ 0
have neg : ¬f' z₀ = 0 ∧ ¬g' z₀ = 0
Tactic: simp
-- 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
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ ¬f' z₀ = 0 ∧ ¬g' z₀ = 0
have neg : ¬f' z₀ = 0
Tactic: tauto
-- 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
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
neg : ¬f' z₀ = 0
⊢ ¬f' z₀ = 0 ∧ ¬g' z₀ = 0
have neg₁ : ¬g' z₀ = 0
Tactic: tauto
-- 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
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') z
have neg : ∀ (t : Set 𝕜) (h₁t : ∀ y ∈ t, f y = (fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z) y)
  (h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) (h₃t : z₀ ∈ t),
  ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') z
Tactic: obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃f'
-- 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
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = (fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z) y
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') z
have neg : ∀ (s : Set 𝕜) (h₁s : ∀ y ∈ s, g y = (fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z) y)
  (h₂s : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) (h₃s : z₀ ∈ s),
  ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') z
Tactic: obtain ⟨s, h₁s, h₂s, h₃s⟩ := eventually_nhds_iff.1 h₃g'
-- 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
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = (fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z) y
h₂t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h₃t : z₀ ∈ t
s : Set 𝕜
h₁s : ∀ y ∈ s, g y = (fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z) y
h₂s : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h₃s : z₀ ∈ s
y : 𝕜
hy : y ∈ t ∩ s
⊢ (f • g) y = (y - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') y
have simp : ((y - z₀) ^ analyticOrderNatAt f z₀ * f' y) • (y - z₀) ^ analyticOrderNatAt g z₀ • g' y =
  (y - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • f' y • g' y
Tactic: simp [h₁t y hy.1, h₁s y hy.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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
⊢ analyticOrderAt (deriv f) x + 1 = analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x
have generalize : ∀ (r : ℕ∞) (h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = r),
  analyticOrderAt (deriv f) x + 1 = r
Tactic: generalize h : analyticOrderAt (f · - f x) x = r
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = ⊤
⊢ analyticOrderAt (deriv f) x + 1 = ⊤
have top : analyticOrderAt (deriv f) x = ⊤
Tactic: suffices analyticOrderAt (deriv f) x = ⊤ by simp_all
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = ⊤
⊢ analyticOrderAt (deriv f) x = ⊤
have top : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x), ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0
Tactic: simp only [analyticOrderAt_eq_top, sub_eq_zero] at 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0
have top : ∀ (U : Set 𝕜) (hUf : ∀ y ∈ U, f y = f x) (hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
  (hUx : x ∈ U), ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0
Tactic: obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = f x
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0
have h₁ : ∀ (y : 𝕜) (hy : y ∈ U), deriv f y = 0
Tactic: filter_upwards [hUo.mem_nhds hUx] with y hy
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
hr : r = 0
⊢ False
have h₁ : f x - f x ≠ 0
Tactic: rw [hr, ENat.coe_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h
Cleared hypotheses: h, hr
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
⊢ analyticOrderAt (deriv f) x + 1 = (↑r : ℕ∞)
have hrne : r ≠ 0
Tactic: have hrne : r ≠ 0 := by
      intro hr
      rw [hr, ENat.coe_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h
      grind
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
hrne : r ≠ 0
⊢ analyticOrderAt (deriv f) x + 1 = (↑r : ℕ∞)
have coe : ∀ (s : ℕ) (h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑(s + 1) : ℕ∞))
  (hrne : s + 1 ≠ 0), analyticOrderAt (deriv f) x + 1 = (↑(s + 1) : ℕ∞)
Tactic: obtain ⟨s, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.pos_of_ne_zero hrne)
Cleared hypotheses: r, h, hrne
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑(s + 1) : ℕ∞)
hrne : s + 1 ≠ 0
⊢ analyticOrderAt (deriv f) x + 1 = HAdd.hAdd (α := ℕ∞) (↑s : ℕ∞) 1
have coe : analyticOrderAt (deriv f) x = (↑s : ℕ∞)
Tactic: congr 1
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑(s + 1) : ℕ∞)
hrne : s + 1 ≠ 0
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)
have h₁ : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ (s + 1) • g z
Tactic: rw [analyticOrderAt_eq_natCast (by fun_prop)] at h
Cleared hypotheses: h, hrne
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
h : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ (s + 1) • g z
hrne : s + 1 ≠ 0
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)
have coe : ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F x) (hFne : F x ≠ 0) (hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ (s + 1) • F z),
  analyticOrderAt (deriv f) x = (↑s : ℕ∞)
Tactic: obtain ⟨F, hFa, hFne, hfF⟩ := h
Cleared hypotheses: h
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ (s + 1) • F z
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)
have hfF₁ : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
Tactic: simp only [sub_eq_iff_eq_add] at hfF
Cleared hypotheses: hfF
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)
have coe : ∀ (U : Set 𝕜) (hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y)
  (hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hUx : x ∈ U),
  analyticOrderAt (deriv f) x = (↑s : ℕ∞)
Tactic: obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp (hfF.and hFa.eventually_analyticAt)
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
y : 𝕜
hy : y ∈ U
⊢ deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
have rw : (y - x) ^ (s + 1) • deriv F y + HSMul.hSMul (α := 𝕜) (deriv (fun (u : 𝕜) ↦ (u - x) ^ (s + 1)) y) (F y) =
  (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
Tactic: rw [EventuallyEq.deriv_eq (eventually_of_mem (hUo.mem_nhds hy) (fun u hu ↦ (hUf u hu).1)),
        deriv_add_const, deriv_fun_smul (by fun_prop) (hUf y hy).2.differentiableAt]
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)
have this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
Tactic: have : ∀ y ∈ U, deriv f y =
        (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y := by
      intro y hy
      rw [EventuallyEq.deriv_eq (eventually_of_mem (hUo.mem_nhds hy) (fun u hu ↦ (hUf u hu).1)),
        deriv_add_const, deriv_fun_smul (by fun_prop) (hUf y hy).2.differentiableAt]
      simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)
have coe : analyticOrderAt.{u_1, u_2} (E := E)
    (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ (s + 1) • deriv F x_1 + (s + 1) • (x_1 - x) ^ s • F x_1) x =
  (↑s : ℕ∞)
Tactic: rw [analyticOrderAt_congr (eventually_of_mem (hUo.mem_nhds hUx) this)]
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ analyticOrderAt.{u_1, u_2} (E := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x = (↑s : ℕ∞)
have rw : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, (s + 1) • (z - x) ^ s • F z = (z - x) ^ s • g z
Tactic: rw [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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
rw : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, (s + 1) • (z - x) ^ s • F z = (z - x) ^ s • g z
⊢ analyticOrderAt.{u_1, u_2} (E := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x = (↑s : ℕ∞)
have rw₁ : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x
Tactic: rw [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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, (s + 1) • (z - x) ^ s • F z = (z - x) ^ s • g z
have refine_1 : Ne.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(s + 1) : 𝕜) (F z)) x) 0
Tactic: refine ⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
refine_1 : Ne.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(s + 1) : 𝕜) (F z)) x) 0
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, (s + 1) • (z - x) ^ s • F z = (z - x) ^ s • g z
have refine_2 : ∀ (y : 𝕜),
  (s + 1) • (y - x) ^ s • F y =
    HSMul.hSMul (β := E) ((y - x) ^ s) ((fun (z : 𝕜) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(s + 1) : 𝕜) (F z)) y)
Tactic: refine ⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ ¬HAdd.hAdd (α := 𝕜) (↑s : 𝕜) 1 = 0
have norm_cast : ¬False
Tactic: norm_cast
-- 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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst_3 : CompleteSpace E
inst_4 : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x
have simp_rw : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
  (fun (y : 𝕜) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(s + 1) : 𝕜) ((y - x) ^ s • F y)) x
Tactic: simp_rw [← Nat.cast_smul_eq_nsmul 𝕜]