Theorem: sum_primesBelow_eq_sum_range_indicator (EulerProducts/Logarithm.lean)

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n : ℕ
⊢ ∑ p ∈ n.primesBelow, f p = ∑ m ∈ Finset.range n, {p | p.Prime}.indicator f m
Tactic:
convert (Finset.sum_indicator_subset f Finset.mem_of_mem_filter).symm using 2 with _ _ m hm
State after:
case h.e'_3.a
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
⊢ {p | p.Prime}.indicator f m = (↑(Finset.filter (fun p => p.Prime) (Finset.range n))).indicator f m

State before:
case h.e'_3.a
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
⊢ {p | p.Prime}.indicator f m = (↑(Finset.filter (fun p => p.Prime) (Finset.range n))).indicator f m
Tactic:
simp only [Set.mem_setOf_eq, Finset.mem_range, Finset.coe_filter, not_and, Set.indicator_apply]
State after:
case h.e'_3.a
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
⊢ (if m.Prime then f m else 0) = if m < n ∧ m.Prime then f m else 0

State before:
case h.e'_3.a
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
⊢ (if m.Prime then f m else 0) = if m < n ∧ m.Prime then f m else 0
Tactic:
split_ifs with h₁ h₂ h₃
State after:
case pos
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : m.Prime
h₂ : m < n ∧ m.Prime
⊢ f m = f m

case neg
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : m.Prime
h₂ : ¬(m < n ∧ m.Prime)
⊢ f m = 0

case pos
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : ¬m.Prime
h₃ : m < n ∧ m.Prime
⊢ 0 = f m

case neg
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : ¬m.Prime
h₃ : ¬(m < n ∧ m.Prime)
⊢ 0 = 0

State before:
case pos
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : m.Prime
h₂ : m < n ∧ m.Prime
⊢ f m = f m
Tactic:
rfl
State after:
no goals

State before:
case neg
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : m.Prime
h₂ : ¬(m < n ∧ m.Prime)
⊢ f m = 0
Tactic:
exact (h₂ ⟨Finset.mem_range.mp hm, h₁⟩).elim
State after:
no goals

State before:
case pos
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : ¬m.Prime
h₃ : m < n ∧ m.Prime
⊢ 0 = f m
Tactic:
exact (h₁ h₃.2).elim
State after:
no goals

State before:
case neg
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : ¬m.Prime
h₃ : ¬(m < n ∧ m.Prime)
⊢ 0 = 0
Tactic:
rfl
State after:
no goals