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

State before:
l m n : Nat
⊢ l % (m * n) / m = l / m % n
Tactic:
cases m.eq_zero_or_pos
State after:
case inl
l m n : Nat
h✝ : m = 0
⊢ l % (m * n) / m = l / m % n

case inr
l m n : Nat
h✝ : m > 0
⊢ l % (m * n) / m = l / m % n

State before:
l m n : Nat
hm : m = 0
⊢ l % (m * n) / m = l / m % n
Tactic:
case inl hm =>
  cases hm; simp
State after:
no goals

State before:
l m n : Nat
hm : m > 0
⊢ l % (m * n) / m = l / m % n
Tactic:
case inr hm =>
cases n.eq_zero_or_pos
case inl hn =>
  cases hn; simp [Nat.mod_zero]
case inr hn =>
  conv =>
    rhs;
    rw [←Nat.div_add_mod l (m*n)]
    rw [Nat.add_comm, Nat.mul_assoc, Nat.add_mul_div_left _ _ hm]
    rw [Nat.add_mul_mod_self_left]
  apply (Nat.mod_eq_of_lt ?_).symm
  apply (div_lt_iff_lt_mul hm).mpr
  rw [Nat.mul_comm]
  exact Nat.mod_lt l (Nat.mul_pos hn hm)
State after:
no goals

State before:
l m n : Nat
hm : m = 0
⊢ l % (m * n) / m = l / m % n
Tactic:
cases hm
State after:
case refl
l n : Nat
⊢ l % (0 * n) / 0 = l / 0 % n

State before:
case refl
l n : Nat
⊢ l % (0 * n) / 0 = l / 0 % n
Tactic:
simp
State after:
no goals

State before:
l m n : Nat
hm : m > 0
⊢ l % (m * n) / m = l / m % n
Tactic:
cases n.eq_zero_or_pos
State after:
case inl
l m n : Nat
hm : m > 0
h✝ : n = 0
⊢ l % (m * n) / m = l / m % n

case inr
l m n : Nat
hm : m > 0
h✝ : n > 0
⊢ l % (m * n) / m = l / m % n

State before:
l m n : Nat
hm : m > 0
hn : n = 0
⊢ l % (m * n) / m = l / m % n
Tactic:
case inl hn =>
  cases hn; simp [Nat.mod_zero]
State after:
no goals

State before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m = l / m % n
Tactic:
case inr hn =>
  conv =>
    rhs;
    rw [←Nat.div_add_mod l (m*n)]
    rw [Nat.add_comm, Nat.mul_assoc, Nat.add_mul_div_left _ _ hm]
    rw [Nat.add_mul_mod_self_left]
  apply (Nat.mod_eq_of_lt ?_).symm
  apply (div_lt_iff_lt_mul hm).mpr
  rw [Nat.mul_comm]
  exact Nat.mod_lt l (Nat.mul_pos hn hm)
State after:
no goals

State before:
l m n : Nat
hm : m > 0
hn : n = 0
⊢ l % (m * n) / m = l / m % n
Tactic:
cases hn
State after:
case refl
l m : Nat
hm : m > 0
⊢ l % (m * 0) / m = l / m % 0

State before:
case refl
l m : Nat
hm : m > 0
⊢ l % (m * 0) / m = l / m % 0
Tactic:
simp [Nat.mod_zero]
State after:
no goals

State before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m = l / m % n
Tactic:
conv =>
  rhs;
  rw [←Nat.div_add_mod l (m*n)]
  rw [Nat.add_comm, Nat.mul_assoc, Nat.add_mul_div_left _ _ hm]
  rw [Nat.add_mul_mod_self_left]
State after:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m = l % (m * n) / m % n

State before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m = l % (m * n) / m % n
Tactic:
apply (Nat.mod_eq_of_lt ?_).symm
State after:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m < n

State before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m < n
Tactic:
apply (div_lt_iff_lt_mul hm).mpr
State after:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) < n * m

State before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) < n * m
Tactic:
rw [Nat.mul_comm]
State after:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (n * m) < n * m

State before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (n * m) < n * m
Tactic:
exact Nat.mod_lt l (Nat.mul_pos hn hm)
State after:
no goals