Theorem: Nat.mul_sub_mod_left (Algdata/Init/Nat.lean)

State before:
l m n : Nat
⊢ m > 0 → l ≥ n → (l * m - n) % l = (l - n) % l
Tactic:
intro hm hln
State after:
l m n : Nat
hm : m > 0
hln : l ≥ n
⊢ (l * m - n) % l = (l - n) % l

State before:
l m n : Nat
hm : m > 0
hln : l ≥ n
⊢ (l * m - n) % l = (l - n) % l
Tactic:
cases hm
State after:
case refl
l n : Nat
hln : l ≥ n
⊢ (l * succ 0 - n) % l = (l - n) % l

case step
l n : Nat
hln : l ≥ n
m✝ : Nat
a✝ : Nat.le (succ 0) m✝
⊢ (l * succ m✝ - n) % l = (l - n) % l

State before:
l n : Nat
hln : l ≥ n
⊢ (l * succ 0 - n) % l = (l - n) % l
Tactic:
case refl => rw [Nat.mul_one]
State after:
no goals

State before:
l n : Nat
hln : l ≥ n
m✝ : Nat
a✝ : Nat.le (succ 0) m✝
⊢ (l * succ m✝ - n) % l = (l - n) % l
Tactic:
case step _ _ =>
  rw [mul_succ, Nat.add_sub_assoc hln, Nat.add_comm, Nat.add_mul_mod_self_left]
State after:
no goals

State before:
l n : Nat
hln : l ≥ n
⊢ (l * succ 0 - n) % l = (l - n) % l
Tactic:
rw [Nat.mul_one]
State after:
no goals

State before:
l n : Nat
hln : l ≥ n
m✝ : Nat
a✝ : Nat.le (succ 0) m✝
⊢ (l * succ m✝ - n) % l = (l - n) % l
Tactic:
rw [mul_succ, Nat.add_sub_assoc hln, Nat.add_comm, Nat.add_mul_mod_self_left]
State after:
no goals