case a
R : Type u
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
⊢ op (star (x / y)) = op (star x / star y)
R : Type u
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
⊢ star (x / y) = star x / star y
apply op_injective
no goals
case a
R : Type u
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
⊢ op (star (x / y)) = op (star x / star y)
rw [division_def, op_div, mul_comm, star_mul, star_inv', op_mul, op_inv]