awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
refine_1 :
  MeromorphicAt f x →
    ∀ (n : ℕ) (hn : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x),
      ∀ᶠ (x_2 : 𝕜) in 𝓝 x,
        Membership.mem (γ := Set 𝕜) {x}ᶜ x_2 → f x_2 = HPow.hPow (β := ℤ) (x_2 - x) (-(↑n : ℤ)) • (x_2 - x) ^ n • f x_2
refine_2 : (∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x
⊢ MeromorphicAt f x ↔ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
refine ⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : MeromorphicAt f x
n : ℕ
hn : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
refine_1 :
  ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z), f z = HPow.hPow (β := ℤ) (z - x) (-(↑n : ℤ)) • (z - x) ^ n • f z
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = HPow.hPow (β := ℤ) (x_1 - x) (-(↑n : ℤ)) • (x_1 - x) ^ n • f x_1

Tactic:
filter_upwards with z hz
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : MeromorphicAt f x
n : ℕ
hn : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
match_scalars : 1 = HPow.hPow (β := ℤ) (z - x) (-(↑n : ℤ)) * ((z - x) ^ n * 1)
⊢ f z = HPow.hPow (β := ℤ) (z - x) (-(↑n : ℤ)) • (z - x) ^ n • f z

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : MeromorphicAt f x
n : ℕ
hn : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
⊢ 1 = HPow.hPow (β := ℤ) (z - x) (-(↑n : ℤ)) * ((z - x) ^ n * 1)

Tactic:
simp [sub_ne_zero.mpr hz]

Premises used: Iff.mpr, sub_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ (∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x

Tactic:
fun ⟨n, g, hg_an, hg_eq⟩ ↦ MeromorphicAt.congr ?_ (EventuallyEq.symm hg_eq)

Premises used: _private.0.MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt.match_2, MeromorphicAt.congr, Filter.EventuallyEq.symm, MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
refine_2 :
  (∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) →
    ∀ (n : ℤ) (g : 𝕜 → E) (hg_an : AnalyticAt 𝕜 g x) (hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
      MeromorphicAt.{u_1, u_3} (E := E) (fun (x_2 : 𝕜) ↦ (x_2 - x) ^ n • g x_2) x
⊢ (∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x

Tactic:
refine fun ⟨n, g, hg_an, hg_eq⟩ ↦ MeromorphicAt.congr ?_ (EventuallyEq.symm hg_eq)
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
n : ℤ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) x

Tactic:
(((MeromorphicAt.id x).sub (.const _ x)).zpow _).smul hg_an.meromorphicAt

Premises used: MeromorphicAt.const, MeromorphicAt.id, MeromorphicAt.sub, MeromorphicAt.zpow, MeromorphicAt.smul, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
n : ℤ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) x

Tactic:
exact (((MeromorphicAt.id x).sub (.const _ x)).zpow _).smul hg_an.meromorphicAt

Premises used: MeromorphicAt.const, MeromorphicAt.id, MeromorphicAt.sub, MeromorphicAt.zpow, MeromorphicAt.smul, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
rw [MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt] at h

Premises used: MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
obtain :
  ∀ (n : ℤ) (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
    MeromorphicAt (deriv f) x
⊢ MeromorphicAt (deriv f) x

Tactic:
obtain ⟨n, g, h₁g, h₂g⟩ := h
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
h :
  ∀ (z₀ : 𝕜) (h₁ : AnalyticAt 𝕜 g z₀) (h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀),
    deriv (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z₀ = ((↑n : 𝕜) * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀
⊢ EventuallyEq.{u_1, u_3} (β := E) (𝓝[≠] x) (deriv fun (z : 𝕜) ↦ (z - x) ^ n • g z) fun (z : 𝕜) ↦
    ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z

Tactic:
filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt,
      eventually_nhdsWithin_of_forall fun _ a ↦ a] with z₀ h₁ h₂

Premises used: eventually_nhdsWithin_of_eventually_nhds, AnalyticAt.eventually_analyticAt, eventually_nhdsWithin_of_forall
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) z₀

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀
⊢ z₀ - x ≠ 0 ∨ 0 ≤ n

Tactic:
simp_all [sub_ne_zero_of_ne h₂]

Premises used: sub_ne_zero_of_ne
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀
funProp : IsBoundedLinearMap.{u_1, u_1, u_3} 𝕜 (F := E) fun (a : 𝕜) ↦ g a
⊢ DifferentiableAt 𝕜 g z₀

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀
h :
  HSMul.hSMul (α := 𝕜) (deriv (fun (x : 𝕜) ↦ x ^ n) (z₀ - x)) (g z₀) + (z₀ - x) ^ n • deriv g z₀ =
    ((↑n : 𝕜) * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀
⊢ deriv (fun (z : 𝕜) ↦ (z - x) ^ n • g z) z₀ = ((↑n : 𝕜) * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀

Tactic:
rw [deriv_fun_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂]))
      (by fun_prop), add_comm, deriv_comp_sub_const (f := (· ^ n))]

Premises used: deriv_fun_smul, add_comm, HPow.hPow, deriv_comp_sub_const
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : Membership.mem (γ := Set 𝕜) {x}ᶜ z₀
⊢ HSMul.hSMul (α := 𝕜) (deriv (fun (x : 𝕜) ↦ x ^ n) (z₀ - x)) (g z₀) + (z₀ - x) ^ n • deriv g z₀ =
    ((↑n : 𝕜) * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ EventuallyEq.{u_1, u_3} (β := E) (𝓝[≠] x) (deriv fun (z : 𝕜) ↦ (z - x) ^ n • g z) fun (z : 𝕜) ↦
    ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z

Tactic:
have : _root_.deriv (fun z ↦ (z - x) ^ n • g z)
      =ᶠ[𝓝[≠] x] fun z ↦ (n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • _root_.deriv g z := by
    filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt,
      eventually_nhdsWithin_of_forall fun _ a ↦ a] with z₀ h₁ h₂
    rw [deriv_fun_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂]))
      (by fun_prop), add_comm, deriv_comp_sub_const (f := (· ^ n))]
    aesop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
