Theorem: HTPI.Theorem_3_4_7 (HTPILib/Chap3.lean)

State before:
⊢ ∀ (n : ℤ), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n
Tactic:
fix n : Int
State after:
n : ℤ
⊢ 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n

State before:
n : ℤ
⊢ 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n
Tactic:
apply Iff.intro
State after:
case mp
n : ℤ
⊢ 6 ∣ n → 2 ∣ n ∧ 3 ∣ n

case mpr
n : ℤ
⊢ 2 ∣ n ∧ 3 ∣ n → 6 ∣ n

State before:
case mp
n : ℤ
⊢ 6 ∣ n → 2 ∣ n ∧ 3 ∣ n
Tactic:
assume h1 : 6 ∣ n
State after:
case mp
n : ℤ
h1 : 6 ∣ n
⊢ 2 ∣ n ∧ 3 ∣ n

State before:
case mp
n : ℤ
h1 : 6 ∣ n
⊢ 2 ∣ n ∧ 3 ∣ n
Tactic:
define at h1
State after:
case mp
n : ℤ
h1 : ∃ c, n = 6 * c
⊢ 2 ∣ n ∧ 3 ∣ n

State before:
case mp
n : ℤ
h1 : ∃ c, n = 6 * c
⊢ 2 ∣ n ∧ 3 ∣ n
Tactic:
obtain (k : Int) (h2 : n = 6 * k) from h1
State after:
case mp
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n ∧ 3 ∣ n

State before:
case mp
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n ∧ 3 ∣ n
Tactic:
apply And.intro
State after:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n

case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 3 ∣ n

State before:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n
Tactic:
define
State after:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ c, n = 2 * c

State before:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ c, n = 2 * c
Tactic:
apply Exists.intro (3 * k)
State after:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * (3 * k)

State before:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * (3 * k)
Tactic:
rewrite [←mul_assoc 2 3 k]
State after:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * 3 * k

State before:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 2 * 3 * k
Tactic:
show n = 2 * 3 * k from h2
State after:
no goals

State before:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 3 ∣ n
Tactic:
define
State after:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ c, n = 3 * c

State before:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ c, n = 3 * c
Tactic:
apply Exists.intro (2 * k)
State after:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 3 * (2 * k)

State before:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 3 * (2 * k)
Tactic:
rewrite [←mul_assoc 3 2 k]
State after:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 3 * 2 * k

State before:
case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ n = 3 * 2 * k
Tactic:
show n = 3 * 2 * k from h2
State after:
no goals

State before:
case mpr
n : ℤ
⊢ 2 ∣ n ∧ 3 ∣ n → 6 ∣ n
Tactic:
assume h1 : 2 ∣ n ∧ 3 ∣ n
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
⊢ 6 ∣ n

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
⊢ 6 ∣ n
Tactic:
have h2 : 2 ∣ n := h1.left
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : 2 ∣ n
⊢ 6 ∣ n

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : 2 ∣ n
⊢ 6 ∣ n
Tactic:
have h3 : 3 ∣ n := h1.right
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : 2 ∣ n
h3 : 3 ∣ n
⊢ 6 ∣ n

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : 2 ∣ n
h3 : 3 ∣ n
⊢ 6 ∣ n
Tactic:
define at h2
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : 3 ∣ n
⊢ 6 ∣ n

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : 3 ∣ n
⊢ 6 ∣ n
Tactic:
define at h3
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
⊢ 6 ∣ n

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
⊢ 6 ∣ n
Tactic:
define
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
⊢ ∃ c, n = 6 * c

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
⊢ ∃ c, n = 6 * c
Tactic:
obtain (j : Int) (h4 : n = 2 * j) from h2
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
⊢ ∃ c, n = 6 * c

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
⊢ ∃ c, n = 6 * c
Tactic:
obtain (k : Int) (h5 : n = 3 * k) from h3
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ ∃ c, n = 6 * c

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ ∃ c, n = 6 * c
Tactic:
have h6 : 6 * (j - k) = n :=
  calc 6 * (j - k)
    _ = 3 * (2 * j) - 2 * (3 * k) := by ring
    _ = 3 * n - 2 * n := by rw [←h4, ←h5]
    _ = n := by ring
State after:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
h6 : 6 * (j - k) = n
⊢ ∃ c, n = 6 * c

State before:
case mpr
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
h6 : 6 * (j - k) = n
⊢ ∃ c, n = 6 * c
Tactic:
show ∃ (c : Int), n = 6 * c from
  Exists.intro (j - k) h6.symm
State after:
no goals

State before:
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 6 * (j - k) = 3 * (2 * j) - 2 * (3 * k)
Tactic:
ring
State after:
no goals

State before:
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 3 * (2 * j) - 2 * (3 * k) = 3 * n - 2 * n
Tactic:
rw [←h4, ←h5]
State after:
no goals

State before:
n : ℤ
h1 : 2 ∣ n ∧ 3 ∣ n
h2 : ∃ c, n = 2 * c
h3 : ∃ c, n = 3 * c
j : ℤ
h4 : n = 2 * j
k : ℤ
h5 : n = 3 * k
⊢ 3 * n - 2 * n = n
Tactic:
ring
State after:
no goals