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

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
⊢ d ∣ a % b
Tactic:
set q : Nat := a / b
State after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
⊢ d ∣ a % b

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
⊢ d ∣ a % b
Tactic:
have h3 : b * q + a % b = a := Nat.div_add_mod a b
State after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
⊢ d ∣ a % b

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
⊢ d ∣ a % b
Tactic:
obtain (j : Nat) (h4 : a = d * j) from h1
State after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
⊢ d ∣ a % b

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
⊢ d ∣ a % b
Tactic:
obtain (k : Nat) (h5 : b = d * k) from h2
State after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ d ∣ a % b

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ d ∣ a % b
Tactic:
define
State after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ∃ c, a % b = d * c

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ∃ c, a % b = d * c
Tactic:
apply Exists.intro (j - k * q)
State after:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ a % b = d * (j - k * q)

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ a % b = d * (j - k * q)
Tactic:
show a % b = d * (j - k * q) from
  calc a % b
    _ = b * q + a % b - b * q := (Nat.add_sub_cancel_left _ _).symm
    _ = a - b * q := by rw [h3]
    _ = d * j - d * (k * q) := by rw [h4, h5, mul_assoc]
    _ = d * (j - k * q) := (Nat.mul_sub_left_distrib _ _ _).symm
State after:
no goals

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ b * q + a % b - b * q = a - b * q
Tactic:
rw [h3]
State after:
no goals

State before:
a b d : ℕ
h1 : d ∣ a
h2 : d ∣ b
q : ℕ := a / b
h3 : b * q + a % b = a
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ a - b * q = d * j - d * (k * q)
Tactic:
rw [h4, h5, mul_assoc]
State after:
no goals