no goals
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime (x • y) z
a b : R
h : a * x • y + b * z = 1
⊢ x • a * y + b * z = 1
rwa [smul_mul_assoc, ← mul_smul_comm]
no goals
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime y z
a b : R
h : a * y + b * z = 1
⊢ x⁻¹ • a * x • y + b * z = 1
rwa [smul_mul_smul, inv_mul_self, one_smul]