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
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

Tactic:
⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩

Premises used: AnalyticAt.fun_const_smul, Filter.Eventually.of_forall, Nat.cast, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, OfNat.ofNat
-- 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
refine_1 : Ne.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(s + 1) : 𝕜) (F z)) x) 0
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)
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, (s + 1) • (z - x) ^ s • F z = (z - x) ^ s • g z

Tactic:
refine ⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩
-- 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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ ¬HAdd.hAdd (α := 𝕜) (↑s : 𝕜) 1 = 0

Tactic:
norm_cast
-- 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
⊢ Ne.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(s + 1) : 𝕜) (F z)) x) 0

Tactic:
simpa using ⟨by norm_cast, hFne⟩
-- 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
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:
simpa only [Nat.cast_smul_eq_nsmul] using smul_comm ..

Premises used: Nat.cast_smul_eq_nsmul, SMulCommClass.smul_comm
-- 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
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
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x

Tactic:
simp_rw [← Nat.cast_smul_eq_nsmul 𝕜]

Premises used: 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
⊢ 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:
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
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 : ℕ∞)

Tactic:
have : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = s := by
      rw [analyticOrderAt_eq_natCast]
      · refine ⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩
        · simpa using ⟨by norm_cast, hFne⟩
        · simpa only [Nat.cast_smul_eq_nsmul] using smul_comm ..
      · simp_rw [← Nat.cast_smul_eq_nsmul 𝕜]
        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
this_1 : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x = (↑s : ℕ∞)
coe :
  analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ (s + 1) • (x_1 - x) ^ s • F x_1) x <
    analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ (s + 1) • deriv F x_1) x
⊢ 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:
rwa [← Pi.add_def, analyticOrderAt_add_eq_right_of_lt]

Premises used: Pi.add_def, analyticOrderAt_add_eq_right_of_lt
-- 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_1 : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x = (↑s : ℕ∞)
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ (s + 1) • deriv F x_1) 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 : ℕ
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_1 : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x = (↑s : ℕ∞)
coe : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ (s + 1) • deriv F z = (z - x) ^ (s + 1) • g z
⊢ analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ (s + 1) • (x_1 - x) ^ s • F x_1) x <
    analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ (s + 1) • deriv F x_1) x

Tactic:
rw [this, ← Order.succ_le_iff_of_not_isMax (not_isMax_iff.mpr ⟨⊤, ENat.coe_lt_top s⟩),
      ENat.succ_def, ← Nat.cast_add_one, natCast_le_analyticOrderAt (by fun_prop)]

Premises used: Iff.mpr, Order.succ_le_iff_of_not_isMax, natCast_le_analyticOrderAt, Exists.intro, not_isMax_iff, ENat.succ_def, Top.top, Nat.cast_add_one, ENat.coe_lt_top
-- 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_1 : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x = (↑s : ℕ∞)
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ (s + 1) • deriv F z = (z - x) ^ (s + 1) • deriv F z

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
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_1 : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (y : 𝕜) ↦ (s + 1) • (y - x) ^ s • F y) x = (↑s : ℕ∞)
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ (s + 1) • deriv F z = (z - x) ^ (s + 1) • g z

Tactic:
exact ⟨deriv F, hFa.deriv, by simp⟩
-- 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
top :
  ∀ (h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = ⊤), analyticOrderAt (deriv f) x + 1 = ⊤
