case h.h
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ ↑(symm (mulLeft₀' ha)) x✝ = ↑(mulLeft₀' (_ : a⁻¹ ≠ 0)) x✝
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
⊢ symm (mulLeft₀' ha) = mulLeft₀' (_ : a⁻¹ ≠ 0)
ext
no goals
case h.h
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ ↑(symm (mulLeft₀' ha)) x✝ = ↑(mulLeft₀' (_ : a⁻¹ ≠ 0)) x✝
rfl