internlm/Lean-Github huggingface dataset:
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case intro.right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ m ≤ y
Tactic:
exact le_of_lt h6r
Proof state after:
no goals
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
d : ℤ
⊢ ¬(IsSquare (2 * d - 1) ∧ IsSquare (5 * d - 1) ∧ IsSquare (d * 13 - 1))
Tactic:
rintro ⟨⟨p, hp⟩, ⟨q, hq⟩, ⟨r, hr⟩⟩
Proof state after:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p * p
q : ℤ
hq : 5 * d - 1 = q * q
r : ℤ
hr : d * 13 - 1 = r * r
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p * p
q : ℤ
hq : 5 * d - 1 = q * q
r : ℤ
hr : d * 13 - 1 = r * r
⊢ False
Tactic:
rw [← pow_two] at hp hq hr
Proof state after:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ False
Tactic:
have hpodd : Odd p := (Int.odd_pow' two_ne_zero).mp (by use d - 1; rw [← hp]; ring)
Proof state after:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
hpodd : Odd p
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
hpodd : Odd p
⊢ False
Tactic:
cases' hpodd with k hk
Proof state after:
case intro.intro.intro.intro.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
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.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
⊢ False
Tactic:
have hp := hp.symm
Proof state after:
case intro.intro.intro.intro.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
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.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
⊢ False
Tactic:
have hdp : d  = 2*(k + k^2) + 1 := by
  rw [hk, ←(add_left_inj 1), sub_add_cancel _] at hp
  ring_nf at hp
  have h422 : (4 : ℤ) = 2 * 2 := by norm_num
  simp only [h422,  ← mul_assoc] at hp
  nth_rw 1 [← one_mul 2] at hp
  rw [← add_mul, ← add_mul, mul_left_inj' two_ne_zero] at hp
  rw [← hp]
  ring
Proof state after:
case intro.intro.intro.intro.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
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.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
⊢ False
Tactic:
have hdodd : Odd d := by use k + k ^ 2
Proof state after:
case intro.intro.intro.intro.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
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.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
⊢ False
Tactic:
have hd_sub_one : Even (d - 1) := by use (k + k ^ 2); rw [hdp]; ring
Proof state after:
case intro.intro.intro.intro.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)
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.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)
⊢ False
Tactic:
have hqeven : Even q := by
  refine (Int.even_pow' two_ne_zero).mp ?_
  have heq : 5 * d - 1 = 5 * (d - 1) + 4 := by ring_nf
  rw [← hq, heq]
  exact Even.add (Even.mul_left hd_sub_one 5) (by use 2; rfl)
Proof state after:
case intro.intro.intro.intro.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)
hqeven : Even q
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.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)
hqeven : Even q
⊢ False
Tactic:
have hreven : Even (r : ℤ) := by
  refine (Int.even_pow' two_ne_zero).mp ?_
  have heq : d * 13 - 1 = 13*(d - 1) + 12 := by
    rw [mul_comm]
    ring_nf
  rw [← hr, heq]
  exact Even.add (Even.mul_left hd_sub_one 13) (by use 6; rfl)
Proof state after:
case intro.intro.intro.intro.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)
hqeven : Even q
hreven : Even r
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.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)
hqeven : Even q
hreven : Even r
⊢ False
Tactic:
cases' hqeven with n hqeven'
Proof state after:
case intro.intro.intro.intro.intro.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)
hreven : Even r
n : ℤ
hqeven' : q = n + n
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.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)
hreven : Even r
n : ℤ
hqeven' : q = n + n
⊢ False
Tactic:
cases' hreven with m hreven'
Proof state after:
case intro.intro.intro.intro.intro.intro.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
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.intro.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
⊢ False
Tactic:
have h8d : d * 8 = 4*m^2 - 4*n^2 := by
  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:
