internlm/Lean-Github huggingface dataset:
Theorem: add_le_of_dvd_of_dvd_of_lt
Proof state before:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n
Tactic:
. exact h₁
Proof state after:
no goals
Theorem: add_le_of_dvd_of_dvd_of_lt
Proof state before:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ m + k < n + ?n
Tactic:
exact Nat.add_lt_add_right h₃ k
Proof state after:
no goals
Theorem: add_le_of_dvd_of_dvd_of_lt
Proof state before:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ m + k
Tactic:
exact Nat.dvd_add h₂ (Nat.dvd_refl _)
Proof state after:
no goals
Theorem: add_le_of_dvd_of_dvd_of_lt
Proof state before:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n
Tactic:
exact h₁
Proof state after:
no goals
Theorem: le_sub_of_dvd_of_dvd_of_lt
Proof state before:
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : n < m
⊢ n ≤ m - k
Tactic:
apply le_tsub_of_add_le_right
Proof state after:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : n < m
⊢ n + k ≤ m
Theorem: le_sub_of_dvd_of_dvd_of_lt
Proof state before:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : n < m
⊢ n + k ≤ m
Tactic:
exact add_le_of_dvd_of_dvd_of_lt h₂ h₁ h₃
Proof state after:
no goals
Theorem: div_mul_eq_of_dvd_of_le_of_lt
Proof state before:
m k x : ℕ
h₁ : k ∣ m
h₂ : m ≤ x
h₃ : x < m + k
⊢ x / k * k = m
Tactic:
have ⟨d, hd⟩ := h₁
Proof state after:
m k x : ℕ
h₁ : k ∣ m
h₂ : m ≤ x
h₃ : x < m + k
d : ℕ
hd : m = k * d
⊢ x / k * k = m
Theorem: div_mul_eq_of_dvd_of_le_of_lt
Proof state before:
m k x : ℕ
h₁ : k ∣ m
h₂ : m ≤ x
h₃ : x < m + k
d : ℕ
hd : m = k * d
⊢ x / k * k = m
Tactic:
rewrite [hd, mul_comm k] at h₂ h₃ ⊢
Proof state after:
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < d * k + k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k
Theorem: div_mul_eq_of_dvd_of_le_of_lt
Proof state before:
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < d * k + k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k
Tactic:
rewrite [← Nat.succ_mul] at h₃
Proof state after:
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < Nat.succ d * k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k
Theorem: div_mul_eq_of_dvd_of_le_of_lt
Proof state before:
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < Nat.succ d * k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k
Tactic:
rw [Nat.div_eq_of_lt_le h₂ h₃]
Proof state after:
no goals
Theorem: div_mul_eq_of_le_of_lt
Proof state before:
m k x : ℕ
h : k ≤ m
⊢ 2 ^ m ≤ x → x < 2 ^ m + 2 ^ k → x / 2 ^ k * 2 ^ k = 2 ^ m
Tactic:
apply div_mul_eq_of_dvd_of_le_of_lt
Proof state after:
case h₁
m k x : ℕ
h : k ≤ m
⊢ 2 ^ k ∣ 2 ^ m
Theorem: div_mul_eq_of_le_of_lt
Proof state before:
case h₁
m k x : ℕ
h : k ≤ m
⊢ 2 ^ k ∣ 2 ^ m
Tactic:
exact pow_dvd_pow 2 h
Proof state after:
no goals
Theorem: div_mul_div_cancel_of_dvd
Proof state before:
n m k : ℕ
h₂ : k ∣ m
⊢ n / k * k / m = n / m
Tactic:
have ⟨d, hd⟩ := h₂
Proof state after:
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / m = n / m
Theorem: div_mul_div_cancel_of_dvd
Proof state before:
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / m = n / m
Tactic:
rewrite [hd]
Proof state after:
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / (k * d) = n / (k * d)
Theorem: div_mul_div_cancel_of_dvd
Proof state before:
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / (k * d) = n / (k * d)
Tactic:
match k with
| 0 => rw [Nat.mul_zero, Nat.zero_mul, Nat.zero_div, Nat.div_zero]
| x + 1 =>
  rewrite [← Nat.div_div_eq_div_mul]
  rewrite [Nat.mul_div_cancel _ (Nat.add_pos_right _ zero_lt_one)]
  exact Nat.div_div_eq_div_mul _ _ _
