internlm/Lean-Github huggingface dataset:
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
qinS : q ∈ S
⊢ False
Tactic:
have qleast : ∀ r ∈ S, q ≤ r := h4.right
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
qleast : ∀ 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
qinS : q ∈ S
qleast : ∀ r ∈ S, q ≤ r
⊢ False
Tactic:
define at qinS
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
⊢ False
Tactic:
obtain (p : Nat) (h5 : p * p = 2 * (q * q) ∧ q ≠ 0) from qinS
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : 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
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
⊢ False
Tactic:
have pqsqrt2 : p * p = 2 * (q * q) := h5.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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
⊢ False
Tactic:
have qne0 : q ≠ 0 := h5.right
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : 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
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
⊢ False
Tactic:
have h6 : nat_even (p * p) := Exists.intro (q * q) pqsqrt2
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even (p * p)
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even (p * p)
⊢ False
Tactic:
rewrite [sq_even_iff_even p] at h6
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
⊢ False
Tactic:
obtain (p' : Nat) (p'halfp : p = 2 * p') from h6
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
⊢ False
Tactic:
have h7 : 2 * (2 * (p' * p')) = 2 * (q * q) := by
  rewrite [←pqsqrt2, p'halfp]
  ring
  done
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (2 * (p' * p')) = 2 * (q * q)
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (2 * (p' * p')) = 2 * (q * q)
⊢ False
Tactic:
have h8 : 2 > 0 := by decide
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (2 * (p' * p')) = 2 * (q * q)
h8 : 2 > 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
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (2 * (p' * p')) = 2 * (q * q)
h8 : 2 > 0
⊢ False
Tactic:
rewrite [mul_left_cancel_iff_of_pos h8] at h7
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 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
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
⊢ False
Tactic:
have h9 : nat_even (q * q) := Exists.intro (p' * p') h7.symm
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even (q * q)
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even (q * q)
⊢ False
Tactic:
rewrite [sq_even_iff_even q] at h9
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
⊢ False
Tactic:
obtain (q' : Nat) (q'halfq : q = 2 * q') from h9
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
⊢ False
Tactic:
have h10 : 2 * (p' * p') = 2 * (2 * (q' * q')) := by
  rewrite [h7, q'halfq]
  ring
  done
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : 2 * (p' * p') = 2 * (2 * (q' * q'))
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : 2 * (p' * p') = 2 * (2 * (q' * q'))
⊢ False
Tactic:
rewrite [mul_left_cancel_iff_of_pos h8] at h10
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
⊢ False
Tactic:
have q'ne0 : q' ≠ 0 := by
  contradict qne0 with h11
  rewrite [q'halfq, h11]
  rfl
  done
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : 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
h2 : ∃ q, q ∈ S
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
⊢ False
Tactic:
have q'inS : q' ∈ S := Exists.intro p' (And.intro h10 q'ne0)
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
q'inS : 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
h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r
q : ℕ
h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
q'inS : q' ∈ S
⊢ False
Tactic:
have qleq' : q ≤ q' := qleast q' q'inS
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
q'inS : q' ∈ S
qleq' : q ≤ q'
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
q'inS : q' ∈ S
qleq' : q ≤ q'
⊢ False
Tactic:
rewrite [q'halfq] at qleq'
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
q'inS : q' ∈ S
qleq' : 2 * q' ≤ q'
⊢ 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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
q'inS : q' ∈ S
qleq' : 2 * q' ≤ q'
⊢ False
Tactic:
contradict q'ne0
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
q'inS : q' ∈ S
qleq' : 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}
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
h10 : p' * p' = 2 * (q' * q')
q'ne0 : q' ≠ 0
q'inS : q' ∈ S
qleq' : 2 * q' ≤ q'
⊢ q' = 0
Tactic:
linarith
Proof state after:
no goals
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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
⊢ 2 * (2 * (p' * p')) = 2 * (q * q)
Tactic:
rewrite [←pqsqrt2, p'halfp]
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
⊢ 2 * (2 * (p' * p')) = 2 * p' * (2 * p')
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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
⊢ 2 * (2 * (p' * p')) = 2 * p' * (2 * p')
Tactic:
ring
Proof state after:
no goals
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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (2 * (p' * p')) = 2 * (q * q)
⊢ 2 > 0
Tactic:
decide
Proof state after:
no goals
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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
⊢ 2 * (p' * p') = 2 * (2 * (q' * q'))
Tactic:
rewrite [h7, q'halfq]
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 : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
⊢ 2 * q' * (2 * q') = 2 * (2 * (q' * q'))
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
qinS : ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0
qleast : ∀ r ∈ S, q ≤ r
p : ℕ
h5 : p * p = 2 * (q * q) ∧ q ≠ 0
pqsqrt2 : p * p = 2 * (q * q)
qne0 : q ≠ 0
h6 : nat_even p
p' : ℕ
p'halfp : p = 2 * p'
h7 : 2 * (p' * p') = q * q
h8 : 2 > 0
h9 : nat_even q
q' : ℕ
q'halfq : q = 2 * q'
⊢ 2 * q' * (2 * q') = 2 * (2 * (q' * q'))
Tactic:
ring
Proof state after:
no goals