awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) ≠ ⊤
hr : meromorphicOrderAt f (g x) = (↑(meromorphicOrderAt f (g x)).untop₀ : WithTop ℤ)
⊢ ∃ (g_1 : 𝕜 → E),
    AnalyticAt 𝕜 g_1 (g x) ∧
      g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • g_1 z

Tactic:
rw [meromorphicOrderAt_ne_top_iff hf] at hf'

Premises used: meromorphicOrderAt_ne_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) ≠ ⊤
hr : meromorphicOrderAt f (g x) = (↑(meromorphicOrderAt f (g x)).untop₀ : WithTop ℤ)
hf'₁ :
  ∃ (g_1 : 𝕜 → E),
    AnalyticAt 𝕜 g_1 (g x) ∧
      g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • g_1 z
⊢ meromorphicOrderAt f (g x) = (↑(meromorphicOrderAt f (g x)).untop₀ : WithTop ℤ)

Tactic:
rw [meromorphicOrderAt_ne_top_iff hf] at hf'

Premises used: meromorphicOrderAt_ne_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' :
  ∃ (g_1 : 𝕜 → E),
    AnalyticAt 𝕜 g_1 (g x) ∧
      g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • g_1 z
hr : meromorphicOrderAt f (g x) = (↑(meromorphicOrderAt f (g x)).untop₀ : WithTop ℤ)
⊢ let r := (meromorphicOrderAt f (g x)).untop₀;
  ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g x) ∧ g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • g_1 z

Tactic:
set r := (meromorphicOrderAt f (g x)).untop₀

Premises used: WithTop.untop₀, meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' :
  ∃ (g_1 : 𝕜 → E),
    AnalyticAt 𝕜 g_1 (g x) ∧
      g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • g_1 z
hr : meromorphicOrderAt f (g x) = (↑(meromorphicOrderAt f (g x)).untop₀ : WithTop ℤ)
hf'₁ :
  let r := (meromorphicOrderAt f (g x)).untop₀;
  ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g x) ∧ g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • g_1 z
⊢ let r := (meromorphicOrderAt f (g x)).untop₀;
  meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)

Tactic:
set r := (meromorphicOrderAt f (g x)).untop₀

Premises used: WithTop.untop₀, meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hf' : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g x) ∧ g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • g_1 z
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
inr :
  meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)

Tactic:
rw [hr]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hf' : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 (g x) ∧ g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • g_1 z
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
inr :
  ∀ (F : 𝕜 → E) (hFan : AnalyticAt 𝕜 F (g x)) (hFne : F (g x) ≠ 0)
    (hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z),
    meromorphicOrderAt (f ∘ g) x =
      (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)

Tactic:
obtain ⟨F, hFan, hFne, hFev⟩ := hf'
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
⊢ f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g

Tactic:
have aux1 : f ∘ g =ᶠ[𝓝[≠] x] (g · - g x) ^ r • (F ∘ g) := hFev.comp_tendsto (hg.map_nhdsNE hg_nc)
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
⊢ AnalyticAt 𝕜 (F ∘ g) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
⊢ ¬AnalyticAt 𝕜 (F ∘ g) x ∨ (F ∘ g) x ≠ 0

Tactic:
.inr hFne

Premises used: Or.inr
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
⊢ ¬AnalyticAt 𝕜 (F ∘ g) x ∨ (F ∘ g) x ≠ 0

Tactic:
exact .inr hFne
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
rw : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt (F ∘ g) x)) 0
rw₁ : Eq (α := WithTop ℤ) (ENat.map Nat.cast 0) 0
rw₂ : Eq (α := WithTop ℤ) (↑(↑0 : ℤ) : WithTop ℤ) 0
rw₃ : Eq (α := WithTop ℤ) (↑0 : WithTop ℤ) 0
rw₄ rw₅ : Eq (α := WithTop ℤ) 0 0
⊢ meromorphicOrderAt (F ∘ g) x = 0

Tactic:
rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop),
      analyticOrderAt_eq_zero.mpr (by exact .inr hFne), ENat.map_zero, CharP.cast_eq_zero,
      WithTop.coe_zero]

Premises used: CharP.cast_eq_zero, Iff.mpr, AnalyticAt.meromorphicOrderAt_eq, WithTop.coe_zero, analyticOrderAt_eq_zero, ENat.map_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
⊢ meromorphicOrderAt (F ∘ g) x = 0

Tactic:
have aux2 : meromorphicOrderAt (F ∘ g) x = 0 := by
    rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop),
      analyticOrderAt_eq_zero.mpr (by exact .inr hFne), ENat.map_zero, CharP.cast_eq_zero,
      WithTop.coe_zero]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
inr : AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
inr₁ : MeromorphicAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x
rw : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r) x
rw₁ : AnalyticAt 𝕜 (F ∘ g) x
⊢ meromorphicOrderAt (f ∘ g) x =
    (↑r : WithTop ℤ) * ENat.map Nat.cast (analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x)

Tactic:
rw [meromorphicOrderAt_congr aux1, meromorphicOrderAt_smul ?_ (AnalyticAt.meromorphicAt ?_),
    aux2, add_zero, meromorphicOrderAt_zpow, AnalyticAt.meromorphicOrderAt_eq]