coe :
  ∀ (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 = r

Tactic:
cases r with
  | top =>
    suffices analyticOrderAt (deriv f) x = ⊤ by simp_all
    simp only [analyticOrderAt_eq_top, sub_eq_zero] at h ⊢
    obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp h
    filter_upwards [hUo.mem_nhds hUx] with y hy
    simp [(eventuallyEq_of_mem (hUo.mem_nhds hy) hUf).deriv_eq]
  | coe r =>
    have hrne : r ≠ 0 := by
      intro hr
      rw [hr, ENat.coe_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h
      grind
    obtain ⟨s, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.pos_of_ne_zero hrne)
    rw [Nat.cast_succ]
    congr 1
    rw [analyticOrderAt_eq_natCast (by fun_prop)] at h
    obtain ⟨F, hFa, hFne, hfF⟩ := h
    simp only [sub_eq_iff_eq_add] at hfF
    obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp (hfF.and hFa.eventually_analyticAt)
    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]
    rw [analyticOrderAt_congr (eventually_of_mem (hUo.mem_nhds hUx) this)]
    have : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = s := by
      rw [analyticOrderAt_eq_natCast]
      · refine ⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩
        · simpa using ⟨by norm_cast, hFne⟩
        · simpa only [Nat.cast_smul_eq_nsmul] using smul_comm ..
      · simp_rw [← Nat.cast_smul_eq_nsmul 𝕜]
        fun_prop
    rwa [← Pi.add_def, analyticOrderAt_add_eq_right_of_lt]
    rw [this, ← Order.succ_le_iff_of_not_isMax (not_isMax_iff.mpr ⟨⊤, ENat.coe_lt_top s⟩),
      ENat.succ_def, ← Nat.cast_add_one, natCast_le_analyticOrderAt (by fun_prop)]
    exact ⟨deriv F, hFa.deriv, by simp⟩

Premises used: Nat.cast_succ, analyticOrderAt_eq_top, sub_eq_zero, natCast_le_analyticOrderAt, AnalyticAt.analyticOrderAt_eq_natCast, Pi.add_def, analyticOrderAt_add_eq_right_of_lt, sub_eq_iff_eq_add, ENat.succ_def, Nat.cast_add_one, 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
hf' : deriv f x ≠ 0
generalize : ∀ (r : ℕ∞) (h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = r), r = 1
⊢ analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = 1

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
hf' : deriv f x ≠ 0
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x

Tactic:
simp_rw [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
hf' : deriv f x ≠ 0
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
⊢ Eq (α := ℕ∞) ⊤ 1

Tactic:
(hf' ?_).elim

Premises used: False.elim
-- 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
hf' : deriv f x ≠ 0
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
top : deriv f x = 0
⊢ Eq (α := ℕ∞) ⊤ 1

Tactic:
refine (hf' ?_).elim

Premises used: False.elim
-- 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
hf' : deriv f x ≠ 0
h : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = f x
top : Eq.{u_2 + 1} (α := E) (deriv (fun (x_1 : 𝕜) ↦ f x) x) 0
top₁ top₂ : Eq.{u_2 + 1} (α := E) 0 0
⊢ deriv f x = 0

Tactic:
rw [EventuallyEq.deriv_eq h, deriv_const]

Premises used: Filter.EventuallyEq.deriv_eq, deriv_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
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
coe : r = 1
⊢ Eq (α := ℕ∞) (↑r : ℕ∞) 1

Tactic:
norm_cast
-- 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
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
⊢ 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
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
coe :
  ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F x) (hFne : F x ≠ 0) (hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z),
    r = 1
⊢ r = 1

Tactic:
obtain ⟨F, hFa, hFne, hfF⟩ := (analyticOrderAt_eq_natCast (by fun_prop)).mp h

Premises used: AnalyticAt.analyticOrderAt_eq_natCast, 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
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
coe : 1 ≤ r
coe₁ : r ≤ 1
⊢ r = 1

Tactic:
apply eq_of_ge_of_le

Premises used: eq_of_ge_of_le
-- 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
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
coe : ∀ (hr : r < 1), False
⊢ 1 ≤ r

Tactic:
by_contra! hr
-- 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
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
hr : r < 1
⊢ f x - f x = (x - x) ^ r • F x

Tactic:
have := hfF.self_of_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
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
hr : r < 1
this : f x - f x = (x - x) ^ r • F x
⊢ False

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
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
coe : ∀ (hf' : 1 < r), deriv f x = 0
⊢ r ≤ 1

Tactic:
contrapose! hf'
-- 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
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
hf' : 1 < r
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x

Tactic:
simp_rw [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
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ r) 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
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
funProp : IsBoundedLinearMap.{u_1, u_1, u_2} 𝕜 (F := E) fun (a : 𝕜) ↦ F a
⊢ DifferentiableAt 𝕜 F 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
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - 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
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ r ≠ 0

Tactic:
lia
-- 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
r : ℕ
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ r - 1 ≠ 0

Tactic:
lia