a✝ b✝ : ℤ
n : ℕ
a b c d : ℤ
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * c / d
a✝ b✝ : ℤ
n : ℕ
a b c d : ℤ
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * (c / d)
rw [← Int.mul_ediv_assoc _ H2]
no goals
a✝ b✝ : ℤ
n : ℕ
a b c d : ℤ
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * c / d
exact (Int.ediv_eq_of_eq_mul_left H4 H5.symm).symm