Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case h.left.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 = ∅
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' ∈ upper_branch
Tactic:
constructor <;> dsimp only
Proof state after:
case h.left.h.left
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)
⊢ H c mx

case h.left.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)
⊢ c < mx