internlm/Lean-Github huggingface dataset:
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inl
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
b : ℕ
hH : H 0 b
⊢ claim
Tactic:
rw [H_symm] at hH
Proof state after:
case intro.intro.intro.inr.inl
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
b : ℕ
hH : H b 0
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inl
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
b : ℕ
hH : H b 0
⊢ claim
Tactic:
solve_by_elim
Proof state after:
no goals
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inr.inl
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a : ℕ
hH : H a a
⊢ claim
Tactic:
solve_by_elim
Proof state after:
no goals
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inr.inr.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
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : H a b
hB : B a = ↑b + ↑a
⊢ claim
Tactic:
rw [H_quad] at hH
Proof state after:
case intro.intro.intro.inr.inr.inr.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
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = 0
hB : B a = ↑b + ↑a
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inr.inr.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
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = 0
hB : B a = ↑b + ↑a
⊢ claim
Tactic:
rcases vieta_formula_quadratic hH with ⟨c, h_root, hV₁, hV₂⟩
Proof state after:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = 0
hB : B a = ↑b + ↑a
c : ℤ
h_root : c * c - B a * c + C a = 0
hV₁ : ↑b + c = B a
hV₂ : ↑b * c = C a
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = 0
hB : B a = ↑b + ↑a
c : ℤ
h_root : c * c - B a * c + C a = 0
hV₁ : ↑b + c = B a
hV₂ : ↑b * c = C a
⊢ claim
Tactic:
simp only [hB, add_right_eq_self, add_right_inj] at hV₁
Proof state after:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = 0
hB : B a = ↑b + ↑a
c : ℤ
h_root : c * c - B a * c + C a = 0
hV₂ : ↑b * c = C a
hV₁ : c = ↑a
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = 0
hB : B a = ↑b + ↑a
c : ℤ
h_root : c * c - B a * c + C a = 0
hV₂ : ↑b * c = C a
hV₁ : c = ↑a
⊢ claim
Tactic:
subst hV₁
Proof state after:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = 0
hB : B a = ↑b + ↑a
h_root : ↑a * ↑a - B a * ↑a + C a = 0
hV₂ : ↑b * ↑a = C a
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = 0
hB : B a = ↑b + ↑a
h_root : ↑a * ↑a - B a * ↑a + C a = 0
hV₂ : ↑b * ↑a = C a
⊢ claim
Tactic:
rw [← Int.ofNat_zero] at *
Proof state after:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = ↑0
hB : B a = ↑b + ↑a
h_root : ↑a * ↑a - B a * ↑a + C a = ↑0
hV₂ : ↑b * ↑a = C a
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = ↑0
hB : B a = ↑b + ↑a
h_root : ↑a * ↑a - B a * ↑a + C a = ↑0
hV₂ : ↑b * ↑a = C a
⊢ claim
Tactic:
rw [← H_quad] at h_root
Proof state after:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = ↑0
hB : B a = ↑b + ↑a
h_root : H a a
hV₂ : ↑b * ↑a = C a
⊢ claim
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.intro.intro.inr.inr.inr.inr.intro.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
a b : ℕ
hH : ↑b * ↑b - B a * ↑b + C a = ↑0
hB : B a = ↑b + ↑a
h_root : H a a
hV₂ : ↑b * ↑a = C a
⊢ claim
Tactic:
solve_by_elim
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
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
exceptional_empty : exceptional = ∅
⊢ S.Nonempty
Tactic:
use p.2
Proof state after:
case h
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
exceptional_empty : exceptional = ∅
⊢ p.2 ∈ S
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case h
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
exceptional_empty : exceptional = ∅
⊢ p.2 ∈ S
Tactic:
apply Set.mem_image_of_mem
Proof state after:
case h.h
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
exceptional_empty : exceptional = ∅
⊢ p ∈ upper_branch \ exceptional
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case h.h
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
exceptional_empty : exceptional = ∅
⊢ p ∈ upper_branch \ exceptional
Tactic:
rwa [exceptional_empty, Set.diff_empty]
Proof state after:
no goals
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case neg.intro.intro
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
exceptional_empty : exceptional = ∅
S_nonempty : S.Nonempty
m : ℕ := ⋯.min S S_nonempty
m_mem : m ∈ S
m_min : ∀ k ∈ S, ¬k < m
p' : ℕ × ℕ
p'_mem : p'.2 ∈ S
p'_small : p'.2 < m
⊢ False
Tactic:
solve_by_elim
Proof state after:
no goals
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case h.right
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)}
S : Set ℕ := Prod.snd '' (upper_branch \ exceptional)
exceptional_empty : exceptional = ∅
S_nonempty : S.Nonempty
m : ℕ := ⋯.min S S_nonempty
m_min : ∀ k ∈ S, ¬k < m
mx my : ℕ
m_eq : my = m
hHm : H mx my
mx_lt_my : mx < my
h_base : ¬base mx my
hm_diag : mx ≠ my
hm_B₁ : B mx ≠ ↑my
hm_B₂ : B mx ≠ ↑my + ↑mx
hmx : 0 < mx
h_quad : ↑my * ↑my - B mx * ↑my + C mx = 0
c : ℕ
h_root : ↑c * ↑c - B mx * ↑c + C mx = 0
hV₂ : ↑c * ↑my = C mx
hV₁ : ↑c = B mx - ↑my
c_lt : ↑c ≤ ↑mx
p' : ℕ × ℕ := (c, mx)
⊢ p'.2 < m
Tactic:
rwa [m_eq] at mx_lt_my
Proof state after:
no goals