internlm/Lean-Github huggingface dataset:
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ (P + X - ↑a - ↑b).natDegree = P.natDegree
Tactic:
rw [sub_sub, ← Int.cast_add]
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ (P + X - ↑(a + b)).natDegree = P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ (P + X - ↑(a + b)).natDegree = P.natDegree
Tactic:
have h₁ : (P + X).natDegree = P.natDegree := by
  rw [natDegree_add_eq_left_of_natDegree_lt]
  simpa using hP
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
h₁ : (P + X).natDegree = P.natDegree
⊢ (P + X - ↑(a + b)).natDegree = P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
h₁ : (P + X).natDegree = P.natDegree
⊢ (P + X - ↑(a + b)).natDegree = P.natDegree
Tactic:
rwa [natDegree_sub_eq_left_of_natDegree_lt]
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
h₁ : (P + X).natDegree = P.natDegree
⊢ (↑(a + b)).natDegree < (P + X).natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
h₁ : (P + X).natDegree = P.natDegree
⊢ (↑(a + b)).natDegree < (P + X).natDegree
Tactic:
rw [h₁, natDegree_intCast]
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
h₁ : (P + X).natDegree = P.natDegree
⊢ 0 < P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
h₁ : (P + X).natDegree = P.natDegree
⊢ 0 < P.natDegree
Tactic:
exact zero_lt_one.trans hP
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ (P + X).natDegree = P.natDegree
Tactic:
rw [natDegree_add_eq_left_of_natDegree_lt]
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ X.natDegree < P.natDegree
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ X.natDegree < P.natDegree
Tactic:
simpa using hP
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
⊢ P + X - ↑a - ↑b ≠ 0
Tactic:
intro h
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False
Tactic:
rw [h, natDegree_zero] at hPab
Proof state after:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : 0 = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : 0 = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False
Tactic:
rw [← hPab] at hP
Proof state after:
P : ℤ[X]
hP : 1 < 0
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : 0 = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
P : ℤ[X]
hP : 1 < 0
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : 0 = P.natDegree
h : P + X - ↑a - ↑b = 0
⊢ False
Tactic:
exact (zero_le_one.not_lt hP).elim
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
⊢ (P.comp P - X).roots.toFinset ⊆ (P + X - ↑a - ↑b).roots.toFinset
Tactic:
intro t ht
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
ht : t ∈ (P.comp P - X).roots.toFinset
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
ht : t ∈ (P.comp P - X).roots.toFinset
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Tactic:
replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
ht : (P.comp P - X).IsRoot t
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
ht : (P.comp P - X).IsRoot t
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Tactic:
rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
ht : Polynomial.eval (Polynomial.eval t P) P = t
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
ht : Polynomial.eval (Polynomial.eval t P) P = t
⊢ t ∈ (P + X - ↑a - ↑b).roots.toFinset
Tactic:
simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def, eval_sub,
  eval_add, eval_X, eval_C, eval_intCast, Int.cast_id, zero_add]
Proof state after:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
ht : Polynomial.eval (Polynomial.eval t P) P = t
⊢ Polynomial.eval t P + t = b + a
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
ht : Polynomial.eval (Polynomial.eval t P) P = t
⊢ Polynomial.eval t P + t = b + a
Tactic:
apply (Int.add_eq_add_of_natAbs_eq_of_natAbs_eq hab _ _).symm <;>
    apply Int.natAbs_eq_of_dvd_dvd <;> set u := P.eval t
Proof state after:
case hmn
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - b ∣ t - a

case hnm
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - a ∣ u - b

case hmn
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - a ∣ t - b

