Theorem: sub_mul_mod_self_left (Fl/Lemmas.lean)

State before:
x y z : ℕ
h : y * z ≤ x
⊢ (x - y * z) % y = x % y
Tactic:
match z with
| 0 => rw [Nat.mul_zero, tsub_zero]
| Nat.succ z =>
  rewrite [Nat.mul_succ] at h
  have k : y * z ≤ x := Nat.le_trans (Nat.le_add_right _ _) h
  have l : y ≤ x - y * z := le_tsub_of_add_le_left h
  rewrite [Nat.mul_succ]
  rewrite [← tsub_tsub]
  rewrite [← Nat.mod_eq_sub_mod l]
  exact sub_mul_mod_self_left x y z k
State after:
no goals

State before:
x y z : ℕ
h : y * 0 ≤ x
⊢ (x - y * 0) % y = x % y
Tactic:
rw [Nat.mul_zero, tsub_zero]
State after:
no goals

State before:
x y z✝ z : ℕ
h : y * Nat.succ z ≤ x
⊢ (x - y * Nat.succ z) % y = x % y
Tactic:
rewrite [Nat.mul_succ] at h
State after:
x y z✝ z : ℕ
h : y * z + y ≤ x
⊢ (x - y * Nat.succ z) % y = x % y

State before:
x y z✝ z : ℕ
h : y * z + y ≤ x
⊢ (x - y * Nat.succ z) % y = x % y
Tactic:
have k : y * z ≤ x := Nat.le_trans (Nat.le_add_right _ _) h
State after:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
⊢ (x - y * Nat.succ z) % y = x % y

State before:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
⊢ (x - y * Nat.succ z) % y = x % y
Tactic:
have l : y ≤ x - y * z := le_tsub_of_add_le_left h
State after:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - y * Nat.succ z) % y = x % y

State before:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - y * Nat.succ z) % y = x % y
Tactic:
rewrite [Nat.mul_succ]
State after:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - (y * z + y)) % y = x % y

State before:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - (y * z + y)) % y = x % y
Tactic:
rewrite [← tsub_tsub]
State after:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - y * z - y) % y = x % y

State before:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - y * z - y) % y = x % y
Tactic:
rewrite [← Nat.mod_eq_sub_mod l]
State after:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - y * z) % y = x % y

State before:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - y * z) % y = x % y
Tactic:
exact sub_mul_mod_self_left x y z k
State after:
no goals