awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g⁻¹ z
⊢ ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g z

Tactic:
use g⁻¹, h₁g.inv h₂g, inv_eq_zero.not.2 h₂g

Premises used: Iff.mpr, inv_eq_zero, Iff.not, AnalyticAt.inv
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
right :
  ∀ (h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ a • g x_1),
    ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
      Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f⁻¹ x_1 = HPow.hPow (β := ℤ) (x_1 - x) ((fun (a : ℤ) ↦ -a) a) • g⁻¹ x_1
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = HPow.hPow (β := ℤ) (z - x) ((fun (a : ℤ) ↦ -a) a) • g⁻¹ z

Tactic:
rw [eventually_nhdsWithin_iff] at *

Premises used: eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ a • g x_1
h :
  ∀ (a_1 : 𝕜),
    (Membership.mem (γ := Set 𝕜) {x}ᶜ a_1 → f a_1 = (a_1 - x) ^ a • g a_1) →
      Membership.mem (γ := Set 𝕜) {x}ᶜ a_1 → f⁻¹ a_1 = (a_1 - x) ^ (-a) • g⁻¹ a_1
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f⁻¹ x_1 = HPow.hPow (β := ℤ) (x_1 - x) ((fun (a : ℤ) ↦ -a) a) • g⁻¹ x_1

Tactic:
filter_upwards [h₃g]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ a • g x_1
a_1 : 𝕜
h₁a : Membership.mem (γ := Set 𝕜) {x}ᶜ a_1 → f a_1 = (a_1 - x) ^ a • g a_1
h₂a : Membership.mem (γ := Set 𝕜) {x}ᶜ a_1
h : (g a_1)⁻¹ * ((a_1 - x) ^ a)⁻¹ = ((a_1 - x) ^ a)⁻¹ * (g a_1)⁻¹
⊢ f⁻¹ a_1 = (a_1 - x) ^ (-a) • g⁻¹ a_1

Tactic:
simp only [Pi.inv_apply, h₁a h₂a, smul_eq_mul, mul_inv_rev, zpow_neg]

Premises used: zpow_neg, mul_inv_rev, smul_eq_mul, Pi.inv_apply
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicAt f x
a : ℤ
ha : (↑a : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ a • g x_1
a_1 : 𝕜
h₁a : Membership.mem (γ := Set 𝕜) {x}ᶜ a_1 → f a_1 = (a_1 - x) ^ a • g a_1
h₂a : Membership.mem (γ := Set 𝕜) {x}ᶜ a_1
⊢ (g a_1)⁻¹ * ((a_1 - x) ^ a)⁻¹ = ((a_1 - x) ^ a)⁻¹ * (g a_1)⁻¹

Tactic:
ring
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f g : 𝕜 → 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
rw : meromorphicOrderAt (f * g⁻¹) x = meromorphicOrderAt f x - meromorphicOrderAt g x
rw₁ : meromorphicOrderAt f x + meromorphicOrderAt g⁻¹ x = meromorphicOrderAt f x - meromorphicOrderAt g x
rw₂ : meromorphicOrderAt f x + -meromorphicOrderAt g x = meromorphicOrderAt f x - meromorphicOrderAt g x
rw₃ rw₄ : meromorphicOrderAt f x + -meromorphicOrderAt g x = meromorphicOrderAt f x + -meromorphicOrderAt g x
⊢ meromorphicOrderAt (f / g) x = meromorphicOrderAt f x - meromorphicOrderAt g x

Tactic:
rw [div_eq_mul_inv, meromorphicOrderAt_mul hf hg.inv, meromorphicOrderAt_inv, sub_eq_add_neg]

Premises used: meromorphicOrderAt_mul, sub_eq_add_neg, meromorphicOrderAt_inv, div_eq_mul_inv, MeromorphicAt.inv
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : meromorphicOrderAt f₁ x = ⊤
rw : f₁ + f₂ =ᶠ[𝓝[≠] x] f₂
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x

Tactic:
rw [meromorphicOrderAt_congr]

Premises used: 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
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : meromorphicOrderAt f₁ x = ⊤
h : ∀ (z : 𝕜) (hz : f₁ z = 0), (f₁ + f₂) z = f₂ z
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] f₂

Tactic:
filter_upwards [meromorphicOrderAt_eq_top_iff.1 hf₁] with z hz

Premises used: meromorphicOrderAt_eq_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : meromorphicOrderAt f₁ x = ⊤
z : 𝕜
hz : f₁ z = 0
⊢ (f₁ + f₂) z = f₂ z

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : meromorphicOrderAt f₂ x = ⊤
rw : meromorphicOrderAt (f₂ + f₁) x = meromorphicOrderAt f₁ x
rw₁ rw₂ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Tactic:
rw [add_comm, meromorphicOrderAt_add_of_top_left hf₂]

Premises used: meromorphicOrderAt_add_of_top_left, add_comm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
pos :
  ∀ (h₂f₁ : meromorphicOrderAt f₁ x = ⊤),
    min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
neg :
  ∀ (h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤),
    min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
by_cases h₂f₁ : meromorphicOrderAt f₁ x = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : meromorphicOrderAt f₁ x = ⊤
pos : f₂ =ᶠ[𝓝[≠] x] f₁ + f₂
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
rw [h₂f₁, min_top_left, meromorphicOrderAt_congr]

