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

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}
State after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
⊢ ¬∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0

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
State after:
S : Set ℕ := {q | ∃ p, p * p = 2 * (q * q) ∧ q ≠ 0}
h1 : ∃ q p, p * p = 2 * (q * q) ∧ q ≠ 0
⊢ False

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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)
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

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
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

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'
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

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
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

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
State after:
no goals

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]
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')

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
State after:
no goals

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
State after:
no goals

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]
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'))

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
State after:
no goals

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' ≠ 0
Tactic:
contradict qne0 with h11
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')
h11 : q' = 0
⊢ q = 0

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')
h11 : q' = 0
⊢ q = 0
Tactic:
rewrite [q'halfq, h11]
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')
h11 : q' = 0
⊢ 2 * 0 = 0

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')
h11 : q' = 0
⊢ 2 * 0 = 0
Tactic:
rfl
State after:
no goals