α : Type u_1
β : Type ?u.226369
γ : Type ?u.226372
δ : Type ?u.226375
inst✝ : CancelCommMonoidWithZero α
a b c d : α
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : αˣ
hu : a * b * ↑u = c * d
v : αˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)
α : Type u_1
β : Type ?u.226369
γ : Type ?u.226372
δ : Type ?u.226375
inst✝ : CancelCommMonoidWithZero α
a b c d : α
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : αˣ
hu : a * b * ↑u = c * d
v : αˣ
hv : c * ↑v = a
⊢ a * (b * ↑(u * v)) = a * d
rw [← hv, mul_assoc c (v : α) d, mul_left_comm c, ← hu]
no goals
α : Type u_1
β : Type ?u.226369
γ : Type ?u.226372
δ : Type ?u.226375
inst✝ : CancelCommMonoidWithZero α
a b c d : α
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : αˣ
hu : a * b * ↑u = c * d
v : αˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)
simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]