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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
neg :
  ∀
    (hmn :
      n ≤
        ⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)),
    ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)
neg₁ :
  (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) →
    ∀ (h_1 : 𝕜 → E) (hh : AnalyticAt 𝕜 h_1 z₀) (hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h_1 z),
      n ≤
        ⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
⊢ n ≤
      ⋯.choose (p := fun (n : ℕ) ↦
        ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
refine ⟨fun hmn ↦ ⟨fun z ↦ (z - z₀) ^ (m - n) • g z, by fun_prop, ?_⟩, fun ⟨h, hh, hfh⟩ ↦ ?_⟩
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
hmn :
  n ≤
    ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
z : 𝕜
hz :
  f z =
    (z - z₀) ^
        ⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
      g z
rwa : f z = ((z - z₀) ^ n * (z - z₀) ^ (m - n)) • g z
rwa₁ : f z = (z - z₀) ^ (n + (m - n)) • g z
rwa₂ rwa₃ rwa₄ rwa₅ :
  f z =
    (z - z₀) ^
        ⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
      g z
⊢ f z = (z - z₀) ^ n • (z - z₀) ^ (m - n) • g z

Tactic:
rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]

Premises used: pow_add, Nat.add_sub_of_le, 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
hmn :
  n ≤
    ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
h₁ :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        Membership.mem (γ := Set 𝕜)
            {x : 𝕜 |
              (fun (z : 𝕜) ↦
                  f z =
                    (z - z₀) ^
                        ⋯.choose (p := fun (n : ℕ) ↦
                          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
                      g z)
                x}
            x →
          Membership.mem (γ := Set 𝕜)
            {x : 𝕜 |
              (fun (z : 𝕜) ↦ f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)) x}
            x}
      a
h₂ h₃ :
  ∀ (z : 𝕜)
    (hz :
      f z =
        (z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
          g z),
    f z = (z - z₀) ^ n • (z - z₀) ^ (m - n) • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)

Tactic:
filter_upwards [hm] with z hz using by rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
neg :
  ∀
    (hg_ne :
      ⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
        n),
    g z₀ = 0
⊢ n ≤
    ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)

Tactic:
contrapose! hg_ne
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀

Tactic:
have : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀ := by 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
neg : Eq.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀) 0
rw : g =ᶠ[𝓝[≠] z₀] fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z
⊢ g z₀ = 0

Tactic:
rw [tendsto_nhds_unique_of_eventuallyEq (l := 𝓝[≠] z₀)
        hg.continuousAt.continuousWithinAt this.continuousWithinAt ?_]

Premises used: ContinuousAt.continuousWithinAt, tendsto_nhds_unique_of_eventuallyEq, 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
⊢ Eq.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀) 0

Tactic:
simp [m, Nat.sub_ne_zero_of_lt hg_ne]

Premises used: Nat.sub_ne_zero_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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
h₁ :
  ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z)
    (hf' :
      f z =
        (z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
          g z)
    (hf'' : f z = (z - z₀) ^ n • h z), g z = (z - z₀) ^ (n - m) • h z
⊢ g =ᶠ[𝓝[≠] z₀] fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z

Tactic:
filter_upwards [self_mem_nhdsWithin, hm.filter_mono nhdsWithin_le_nhds,
          hfh.filter_mono nhdsWithin_le_nhds] with z hz hf' hf''

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds, self_mem_nhdsWithin
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hf' :
  f z =
    (z - z₀) ^
        ⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
      g z
hf'' : f z = (z - z₀) ^ n • h z
⊢ ((z - z₀) ^ n *
        ((z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
      h z =
    g z

Tactic:
rw [← inv_smul_eq_iff₀ (pow_ne_zero _ <| sub_ne_zero_of_ne hz), hf'', smul_comm,
          ← mul_smul] at hf'

Premises used: pow_ne_zero, inv_smul_eq_iff₀, sub_ne_zero_of_ne, SMulCommClass.smul_comm, 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hf' :
  f z =
    (z - z₀) ^
        ⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
      g z
hf'' : f z = (z - z₀) ^ n • h z
hf'₁ :
  ((z - z₀) ^ n *
        ((z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
      h z =
    g z
⊢ f z = (z - z₀) ^ n • h z

Tactic:
rw [← inv_smul_eq_iff₀ (pow_ne_zero _ <| sub_ne_zero_of_ne hz), hf'', smul_comm,
          ← mul_smul] at hf'

Premises used: pow_ne_zero, inv_smul_eq_iff₀, sub_ne_zero_of_ne, SMulCommClass.smul_comm, 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hf' :
  ((z - z₀) ^ n *
        ((z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
      h z =
    g z
hf'' : f z = (z - z₀) ^ n • h z
⊢ m ≤ n

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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hf' :
  ((z - z₀) ^ n *
        ((z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
      h z =
    g z
hf'' : f z = (z - z₀) ^ n • h z
h₁ : g z = ((z - z₀) ^ n * ((z - z₀) ^ m)⁻¹) • h z
h₂ h₃ :
  ((z - z₀) ^ n *
        ((z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
      h z =
    ((z - z₀) ^ n * ((z - z₀) ^ m)⁻¹) • h z
⊢ g z = (z - z₀) ^ (n - m) • h z

Tactic:
rw [pow_sub₀ _ (sub_ne_zero_of_ne hz) (by lia), ← hf']

Premises used: sub_ne_zero_of_ne, pow_sub₀
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = analyticOrderAt g z₀
neg : ∀ (hf : ¬AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = analyticOrderAt g z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀

Tactic:
by_cases hf : AnalyticAt 𝕜 f 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 g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀

Tactic:
ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_

Premises used: ENat.eq_of_forall_natCast_le_iff
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
pos : ∀ (n : ℕ), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ (↑n : ℕ∞) ≤ analyticOrderAt g z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀

Tactic:
refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_

Premises used: ENat.eq_of_forall_natCast_le_iff
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
n : ℕ
pos :
  (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z
⊢ (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ (↑n : ℕ∞) ≤ analyticOrderAt g z₀

Tactic:
simp only [natCast_le_analyticOrderAt, hf, hf.congr hfg]

Premises used: natCast_le_analyticOrderAt, AnalyticAt.congr
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
n : ℕ
pos : ∀ (x : 𝕜 → E), (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • x z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • x z
⊢ (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • g_1 z

Tactic:
congr! 3
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
n : ℕ
x : 𝕜 → E
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • x z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • x z

Tactic:
hfg.congr_left

Premises used: Filter.EventuallyEq, Filter.EventuallyEq.congr_left
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
n : ℕ
x : 𝕜 → E
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • x z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • x z

Tactic:
exact hfg.congr_left

Premises used: Filter.EventuallyEq.congr_left
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : ¬AnalyticAt 𝕜 f z₀
neg : 0 = analyticOrderAt g z₀
neg₁ neg₂ : Eq (α := ℕ∞) 0 0
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀

Tactic:
rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt fun hg ↦ hf <| hg.congr hfg.symm]

Premises used: AnalyticAt.congr, analyticOrderAt_of_not_analyticAt, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ 1) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
⊢ Ne.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ (1 : 𝕜)) 0) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, id z = HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℕ) (z - 0) 1) ((fun (x : 𝕜) ↦ (1 : 𝕜)) 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
z₀ : 𝕜
pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
neg : ∀ (hf : ¬AnalyticAt 𝕜 f z₀), analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

Tactic:
by_cases hf : AnalyticAt 𝕜 f 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

Tactic:
ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_

Premises used: ENat.eq_of_forall_natCast_le_iff