awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt (HPow.hPow (β := ℕ) f 0) z₀ = HSMul.hSMul (α := ℕ) 0 (analyticOrderAt f z₀)

Tactic:
simp [analyticOrderAt_eq_zero]

Premises used: analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ analyticOrderAt (f ^ (n + 1)) z₀ = (n + 1) • analyticOrderAt f z₀

Tactic:
simp [add_mul, pow_add, analyticOrderAt_mul (hf.pow n), analyticOrderAt_pow, hf]

Premises used: add_mul, pow_add, analyticOrderAt_mul, AnalyticAt.pow
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ analyticOrderNatAt (f ^ n) z₀ = n • analyticOrderNatAt f z₀

Tactic:
simp [analyticOrderNatAt, analyticOrderAt_pow, hf]

Premises used: analyticOrderNatAt, analyticOrderAt_pow
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
pos :
  ∀ (hg_nc : EventuallyConst g (𝓝 z₀)),
    analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
neg :
  ∀ (hg_nc : ¬EventuallyConst g (𝓝 z₀)),
    analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

Tactic:
by_cases hg_nc : EventuallyConst g (𝓝 z₀)

Premises used: Filter.EventuallyConst, 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
⊢ EventuallyConst (f ∘ g) (𝓝 z₀)

Tactic:
have := hg_nc.comp f
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
this : EventuallyConst (f ∘ g) (𝓝 z₀)
⊢ analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤

Tactic:
rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc this

Premises used: eventuallyConst_iff_analyticOrderAt_sub_eq_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
this : EventuallyConst (f ∘ g) (𝓝 z₀)
hg_nc₁ : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
⊢ analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤

Tactic:
rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc this

Premises used: eventuallyConst_iff_analyticOrderAt_sub_eq_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
pos : analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

