no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a b c : A
h₁ : (↑↑ₐ r - a) * b = 1
h₂ : c * (↑↑ₐ r - a) = 1
⊢ b * (↑↑ₐ r - a) = 1
rwa [← left_inv_eq_right_inv h₂ h₁]