-- Mathlib/Analysis/Meromorphic/Order.lean
theorem order_smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} {x : 𝕜}
    (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    (hf.smul hg).order = hf.order + hg.order

Proof state:
case coe.coe.intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Tactic:
obtain ⟨G, h₁G, h₂G, h₃G⟩ := (hg.order_eq_int_iff _).1 h₂g

Result:
case coe.coe.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Proof state:
case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0

Tactic:
filter_upwards [h₂f] with z hz using by simp [hz]

Result:
no goals

Proof state:
case coe.top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0

Tactic:
filter_upwards [h₂g] with z hz using by simp [hz]

Result:
no goals

Proof state:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • (F • G) z

Tactic:
filter_upwards [self_mem_nhdsWithin, h₃F, h₃G] with a ha hfa hga

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
a : 𝕜
ha : a ∈ {x}ᶜ
hfa : f a = (a - x) ^ m • F a
hga : g a = (a - x) ^ n • G a
⊢ (f • g) a = (a - x) ^ (m + n) • (F • G) a

Proof state:
case coe.coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
⊢ ⋯.order = ↑m + ↑n

Tactic:
rw [← WithTop.coe_add, order_eq_int_iff]

Result:
case coe.coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Proof state:
case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₂f : hf.order = ⊤
⊢ ⋯.order = ⊤ + hg.order

Tactic:
simp only [top_add, order_eq_top_iff] at h₂f ⊢

Result:
case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0

Proof state:
case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
⊢ ⋯.order = ↑m + hg.order

Tactic:
cases h₂g : hg.order with
| top =>
  simp only [add_top, order_eq_top_iff] at h₂g ⊢
  filter_upwards [h₂g] with z hz using by simp [hz]
| coe n => rw [← WithTop.coe_add, order_eq_int_iff]
  obtain ⟨F, h₁F, h₂F, h₃F⟩ := (hf.order_eq_int_iff _).1 h₂f
  obtain ⟨G, h₁G, h₂G, h₃G⟩ := (hg.order_eq_int_iff _).1 h₂g
  use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]
  filter_upwards [self_mem_nhdsWithin, h₃F, h₃G] with a ha hfa hga
  simp [hfa, hga, smul_comm (F a), zpow_add₀ (sub_ne_zero.mpr ha), mul_smul]

Result:
no goals

Proof state:
case coe.coe.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Tactic:
use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]

Result:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • (F • G) z

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
n : ℤ
h₂g : hg.order = ↑n
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
⊢ (F • G) x ≠ 0

Tactic:
simp [h₂F, h₂G]

Result:
no goals

Proof state:
case coe.top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
h₂g : hg.order = ⊤
⊢ ⋯.order = ↑m + ⊤

Tactic:
simp only [add_top, order_eq_top_iff] at h₂g ⊢

Result:
case coe.top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → 𝕜
g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : hf.order = ↑m
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0