case pos
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a = 0
⊢ a ^ 2 * b / a = a * b

case neg
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : ¬a = 0
⊢ a ^ 2 * b / a = a * b
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
⊢ a ^ 2 * b / a = a * b
by_cases ha : a = 0
no goals
case neg
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : ¬a = 0
⊢ a ^ 2 * b / a = a * b
rw [sq, mul_assoc, mul_div_cancel_left _ ha]
no goals
case pos
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a = 0
⊢ a ^ 2 * b / a = a * b
simp [ha]