this :
  EventuallyEq.{u_1, u_3} (β := E) (𝓝[≠] x) (deriv fun (z : 𝕜) ↦ (z - x) ^ n • g z) fun (z : 𝕜) ↦
    ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z
rw : MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z) x
⊢ MeromorphicAt (deriv f) x

Tactic:
rw [MeromorphicAt.meromorphicAt_congr (Filter.EventuallyEq.nhdsNE_deriv h₂g),
    MeromorphicAt.meromorphicAt_congr this]

Premises used: MeromorphicAt.meromorphicAt_congr, Filter.EventuallyEq.nhdsNE_deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
this :
  EventuallyEq.{u_1, u_3} (β := E) (𝓝[≠] x) (deriv fun (z : 𝕜) ↦ (z - x) ^ n • g z) fun (z : 𝕜) ↦
    ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ ((↑n : 𝕜) * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • deriv g z) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ deriv f z) x

Tactic:
h.deriv

Premises used: MeromorphicAt.deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt (deriv^[0] f) x

Tactic:
h

Premises used: Nat.iterate
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt (deriv^[0] f) x

Tactic:
exact h
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
n : ℕ
IH : MeromorphicAt (deriv^[n] f) x
⊢ MeromorphicAt (deriv^[n + 1] f) x

Tactic:
simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Premises used: Function.iterate_succ', Function.comp_apply, MeromorphicAt.deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
n : ℕ
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
zero : MeromorphicAt (deriv^[0] f) x
succ : ∀ (n : ℕ) (IH : MeromorphicAt (deriv^[n] f) x), MeromorphicAt (deriv^[n + 1] f) x
⊢ MeromorphicAt (deriv^[n] f) x

Tactic:
induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
n : ℕ
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ deriv^[n] f z) x

Tactic:
h.iterated_deriv

Premises used: MeromorphicAt.iterated_deriv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
⊢ MeromorphicAt (g • f) x ↔ MeromorphicAt f x

Tactic:
⟨fun hfg ↦ ?_, hg.meromorphicAt.smul⟩

Premises used: Iff.intro, MeromorphicAt.smul, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
refine : ∀ (hfg : MeromorphicAt (g • f) x), MeromorphicAt f x
⊢ MeromorphicAt (g • f) x ↔ MeromorphicAt f x

Tactic:
refine ⟨fun hfg ↦ ?_, hg.meromorphicAt.smul⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hfg : MeromorphicAt (g • f) x
⊢ MeromorphicAt f x

