Theorem: six_dvd_n_cubed_minus_n (meetings/ex3.lean)

State before:
n : ℕ
⊢ 6 ∣ n ^ 3 - n
Tactic:
have gt_pow3 (n : ℕ) : n ≤ n ^ 3 := by
  apply Nat.le_self_pow
  simp
State after:
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ n ^ 3 - n

State before:
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ n ^ 3 - n
Tactic:
zify [gt_pow3 n]
State after:
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑n ^ 3 - ↑n

State before:
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑n ^ 3 - ↑n
Tactic:
induction' n using Nat.caseStrongInductionOn with n ih
State after:
case zero
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑0 ^ 3 - ↑0

case ind
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)

State before:
n✝ n : ℕ
⊢ n ≤ n ^ 3
Tactic:
apply Nat.le_self_pow
State after:
case hn
n✝ n : ℕ
⊢ 3 ≠ 0

State before:
case hn
n✝ n : ℕ
⊢ 3 ≠ 0
Tactic:
simp
State after:
no goals

State before:
case zero
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑0 ^ 3 - ↑0
Tactic:
exact dvd_zero 6
State after:
no goals

State before:
case ind
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
by_cases hp : n ≤ 3
State after:
case pos
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n ≤ 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)

case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)

State before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
let k : ℕ := n - 3
State after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)

State before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
have hk : Nat.succ n = k + 4 := by
  zify [le_of_not_le hp]
  ring_nf
State after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)

State before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
rw [hk]
State after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(k + 4) ^ 3 - ↑(k + 4)

State before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(k + 4) ^ 3 - ↑(k + 4)
Tactic:
push_cast (config := { zeta := false })
State after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ (↑k + 4) ^ 3 - (↑k + 4)

State before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ (↑k + 4) ^ 3 - (↑k + 4)
Tactic:
have hring (k : ℤ) :
  (k + 4) ^ 3 - (k + 4)
  = (k ^ 3 - k) + 6 * (2 * k ^ 2 + 8 * k + 10) := by
  ring_nf
State after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ 6 ∣ (↑k + 4) ^ 3 - (↑k + 4)

State before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ 6 ∣ (↑k + 4) ^ 3 - (↑k + 4)
Tactic:
rw [hring k]
State after:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ 6 ∣ ↑k ^ 3 - ↑k + 6 * (2 * ↑k ^ 2 + 8 * ↑k + 10)

State before:
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ 6 ∣ ↑k ^ 3 - ↑k + 6 * (2 * ↑k ^ 2 + 8 * ↑k + 10)
Tactic:
rcases ih k (by simp) with ⟨m, hm⟩
State after:
case neg.intro
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
m : ℤ
hm : ↑k ^ 3 - ↑k = 6 * m
⊢ 6 ∣ ↑k ^ 3 - ↑k + 6 * (2 * ↑k ^ 2 + 8 * ↑k + 10)

State before:
case neg.intro
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
m : ℤ
hm : ↑k ^ 3 - ↑k = 6 * m
⊢ 6 ∣ ↑k ^ 3 - ↑k + 6 * (2 * ↑k ^ 2 + 8 * ↑k + 10)
Tactic:
rw [hm, ←mul_add]
State after:
case neg.intro
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
m : ℤ
hm : ↑k ^ 3 - ↑k = 6 * m
⊢ 6 ∣ 6 * (m + (2 * ↑k ^ 2 + 8 * ↑k + 10))

State before:
case neg.intro
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
m : ℤ
hm : ↑k ^ 3 - ↑k = 6 * m
⊢ 6 ∣ 6 * (m + (2 * ↑k ^ 2 + 8 * ↑k + 10))
Tactic:
simp only [ge_iff_le, dvd_mul_right]
State after:
no goals

State before:
case pos
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n ≤ 3
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
Tactic:
rw [Nat.succ_eq_add_one]
State after:
case pos
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n ≤ 3
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)

State before:
case pos
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n ≤ 3
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
rcases hp with _ | hp
State after:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(3 + 1) ^ 3 - ↑(3 + 1)

case pos.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 2
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)

State before:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(3 + 1) ^ 3 - ↑(3 + 1)
Tactic:
ring_nf
State after:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 60

State before:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 60
Tactic:
have : (60 : ℤ) = 6 * 10 := by ring
State after:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
this : 60 = 6 * 10
⊢ 6 ∣ 60

State before:
case pos.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
this : 60 = 6 * 10
⊢ 6 ∣ 60
Tactic:
simp_rw [this, dvd_mul_right]
State after:
no goals

State before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 3, 6 ∣ ↑m ^ 3 - ↑m
⊢ 60 = 6 * 10
Tactic:
ring
State after:
no goals

State before:
case pos.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 2
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
rcases hp with _ | hp
State after:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(2 + 1) ^ 3 - ↑(2 + 1)

case pos.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 1
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)

State before:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(2 + 1) ^ 3 - ↑(2 + 1)
Tactic:
ring_nf
State after:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 24

State before:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 24
Tactic:
have : (24 : ℤ) = 6 * 4 := by ring
State after:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
this : 24 = 6 * 4
⊢ 6 ∣ 24

State before:
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
this : 24 = 6 * 4
⊢ 6 ∣ 24
Tactic:
simp_rw [this, dvd_mul_right]
State after:
no goals

State before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 24 = 6 * 4
Tactic:
ring
State after:
no goals

State before:
case pos.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 1
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
rcases hp with _ | hp
State after:
case pos.step.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 1, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(1 + 1) ^ 3 - ↑(1 + 1)

case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 0
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)

State before:
case pos.step.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 1, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(1 + 1) ^ 3 - ↑(1 + 1)
Tactic:
ring_nf
State after:
case pos.step.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 1, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 6

State before:
case pos.step.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 1, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 6
Tactic:
exact Int.dvd_refl 6
State after:
no goals

State before:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 0
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
simp at hp
State after:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n = 0
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)

State before:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n = 0
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
Tactic:
rw [hp]
State after:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n = 0
⊢ 6 ∣ ↑(0 + 1) ^ 3 - ↑(0 + 1)

State before:
case pos.step.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : n = 0
⊢ 6 ∣ ↑(0 + 1) ^ 3 - ↑(0 + 1)
Tactic:
exact dvd_zero 6
State after:
no goals

State before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ Nat.succ n = k + 4
Tactic:
zify [le_of_not_le hp]
State after:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ ↑n + 1 = ↑n - 3 + 4

State before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
⊢ ↑n + 1 = ↑n - 3 + 4
Tactic:
ring_nf
State after:
no goals

State before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k✝ : ℕ := n - 3
hk : Nat.succ n = k✝ + 4
k : ℤ
⊢ (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
Tactic:
ring_nf
State after:
no goals

State before:
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
hring : ∀ (k : ℤ), (k + 4) ^ 3 - (k + 4) = k ^ 3 - k + 6 * (2 * k ^ 2 + 8 * k + 10)
⊢ k ≤ n
Tactic:
simp
State after:
no goals