R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ (Finset.sum Finset.univ fun x => Finsupp.single i a) = Finsupp.single i a

case w
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ ∀ (x : n), x ∈ {i} → Finsupp.single x (if i = x then a else 0) = Finsupp.single i a

case w'
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ ∀ (x : n), ¬x ∈ {i} → Finsupp.single x (if i = x then a else 0) = 0
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ (Finset.sum Finset.univ fun x => Finsupp.single x (if i = x then a else 0)) = Finsupp.single i a
rw [Finset.sum_congr_set {i} (fun x : n => Finsupp.single x (ite (i = x) a 0)) fun _ =>
    Finsupp.single i a]
case w'
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
⊢ Finsupp.single x (if i = x then a else 0) = 0
case w'
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ ∀ (x : n), ¬x ∈ {i} → Finsupp.single x (if i = x then a else 0) = 0
intro x hx
case w'
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
hx' : ¬i = x
⊢ Finsupp.single x (if i = x then a else 0) = 0
case w'
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
⊢ Finsupp.single x (if i = x then a else 0) = 0
have hx' : ¬i = x := by
  refine' ne_comm.mp _
  rwa [mem_singleton_iff] at hx
no goals
case w'
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
hx' : ¬i = x
⊢ Finsupp.single x (if i = x then a else 0) = 0
simp [hx']
no goals
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ (Finset.sum Finset.univ fun x => Finsupp.single i a) = Finsupp.single i a
simp
case w
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : x ∈ {i}
⊢ Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
case w
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ ∀ (x : n), x ∈ {i} → Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
intro x hx
case w
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : x = i
⊢ Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
case w
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : x ∈ {i}
⊢ Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
rw [Set.mem_singleton_iff] at hx
no goals
case w
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : x = i
⊢ Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
simp [hx]
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
⊢ x ≠ i
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
⊢ ¬i = x
refine' ne_comm.mp _
no goals
R : Type u_1
M : Type ?u.93176
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
⊢ x ≠ i
rwa [mem_singleton_iff] at hx