Theorem: Nat.mod_mul (Lib.lean)

State before:
a b c : ℕ
⊢ a % (b * c) = b * (a / b % c) + a % b
Tactic:
match b with
| 0 => simp
| b + 1 =>
  match c with
  | 0 => simp[Nat.div_add_mod]
  | c + 1 =>
    apply Eq.trans
    apply congrArg₂ _ (Nat.div_add_mod a (b + 1)).symm rfl
    apply Eq.trans
    apply Nat.add_mod
    apply Eq.trans
    exact congrArg₂ _ (congrArg₂ _ (Nat.mul_mod_mul_left _ _ _) (Nat.mod_eq_of_lt (lt_of_lt_of_le (Nat.mod_lt _ (Nat.zero_lt_succ _)) (Nat.le_mul_of_pos_right (Nat.zero_lt_succ _))))) rfl
    apply Nat.mod_eq_of_lt
    apply Nat.lt_of_succ_le
    apply le_trans
    apply Nat.succ_le_succ
    apply add_le_add
    apply Nat.mul_le_mul_left
    apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
    apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
    simp [Nat.succ_eq_add_one, left_distrib, right_distrib, ← add_assoc]
State after:
no goals

State before:
a b c : ℕ
⊢ a % (0 * c) = 0 * (a / 0 % c) + a % 0
Tactic:
simp
State after:
no goals

State before:
a b✝ c b : ℕ
⊢ a % ((b + 1) * c) = (b + 1) * (a / (b + 1) % c) + a % (b + 1)
Tactic:
match c with
| 0 => simp[Nat.div_add_mod]
| c + 1 =>
  apply Eq.trans
  apply congrArg₂ _ (Nat.div_add_mod a (b + 1)).symm rfl
  apply Eq.trans
  apply Nat.add_mod
  apply Eq.trans
  exact congrArg₂ _ (congrArg₂ _ (Nat.mul_mod_mul_left _ _ _) (Nat.mod_eq_of_lt (lt_of_lt_of_le (Nat.mod_lt _ (Nat.zero_lt_succ _)) (Nat.le_mul_of_pos_right (Nat.zero_lt_succ _))))) rfl
  apply Nat.mod_eq_of_lt
  apply Nat.lt_of_succ_le
  apply le_trans
  apply Nat.succ_le_succ
  apply add_le_add
  apply Nat.mul_le_mul_left
  apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
  apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
  simp [Nat.succ_eq_add_one, left_distrib, right_distrib, ← add_assoc]
State after:
no goals

State before:
a b✝ c b : ℕ
⊢ a % ((b + 1) * 0) = (b + 1) * (a / (b + 1) % 0) + a % (b + 1)
Tactic:
simp[Nat.div_add_mod]
State after:
no goals

State before:
a b✝ c✝ b c : ℕ
⊢ a % ((b + 1) * (c + 1)) = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Tactic:
apply Eq.trans
State after:
case h₁
a b✝ c✝ b c : ℕ
⊢ a % ((b + 1) * (c + 1)) = ?b

case h₂
a b✝ c✝ b c : ℕ
⊢ ?b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case b
a b✝ c✝ b c : ℕ
⊢ ℕ

State before:
case h₁
a b✝ c✝ b c : ℕ
⊢ a % ((b + 1) * (c + 1)) = ?b

case h₂
a b✝ c✝ b c : ℕ
⊢ ?b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case b
a b✝ c✝ b c : ℕ
⊢ ℕ
Tactic:
apply congrArg₂ _ (Nat.div_add_mod a (b + 1)).symm rfl
State after:
case h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

State before:
case h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Tactic:
apply Eq.trans
State after:
case h₂.h₁
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) = ?h₂.b

case h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ?h₂.b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case h₂.b
a b✝ c✝ b c : ℕ
⊢ ℕ

State before:
case h₂.h₁
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) = ?h₂.b

case h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ?h₂.b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case h₂.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Tactic:
apply Nat.add_mod
State after:
case h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) % ((b + 1) * (c + 1)) + a % (b + 1) % ((b + 1) * (c + 1))) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

