Theorem: HTPI.Theorem_7_2_2_Int (HTPILib/Chap7.lean)

State before:
a c : ℕ
b : ℤ
h1 : ↑c ∣ ↑a * b
h2 : rel_prime a c
⊢ ↑c ∣ b
Tactic:
rewrite [Int.coe_nat_dvd_left, Int.natAbs_mul,
  Int.natAbs_ofNat] at h1
State after:
a c : ℕ
b : ℤ
h1 : c ∣ a * Int.natAbs b
h2 : rel_prime a c
⊢ ↑c ∣ b

State before:
a c : ℕ
b : ℤ
h1 : c ∣ a * Int.natAbs b
h2 : rel_prime a c
⊢ ↑c ∣ b
Tactic:
rewrite [Int.coe_nat_dvd_left]
State after:
a c : ℕ
b : ℤ
h1 : c ∣ a * Int.natAbs b
h2 : rel_prime a c
⊢ c ∣ Int.natAbs b

State before:
a c : ℕ
b : ℤ
h1 : c ∣ a * Int.natAbs b
h2 : rel_prime a c
⊢ c ∣ Int.natAbs b
Tactic:
show c ∣ Int.natAbs b from Theorem_7_2_2 h1 h2
State after:
no goals