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
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
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
have : f₁ + f₂ =ᶠ[𝓝[≠] x] ((· - x) ^ n) • g := by
    filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin]
    simp_all [g, ← smul_assoc, ← zpow_add', sub_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₁ 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
this : f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) 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₂
h₁g : AnalyticAt 𝕜 g x
this : f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x

Tactic:
have t₀ : MeromorphicAt ((· - x) ^ n) x := by 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₂
h₁g : AnalyticAt 𝕜 g x
this : f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
t₀ : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x
⊢ Ne.{u_1 + 1} (α := 𝕜) (1 x) 0 ∧
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
      HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n z = HSMul.hSMul (β := 𝕜) ((z - x) ^ n) (1 z)

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
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
this : f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
t₀ : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x
⊢ meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x = (↑n : WithTop ℤ)

Tactic:
have t₁ : meromorphicOrderAt ((· - x) ^ n) x = n :=
    (meromorphicOrderAt_eq_int_iff t₀).2 ⟨1, analyticAt_const, by 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
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
this : f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
t₀ : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x
t₁ : meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x = (↑n : WithTop ℤ)
neg : min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ (↑n : WithTop ℤ) + meromorphicOrderAt g x
⊢ min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ meromorphicOrderAt (f₁ + f₂) x

Tactic:
rw [meromorphicOrderAt_congr this, meromorphicOrderAt_smul t₀ h₁g.meromorphicAt, t₁]

Premises used: meromorphicOrderAt_smul, 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
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
this : f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
t₀ : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x
t₁ : meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x = (↑n : WithTop ℤ)
⊢ min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ (↑n : WithTop ℤ) + meromorphicOrderAt g x

Tactic:
le_add_of_nonneg_right h₁g.meromorphicOrderAt_nonneg

Premises used: AnalyticAt.meromorphicOrderAt_nonneg, le_add_of_nonneg_right
-- 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
this : f₁ + f₂ =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
t₀ : MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x
t₁ : meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x = (↑n : WithTop ℤ)
⊢ min (↑n₁ : WithTop ℤ) (↑n₂ : WithTop ℤ) ≤ (↑n : WithTop ℤ) + meromorphicOrderAt g x

Tactic:
exact le_add_of_nonneg_right h₁g.meromorphicOrderAt_nonneg

Premises used: AnalyticAt.meromorphicOrderAt_nonneg, le_add_of_nonneg_right
-- 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
pos : ∀ (hf₁ : MeromorphicAt f₁ x), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
neg : ∀ (hf₁ : ¬MeromorphicAt f₁ x), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
contrapose : ∀ (hf₁ : MeromorphicAt (f₁ + f₂) x), MeromorphicAt f₁ x
⊢ ¬MeromorphicAt (f₁ + f₂) x

Tactic:
contrapose hf₁
-- 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt (f₁ + f₂) x
⊢ MeromorphicAt f₁ x

Tactic:
simpa using hf₁.sub hf₂

Premises used: MeromorphicAt.sub
-- 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt (f₁ + f₂) x

Tactic:
have : ¬ (MeromorphicAt (f₁ + f₂) x) := by
      contrapose hf₁
      simpa using hf₁.sub hf₂
-- 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
this : ¬MeromorphicAt (f₁ + f₂) x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Tactic:
simp [this, hf₁]
-- 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
pos : ∀ (h₁f₂ : meromorphicOrderAt f₂ x = ⊤), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
neg : ∀ (h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
pos : 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₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
h₁ : ∀ (a : 𝕜), f₂ a = 0 → (f₁ + f₂) a = f₁ a
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ ∀ (a : 𝕜), f₂ a = 0 → (f₁ + f₂) a = 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt 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
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
neg :
  ∀ (n₂ : ℤ) (hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x)
    (meromorphicOrderAt_add_eq_left_of_lt :
      ∀ (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)),
        meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x)
    (h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)), meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt 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
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)
⊢ meromorphicOrderAt f₁ x ≠ ⊤

Tactic:
h.ne_top

Premises used: LT.lt.ne_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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
meromorphicOrderAt_add_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)
neg :
  ∀ (n₁ : ℤ) (hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x)
    (meromorphicOrderAt_add_eq_left_of_lt :
      ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
        meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ))
    (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)), meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

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

Premises used: LT.lt.ne_top, 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_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
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),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
⊢ meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)

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_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
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),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
⊢ meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)

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_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
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
neg : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • g z
⊢ meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)

Tactic:
rw [meromorphicOrderAt_eq_int_iff (hf₁.add hf₂)]

Premises used: meromorphicOrderAt_eq_int_iff, MeromorphicAt.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_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
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
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • g z

Tactic:
⟨g₁ + (· - x) ^ (n₂ - n₁) • g₂, ?_, ?_, ?_⟩

Premises used: HSub.hSub, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul
-- 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_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
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
neg : AnalyticAt 𝕜 (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x
neg₁ : (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x ≠ 0
neg₂ :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • g z

Tactic:
refine ⟨g₁ + (· - x) ^ (n₂ - n₁) • 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_eq_left_of_lt :
  ∀ (hf₂ : MeromorphicAt f₂ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
    meromorphicOrderAt (f₁ + f₂) x = (↑n₁ : WithTop ℤ)
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
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
apply : AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁)) x
⊢ AnalyticAt 𝕜 (g₁ + HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n₂ - n₁) • g₂) x

Tactic:
apply h₁g₁.add (AnalyticAt.smul _ h₁g₂)

Premises used: AnalyticAt.smul, AnalyticAt.add