no goals
α : Type u_2
β : Type ?u.473549
γ : Type ?u.473552
ι : Type ?u.473555
M : Type u_1
M' : Type ?u.473561
N : Type ?u.473564
P : Type ?u.473567
G : Type ?u.473570
H : Type ?u.473573
R : Type ?u.473576
S : Type ?u.473579
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
classical
  simp_rw [FunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
  exact Pi.single_add_single_eq_single_add_single hu hv
α : Type u_2
β : Type ?u.473549
γ : Type ?u.473552
ι : Type ?u.473555
M : Type u_1
M' : Type ?u.473561
N : Type ?u.473564
P : Type ?u.473567
G : Type ?u.473570
H : Type ?u.473573
R : Type ?u.473576
S : Type ?u.473579
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ ((fun a => (Pi.single k u + Pi.single l v) a) = fun a => (Pi.single m u + Pi.single n v) a) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
α : Type u_2
β : Type ?u.473549
γ : Type ?u.473552
ι : Type ?u.473555
M : Type u_1
M' : Type ?u.473561
N : Type ?u.473564
P : Type ?u.473567
G : Type ?u.473570
H : Type ?u.473573
R : Type ?u.473576
S : Type ?u.473579
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
simp_rw [FunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
no goals
α : Type u_2
β : Type ?u.473549
γ : Type ?u.473552
ι : Type ?u.473555
M : Type u_1
M' : Type ?u.473561
N : Type ?u.473564
P : Type ?u.473567
G : Type ?u.473570
H : Type ?u.473573
R : Type ?u.473576
S : Type ?u.473579
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ ((fun a => (Pi.single k u + Pi.single l v) a) = fun a => (Pi.single m u + Pi.single n v) a) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
exact Pi.single_add_single_eq_single_add_single hu hv