internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Example_6_3_2
Proof state before:
case Induction_Step
a : ℝ
m n : ℕ
⊢ a ^ (m + n) = a ^ m * a ^ n → a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
Tactic:
assume ih : a ^ (m + n) = a ^ m * a ^ n
Proof state after:
case Induction_Step
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
Theorem: HTPI.Example_6_3_2
Proof state before:
case Induction_Step
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
Tactic:
show a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1) from
  calc a ^ (m + (n + 1))
    _ = a ^ ((m + n) + 1) := by rw [add_assoc]
    _ = a * a ^ (m + n) := by rfl
    _ = a * (a ^ m * a ^ n) := by rw [ih]
    _ = a ^ m * (a * a ^ n) := by
          rw [←mul_assoc, mul_comm a, mul_assoc]
    _ = a ^ m * (a ^ (n + 1)) := by rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + (n + 1)) = a ^ (m + n + 1)
Tactic:
rw [add_assoc]
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + n + 1) = a * a ^ (m + n)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a * a ^ (m + n) = a * (a ^ m * a ^ n)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a * (a ^ m * a ^ n) = a ^ m * (a * a ^ n)
Tactic:
rw [←mul_assoc, mul_comm a, mul_assoc]
Proof state after:
no goals
Theorem: HTPI.Example_6_3_2
Proof state before:
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ m * (a * a ^ n) = a ^ m * a ^ (n + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
⊢ ∀ x > -1, ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x
Tactic:
fix x : Real
Proof state after:
x : ℝ
⊢ x > -1 → ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
⊢ x > -1 → ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x
Tactic:
assume h1 : x > -1
Proof state after:
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x
Tactic:
by_induc
Proof state after:
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥ 1 + ↑0 * x

case Induction_Step
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x → (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Theorem: HTPI.Example_6_3_4
Proof state before:
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥ 1 + ↑0 * x
Tactic:
rewrite [Nat.cast_zero]
Proof state after:
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥ 1 + 0 * x
Theorem: HTPI.Example_6_3_4
Proof state before:
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥ 1 + 0 * x
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
case Induction_Step
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x → (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
⊢ (1 + x) ^ n ≥ 1 + ↑n * x → (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Theorem: HTPI.Example_6_3_4
Proof state before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
⊢ (1 + x) ^ n ≥ 1 + ↑n * x → (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Tactic:
assume ih : (1 + x) ^ n ≥ 1 + n * x
Proof state after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Theorem: HTPI.Example_6_3_4
Proof state before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Tactic:
rewrite [Nat.cast_succ]
Proof state after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Theorem: HTPI.Example_6_3_4
Proof state before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Tactic:
have h2 : 0 ≤ 1 + x := by linarith
Proof state after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Theorem: HTPI.Example_6_3_4
Proof state before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Tactic:
have h3 : x ^ 2 ≥ 0 := sq_nonneg x
Proof state after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Theorem: HTPI.Example_6_3_4
Proof state before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Tactic:
have h4 : n * x ^ 2 ≥ 0 :=
  calc n * x ^ 2
    _ ≥ n * 0 := by rel [h3]
    _ = 0 := by ring
Proof state after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Theorem: HTPI.Example_6_3_4
Proof state before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Tactic:
show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
  calc (1 + x) ^ (n + 1)
    _ = (1 + x) * (1 + x) ^ n := by rfl
    _ ≥ (1 + x) * (1 + n * x) := by rel [ih]
    _ = 1 + x + n * x + n * x ^ 2 := by ring
    _ ≥ 1 + x + n * x + 0 := by rel [h4]
    _ = 1 + (n + 1) * x := by ring
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ 0 ≤ 1 + x
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
⊢ ↑n * x ^ 2 ≥ ↑n * 0
Tactic:
rel [h3]
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
⊢ ↑n * 0 = 0
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) = (1 + x) * (1 + x) ^ n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) * (1 + x) ^ n ≥ (1 + x) * (1 + ↑n * x)
Tactic:
rel [ih]
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) * (1 + ↑n * x) = 1 + x + ↑n * x + ↑n * x ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ 1 + x + ↑n * x + ↑n * x ^ 2 ≥ 1 + x + ↑n * x + 0
Tactic:
rel [h4]
Proof state after:
no goals
Theorem: HTPI.Example_6_3_4
Proof state before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ 1 + x + ↑n * x + 0 = 1 + (↑n + 1) * x
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_6_4_1
Proof state before:
⊢ ∀ m > 0, ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m
Tactic:
fix m : Nat
Proof state after:
m : ℕ
⊢ m > 0 → ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m
Theorem: HTPI.Example_6_4_1
Proof state before:
m : ℕ
⊢ m > 0 → ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m
Tactic:
assume h1 : m > 0
Proof state after:
m : ℕ
h1 : m > 0
⊢ ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m
Theorem: HTPI.Example_6_4_1
Proof state before:
m : ℕ
h1 : m > 0
⊢ ∀ (n : ℕ), ∃ q r, n = m * q + r ∧ r < m
Tactic:
by_strong_induc
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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)
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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'
Proof 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
Theorem: HTPI.Example_6_4_1
Proof 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
Proof 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'
Theorem: HTPI.Example_6_4_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Example_6_4_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Example_6_4_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Example_6_4_1
Proof 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]
Proof state after:
no goals
Theorem: HTPI.Example_6_4_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.exists_eq_add_one_of_ne_zero
Proof state before:
n : ℕ
h1 : n ≠ 0
⊢ ∃ k, n = k + 1
Tactic:
have h2 : 1 ≤ n := Nat.pos_of_ne_zero h1
Proof state after:
n : ℕ
h1 : n ≠ 0
h2 : 1 ≤ n
⊢ ∃ k, n = k + 1
Theorem: HTPI.exists_eq_add_one_of_ne_zero
Proof state before:
n : ℕ
h1 : n ≠ 0
h2 : 1 ≤ n
⊢ ∃ k, n = k + 1
Tactic:
show ∃ (k : Nat), n = k + 1 from Nat.exists_eq_add_of_le' h2
Proof state after:
no goals
Theorem: HTPI.exists_eq_add_two_of_ne_zero_one
Proof state before:
n : ℕ
h1 : n ≠ 0
h2 : n ≠ 1
⊢ ∃ k, n = k + 2
Tactic:
have h3 : 1 ≤ n := Nat.pos_of_ne_zero h1
Proof state after:
n : ℕ
h1 : n ≠ 0
h2 : n ≠ 1
h3 : 1 ≤ n
⊢ ∃ k, n = k + 2
Theorem: HTPI.exists_eq_add_two_of_ne_zero_one
Proof state before:
n : ℕ
h1 : n ≠ 0
h2 : n ≠ 1
h3 : 1 ≤ n
⊢ ∃ k, n = k + 2
Tactic:
have h4 : 2 ≤ n := lt_of_le_of_ne' h3 h2
Proof state after:
n : ℕ
h1 : n ≠ 0
h2 : n ≠ 1
h3 : 1 ≤ n
h4 : 2 ≤ n
⊢ ∃ k, n = k + 2
Theorem: HTPI.exists_eq_add_two_of_ne_zero_one
Proof state before:
n : ℕ
h1 : n ≠ 0
h2 : n ≠ 1
h3 : 1 ≤ n
h4 : 2 ≤ n
⊢ ∃ k, n = k + 2
Tactic:
show ∃ (k : Nat), n = k + 2 from Nat.exists_eq_add_of_le' h4
Proof state after:
no goals
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
⊢ (∃ n, n ∈ S) → ∃ n ∈ S, ∀ m ∈ S, n ≤ m
Tactic:
contrapos
Proof state after:
S : Set ℕ
⊢ (¬∃ n ∈ S, ∀ m ∈ S, n ≤ m) → ¬∃ n, n ∈ S
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
⊢ (¬∃ n ∈ S, ∀ m ∈ S, n ≤ m) → ¬∃ n, n ∈ S
Tactic:
assume h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ¬∃ n, n ∈ S
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ¬∃ n, n ∈ S
Tactic:
quant_neg
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ∀ (n : ℕ), n ∉ S
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ∀ (n : ℕ), n ∉ S
Tactic:
by_strong_induc
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ∀ (n : ℕ), (∀ n_1 < n, n_1 ∉ S) → n ∉ S
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ∀ (n : ℕ), (∀ n_1 < n, n_1 ∉ S) → n ∉ S
Tactic:
fix n : Nat
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
⊢ (∀ n_1 < n, n_1 ∉ S) → n ∉ S
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
⊢ (∀ n_1 < n, n_1 ∉ S) → n ∉ S
Tactic:
assume ih : ∀ n_1 < n, n_1 ∉ S
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
⊢ n ∉ S
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
⊢ n ∉ S
Tactic:
contradict h1 with h2
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ ∃ n ∈ S, ∀ m ∈ S, n ≤ m
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ ∃ n ∈ S, ∀ m ∈ S, n ≤ m
Tactic:
apply Exists.intro n
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ n ∈ S ∧ ∀ m ∈ S, n ≤ m
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ n ∈ S ∧ ∀ m ∈ S, n ≤ m
Tactic:
apply And.intro h2
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ ∀ m ∈ S, n ≤ m
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ ∀ m ∈ S, n ≤ m
Tactic:
fix m : Nat
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
⊢ m ∈ S → n ≤ m
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
⊢ m ∈ S → n ≤ m
Tactic:
assume h3 : m ∈ S
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
⊢ n ≤ m
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
⊢ n ≤ m
Tactic:
have h4 : m < n → m ∉ S := ih m
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m < n → m ∉ S
⊢ n ≤ m
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m < n → m ∉ S
⊢ n ≤ m
Tactic:
contrapos at h4
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m ∈ S → ¬m < n
⊢ n ≤ m
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m ∈ S → ¬m < n
⊢ n ≤ m
Tactic:
have h5 : ¬m < n := h4 h3
Proof state after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m ∈ S → ¬m < n
h5 : ¬m < n
⊢ n ≤ m
Theorem: HTPI.well_ord_princ
Proof state before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m ∈ S → ¬m < n
h5 : ¬m < n
⊢ n ≤ m
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Theorem_6_4_5
Proof state before:
⊢ ¬∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
Tactic:
set S : Set Nat :=
  {q : Nat | ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0}
Proof state after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
⊢ ¬∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
Theorem: HTPI.Theorem_6_4_5
Proof state before:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
⊢ ¬∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
Tactic:
by_contra h1
Proof state after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
⊢ False
Theorem: HTPI.Theorem_6_4_5
Proof state before:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
⊢ False
Tactic:
have h2 : ∃ (q : Nat), q ∈ S := h1
Proof state after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
⊢ False
Theorem: HTPI.Theorem_6_4_5
Proof state before:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
⊢ False
Tactic:
have h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r := well_ord_princ S h2
Proof state after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
⊢ False
Theorem: HTPI.Theorem_6_4_5
Proof state before:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
⊢ False
Tactic:
obtain (q : Nat) (h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r) from h3
Proof state after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
⊢ False
Theorem: HTPI.Theorem_6_4_5
Proof state before:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
⊢ False
Tactic:
have qinS : q ∈ S := h4.left
Proof state after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : q ∈ S
⊢ False