α : Type ?u.19055
M₀ : Type ?u.19058
G₀ : Type u_1
M₀' : Type ?u.19064
G₀' : Type ?u.19067
F : Type ?u.19070
F' : Type ?u.19073
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b⁻¹ ≠ 0
α : Type ?u.19055
M₀ : Type ?u.19058
G₀ : Type u_1
M₀' : Type ?u.19064
G₀' : Type ?u.19067
F : Type ?u.19070
F' : Type ?u.19073
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a / b ≠ 0
rw [div_eq_mul_inv]
no goals
α : Type ?u.19055
M₀ : Type ?u.19058
G₀ : Type u_1
M₀' : Type ?u.19064
G₀' : Type ?u.19067
F : Type ?u.19070
F' : Type ?u.19073
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b⁻¹ ≠ 0
exact mul_ne_zero ha (inv_ne_zero hb)