no goals
α : Type u_2
β : Type ?u.130294
γ : Type ?u.130297
ι : Type ?u.130300
M : Type u_1
M' : Type ?u.130306
N : Type ?u.130309
P : Type ?u.130312
G : Type ?u.130315
H : Type ?u.130318
R : Type ?u.130321
S : Type ?u.130324
inst✝ : Zero M
a a' : α
b✝ : M
a₁ a₂ : α
b : M
⊢ ↑(single a₁ b) a₂ = ↑(single a₂ b) a₁
classical simp only [single_apply, eq_comm]
no goals
α : Type u_2
β : Type ?u.130294
γ : Type ?u.130297
ι : Type ?u.130300
M : Type u_1
M' : Type ?u.130306
N : Type ?u.130309
P : Type ?u.130312
G : Type ?u.130315
H : Type ?u.130318
R : Type ?u.130321
S : Type ?u.130324
inst✝ : Zero M
a a' : α
b✝ : M
a₁ a₂ : α
b : M
⊢ ↑(single a₁ b) a₂ = ↑(single a₂ b) a₁
simp only [single_apply, eq_comm]