internlm/Lean-Github huggingface dataset:
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even (q ^ 2)
Tactic:
rw [← hq, heq]
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even (5 * (d - 1) + 4)
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even (5 * (d - 1) + 4)
Tactic:
exact Even.add (Even.mul_left hd_sub_one 5) (by use 2; rfl)
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ 5 * d - 1 = 5 * (d - 1) + 4
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even 4
Tactic:
use 2
Proof state after:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ 4 = 2 + 2
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ 4 = 2 + 2
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ Even r
Tactic:
refine (Int.even_pow' two_ne_zero).mp ?_
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ Even (r ^ 2)
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ Even (r ^ 2)
Tactic:
have heq : d * 13 - 1 = 13*(d - 1) + 12 := by
  rw [mul_comm]
  ring_nf
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even (r ^ 2)
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even (r ^ 2)
Tactic:
rw [← hr, heq]
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even (13 * (d - 1) + 12)
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even (13 * (d - 1) + 12)
Tactic:
exact Even.add (Even.mul_left hd_sub_one 13) (by use 6; rfl)
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ d * 13 - 1 = 13 * (d - 1) + 12
Tactic:
rw [mul_comm]
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ 13 * d - 1 = 13 * (d - 1) + 12
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ 13 * d - 1 = 13 * (d - 1) + 12
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even 12
Tactic:
use 6
Proof state after:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ 12 = 6 + 6
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ 12 = 6 + 6
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ d * 8 = 4 * m ^ 2 - 4 * n ^ 2
Tactic:
calc d * 8 = (d * 13 - 1) - (5 * d - 1) := by ring
      _ = r^2 - q^2 := by rw [hr, hq]
      _ = (m + m)^2 - (n + n)^2 := by rw [hqeven', hreven']
      _ = 4*m^2 - 4*n^2 := by ring
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ d * 8 = d * 13 - 1 - (5 * d - 1)
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ d * 13 - 1 - (5 * d - 1) = r ^ 2 - q ^ 2
Tactic:
rw [hr, hq]
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ r ^ 2 - q ^ 2 = (m + m) ^ 2 - (n + n) ^ 2
Tactic:
rw [hqeven', hreven']
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ (m + m) ^ 2 - (n + n) ^ 2 = 4 * m ^ 2 - 4 * n ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
Tactic:
ring_nf
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ d * 8 = m ^ 2 * 4 - n ^ 2 * 4
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ d * 8 = m ^ 2 * 4 - n ^ 2 * 4
Tactic:
rw [h8d]
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ 4 * m ^ 2 - 4 * n ^ 2 = m ^ 2 * 4 - n ^ 2 * 4
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ 4 * m ^ 2 - 4 * n ^ 2 = m ^ 2 * 4 - n ^ 2 * 4
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 2 * d = (m + n) * (m - n)
Tactic:
rw [← pow_two_sub_pow_two]
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 2 * d = m ^ 2 - n ^ 2
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 2 * d = m ^ 2 - n ^ 2
Tactic:
refine (mul_right_inj' ?_).mp h4d
Proof state after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 4 ≠ 0
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 4 ≠ 0
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
⊢ Even ((m + n) * (m - n))
Tactic:
use d
Proof state after:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
⊢ (m + n) * (m - n) = d + d
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
⊢ (m + n) * (m - n) = d + d
Tactic:
rw [← two_mul, hnm']
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
⊢ Even m ↔ Even n
Tactic:
cases' Int.even_mul.mp h2d with hmneven hmneven
Proof state after:
case inl
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hmneven : Even (m + n)
⊢ Even m ↔ Even n

case inr
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hmneven : Even (m - n)
⊢ Even m ↔ Even n
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case inl
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hmneven : Even (m + n)
⊢ Even m ↔ Even n
Tactic:
exact Int.even_add.mp hmneven
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case inr
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hmneven : Even (m - n)
⊢ Even m ↔ Even n
Tactic:
exact Int.even_sub.mp hmneven
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
⊢ Even d
Tactic:
cases' hnm_sub with v hnm_sub
Proof state after:
case intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_add : Even (m + n)
v : ℤ
hnm_sub : m - n = v + v
⊢ Even d
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_add : Even (m + n)
v : ℤ
hnm_sub : m - n = v + v
⊢ Even d
Tactic:
cases' hnm_add with w hnm_add
Proof state after:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
⊢ Even d
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
⊢ Even d
Tactic:
simp only [hnm_sub, hnm_add, ← two_mul] at hnm'
Proof state after:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
hnm' : 2 * d = 2 * w * (2 * v)
⊢ Even d
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
hnm' : 2 * d = 2 * w * (2 * v)
⊢ Even d
Tactic:
rw [mul_assoc,  mul_right_inj' two_ne_zero, ← mul_assoc, mul_comm w, mul_assoc, two_mul] at hnm'
Proof state after:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
hnm' : d = w * v + w * v
⊢ Even d
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
hnm' : d = w * v + w * v
⊢ Even d
Tactic:
exact ⟨w * v, hnm'⟩
Proof state after:
no goals
Theorem: Imo2008P5.even_subsets_card
Proof state before:
α : Type
inst✝ : Fintype α
⊢ Fintype.card { s // Even s.card } = 2 ^ (Fintype.card α - 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: Imo2008P5.claim
Proof state before:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
let c : Fin n → ℕ := fun i ↦ Nat.card { j | f.val j = ⟨i, by omega⟩ }
Proof state after:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Theorem: Imo2008P5.claim
Proof state before:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
have hcp : ∀ i : Fin n, 0 < c i := by sorry
Proof state after:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
hcp : ∀ (i : Fin n), 0 < c i
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Theorem: Imo2008P5.claim
Proof state before:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
hcp : ∀ (i : Fin n), 0 < c i
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
have hc : ∑ i : Fin n, c i = k := by sorry
Proof state after:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
hcp : ∀ (i : Fin n), 0 < c i
hc : ∑ i : Fin n, c i = k
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Theorem: Imo2008P5.claim
Proof state before:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
hcp : ∀ (i : Fin n), 0 < c i
hc : ∑ i : Fin n, c i = k
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)
Tactic:
let S : Type :=
  (i : Fin n) →
    {s : Finset { j : Fin k | f.val j = ⟨i, by omega⟩} // Even (Finset.card s) }
Proof state after:
n k : ℕ
hn : 0 < n
hnk : n ≤ k
he : Even (k - n)
f : { b // MSequence n k b }
c : Fin n → ℕ := fun i => Nat.card ↑{j | ↑f j = ⟨↑i, ⋯⟩}
hcp : ∀ (i : Fin n), 0 < c i
hc : ∑ i : Fin n, c i = k
S : Type := (i : Fin n) → { s // Even s.card }
⊢ {g | ψ n k g = f}.ncard = 2 ^ (k - n)