Theorem: Aux.sum_intro (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = ∑ k ∈ s, if k = d then f k else 0
Tactic:
trans (∑ k in s, if k = d then f d else 0)
State after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = ∑ k ∈ s, if k = d then f d else 0

α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ (∑ k ∈ s, if k = d then f d else 0) = ∑ k ∈ s, if k = d then f k else 0

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ (∑ k ∈ s, if k = d then f d else 0) = ∑ k ∈ s, if k = d then f k else 0
Tactic:
apply sum_congr rfl
State after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ x ∈ s, (if x = d then f d else 0) = if x = d then f x else 0

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ x ∈ s, (if x = d then f d else 0) = if x = d then f x else 0
Tactic:
intro k _
State after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ (if k = d then f d else 0) = if k = d then f k else 0

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ (if k = d then f d else 0) = if k = d then f k else 0
Tactic:
apply if_ctx_congr Iff.rfl _ (fun _ => rfl)
State after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ k = d → f d = f k

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ k = d → f d = f k
Tactic:
intro h
State after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
h : k = d
⊢ f d = f k

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
h : k = d
⊢ f d = f k
Tactic:
rw [h]
State after:
no goals

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = ∑ k ∈ s, if k = d then f d else 0
Tactic:
rw [sum_eq_single_of_mem d hd]
State after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = if d = d then f d else 0

α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = if d = d then f d else 0

α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0
Tactic:
rw [if_pos rfl]
State after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0
Tactic:
intro _ _ h
State after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ d
⊢ (if b✝ = d then f d else 0) = 0

State before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ d
⊢ (if b✝ = d then f d else 0) = 0
Tactic:
rw [if_neg h]
State after:
no goals