-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma add {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    MeromorphicAt (f + g) x

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
⊢ MeromorphicAt (f + g) x

Tactic:
rcases hf with ⟨m, hf⟩

Result:
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
hg : MeromorphicAt g x
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
⊢ MeromorphicAt (f + g) x

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
⊢ AnalyticAt 𝕜 (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) x

Tactic:
have : (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦ (z - x) ^ (max m n - m) •
    ((z - x) ^ m • f z) + (z - x) ^ (max m n - n) • ((z - x) ^ n • g z) := by
  simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _),
    Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add]

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
this :
  (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) = fun z =>
    (z - x) ^ (m ⊔ n - m) • (z - x) ^ m • f z + (z - x) ^ (m ⊔ n - n) • (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) x

Proof state:
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
hg : MeromorphicAt g x
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
⊢ MeromorphicAt (f + g) x

Tactic:
rcases hg with ⟨n, hg⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
⊢ MeromorphicAt (f + g) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
⊢ (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) = fun z =>
    (z - x) ^ (m ⊔ n - m) • (z - x) ^ m • f z + (z - x) ^ (m ⊔ n - n) • (z - x) ^ n • g z

Tactic:
simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _),
  Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add]

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
this :
  (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) = fun z =>
    (z - x) ^ (m ⊔ n - m) • (z - x) ^ m • f z + (z - x) ^ (m ⊔ n - n) • (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) x

Tactic:
rw [this]

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
this :
  (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) = fun z =>
    (z - x) ^ (m ⊔ n - m) • (z - x) ^ m • f z + (z - x) ^ (m ⊔ n - n) • (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z => (z - x) ^ (m ⊔ n - m) • (z - x) ^ m • f z + (z - x) ^ (m ⊔ n - n) • (z - x) ^ n • g z) x

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
this :
  (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) = fun z =>
    (z - x) ^ (m ⊔ n - m) • (z - x) ^ m • f z + (z - x) ^ (m ⊔ n - n) • (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z => (z - x) ^ (m ⊔ n - m) • (z - x) ^ m • f z + (z - x) ^ (m ⊔ n - n) • (z - x) ^ n • g z) x

Tactic:
exact (((analyticAt_id.sub analyticAt_const).pow _).smul hf).add
 (((analyticAt_id.sub analyticAt_const).pow _).smul hg)

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
⊢ MeromorphicAt (f + g) x

Tactic:
refine ⟨max m n, ?_⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x
⊢ AnalyticAt 𝕜 (fun z => (z - x) ^ (m ⊔ n) • (f + g) z) x