Tactic:
rw [hg_nc]
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
pos : ∀ (hf' : f (g z₀) = 0), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
neg : ∀ (hf' : ¬f (g z₀) = 0), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤

Tactic:
by_cases hf' : f (g z₀) = 0
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : f (g z₀) = 0
⊢ analyticOrderAt f (g z₀) ≠ 0

Tactic:
grind [analyticOrderAt_ne_zero]

Premises used: analyticOrderAt_ne_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : f (g z₀) = 0
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤

Tactic:
simpa [hf', show analyticOrderAt f (g z₀) ≠ 0 by grind [analyticOrderAt_ne_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
neg : analyticOrderAt (f ∘ g) z₀ = 0
rw : analyticOrderAt f (g z₀) = 0
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤

Tactic:
rw [show analyticOrderAt f (g z₀) = 0 from ?_, zero_mul]

Premises used: MulZeroClass.zero_mul
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
⊢ analyticOrderAt (f ∘ g) z₀ = 0

Tactic:
grind [hf.comp hg, AnalyticAt.analyticOrderAt_eq_zero]

Premises used: AnalyticAt.comp, 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
hf' : ¬f (g z₀) = 0
⊢ analyticOrderAt f (g z₀) = 0

Tactic:
grind [hf.comp hg, AnalyticAt.analyticOrderAt_eq_zero]

Premises used: AnalyticAt.comp, 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
pos :
  ∀ (hf' : analyticOrderAt f (g z₀) = ⊤),
    analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
neg :
  ∀ (hf' : ¬analyticOrderAt f (g z₀) = ⊤),
    analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

Tactic:
by_cases hf' : analyticOrderAt f (g z₀) = ⊤

Premises used: 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
pos : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ ≠ 0
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

Tactic:
rw [hf', analyticOrderAt_eq_top.mpr
      (EventuallyEq.comp_tendsto (analyticOrderAt_eq_top.mp hf') hg.continuousAt), ENat.top_mul]

Premises used: Iff.mpr, Filter.EventuallyEq.comp_tendsto, analyticOrderAt_eq_top, Iff.mp, AnalyticAt.continuousAt, ENat.top_mul
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
pos : g z₀ - g z₀ = 0
pos₁ pos₂ : g z₀ = g z₀
⊢ analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ ≠ 0

Tactic:
rw [AnalyticAt.analyticOrderAt_ne_zero (by fun_prop), sub_eq_zero]

Premises used: sub_eq_zero, AnalyticAt.analyticOrderAt_ne_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤

Tactic:
rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc

Premises used: eventuallyConst_iff_analyticOrderAt_sub_eq_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : ¬analyticOrderAt f (g z₀) = ⊤
hg_nc₁ : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
⊢ ¬analyticOrderAt f (g z₀) = ⊤

Tactic:
rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc

Premises used: eventuallyConst_iff_analyticOrderAt_sub_eq_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
neg :
  ∀ (r : ℕ) (hr : (↑r : ℕ∞) = analyticOrderAt f (g z₀)),
    analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

Tactic:
obtain ⟨r, hr⟩ := ENat.ne_top_iff_exists.mp hf'

Premises used: ENat.ne_top_iff_exists, 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : (↑r : ℕ∞) = analyticOrderAt f (g z₀)
neg :
  ∀ (s : ℕ) (hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀),
    analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

Tactic:
obtain ⟨s, hs⟩ := ENat.ne_top_iff_exists.mp hg_nc

Premises used: ENat.ne_top_iff_exists, 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : (↑r : ℕ∞) = analyticOrderAt f (g z₀)
s : ℕ
hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
neg : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

Tactic:
rw [← hr, ← hs, ← ENat.coe_mul, (hf.comp hg).analyticOrderAt_eq_natCast]

Premises used: ENat.coe_mul, AnalyticAt.analyticOrderAt_eq_natCast, AnalyticAt.comp
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : (↑r : ℕ∞) = analyticOrderAt f (g z₀)
s : ℕ
hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
neg :
  ∀
    (hr :
      ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g z₀) ∧ g_1 (g z₀) ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • g_1 z)
    (s : ℕ) (hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀),
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
rw [Eq.comm, hf.analyticOrderAt_eq_natCast] at hr

Premises used: AnalyticAt.analyticOrderAt_eq_natCast, Eq.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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g z₀) ∧ g_1 (g z₀) ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • g_1 z
s : ℕ
hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
neg :
  ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F (g z₀)) (hFne : F (g z₀) ≠ 0)
    (hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z),
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
rcases hr with ⟨F, hFa, hFne, hfF⟩
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = (↑s : ℕ∞)
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : (↑s : ℕ∞) = analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
neg :
  ∀ (hs : ∃ (g_1 : 𝕜 → 𝕜), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • g_1 z)
    (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F (g z₀)) (hFne : F (g z₀) ≠ 0)
    (hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z),
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
rw [Eq.comm, AnalyticAt.analyticOrderAt_eq_natCast (by fun_prop)] at hs

Premises used: AnalyticAt.analyticOrderAt_eq_natCast, Eq.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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : ∃ (g_1 : 𝕜 → 𝕜), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • g_1 z
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
neg :
  ∀ (G : 𝕜 → 𝕜) (hGa : AnalyticAt 𝕜 G z₀) (hGne : G z₀ ≠ 0) (hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z),
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
rcases hs with ⟨G, hGa, hGne, hgG⟩
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ G z ^ r • F (g z)) z₀

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
⊢ Ne.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ G z ^ r • F (g z)) z₀) 0

Tactic:
aesop
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
neg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = HSMul.hSMul (β := E) ((z - z₀) ^ (r * s)) ((fun (z : 𝕜) ↦ G z ^ r • F (g z)) z)
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
refine ⟨fun z ↦ (G z) ^ r • F (g z), by fun_prop, by aesop, ?_⟩
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
h :
  ∀ (z : 𝕜) (hfz : (f ∘ g) z = ((fun (x : 𝕜) ↦ (x - g z₀) ^ r • F x) ∘ g) z) (hgz : g z - g z₀ = (z - z₀) ^ s • G z),
    (f ∘ g) z = (z - z₀) ^ (r * s) • G z ^ r • F (g z)
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = HSMul.hSMul (β := E) ((z - z₀) ^ (r * s)) ((fun (z : 𝕜) ↦ G z ^ r • F (g z)) z)

Tactic:
filter_upwards [EventuallyEq.comp_tendsto hfF hg.continuousAt, hgG] with z hfz hgz

Premises used: Filter.EventuallyEq.comp_tendsto, AnalyticAt.continuousAt
-- 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
z : 𝕜
hfz : (f ∘ g) z = ((fun (x : 𝕜) ↦ (x - g z₀) ^ r • F x) ∘ g) z
hgz : g z - g z₀ = (z - z₀) ^ s • G z
⊢ (f ∘ g) z = (z - z₀) ^ (r * s) • G z ^ r • F (g z)

Tactic:
simp only [hfz, Function.comp_def, hgz, smul_eq_mul, mul_pow, mul_smul, mul_comm r s, pow_mul]

Premises used: pow_mul, Function.comp_def, mul_comm, smul_eq_mul, mul_pow, 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
pos : ∀ (hf : AnalyticAt 𝕜 f (g z₀)), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
neg : ∀ (hf : ¬AnalyticAt 𝕜 f (g z₀)), analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)

Tactic:
by_cases hf : AnalyticAt 𝕜 f (g z₀)

Premises used: 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
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)

Tactic:
simp [hf.analyticOrderAt_comp hg, hg.analyticOrderAt_sub_eq_one_of_deriv_ne_zero hg']

Premises used: AnalyticAt.analyticOrderAt_comp, AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
neg : ¬AnalyticAt 𝕜 (f ∘ g) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)

Tactic:
rw [analyticOrderAt_of_not_analyticAt hf, analyticOrderAt_of_not_analyticAt]

Premises used: analyticOrderAt_of_not_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
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf neg neg₁ neg₂ neg₃ : ¬AnalyticAt 𝕜 f (g z₀)
⊢ ¬AnalyticAt 𝕜 (f ∘ g) z₀

Tactic:
rwa [analyticAt_comp_iff_of_deriv_ne_zero hg hg']

Premises used: analyticAt_comp_iff_of_deriv_ne_zero