-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    MeromorphicAt (f • g) 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:
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 ⟨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

Proof state:
case h.e'_9.h
𝕜 : 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
z : 𝕜
⊢ (z - x) ^ (m + n) • (f • g) z = ((z - x) ^ m • f z) • (z - x) ^ n • g z

Tactic:
rw [Pi.smul_apply', smul_eq_mul]

Result:
case h.e'_9.h
𝕜 : 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
z : 𝕜
⊢ (z - x) ^ (m + n) • f z • g z = ((z - x) ^ m * f z) • (z - x) ^ n • g z

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:
convert hf.smul' hg using 2 with z

Result:
case h.e'_9.h
𝕜 : 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
z : 𝕜
⊢ (z - x) ^ (m + n) • (f • g) z = ((z - x) ^ m • f z) • (z - x) ^ n • 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
⊢ 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 h.e'_9.h
𝕜 : 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
z : 𝕜
⊢ (z - x) ^ (m + n) • f z • g z = ((z - x) ^ m * f z) • (z - x) ^ n • g z

Tactic:
module

Result:
no goals