case intro.intro.intro.intro.intro.intro.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
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.intro.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
⊢ False
Tactic:
have h4d : 4 * (2 * d) = 4 * (m^2 - n^2) := by ring_nf; rw [h8d]; ring_nf
Proof state after:
case intro.intro.intro.intro.intro.intro.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)
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.intro.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)
⊢ False
Tactic:
have hnm' : 2*d = (m + n)*(m - n):= by
  rw [← pow_two_sub_pow_two]
  refine (mul_right_inj' ?_).mp h4d
  decide
Proof state after:
case intro.intro.intro.intro.intro.intro.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)
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.intro.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)
⊢ False
Tactic:
have h2d : Even ((m + n) * (m - n)) := by use d; rw [← two_mul, hnm']
Proof state after:
case intro.intro.intro.intro.intro.intro.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))
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.intro.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
⊢ False
Tactic:
have hnm_sub : Even (m - n) := Int.even_sub.mpr hnm_parity
Proof state after:
case intro.intro.intro.intro.intro.intro.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
hnm_sub : Even (m - n)
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.intro.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
hnm_sub : Even (m - n)
⊢ False
Tactic:
have hnm_add : Even (m + n) := Int.even_add.mpr hnm_parity
Proof state after:
case intro.intro.intro.intro.intro.intro.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
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.intro.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
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
⊢ False
Tactic:
have hdeven : Even d := by
  cases' hnm_sub with v hnm_sub
  cases' hnm_add with w hnm_add
  simp only [hnm_sub, hnm_add, ← two_mul] at hnm'
  rw [mul_assoc,  mul_right_inj' two_ne_zero, ← mul_assoc, mul_comm w, mul_assoc, two_mul] at hnm'
  exact ⟨w * v, hnm'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.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
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
hdeven : Even d
⊢ False
Theorem: Imo1986P1.imo1986_p1'
Proof state before:
case intro.intro.intro.intro.intro.intro.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
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
hdeven : Even d
⊢ False
Tactic:
exact Int.even_iff_not_odd.mp hdeven hdodd
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
⊢ Odd (p ^ 2)
Tactic:
use d - 1
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
⊢ p ^ 2 = 2 * (d - 1) + 1
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
⊢ p ^ 2 = 2 * (d - 1) + 1
Tactic:
rw [← hp]
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
⊢ 2 * d - 1 = 2 * (d - 1) + 1
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
⊢ 2 * d - 1 = 2 * (d - 1) + 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
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
rw [hk, ←(add_left_inj 1), sub_add_cancel _] at hp
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 : (2 * k + 1) ^ 2 + 1 = 2 * d
⊢ d = 2 * (k + k ^ 2) + 1
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 : (2 * k + 1) ^ 2 + 1 = 2 * d
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
ring_nf at hp
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 : 2 + k * 4 + k ^ 2 * 4 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
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 : 2 + k * 4 + k ^ 2 * 4 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
have h422 : (4 : ℤ) = 2 * 2 := by norm_num
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 : 2 + k * 4 + k ^ 2 * 4 = d * 2
h422 : 4 = 2 * 2
⊢ d = 2 * (k + k ^ 2) + 1
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 : 2 + k * 4 + k ^ 2 * 4 = d * 2
h422 : 4 = 2 * 2
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
simp only [h422,  ← mul_assoc] at hp
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
h422 : 4 = 2 * 2
hp : 2 + k * 2 * 2 + k ^ 2 * 2 * 2 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
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
h422 : 4 = 2 * 2
hp : 2 + k * 2 * 2 + k ^ 2 * 2 * 2 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
nth_rw 1 [← one_mul 2] at hp
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
h422 : 4 = 2 * 2
hp : 1 * 2 + k * 2 * 2 + k ^ 2 * 2 * 2 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
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
h422 : 4 = 2 * 2
hp : 1 * 2 + k * 2 * 2 + k ^ 2 * 2 * 2 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
rw [← add_mul, ← add_mul, mul_left_inj' two_ne_zero] at hp
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
h422 : 4 = 2 * 2
hp : 1 + k * 2 + k ^ 2 * 2 = d
⊢ d = 2 * (k + k ^ 2) + 1
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
h422 : 4 = 2 * 2
hp : 1 + k * 2 + k ^ 2 * 2 = d
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
rw [← hp]
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
h422 : 4 = 2 * 2
hp : 1 + k * 2 + k ^ 2 * 2 = d
⊢ 1 + k * 2 + k ^ 2 * 2 = 2 * (k + k ^ 2) + 1
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
h422 : 4 = 2 * 2
hp : 1 + k * 2 + k ^ 2 * 2 = d
⊢ 1 + k * 2 + k ^ 2 * 2 = 2 * (k + k ^ 2) + 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 : 2 + k * 4 + k ^ 2 * 4 = d * 2
⊢ 4 = 2 * 2
Tactic:
norm_num
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
⊢ Odd d
Tactic:
use k + k ^ 2
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
⊢ Even (d - 1)
Tactic:
use (k + k ^ 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
⊢ d - 1 = k + k ^ 2 + (k + k ^ 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
⊢ d - 1 = k + k ^ 2 + (k + k ^ 2)
Tactic:
rw [hdp]
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
⊢ 2 * (k + k ^ 2) + 1 - 1 = k + k ^ 2 + (k + k ^ 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
⊢ 2 * (k + k ^ 2) + 1 - 1 = k + k ^ 2 + (k + k ^ 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)
⊢ Even q
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)
⊢ Even (q ^ 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)
⊢ Even (q ^ 2)
Tactic:
have heq : 5 * d - 1 = 5 * (d - 1) + 4 := by 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)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even (q ^ 2)