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

State before:
a m n : Nat
⊢ m > 0 → m ≤ n → a % m % n = a % m
Tactic:
intro hm hle
State after:
a m n : Nat
hm : m > 0
hle : m ≤ n
⊢ a % m % n = a % m

State before:
a m n : Nat
hm : m > 0
hle : m ≤ n
⊢ a % m % n = a % m
Tactic:
have : a % m < n := Trans.trans (Nat.mod_lt a hm) hle
State after:
a m n : Nat
hm : m > 0
hle : m ≤ n
this : a % m < n
⊢ a % m % n = a % m

State before:
a m n : Nat
hm : m > 0
hle : m ≤ n
this : a % m < n
⊢ a % m % n = a % m
Tactic:
rw [Nat.mod_eq_of_lt this]
State after:
no goals