internlm/Lean-Github huggingface dataset:
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False
Tactic:
rw [← hrk] at hqn hpn h0
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False
Tactic:
clear hrk
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
⊢ False
Tactic:
have h1 := (Nat.mem_factors h0).mpr ⟨hp, hpn⟩
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ (r ^ k).factors
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ (r ^ k).factors
⊢ False
Tactic:
rw [Nat.Prime.factors_pow hr] at h1
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
⊢ False
Tactic:
have h3 := (List.mem_replicate.mp h1).2
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
⊢ False
Tactic:
have h2 := (Nat.mem_factors h0).mpr ⟨hq, hqn⟩
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ (r ^ k).factors
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ (r ^ k).factors
⊢ False
Tactic:
rw [Nat.Prime.factors_pow hr] at h2
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
⊢ False
Tactic:
have h4 := (List.mem_replicate.mp h2).2
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False
Tactic:
rw [h3, h4] at hpq
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
r : ℕ
hpq : r ≠ r
k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
r : ℕ
hpq : r ≠ r
k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False
Tactic:
exact hpq rfl
Proof state after:
no goals
Theorem: Imo1989P5.lemma1
Proof state before:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
⊢ (p1 * p2).Coprime q
Tactic:
have h1 : Nat.Coprime p1 q := Iff.mpr (Nat.coprime_primes hp1 hq) hp1q
Proof state after:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
⊢ (p1 * p2).Coprime q
Theorem: Imo1989P5.lemma1
Proof state before:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
⊢ (p1 * p2).Coprime q
Tactic:
have h2 : Nat.Coprime p2 q := Iff.mpr (Nat.coprime_primes hp2 hq) hp2q
Proof state after:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
h2 : p2.Coprime q
⊢ (p1 * p2).Coprime q
Theorem: Imo1989P5.lemma1
Proof state before:
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
h2 : p2.Coprime q
⊢ (p1 * p2).Coprime q
Tactic:
exact Nat.Coprime.mul h1 h2
Proof state after:
no goals
Theorem: Imo1989P5.lemma2
Proof state before:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
⊢ (p1 * p2).Coprime (q1 * q2)
Tactic:
have h1 := lemma1 hp1 hp2 hq1 hp1q1 hp2q1
Proof state after:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
⊢ (p1 * p2).Coprime (q1 * q2)
Theorem: Imo1989P5.lemma2
Proof state before:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
⊢ (p1 * p2).Coprime (q1 * q2)
Tactic:
have h2 := lemma1 hp1 hp2 hq2 hp1q2 hp2q2
Proof state after:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
h2 : (p1 * p2).Coprime q2
⊢ (p1 * p2).Coprime (q1 * q2)
Theorem: Imo1989P5.lemma2
Proof state before:
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
h2 : (p1 * p2).Coprime q2
⊢ (p1 * p2).Coprime (q1 * q2)
Tactic:
exact Nat.Coprime.mul_right h1 h2
Proof state after:
no goals
Theorem: Imo1989P5.lemma3
Proof state before:
α : Type
l : List α
hl : l.Nodup
i j : Fin l.length
hij : i ≠ j
⊢ l.get i ≠ l.get j
Tactic:
intro hij'
Proof state after:
α : Type
l : List α
hl : l.Nodup
i j : Fin l.length
hij : i ≠ j
hij' : l.get i = l.get j
⊢ False
Theorem: Imo1989P5.lemma3
Proof state before:
α : Type
l : List α
hl : l.Nodup
i j : Fin l.length
hij : i ≠ j
hij' : l.get i = l.get j
⊢ False
Tactic:
exact hij (List.nodup_iff_injective_get.mp hl hij')
Proof state after:
no goals
Theorem: Imo1989P5.lemma4
Proof state before:
a b : ℕ
h : a ≡ b [MOD b]
⊢ a ≡ 0 [MOD b]
Tactic:
have h1 : a % b = b % b := h
Proof state after:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = b % b
⊢ a ≡ 0 [MOD b]
Theorem: Imo1989P5.lemma4
Proof state before:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = b % b
⊢ a ≡ 0 [MOD b]
Tactic:
have h2 : b % b = 0 := Nat.mod_self b
Proof state after:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = b % b
h2 : b % b = 0
⊢ a ≡ 0 [MOD b]
Theorem: Imo1989P5.lemma4
Proof state before:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = b % b
h2 : b % b = 0
⊢ a ≡ 0 [MOD b]
Tactic:
rw [h2] at h1
Proof state after:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = 0
h2 : b % b = 0
⊢ a ≡ 0 [MOD b]
Theorem: Imo1989P5.lemma4
Proof state before:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = 0
h2 : b % b = 0
⊢ a ≡ 0 [MOD b]
Tactic:
exact h1
Proof state after:
no goals
Theorem: Usa2001P4.lemma1
Proof state before:
a b c d : ℝ
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
let v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
Proof state after:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Theorem: Usa2001P4.lemma1
Proof state before:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
let v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
Proof state after:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Theorem: Usa2001P4.lemma1
Proof state before:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
have h2 : a * c + b * d ≤ |a * c + b * d| := le_abs_self _
Proof state after:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
h2 : a * c + b * d ≤ |a * c + b * d|
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Theorem: Usa2001P4.lemma1
Proof state before:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
h2 : a * c + b * d ≤ |a * c + b * d|
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
have h1 := abs_real_inner_le_norm v1 v2
Proof state after:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
h2 : a * c + b * d ≤ |a * c + b * d|
h1 : |⟪v1, v2⟫_ℝ| ≤ ‖v1‖ * ‖v2‖
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Theorem: Usa2001P4.lemma1
Proof state before:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
h2 : a * c + b * d ≤ |a * c + b * d|
h1 : |⟪v1, v2⟫_ℝ| ≤ ‖v1‖ * ‖v2‖
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
simp [EuclideanSpace.norm_eq] at h1
Proof state after:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
h2 : a * c + b * d ≤ |a * c + b * d|
h1 : |v1 0 * v2 0 + v1 1 * v2 1| ≤ √(v1 0 ^ 2 + v1 1 ^ 2) * √(v2 0 ^ 2 + v2 1 ^ 2)
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Theorem: Usa2001P4.lemma1
Proof state before:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
h2 : a * c + b * d ≤ |a * c + b * d|
h1 : |v1 0 * v2 0 + v1 1 * v2 1| ≤ √(v1 0 ^ 2 + v1 1 ^ 2) * √(v2 0 ^ 2 + v2 1 ^ 2)
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
exact h2.trans h1
Proof state after:
no goals
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
⊢ claim
Tactic:
wlog hxy : x ≤ y
Proof state after:
case inr
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
this :
  ∀ (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop},
    H x y →
      ∀ (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop),
        (∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) →
          (∀ {x y : ℕ}, H x y ↔ H y x) →
            (∀ {x : ℕ}, H x 0 → claim) →
              (∀ {x : ℕ}, H x x → claim) →
                (∀ {x y : ℕ},
                    0 < x →
                      x < y →
                        ¬base x y →
                          H x y →
                            ∀ (y' : ℤ),
                              y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) →
                  (∀ {x y : ℕ}, H x y → base x y → claim) → x ≤ y → claim
hxy : ¬x ≤ y
⊢ claim

x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x ≤ y
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x ≤ y
⊢ claim
Tactic:
by_cases x_eq_y : x = y
Proof state after:
case pos
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x ≤ y
x_eq_y : x = y
⊢ claim

case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x ≤ y
x_eq_y : ¬x = y
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x ≤ y
x_eq_y : ¬x = y
⊢ claim
Tactic:
replace hxy : x < y := lt_of_le_of_ne hxy x_eq_y
Proof state after:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
x_eq_y : ¬x = y
hxy : x < y
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
x_eq_y : ¬x = y
hxy : x < y
⊢ claim
Tactic:
clear x_eq_y
Proof state after:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
⊢ claim
Tactic:
let upper_branch : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ p.1 < p.2}
Proof state after:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
upper_branch : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ p.1 < p.2}
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
upper_branch : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ p.1 < p.2}
⊢ claim
Tactic:
let p : ℕ × ℕ := ⟨x, y⟩
Proof state after:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
upper_branch : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ p.1 < p.2}
p : ℕ × ℕ := (x, y)
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
upper_branch : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ p.1 < p.2}
p : ℕ × ℕ := (x, y)
⊢ claim
Tactic:
have hp : p ∈ upper_branch := ⟨h₀, hxy⟩
Proof state after:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
upper_branch : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ p.1 < p.2}
p : ℕ × ℕ := (x, y)
hp : p ∈ upper_branch
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
upper_branch : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ p.1 < p.2}
p : ℕ × ℕ := (x, y)
hp : p ∈ upper_branch
⊢ claim
Tactic:
let exceptional : Set (ℕ × ℕ) :=
  {p | H p.1 p.2 ∧ (base p.1 p.2 ∨ p.1 = 0 ∨ p.1 = p.2 ∨ B p.1 = p.2 ∨ B p.1 = p.2 + p.1)}
Proof state after:
case neg
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H x y
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
hxy : x < y
upper_branch : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ p.1 < p.2}
p : ℕ × ℕ := (x, y)
hp : p ∈ upper_branch
exceptional : Set (ℕ × ℕ) := {p | H p.1 p.2 ∧ (base p.1 p.2 ∨ p.1 = 0 ∨ p.1 = p.2 ∨ B p.1 = ↑p.2 ∨ B p.1 = ↑p.2 + ↑p.1)}
⊢ claim