internlm/Lean-Github huggingface dataset:
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.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)
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 ∧ mx ≠ 0 ∧ mx ≠ my ∧ B mx ≠ ↑my ∧ B mx ≠ ↑my + ↑mx
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
rcases h_base with ⟨h_base, hmx, hm_diag, hm_B₁, hm_B₂⟩
Proof state after:
case intro.mk.intro.intro.intro.intro.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)
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
hmx : mx ≠ 0
hm_diag : mx ≠ my
hm_B₁ : B mx ≠ ↑my
hm_B₂ : B mx ≠ ↑my + ↑mx
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.intro.intro.intro.intro.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)
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
hmx : mx ≠ 0
hm_diag : mx ≠ my
hm_B₁ : B mx ≠ ↑my
hm_B₂ : B mx ≠ ↑my + ↑mx
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
replace hmx : 0 < mx := pos_iff_ne_zero.mpr hmx
Proof state after:
case intro.mk.intro.intro.intro.intro.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)
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
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.intro.intro.intro.intro.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)
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
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
have h_quad := hHm
Proof state after:
case intro.mk.intro.intro.intro.intro.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)
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 : H mx my
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.intro.intro.intro.intro.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)
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 : H mx my
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
rw [H_quad] at h_quad
Proof state after:
case intro.mk.intro.intro.intro.intro.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)
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
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.intro.intro.intro.intro.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)
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
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
rcases vieta_formula_quadratic h_quad with ⟨c, h_root, hV₁, hV₂⟩
Proof state after:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.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)
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₁ : ↑my + c = B mx
hV₂ : ↑my * c = C mx
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.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)
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₁ : ↑my + c = B mx
hV₂ : ↑my * c = C mx
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
replace hV₁ : c = B mx - my := eq_sub_of_add_eq' hV₁
Proof state after:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.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)
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₂ : ↑my * c = C mx
hV₁ : c = B mx - ↑my
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.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)
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₂ : ↑my * c = C mx
hV₁ : c = B mx - ↑my
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
rw [mul_comm] at hV₂
Proof state after:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.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)
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
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.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)
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
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
have Hc := H_desc hmx mx_lt_my h_base hHm c h_root hV₁ hV₂
Proof state after:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.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)
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
Hc : 0 ≤ c ∧ c ≤ ↑mx
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.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)
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
Hc : 0 ≤ c ∧ c ≤ ↑mx
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m
Tactic:
cases' Hc with c_nonneg c_lt
Proof state after:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.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)
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_nonneg : 0 ≤ c
c_lt : c ≤ ↑mx
⊢ ∃ p', p'.2 ∈ S ∧ p'.2 < m