Proof state after:
no goals
Theorem: div_mul_div_cancel_of_dvd
Proof state before:
n m k d : ℕ
h₂ : 0 ∣ m
hd : m = 0 * d
⊢ n / 0 * 0 / (0 * d) = n / (0 * d)
Tactic:
rw [Nat.mul_zero, Nat.zero_mul, Nat.zero_div, Nat.div_zero]
Proof state after:
no goals
Theorem: div_mul_div_cancel_of_dvd
Proof state before:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) * (x + 1) / ((x + 1) * d) = n / ((x + 1) * d)
Tactic:
rewrite [← Nat.div_div_eq_div_mul]
Proof state after:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) * (x + 1) / (x + 1) / d = n / ((x + 1) * d)
Theorem: div_mul_div_cancel_of_dvd
Proof state before:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) * (x + 1) / (x + 1) / d = n / ((x + 1) * d)
Tactic:
rewrite [Nat.mul_div_cancel _ (Nat.add_pos_right _ zero_lt_one)]
Proof state after:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) / d = n / ((x + 1) * d)
Theorem: div_mul_div_cancel_of_dvd
Proof state before:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) / d = n / ((x + 1) * d)
Tactic:
exact Nat.div_div_eq_div_mul _ _ _
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a = b - a
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a ≤ b - a

case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - a ≤ (b - 1) / a * a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a ≤ b - a

case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - a ≤ (b - 1) / a * a
Tactic:
. apply le_sub_of_dvd_of_dvd_of_lt
  . exact Nat.dvd_mul_left _ _
  . exact h₁
  . apply Nat.lt_of_le_of_lt (m := b - 1)
    . exact Nat.div_mul_le_self _ _
    . apply tsub_lt_self h₂ zero_lt_one
Proof state after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - a ≤ (b - 1) / a * a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - a ≤ (b - 1) / a * a
Tactic:
. rewrite [tsub_le_iff_right]
  rewrite [← Nat.succ_mul]
  rewrite [← Nat.add_div_right _ h₀]
  rewrite [tsub_add_eq_add_tsub (Nat.one_le_of_lt h₂)]
  rewrite [add_tsub_assoc_of_le (Nat.one_le_of_lt h₀)]
  trans b / a * a
  . rw [Nat.div_mul_cancel h₁]
  . apply Nat.mul_le_mul_right
    apply Nat.div_le_div_right
    exact Nat.le_add_right _ _
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a ≤ b - a
Tactic:
apply le_sub_of_dvd_of_dvd_of_lt
Proof state after:
case h₁.h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ (b - 1) / a * a

case h₁.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ b

case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ (b - 1) / a * a

case h₁.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ b

case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
Tactic:
. exact Nat.dvd_mul_left _ _
Proof state after:
case h₁.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ b

case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ b

case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
Tactic:
. exact h₁
Proof state after:
case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
Tactic:
. apply Nat.lt_of_le_of_lt (m := b - 1)
  . exact Nat.div_mul_le_self _ _
  . apply tsub_lt_self h₂ zero_lt_one
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ (b - 1) / a * a
Tactic:
exact Nat.dvd_mul_left _ _
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ b
Tactic:
exact h₁
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
Tactic:
apply Nat.lt_of_le_of_lt (m := b - 1)
Proof state after:
case h₁.h₃.h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a ≤ b - 1

case h₁.h₃.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - 1 < b
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₃.h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a ≤ b - 1

