Theorem: LSeries.term_mul (EulerProducts/EulerProduct.lean)

State before:
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Tactic:
rcases eq_or_ne (m * n) 0 with H | H
State after:
case inl
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n = 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n

case inr
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n ≠ 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n

State before:
case inl
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n = 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Tactic:
rcases mul_eq_zero.mp H with rfl | rfl <;> simp only [term_zero, mul_zero, zero_mul]
State after:
no goals

State before:
case inr
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n ≠ 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Tactic:
obtain ⟨hm, hn⟩ := mul_ne_zero_iff.mp H
State after:
case inr.intro
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n ≠ 0
hm : m ≠ 0
hn : n ≠ 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n

State before:
case inr.intro
f₁ f₂ f : ℕ → ℂ
m n : ℕ
h : f (m * n) = f₁ m * f₂ n
s : ℂ
H : m * n ≠ 0
hm : m ≠ 0
hn : n ≠ 0
⊢ term f s (m * n) = term f₁ s m * term f₂ s n
Tactic:
simp only [ne_eq, H, not_false_eq_true, term_of_ne_zero, Nat.cast_mul, hm, hn, h, term_mul_aux]
State after:
no goals