Premises used: AnalyticAt.meromorphicOrderAt_eq, meromorphicOrderAt_smul, meromorphicOrderAt_zpow, add_zero, AnalyticAt.meromorphicAt, meromorphicOrderAt_congr
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ MeromorphicAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hr : meromorphicOrderAt f (g x) = (↑r : WithTop ℤ)
F : 𝕜 → E
hFan : AnalyticAt 𝕜 F (g x)
hFne : F (g x) ≠ 0
hFev : f =ᶠ[𝓝[≠] g x] fun (z : 𝕜) ↦ (z - g x) ^ r • F z
aux1 : f ∘ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) r • F ∘ g
aux2 : meromorphicOrderAt (F ∘ g) x = 0
⊢ AnalyticAt 𝕜 (F ∘ g) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
pos : ∀ (hf : MeromorphicAt f (g x)), meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
neg : ∀ (hf : ¬MeromorphicAt f (g x)), meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

Tactic:
by_cases hf : MeromorphicAt f (g x)

Premises used: MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : MeromorphicAt f (g x)
⊢ analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = 1

Tactic:
have hgo : analyticOrderAt _ x = 1 := hg.analyticOrderAt_sub_eq_one_of_deriv_ne_zero hg'
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : MeromorphicAt f (g x)
hgo : analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = 1
pos : meromorphicOrderAt f (g x) * ENat.map Nat.cast 1 = meromorphicOrderAt f (g x)
pos₁ : ¬EventuallyConst g (𝓝 x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

Tactic:
rw [hf.meromorphicOrderAt_comp hg, hgo]

Premises used: MeromorphicAt.meromorphicOrderAt_comp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : MeromorphicAt f (g x)
hgo : analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = 1
⊢ meromorphicOrderAt f (g x) * ENat.map Nat.cast 1 = meromorphicOrderAt f (g x)

Tactic:
simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top, hgo]

Premises used: eventuallyConst_iff_analyticOrderAt_sub_eq_top
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : MeromorphicAt f (g x)
hgo : analyticOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ g x_1 - g x) x = 1
⊢ ¬EventuallyConst g (𝓝 x)

Tactic:
simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top, hgo]

Premises used: eventuallyConst_iff_analyticOrderAt_sub_eq_top
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
neg : ¬MeromorphicAt (f ∘ g) x
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

Tactic:
rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]

Premises used: meromorphicOrderAt_of_not_meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst_3 : CompleteSpace 𝕜
inst_4 : CharZero 𝕜
hf neg neg₁ neg₂ neg₃ : ¬MeromorphicAt f (g x)
⊢ ¬MeromorphicAt (f ∘ g) x

Tactic:
rwa [meromorphicAt_comp_iff_of_deriv_ne_zero hg hg']

Premises used: meromorphicAt_comp_iff_of_deriv_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
neg : ∀ (hf : ¬MeromorphicAt f x), meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
by_cases hf : MeromorphicAt f x

Premises used: MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
simp [meromorphicOrderAt_smul hg.meromorphicAt hf, hg.meromorphicOrderAt_eq,
      hg.analyticOrderAt_eq_zero.mpr hg']

Premises used: Iff.mpr, AnalyticAt.meromorphicOrderAt_eq, meromorphicOrderAt_smul, AnalyticAt.meromorphicAt, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
neg : ¬MeromorphicAt (g • f) x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]

Premises used: meromorphicOrderAt_of_not_meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf neg neg₁ neg₂ neg₃ : ¬MeromorphicAt f x
⊢ ¬MeromorphicAt (g • f) x

Tactic:
rwa [meromorphicAt_smul_iff_of_ne_zero hg hg']

Premises used: meromorphicAt_smul_iff_of_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
g f : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
⊢ meromorphicOrderAt (g * f) x = meromorphicOrderAt f x

Tactic:
meromorphicOrderAt_smul_of_ne_zero hg hg'

Premises used: meromorphicOrderAt_smul_of_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
pos : (h₁ : MeromorphicAt f x) → E
neg : (h₁ : ¬MeromorphicAt f x) → E
⊢ E

Tactic:
by_cases h₁ : MeromorphicAt f x

Premises used: MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
pos : (h₂ : meromorphicOrderAt f x = ⊤) → E
neg : (h₂ : ¬meromorphicOrderAt f x = ⊤) → E
⊢ E

Tactic:
by_cases h₂ : meromorphicOrderAt f x = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ E

Tactic:
exact 0
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ E

Tactic:
exact ((meromorphicOrderAt_ne_top_iff h₁).1 h₂).choose x

Premises used: meromorphicOrderAt_ne_top_iff, Iff.mp, Exists.choose
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁ : ¬MeromorphicAt f x
⊢ E

Tactic:
exact 0
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : ¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f x = 0

Tactic:
simp [meromorphicTrailingCoeffAt, h]

Premises used: meromorphicTrailingCoeffAt
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt f x = 0

Tactic:
simp_all [meromorphicTrailingCoeffAt]

Premises used: meromorphicTrailingCoeffAt
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
rw : MeromorphicAt.{u_1, u_2} (E := E) (fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x
⊢ MeromorphicAt f x

Tactic:
rw [MeromorphicAt.meromorphicAt_congr h]

Premises used: MeromorphicAt.meromorphicAt_congr
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ MeromorphicAt.{u_1, u_2} (E := E) (fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ MeromorphicAt f x

Tactic:
have h₁f : MeromorphicAt f x := by
    rw [MeromorphicAt.meromorphicAt_congr h]
    fun_prop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
pos : ∀ (h₃ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f x = g x
neg : ∀ (h₃ : ¬meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt f x = g x
⊢ meromorphicTrailingCoeffAt f x = g x

Tactic:
by_cases h₃ : meromorphicOrderAt f x = ⊤

Premises used: meromorphicOrderAt