[GOAL]
a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
⊢ a = c / b * d
[PROOFSTEP]
cases' hbc with k hk
[GOAL]
case intro
a b c d : ℤ
hb : b ≠ 0
h : b * a = c * d
k : ℤ
hk : c = b * k
⊢ a = c / b * d
[PROOFSTEP]
subst hk
[GOAL]
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d
[PROOFSTEP]
rw [Int.mul_ediv_cancel_left _ hb]
[GOAL]
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
[PROOFSTEP]
rw [mul_assoc] at h 
[GOAL]
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * (k * d)
⊢ a = k * d
[PROOFSTEP]
apply mul_left_cancel₀ hb h
[GOAL]
a b : ℤ
w : a ∣ b
h : natAbs b < natAbs a
⊢ b = 0
[PROOFSTEP]
rw [← natAbs_dvd, ← dvd_natAbs, coe_nat_dvd] at w 
[GOAL]
a b : ℤ
w : natAbs a ∣ natAbs b
h : natAbs b < natAbs a
⊢ b = 0
[PROOFSTEP]
rw [← natAbs_eq_zero]
[GOAL]
a b : ℤ
w : natAbs a ∣ natAbs b
h : natAbs b < natAbs a
⊢ natAbs b = 0
[PROOFSTEP]
exact eq_zero_of_dvd_of_lt w h
[GOAL]
m n : ℕ
h : Nat.succ n ≤ m
⊢ ofNat m + -[n+1] = ofNat (m - Nat.succ n)
[PROOFSTEP]
rw [negSucc_eq, ofNat_eq_cast, ofNat_eq_cast, ← Nat.cast_one, ← Nat.cast_add, ← sub_eq_add_neg, ← Nat.cast_sub h]
