Theorem: div_mul_pred_eq_sub_of_pos_of_dvd (Fl/Lemmas.lean)

State before:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a = b - a
Tactic:
apply Nat.le_antisymm
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

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
State after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - a ≤ (b - 1) / a * a

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 _ _
State after:
no goals

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
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

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 _ _
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

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₁
State after:
case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b

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
State after:
no goals

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 _ _
State after:
no goals

State before:
case h₁.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ b
Tactic:
exact h₁
State after:
no goals

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)
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

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 _ _
State after:
case h₁.h₃.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - 1 < b

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
State after:
no goals

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 _ _
State after:
no goals

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
State after:
no goals

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]
State after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b - 1) / a * a + a

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]
State after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ Nat.succ ((b - 1) / a) * a

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₀]
State after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b - 1 + a) / a * a

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₂)]
State after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b + a - 1) / a * a

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₀)]
State after:
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b + (a - 1)) / a * a

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
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

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₁]
State after:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a * a ≤ (b + (a - 1)) / a * a

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 _ _
State after:
no goals

State before:
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ b / a * a
Tactic:
rw [Nat.div_mul_cancel h₁]
State after:
no goals

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
State after:
case h
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a ≤ (b + (a - 1)) / a

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
State after:
case h.h
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ b + (a - 1)

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 _ _
State after:
no goals