no goals
α : Type u_2
β : Type ?u.118394
A : Type ?u.118397
B : Type ?u.118400
M : Type ?u.118403
N : Type ?u.118406
P : Type ?u.118409
R : Type u_1
S : Type ?u.118415
G : Type ?u.118418
M₀ : Type ?u.118421
G₀ : Type ?u.118424
ι : Sort ?u.118427
inst✝¹ : One R
inst✝ : AddGroup R
f : α → R
⊢ mulSupport (1 - f) = support f
rw [sub_eq_add_neg, mulSupport_one_add', support_neg']