Premises used: min_top_left, 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
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : meromorphicOrderAt f₁ x = ⊤
h : ∀ (a : 𝕜), f₁ a = 0 → f₂ a = (f₁ + f₂) a
⊢ f₂ =ᶠ[𝓝[≠] x] f₁ + f₂

Tactic:
filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₂f₁]

Premises used: meromorphicOrderAt_eq_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ ∀ (a : 𝕜), f₁ a = 0 → f₂ a = (f₁ + f₂) a

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
pos :
  ∀ (h₂f₂ : meromorphicOrderAt f₂ x = ⊤),
    min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
neg :
  ∀ (h₂f₂ : ¬meromorphicOrderAt f₂ x = ⊤),
    min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
by_cases h₂f₂ : meromorphicOrderAt f₂ x = ⊤

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

Tactic:
simp only [h₂f₂, le_top, inf_of_le_left]

Premises used: inf_of_le_left, le_top
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₂f₂ : meromorphicOrderAt f₂ x = ⊤
pos : f₁ =ᶠ[𝓝[≠] x] f₁ + f₂
⊢ meromorphicOrderAt f₁ x ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
rw [meromorphicOrderAt_congr]

Premises used: 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
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₂f₂ : meromorphicOrderAt f₂ x = ⊤
h : ∀ (a : 𝕜), f₂ a = 0 → f₁ a = (f₁ + f₂) a
⊢ f₁ =ᶠ[𝓝[≠] x] f₁ + f₂

Tactic:
filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₂f₂]

Premises used: meromorphicOrderAt_eq_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₂f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ ∀ (a : 𝕜), f₂ a = 0 → f₁ a = (f₁ + f₂) a

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

Tactic:
h₂f₁
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₂f₂ : ¬meromorphicOrderAt f₂ x = ⊤
neg :
  ∀ (n₁ : ℤ) (hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x)
    (meromorphicOrderAt_add :
      ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
        min (↑n₁ : WithTop ℤ) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x),
    min (↑n₁ : WithTop ℤ) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
lift meromorphicOrderAt f₁ x to ℤ using h₂f₁ with n₁ hn₁

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₂ : ¬meromorphicOrderAt f₂ x = ⊤
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ meromorphicOrderAt f₂ x ≠ ⊤

Tactic:
h₂f₂
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂f₂ : ¬meromorphicOrderAt f₂ x = ⊤
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
neg :
  ∀ (n₂ : ℤ) (hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x)
    (meromorphicOrderAt_add :
      ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
        min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ min (↑n₁ : WithTop ℤ) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
lift meromorphicOrderAt f₂ x to ℤ using h₂f₂ with n₂ hn₂

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
neg :
  ∀ (g₁ : 𝕜 → E) (h₁g₁ : AnalyticAt 𝕜 g₁ x) (h₂g₁ : g₁ x ≠ 0) (h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn₁.symm

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
neg :
  ∀ (g₂ : 𝕜 → E) (h₁g₂ : AnalyticAt 𝕜 g₂ x) (h₂g₂ : g₂ x ≠ 0) (h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
⊢ min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E :=
  HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁ +
    HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂
hf : AnalyticAt 𝕜 (HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁) x
hg : AnalyticAt 𝕜 (HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂) x
⊢ AnalyticAt 𝕜 g x

Tactic:
apply AnalyticAt.add

Premises used: AnalyticAt.add
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E :=
  HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁ +
    HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - 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
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E :=
  HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁ +
    HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂
⊢ AnalyticAt 𝕜 (HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁) x

Tactic:
apply (AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (min_le_left n₁ n₂))).smul h₁g₁

Premises used: Iff.mpr, AnalyticAt.smul, min_le_left, AnalyticAt.zpow_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E :=
  HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁ +
    HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂
⊢ AnalyticAt 𝕜 (HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂) x

Tactic:
apply (AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (min_le_right n₁ n₂))).smul h₁g₂

Premises used: Iff.mpr, AnalyticAt.smul, AnalyticAt.zpow_nonneg, min_le_right, sub_nonneg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E :=
  HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁ +
    HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂
⊢ AnalyticAt 𝕜 g x

Tactic:
have h₁g : AnalyticAt 𝕜 g x := by
    apply AnalyticAt.add
    · apply (AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (min_le_left n₁ n₂))).smul h₁g₁
    apply (AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (min_le_right n₁ n₂))).smul h₁g₂
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E :=
  HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁ +
    HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂
h₁g : AnalyticAt 𝕜 g x
h :
  ∀ (a : 𝕜),
    f₁ a = (a - x) ^ n₁ • g₁ a →
      f₂ a = (a - x) ^ n₂ • g₂ a →
        Membership.mem (γ := Set 𝕜) {x}ᶜ a → (f₁ + f₂) a = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) a
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add :
  ∀ (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x),
    min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E :=
  HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₁ - n)) g₁ +
    HSMul.hSMul (α := (z : 𝕜) → 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (n₂ - n)) g₂
h₁g : AnalyticAt 𝕜 g x
⊢ ∀ (a : 𝕜),
    f₁ a = (a - x) ^ n₁ • g₁ a →
      f₂ a = (a - x) ^ n₂ • g₂ a →
        Membership.mem (γ := Set 𝕜) {x}ᶜ a → (f₁ + f₂) a = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) a

Tactic:
simp_all [g, ← smul_assoc, ← zpow_add', sub_ne_zero]

Premises used: smul_assoc, sub_ne_zero, zpow_add'