Theorem: HTPI.Example_6_4_1 (HTPILib/Chap6.lean)

State before:
⊢ ∀ m > 0, ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m
Tactic:
fix m : Nat
State after:
m : ℕ
⊢ m > 0 → ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m

State before:
m : ℕ
⊢ m > 0 → ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m
Tactic:
assume h1 : m > 0
State after:
m : ℕ
h1 : m > 0
⊢ ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m

State before:
m : ℕ
h1 : m > 0
⊢ ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m
Tactic:
by_strong_induc
State after:
m : ℕ
h1 : m > 0
⊢ ∀ (n : ℕ), (∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m) → ∃ q r, n = m * q + r ∧ r < m

State before:
m : ℕ
h1 : m > 0
⊢ ∀ (n : ℕ), (∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m) → ∃ q r, n = m * q + r ∧ r < m
Tactic:
fix n : Nat
State after:
m : ℕ
h1 : m > 0
n : ℕ
⊢ (∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m) → ∃ q r, n = m * q + r ∧ r < m

State before:
m : ℕ
h1 : m > 0
n : ℕ
⊢ (∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m) → ∃ q r, n = m * q + r ∧ r < m
Tactic:
assume ih : ∀ n_1 < n, ∃ (q r : Nat), n_1 = m * q + r ∧ r < m
State after:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
⊢ ∃ q r, n = m * q + r ∧ r < m

State before:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
by_cases h2 : n < m
State after:
case pos
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : n < m
⊢ ∃ q r, n = m * q + r ∧ r < m

case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
⊢ ∃ q r, n = m * q + r ∧ r < m

State before:
case pos
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : n < m
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
apply Exists.intro 0
State after:
case pos
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : n < m
⊢ ∃ r, n = m * 0 + r ∧ r < m

State before:
case pos
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : n < m
⊢ ∃ r, n = m * 0 + r ∧ r < m
Tactic:
apply Exists.intro n
State after:
case pos
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : n < m
⊢ n = m * 0 + n ∧ n < m

State before:
case pos
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : n < m
⊢ n = m * 0 + n ∧ n < m
Tactic:
apply And.intro _ h2
State after:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : n < m
⊢ n = m * 0 + n

State before:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : n < m
⊢ n = m * 0 + n
Tactic:
ring
State after:
no goals

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
have h3 : m ≤ n := by linarith
State after:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
⊢ ∃ q r, n = m * q + r ∧ r < m

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
obtain (k : Nat) (h4 : n = k + m) from Nat.exists_eq_add_of_le' h3
State after:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
⊢ ∃ q r, n = m * q + r ∧ r < m

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
have h5 : k < n := by linarith
State after:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
⊢ ∃ q r, n = m * q + r ∧ r < m

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
have h6 : ∃ (q r : Nat), k = m * q + r ∧ r < m := ih k h5
State after:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
⊢ ∃ q r, n = m * q + r ∧ r < m

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
obtain (q' : Nat)
  (h7 : ∃ (r : Nat), k = m * q' + r ∧ r < m) from h6
State after:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
⊢ ∃ q r, n = m * q + r ∧ r < m

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
obtain (r' : Nat) (h8 : k = m * q' + r' ∧ r' < m) from h7
State after:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ ∃ q r, n = m * q + r ∧ r < m

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ ∃ q r, n = m * q + r ∧ r < m
Tactic:
apply Exists.intro (q' + 1)
State after:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ ∃ r, n = m * (q' + 1) + r ∧ r < m

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ ∃ r, n = m * (q' + 1) + r ∧ r < m
Tactic:
apply Exists.intro r'
State after:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ n = m * (q' + 1) + r' ∧ r' < m

State before:
case neg
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ n = m * (q' + 1) + r' ∧ r' < m
Tactic:
apply And.intro _ h8.right
State after:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ n = m * (q' + 1) + r'

State before:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ n = m * (q' + 1) + r'
Tactic:
show n = m * (q' + 1) + r' from
  calc n
    _ = k + m := h4
    _ = m * q' + r' + m := by rw [h8.left]
    _ = m * (q' + 1) + r' := by ring
State after:
no goals

State before:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
⊢ m ≤ n
Tactic:
linarith
State after:
no goals

State before:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
⊢ k < n
Tactic:
linarith
State after:
no goals

State before:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ k + m = m * q' + r' + m
Tactic:
rw [h8.left]
State after:
no goals

State before:
m : ℕ
h1 : m > 0
n : ℕ
ih : ∀ n_1 < n, ∃ q r, n_1 = m * q + r ∧ r < m
h2 : ¬n < m
h3 : m ≤ n
k : ℕ
h4 : n = k + m
h5 : k < n
h6 : ∃ q r, k = m * q + r ∧ r < m
q' : ℕ
h7 : ∃ r, k = m * q' + r ∧ r < m
r' : ℕ
h8 : k = m * q' + r' ∧ r' < m
⊢ m * q' + r' + m = m * (q' + 1) + r'
Tactic:
ring
State after:
no goals