awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Order
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 ∧ ¬g' z₀ = 0
⊢ (f' • g') z₀ ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Order
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
neg₁ : ¬g' z₀ = 0
⊢ ¬f' z₀ = 0 ∧ ¬g' z₀ = 0

Tactic:
tauto
-- Module: Mathlib.Analysis.Analytic.Order
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 :
  ∀ (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
⊢ ∀ᶠ (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'

Premises used: eventually_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ ∀ᶠ (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'

Premises used: eventually_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ (f • g) y = (y - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') y

Tactic:
simp [h₁t y hy.1, h₁s y hy.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ ((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:
module
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • (f' • g') z

Tactic:
exact eventually_nhds_iff.2
      ⟨t ∩ s, fun y hy ↦ (by simp [h₁t y hy.1, h₁s y hy.2]; module), h₂t.inter h₂s, h₃t, h₃s⟩

Premises used: Iff.mpr, Inter.inter, eventually_nhds_iff, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Order
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 𝕜
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
⊢ analyticOrderAt (deriv f) x + 1 = analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x

Tactic:
generalize h : analyticOrderAt (f · - f x) x = r

Premises used: HSub.hSub, analyticOrderAt
-- Module: Mathlib.Analysis.Analytic.Order
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 = ⊤
this : analyticOrderAt (deriv f) x = ⊤
⊢ analyticOrderAt (deriv f) x + 1 = ⊤

Tactic:
simp_all
-- Module: Mathlib.Analysis.Analytic.Order
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 = ⊤
top : analyticOrderAt (deriv f) x = ⊤
⊢ analyticOrderAt (deriv f) x + 1 = ⊤

Tactic:
suffices analyticOrderAt (deriv f) x = ⊤ by simp_all
-- Module: Mathlib.Analysis.Analytic.Order
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 = ⊤
top : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x), ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0
⊢ analyticOrderAt (deriv f) x = ⊤

Tactic:
simp only [analyticOrderAt_eq_top, sub_eq_zero] at h ⊢

Premises used: analyticOrderAt_eq_top, sub_eq_zero
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0

Tactic:
obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp h

Premises used: eventually_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Order
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
h₁ : ∀ (y : 𝕜) (hy : y ∈ U), deriv f y = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, deriv f z = 0

Tactic:
filter_upwards [hUo.mem_nhds hUx] with y hy

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Analytic.Order
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
y : 𝕜
hy : y ∈ U
⊢ deriv f y = 0

Tactic:
simp [(eventuallyEq_of_mem (hUo.mem_nhds hy) hUf).deriv_eq]

Premises used: Filter.eventuallyEq_of_mem, Filter.EventuallyEq.deriv_eq, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Analytic.Order
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 = 0
hr : r = 0
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ f x - f x ≠ 0

Tactic:
rw [hr, ENat.coe_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h

Premises used: ENat.coe_zero, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Analytic.Order
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
h₁ : f x - f x ≠ 0
⊢ r = 0

Tactic:
rw [hr, ENat.coe_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h

Premises used: ENat.coe_zero, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Analytic.Order
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 : f x - f x ≠ 0
hr : r = 0
⊢ False

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ∞)
⊢ 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
-- Module: Mathlib.Analysis.Analytic.Order
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
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) : ℕ∞)
⊢ analyticOrderAt (deriv f) x + 1 = (↑r : ℕ∞)

Tactic:
obtain ⟨s, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.pos_of_ne_zero hrne)

Premises used: Iff.mpr, Nat.pos_of_ne_zero, Nat.exists_add_one_eq, rfl
-- Module: Mathlib.Analysis.Analytic.Order
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
coe : analyticOrderAt (deriv f) x = (↑s : ℕ∞)
⊢ analyticOrderAt (deriv f) x + 1 = HAdd.hAdd (α := ℕ∞) (↑s : ℕ∞) 1

Tactic:
congr 1
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ ∃ (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

Premises used: AnalyticAt.analyticOrderAt_eq_natCast
-- Module: Mathlib.Analysis.Analytic.Order
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
h₁ : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ (s + 1) • g z
⊢ s + 1 ≠ 0

Tactic:
rw [analyticOrderAt_eq_natCast (by fun_prop)] at h

Premises used: AnalyticAt.analyticOrderAt_eq_natCast
-- Module: Mathlib.Analysis.Analytic.Order
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
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 : ℕ∞)
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)

Tactic:
obtain ⟨F, hFa, hFne, hfF⟩ := h
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x

Tactic:
simp only [sub_eq_iff_eq_add] at hfF

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Analysis.Analytic.Order
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
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 : ℕ∞)
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)

Tactic:
obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp (hfF.and hFa.eventually_analyticAt)

Premises used: Filter.Eventually.and, eventually_nhds_iff, Iff.mp, AnalyticAt.eventually_analyticAt
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (u : 𝕜) ↦ (u - x) ^ (s + 1)) y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ deriv 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]

Premises used: deriv_fun_smul, Filter.eventually_of_mem, Filter.EventuallyEq.deriv_eq, And.right, And.left, AnalyticAt.differentiableAt, IsOpen.mem_nhds, deriv_add_const
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ (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:
simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]

Premises used: add_smul, Nat.cast_smul_eq_nsmul, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Analytic.Order
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 ∈ 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]
-- Module: Mathlib.Analysis.Analytic.Order
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
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 : ℕ∞)
⊢ analyticOrderAt (deriv f) x = (↑s : ℕ∞)

Tactic:
rw [analyticOrderAt_congr (eventually_of_mem (hUo.mem_nhds hUx) this)]

Premises used: analyticOrderAt_congr, Filter.eventually_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Analytic.Order
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
rw₁ : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x
⊢ analyticOrderAt.{u_1, u_2} (E := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x = (↑s : ℕ∞)

Tactic:
rw [analyticOrderAt_eq_natCast]

Premises used: AnalyticAt.analyticOrderAt_eq_natCast