State before:
case h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) % ((b + 1) * (c + 1)) + a % (b + 1) % ((b + 1) * (c + 1))) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Tactic:
apply Eq.trans
State after:
case h₂.h₂.h₁
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) % ((b + 1) * (c + 1)) + a % (b + 1) % ((b + 1) * (c + 1))) % ((b + 1) * (c + 1)) = ?h₂.h₂.b

case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ?h₂.h₂.b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case h₂.h₂.b
a b✝ c✝ b c : ℕ
⊢ ℕ

State before:
case h₂.h₂.h₁
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1)) % ((b + 1) * (c + 1)) + a % (b + 1) % ((b + 1) * (c + 1))) % ((b + 1) * (c + 1)) = ?h₂.h₂.b

case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ?h₂.h₂.b = (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

case h₂.h₂.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Tactic:
exact congrArg₂ _ (congrArg₂ _ (Nat.mul_mod_mul_left _ _ _) (Nat.mod_eq_of_lt (lt_of_lt_of_le (Nat.mod_lt _ (Nat.zero_lt_succ _)) (Nat.le_mul_of_pos_right (Nat.zero_lt_succ _))))) rfl
State after:
case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)

State before:
case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
Tactic:
apply Nat.mod_eq_of_lt
State after:
case h₂.h₂.h₂.h
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) < (b + 1) * (c + 1)

State before:
case h₂.h₂.h₂.h
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) < (b + 1) * (c + 1)
Tactic:
apply Nat.lt_of_succ_le
State after:
case h₂.h₂.h₂.h.h
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) ≤ (b + 1) * (c + 1)

State before:
case h₂.h₂.h₂.h.h
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) ≤ (b + 1) * (c + 1)
Tactic:
apply le_trans
State after:
case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) ≤ ?h₂.h₂.h₂.h.h.b

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ ?h₂.h₂.h₂.h.h.b ≤ (b + 1) * (c + 1)

case h₂.h₂.h₂.h.h.b
a b✝ c✝ b c : ℕ
⊢ ℕ

State before:
case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) ≤ ?h₂.h₂.h₂.h.h.b

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ ?h₂.h₂.h₂.h.h.b ≤ (b + 1) * (c + 1)

case h₂.h₂.h₂.h.h.b
a b✝ c✝ b c : ℕ
⊢ ℕ
Tactic:
apply Nat.succ_le_succ
State after:
case h₂.h₂.h₂.h.h.a.a
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.m

case h₂.h₂.h₂.h.h.a.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ?h₂.h₂.h₂.h.h.a.m ≤ (b + 1) * (c + 1)

State before:
case h₂.h₂.h₂.h.h.a.a
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.m

case h₂.h₂.h₂.h.h.a.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ?h₂.h₂.h₂.h.h.a.m ≤ (b + 1) * (c + 1)
Tactic:
apply add_le_add
State after:
case h₂.h₂.h₂.h.h.a.a.h₁
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) ≤ ?h₂.h₂.h₂.h.h.a.a.b

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.b
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ (?h₂.h₂.h₂.h.h.a.a.b + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)

State before:
case h₂.h₂.h₂.h.h.a.a.h₁
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) ≤ ?h₂.h₂.h₂.h.h.a.a.b

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.b
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ (?h₂.h₂.h₂.h.h.a.a.b + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Tactic:
apply Nat.mul_le_mul_left
State after:
case h₂.h₂.h₂.h.h.a.a.h₁.h
a b✝ c✝ b c : ℕ
⊢ a / (b + 1) % (c + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.h₁.m

case h₂.h₂.h₂.h.h.a.a.h₁.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * ?h₂.h₂.h₂.h.h.a.a.h₁.m + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)

State before:
case h₂.h₂.h₂.h.h.a.a.h₁.h
a b✝ c✝ b c : ℕ
⊢ a / (b + 1) % (c + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.h₁.m

case h₂.h₂.h₂.h.h.a.a.h₁.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * ?h₂.h₂.h₂.h.h.a.a.h₁.m + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Tactic:
apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
State after:
case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * c + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)

State before:
case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * c + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)
Tactic:
apply Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ _))
State after:
case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * c + b) ≤ (b + 1) * (c + 1)

State before:
case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ((b + 1) * c + b) ≤ (b + 1) * (c + 1)
Tactic:
simp [Nat.succ_eq_add_one, left_distrib, right_distrib, ← add_assoc]
State after:
no goals