case h₁.h₃.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - 1 < b
Tactic:
. exact Nat.div_mul_le_self _ _
Proof state after:
case h₁.h₃.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - 1 < b
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₃.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - 1 < b
Tactic:
. apply tsub_lt_self h₂ zero_lt_one
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₃.h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a ≤ b - 1
Tactic:
exact Nat.div_mul_le_self _ _
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₁.h₃.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - 1 < b
Tactic:
apply tsub_lt_self h₂ zero_lt_one
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - a ≤ (b - 1) / a * a
Tactic:
rewrite [tsub_le_iff_right]
Proof state after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b - 1) / a * a + a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b - 1) / a * a + a
Tactic:
rewrite [← Nat.succ_mul]
Proof state after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ Nat.succ ((b - 1) / a) * a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ Nat.succ ((b - 1) / a) * a
Tactic:
rewrite [← Nat.add_div_right _ h₀]
Proof state after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b - 1 + a) / a * a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b - 1 + a) / a * a
Tactic:
rewrite [tsub_add_eq_add_tsub (Nat.one_le_of_lt h₂)]
Proof state after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b + a - 1) / a * a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b + a - 1) / a * a
Tactic:
rewrite [add_tsub_assoc_of_le (Nat.one_le_of_lt h₀)]
Proof state after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b + (a - 1)) / a * a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b + (a - 1)) / a * a
Tactic:
trans b / a * a
Proof state after:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ b / a * a

a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a * a ≤ (b + (a - 1)) / a * a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ b / a * a

a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a * a ≤ (b + (a - 1)) / a * a
Tactic:
. rw [Nat.div_mul_cancel h₁]
Proof state after:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a * a ≤ (b + (a - 1)) / a * a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a * a ≤ (b + (a - 1)) / a * a
Tactic:
. apply Nat.mul_le_mul_right
  apply Nat.div_le_div_right
  exact Nat.le_add_right _ _
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ b / a * a
Tactic:
rw [Nat.div_mul_cancel h₁]
Proof state after:
no goals
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a * a ≤ (b + (a - 1)) / a * a
Tactic:
apply Nat.mul_le_mul_right
Proof state after:
case h
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a ≤ (b + (a - 1)) / a
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a ≤ (b + (a - 1)) / a
Tactic:
apply Nat.div_le_div_right
Proof state after:
case h.h
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ b + (a - 1)
Theorem: div_mul_pred_eq_sub_of_pos_of_dvd
Proof state before:
case h.h
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ b + (a - 1)
Tactic:
exact Nat.le_add_right _ _
Proof state after:
no goals
Theorem: sub_mul_mod_self_left
Proof 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
Proof state after:
no goals
Theorem: sub_mul_mod_self_left
Proof state before:
x y z : ℕ
h : y * 0 ≤ x
⊢ (x - y * 0) % y = x % y
Tactic:
rw [Nat.mul_zero, tsub_zero]
Proof state after:
no goals
Theorem: sub_mul_mod_self_left
Proof 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
Proof state after:
x y z✝ z : ℕ
h : y * z + y ≤ x
⊢ (x - y * Nat.succ z) % y = x % y
Theorem: sub_mul_mod_self_left
Proof 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
Proof state after:
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
⊢ (x - y * Nat.succ z) % y = x % y
Theorem: sub_mul_mod_self_left
Proof 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
Proof 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
Theorem: sub_mul_mod_self_left
Proof 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]
Proof 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
Theorem: sub_mul_mod_self_left
Proof 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]
Proof 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
Theorem: sub_mul_mod_self_left
Proof 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]
Proof 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
Theorem: sub_mul_mod_self_left
Proof 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
Proof state after:
no goals
Theorem: mod_sub_mod
Proof state before:
m n k : ℕ
h : k ≤ m
⊢ (m - k) % n = (m - k % n) % n
Tactic:
conv => lhs ; rewrite [← Nat.mod_add_div k n, ← tsub_tsub]
Proof state after:
m n k : ℕ
h : k ≤ m
⊢ (m - k % n - n * (k / n)) % n = (m - k % n) % n
Theorem: mod_sub_mod
Proof state before:
m n k : ℕ
h : k ≤ m
⊢ (m - k % n - n * (k / n)) % n = (m - k % n) % n
Tactic:
apply sub_mul_mod_self_left
Proof state after:
case h
m n k : ℕ
h : k ≤ m
⊢ n * (k / n) ≤ m - k % n
Theorem: mod_sub_mod
Proof state before:
case h
m n k : ℕ
h : k ≤ m
⊢ n * (k / n) ≤ m - k % n
Tactic:
apply le_tsub_of_add_le_left
Proof state after:
case h.h
m n k : ℕ
h : k ≤ m
⊢ k % n + n * (k / n) ≤ m
Theorem: mod_sub_mod
Proof state before:
case h.h
m n k : ℕ
h : k ≤ m
⊢ k % n + n * (k / n) ≤ m
Tactic:
rewrite [Nat.mod_add_div]
Proof state after:
case h.h
m n k : ℕ
h : k ≤ m
⊢ k ≤ m
Theorem: mod_sub_mod
Proof state before:
case h.h
m n k : ℕ
h : k ≤ m
⊢ k ≤ m
Tactic:
exact h
Proof state after:
no goals
Theorem: size_of_le_of_lt
Proof state before:
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.size x = n
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.size x ≤ n

