Theorem: Section15sheet2Solutions.lemma1 (FormalisingMathematics2024/Solutions/Section15numberTheory/Sheet2.lean)

State before:
x : ℤ
⊢ x - 3 ∣ x ^ 3 - 3 ↔ x - 3 ∣ 24
Tactic:
have h : x - 3 ∣ x ^ 3 - 27
State after:
case h
x : ℤ
⊢ x - 3 ∣ x ^ 3 - 27

x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ x ^ 3 - 3 ↔ x - 3 ∣ 24

State before:
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ x ^ 3 - 3 ↔ x - 3 ∣ 24
Tactic:
constructor
State after:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ x ^ 3 - 3 → x - 3 ∣ 24

case mpr
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ 24 → x - 3 ∣ x ^ 3 - 3

State before:
case h
x : ℤ
⊢ x - 3 ∣ x ^ 3 - 27
Tactic:
use x ^ 2 + 3 * x + 9
State after:
case h
x : ℤ
⊢ x ^ 3 - 27 = (x - 3) * (x ^ 2 + 3 * x + 9)

State before:
case h
x : ℤ
⊢ x ^ 3 - 27 = (x - 3) * (x ^ 2 + 3 * x + 9)
Tactic:
ring
State after:
no goals

State before:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ x ^ 3 - 3 → x - 3 ∣ 24
Tactic:
intro h1
State after:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
⊢ x - 3 ∣ 24

State before:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
⊢ x - 3 ∣ 24
Tactic:
have h2 := dvd_sub h1 h
State after:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
h2 : x - 3 ∣ x ^ 3 - 3 - (x ^ 3 - 27)
⊢ x - 3 ∣ 24

State before:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
h2 : x - 3 ∣ x ^ 3 - 3 - (x ^ 3 - 27)
⊢ x - 3 ∣ 24
Tactic:
convert h2
State after:
case h.e'_4
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
h2 : x - 3 ∣ x ^ 3 - 3 - (x ^ 3 - 27)
⊢ 24 = x ^ 3 - 3 - (x ^ 3 - 27)

State before:
case h.e'_4
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
h2 : x - 3 ∣ x ^ 3 - 3 - (x ^ 3 - 27)
⊢ 24 = x ^ 3 - 3 - (x ^ 3 - 27)
Tactic:
ring
State after:
no goals

State before:
case mpr
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ 24 → x - 3 ∣ x ^ 3 - 3
Tactic:
intro h1
State after:
case mpr
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ 24
⊢ x - 3 ∣ x ^ 3 - 3

State before:
case mpr
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ 24
⊢ x - 3 ∣ x ^ 3 - 3
Tactic:
convert dvd_add h h1 using 1
State after:
case h.e'_4
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ 24
⊢ x ^ 3 - 3 = x ^ 3 - 27 + 24

State before:
case h.e'_4
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ 24
⊢ x ^ 3 - 3 = x ^ 3 - 27 + 24
Tactic:
ring
State after:
no goals