no goals
α : Type u
β : Type v
γ : Type w
inst✝⁵ : Group α
inst✝⁴ : Monoid β
inst✝³ : AddGroup β
inst✝² : DistribMulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
r : α
a : β
⊢ IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]