Tactic:
(hg.inv hg').meromorphicAt.smul hfg |>.congr ?_

Premises used: AnalyticAt.inv, MeromorphicAt.congr, MeromorphicAt.smul, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hfg : MeromorphicAt (g • f) x
refine : g⁻¹ • g • f =ᶠ[𝓝[≠] x] f
⊢ MeromorphicAt f x

Tactic:
refine (hg.inv hg').meromorphicAt.smul hfg |>.congr ?_

Premises used: AnalyticAt.inv, MeromorphicAt.congr, MeromorphicAt.smul, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hfg : MeromorphicAt (g • f) x
h : ∀ (z : 𝕜) (hz : g z ≠ 0), (g⁻¹ • g • f) z = f z
⊢ g⁻¹ • g • f =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [(hg.continuousAt.mono_left nhdsWithin_le_nhds).eventually_ne hg'] with z hz

Premises used: Filter.Tendsto.eventually_ne, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, AnalyticAt.continuousAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hfg : MeromorphicAt (g • f) x
z : 𝕜
hz : g z ≠ 0
⊢ (g⁻¹ • g • f) z = f z

Tactic:
simp [inv_smul_smul₀ hz]

Premises used: inv_smul_smul₀
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
⊢ MeromorphicAt (g * f) x ↔ MeromorphicAt f x

Tactic:
meromorphicAt_smul_iff_of_ne_zero hg hg'

Premises used: meromorphicAt_smul_iff_of_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
obtain :
  ∀ (r : ℕ) (hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)),
    MeromorphicAt (f ∘ g) x
⊢ MeromorphicAt (f ∘ g) x

Tactic:
obtain ⟨r, hr⟩ := hf
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
pos : ∀ (hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤), MeromorphicAt (f ∘ g) x
neg : ∀ (hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤), MeromorphicAt (f ∘ g) x
⊢ MeromorphicAt (f ∘ g) x

Tactic:
by_cases hg' : analyticOrderAt (g · - g x) x = ⊤

Premises used: HSub.hSub, analyticOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicAt (f ∘ g) x

Tactic:
.congr (.const (f (g x)) x) ?_

Premises used: MeromorphicAt.const, MeromorphicAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
pos : (fun (x_1 : 𝕜) ↦ f (g x)) =ᶠ[𝓝[≠] x] f ∘ g
⊢ MeromorphicAt (f ∘ g) x

Tactic:
refine .congr (.const (f (g x)) x) ?_
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
h : ∀ (z : 𝕜) (hz : g z - g x = 0), f (g x) = (f ∘ g) z
⊢ (fun (x_1 : 𝕜) ↦ f (g x)) =ᶠ[𝓝[≠] x] f ∘ g

Tactic:
filter_upwards [nhdsWithin_le_nhds <| analyticOrderAt_eq_top.mp hg'] with z hz

Premises used: analyticOrderAt_eq_top, nhdsWithin_le_nhds, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
z : 𝕜
hz : g z - g x = 0
⊢ f (g x) = (f ∘ g) z

Tactic:
grind
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
neg :
  ∀ (n : ℕ) (hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x),
    MeromorphicAt (f ∘ g) x
⊢ MeromorphicAt (f ∘ g) x

Tactic:
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp hg'

Premises used: WithTop.ne_top_iff_exists, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
neg :
  ∀ (h : 𝕜 → 𝕜') (han : AnalyticAt 𝕜 h x) (hne : h x ≠ 0) (heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z),
    MeromorphicAt (f ∘ g) x
⊢ MeromorphicAt (f ∘ g) x

Tactic:
obtain ⟨h, han, hne, heq⟩ := (hg.fun_sub analyticAt_const).analyticOrderAt_eq_natCast.mp hn.symm

Premises used: AnalyticAt.analyticOrderAt_eq_natCast, analyticAt_const, Iff.mp, AnalyticAt.fun_sub, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt.{u_2, u_2, u_4} 𝕜' (F := F) (fun (z : 𝕜') ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = analyticOrderAt.{u_1, u_2} (E := 𝕜') (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
⊢ let j : (z : 𝕜') → F := fun (z : 𝕜') ↦ (z - g x) ^ r • f z;
  AnalyticAt 𝕜' j (g x)

Tactic:
set j := fun z ↦ (z - g x) ^ r • f z

Premises used: HSub.hSub, HPow.hPow, HSMul.hSMul