case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x
Theorem: size_of_le_of_lt
Proof state before:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.size x ≤ n

case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x
Tactic:
. rewrite [Nat.size_le]
  exact hr
Proof state after:
case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x
Theorem: size_of_le_of_lt
Proof state before:
case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x
Tactic:
. apply Nat.le_of_pred_lt
  rewrite [← Nat.sub_one, Nat.lt_size]
  exact hl
Proof state after:
no goals
Theorem: size_of_le_of_lt
Proof state before:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.size x ≤ n
Tactic:
rewrite [Nat.size_le]
Proof state after:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ x < 2 ^ n
Theorem: size_of_le_of_lt
Proof state before:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ x < 2 ^ n
Tactic:
exact hr
Proof state after:
no goals
Theorem: size_of_le_of_lt
Proof state before:
case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x
Tactic:
apply Nat.le_of_pred_lt
Proof state after:
case h₂.a
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.pred n < Nat.size x
Theorem: size_of_le_of_lt
Proof state before:
case h₂.a
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.pred n < Nat.size x
Tactic:
rewrite [← Nat.sub_one, Nat.lt_size]
Proof state after:
case h₂.a
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ 2 ^ (n - 1) ≤ x
Theorem: size_of_le_of_lt
Proof state before:
case h₂.a
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ 2 ^ (n - 1) ≤ x
Tactic:
exact hl
Proof state after:
no goals
Theorem: le_size_of_pos
Proof state before:
x : ℕ
pos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
rewrite [← Nat.lt_size]
Proof state after:
x : ℕ
pos : 0 < x
⊢ Nat.size x - 1 < Nat.size x
Theorem: le_size_of_pos
Proof state before:
x : ℕ
pos : 0 < x
⊢ Nat.size x - 1 < Nat.size x
Tactic:
exact tsub_lt_self (Nat.size_pos.mpr pos) one_pos
Proof state after:
no goals
Theorem: lt_of_size_lt_size
Proof state before:
x y : ℕ
h : Nat.size x < Nat.size y
⊢ x < y
Tactic:
apply Nat.lt_of_not_le
Proof state after:
case a
x y : ℕ
h : Nat.size x < Nat.size y
⊢ ¬y ≤ x
Theorem: lt_of_size_lt_size
Proof state before:
case a
x y : ℕ
h : Nat.size x < Nat.size y
⊢ ¬y ≤ x
Tactic:
intro (hle : y ≤ x)
Proof state after:
case a
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ False
Theorem: lt_of_size_lt_size
Proof state before:
case a
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ False
Tactic:
apply Nat.lt_le_asymm h
Proof state after:
case a
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ Nat.size y ≤ Nat.size x
Theorem: lt_of_size_lt_size
Proof state before:
case a
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ Nat.size y ≤ Nat.size x
Tactic:
apply Nat.size_le_size
Proof state after:
case a.h
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ y ≤ x
Theorem: lt_of_size_lt_size
Proof state before:
case a.h
x y : ℕ
h : Nat.size x < Nat.size y
hle : y ≤ x
⊢ y ≤ x
Tactic:
exact hle
Proof state after:
no goals
Theorem: size_mul_pow
Proof state before:
x : ℕ
h : 0 < x
k : ℕ
⊢ Nat.size (x * 2 ^ k) = Nat.size x + k
Tactic:
have nz : x ≠ 0 := by rwa [← Nat.pos_iff_ne_zero]
Proof state after:
x : ℕ
h : 0 < x
k : ℕ
nz : x ≠ 0
⊢ Nat.size (x * 2 ^ k) = Nat.size x + k
Theorem: size_mul_pow
Proof state before:
x : ℕ
h : 0 < x
k : ℕ
nz : x ≠ 0
⊢ Nat.size (x * 2 ^ k) = Nat.size x + k
Tactic:
rewrite [← Nat.shiftLeft_eq_mul_pow x k]
Proof state after:
x : ℕ
h : 0 < x
k : ℕ
nz : x ≠ 0
⊢ Nat.size (x <<< k) = Nat.size x + k
Theorem: size_mul_pow
Proof state before:
x : ℕ
h : 0 < x
k : ℕ
nz : x ≠ 0
⊢ Nat.size (x <<< k) = Nat.size x + k
Tactic:
rw [Nat.size_shiftLeft nz]
Proof state after:
no goals
Theorem: size_mul_pow
Proof state before:
x : ℕ
h : 0 < x
k : ℕ
⊢ x ≠ 0
Tactic:
rwa [← Nat.pos_iff_ne_zero]
Proof state after:
no goals
Theorem: size_pow_mul
Proof state before:
x : ℕ
h : 0 < x
k : ℕ
⊢ Nat.size (2 ^ k * x) = Nat.size x + k
Tactic:
rw [Nat.mul_comm, size_mul_pow h k]
Proof state after:
no goals
Theorem: size_div_pow
Proof state before:
x m : ℕ
h : 2 ^ m ≤ x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
Tactic:
have pos : 0 < x := Nat.lt_of_lt_of_le two_pow_pos h
Proof state after:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
Theorem: size_div_pow
Proof state before:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
Tactic:
have lt_size : m < Nat.size x := by rwa [Nat.lt_size]
Proof state after:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
Theorem: size_div_pow
Proof state before:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
Tactic:
apply size_of_le_of_lt
Proof state after:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m

