no goals
α : Type u_1
β : Type u_2
γ : Type ?u.38931
ι : Type ?u.38934
M : Type u_3
M' : Type ?u.38940
N : Type ?u.38943
P : Type ?u.38946
G : Type ?u.38949
H : Type ?u.38952
R : Type ?u.38955
S : Type ?u.38958
inst✝ : Zero M
a a' : α
b : M
f : α → β
hf : Injective f
x z : α
y : M
⊢ ↑(single (f x) y) (f z) = ↑(single x y) z
classical simp only [single_apply, hf.eq_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.38931
ι : Type ?u.38934
M : Type u_3
M' : Type ?u.38940
N : Type ?u.38943
P : Type ?u.38946
G : Type ?u.38949
H : Type ?u.38952
R : Type ?u.38955
S : Type ?u.38958
inst✝ : Zero M
a a' : α
b : M
f : α → β
hf : Injective f
x z : α
y : M
⊢ ↑(single (f x) y) (f z) = ↑(single x y) z
simp only [single_apply, hf.eq_iff]