case hnm
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - b ∣ u - a
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case hmn
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - b ∣ t - a
Tactic:
rw [← ha, ← ht]
Proof state after:
case hmn
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - b ∣ Polynomial.eval u P - Polynomial.eval b P
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case hmn
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - b ∣ Polynomial.eval u P - Polynomial.eval b P
Tactic:
apply sub_dvd_eval_sub
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case hnm
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - a ∣ u - b
Tactic:
apply sub_dvd_eval_sub
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case hmn
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - a ∣ t - b
Tactic:
rw [← ht]
Proof state after:
case hmn
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - a ∣ Polynomial.eval u P - b
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case hmn
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ u - a ∣ Polynomial.eval u P - b
Tactic:
apply sub_dvd_eval_sub
Proof state after:
no goals
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case hnm
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - b ∣ u - a
Tactic:
rw [← ha]
Proof state after:
case hnm
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - b ∣ u - Polynomial.eval b P
Theorem: Imo2006P5.imo2006_p5'
Proof state before:
case hnm
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
hPab' : P + X - ↑a - ↑b ≠ 0
t : ℤ
u : ℤ := Polynomial.eval t P
ht : Polynomial.eval u P = t
⊢ t - b ∣ u - Polynomial.eval b P
Tactic:
apply sub_dvd_eval_sub
Proof state after:
no goals
Theorem: Bulgaria1998P6.lemma_1'
Proof state before:
a b c : ℕ
ha : 0 < a
hb : 0 < b
hc : 0 < c
h : a ^ 4 = b ^ 4 + c ^ 2
⊢ False
Tactic:
induction' a using Nat.strongInductionOn with a ih
Proof state after:
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
⊢ False
Theorem: Bulgaria1998P6.lemma_1'
Proof state before:
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
⊢ False
Tactic:
have hab : Nat.gcd a b = 1 := sorry
Proof state after:
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
⊢ False
Theorem: Bulgaria1998P6.lemma_1'
Proof state before:
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
⊢ False
Tactic:
obtain c_even | c_odd := Nat.even_or_odd c
Proof state after:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
⊢ False

case ind.inr
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_odd : Odd c
⊢ False
Theorem: Bulgaria1998P6.lemma_1'
Proof state before:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
⊢ False
Tactic:
have a_odd : Odd a := sorry
Proof state after:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
⊢ False
Theorem: Bulgaria1998P6.lemma_1'
Proof state before:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
⊢ False
Tactic:
have b_odd : Odd b := sorry
Proof state after:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
b_odd : Odd b
⊢ False
Theorem: Bulgaria1998P6.lemma_1'
Proof state before:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
b_odd : Odd b
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: Bulgaria1998P6.lemma_1'
Proof state before:
case ind.inr
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_odd : Odd c
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
s t u : ℤ
hs : 0 < s
ht : 0 < t
hu : 0 < u
h : s ^ 4 - t ^ 4 = u ^ 2
⊢ False
Tactic:
replace h : s^4 = t^4 + u^2 := eq_add_of_sub_eq' h
Proof state after:
s t u : ℤ
hs : 0 < s
ht : 0 < t
hu : 0 < u
h : s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
s t u : ℤ
hs : 0 < s
ht : 0 < t
hu : 0 < u
h : s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Tactic:
lift s to ℕ using Int.le_of_lt hs
Proof state after:
case intro
t u : ℤ
ht : 0 < t
hu : 0 < u
s : ℕ
hs : 0 < ↑s
h : ↑s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
case intro
t u : ℤ
ht : 0 < t
hu : 0 < u
s : ℕ
hs : 0 < ↑s
h : ↑s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Tactic:
lift t to ℕ using Int.le_of_lt ht
Proof state after:
case intro.intro
u : ℤ
hu : 0 < u
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
h : ↑s ^ 4 = ↑t ^ 4 + u ^ 2
⊢ False
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
case intro.intro
u : ℤ
hu : 0 < u
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
h : ↑s ^ 4 = ↑t ^ 4 + u ^ 2
⊢ False
Tactic:
lift u to ℕ using Int.le_of_lt hu
Proof state after:
case intro.intro.intro
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
⊢ False
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
case intro.intro.intro
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
⊢ False
Tactic:
replace hs : 0 < s := Int.ofNat_pos.mp hs
Proof state after:
case intro.intro.intro
s t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
⊢ False
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
case intro.intro.intro
s t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
⊢ False
Tactic:
replace ht : 0 < t := Int.ofNat_pos.mp ht
Proof state after:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
⊢ False
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
⊢ False
Tactic:
replace hy : 0 < u := Int.ofNat_pos.mp hu
Proof state after:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
⊢ False
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
⊢ False
Tactic:
have h' : s ^ 4 = t ^ 4 + u ^ 2 := by exact Int.ofNat_inj.mp h
Proof state after:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
h' : s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
h' : s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Tactic:
exact lemma_1' s t u hs ht hy h'
Proof state after:
no goals
Theorem: Bulgaria1998P6.lemma_1
Proof state before:
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
⊢ s ^ 4 = t ^ 4 + u ^ 2
Tactic:
exact Int.ofNat_inj.mp h
Proof state after:
no goals
Theorem: UpperLowerContinuous.real_induction
Proof state before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
⊢ Set.Ici z ⊆ S
Tactic:
by_contra H
Proof state after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ¬Set.Ici z ⊆ S
⊢ False
Theorem: UpperLowerContinuous.real_induction
Proof state before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ¬Set.Ici z ⊆ S
⊢ False
Tactic:
rw[Set.subset_def] at H
Proof state after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ¬∀ x ∈ Set.Ici z, x ∈ S
⊢ False