case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Theorem: size_div_pow
Proof state before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m

case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Tactic:
. have le_size_pred : m ≤ Nat.size x - 1 := Nat.le_pred_of_lt lt_size
  rewrite [tsub_right_comm]
  rewrite [← Nat.pow_div le_size_pred two_pos]
  apply Nat.div_le_div_right
  exact le_size_of_pos pos
Proof state after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Theorem: size_div_pow
Proof state before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Tactic:
. have pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x := pow_dvd_pow 2 lt_size.le
  rewrite [Nat.div_lt_iff_lt_mul two_pow_pos]
  rewrite [← Nat.pow_div lt_size.le two_pos]
  rewrite [Nat.div_mul_cancel pow_dvd]
  exact Nat.lt_size_self x
Proof state after:
no goals
Theorem: size_div_pow
Proof state before:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
⊢ m < Nat.size x
Tactic:
rwa [Nat.lt_size]
Proof state after:
no goals
Theorem: size_div_pow
Proof state before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m
Tactic:
have le_size_pred : m ≤ Nat.size x - 1 := Nat.le_pred_of_lt lt_size
Proof state after:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m
Theorem: size_div_pow
Proof state before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m
Tactic:
rewrite [tsub_right_comm]
Proof state after:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1 - m) ≤ x / 2 ^ m
Theorem: size_div_pow
Proof state before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1 - m) ≤ x / 2 ^ m
Tactic:
rewrite [← Nat.pow_div le_size_pred two_pos]
Proof state after:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1) / 2 ^ m ≤ x / 2 ^ m
Theorem: size_div_pow
Proof state before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1) / 2 ^ m ≤ x / 2 ^ m
Tactic:
apply Nat.div_le_div_right
Proof state after:
case hl.h
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1) ≤ x
Theorem: size_div_pow
Proof state before:
case hl.h
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
exact le_size_of_pos pos
Proof state after:
no goals
Theorem: size_div_pow
Proof state before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Tactic:
have pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x := pow_dvd_pow 2 lt_size.le
Proof state after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)