internlm/Lean-Github huggingface dataset:
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
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
Tactic:
rw [H_symm, H_quad]
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)
⊢ ↑c * ↑c - B mx * ↑c + C mx = 0
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
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)
⊢ ↑c * ↑c - B mx * ↑c + C mx = 0
Tactic:
simpa using h_root
Proof state after:
no goals
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
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
Tactic:
suffices hc : c ≠ mx from lt_of_le_of_ne (mod_cast c_lt) hc
Proof state after:
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
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
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
Tactic:
contrapose! hm_B₂
Proof state after:
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
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)
hm_B₂ : c = mx
⊢ B mx = ↑my + ↑mx
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
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
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)
hm_B₂ : c = mx
⊢ B mx = ↑my + ↑mx
Tactic:
subst c
Proof state after:
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
hmx : 0 < mx
h_quad : ↑my * ↑my - B mx * ↑my + C mx = 0
h_root : ↑mx * ↑mx - B mx * ↑mx + C mx = 0
hV₂ : ↑mx * ↑my = C mx
hV₁ : ↑mx = B mx - ↑my
c_lt : ↑mx ≤ ↑mx
p' : ℕ × ℕ := (mx, mx)
⊢ B mx = ↑my + ↑mx
Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
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
hmx : 0 < mx
h_quad : ↑my * ↑my - B mx * ↑my + C mx = 0
h_root : ↑mx * ↑mx - B mx * ↑mx + C mx = 0
hV₂ : ↑mx * ↑my = C mx
hV₁ : ↑mx = B mx - ↑my
c_lt : ↑mx ≤ ↑mx
p' : ℕ × ℕ := (mx, mx)
⊢ B mx = ↑my + ↑mx
Tactic:
simp [hV₁]
Proof state after:
no goals
Theorem: Usa2023P4.halve_even
Proof state before:
x : ℕ+
he : Even ↑x
⊢ 0 < ↑x / 2
Tactic:
obtain ⟨x, hx⟩ := x
Proof state after:
case mk
x : ℕ
hx : 0 < x
he : Even ↑⟨x, hx⟩
⊢ 0 < ↑⟨x, hx⟩ / 2
Theorem: Usa2023P4.halve_even
Proof state before:
case mk
x : ℕ
hx : 0 < x
he : Even ↑⟨x, hx⟩
⊢ 0 < ↑⟨x, hx⟩ / 2
Tactic:
obtain ⟨t, ht⟩ := he
Proof state after:
case mk.intro
x : ℕ
hx : 0 < x
t : ℕ
ht : ↑⟨x, hx⟩ = t + t
⊢ 0 < ↑⟨x, hx⟩ / 2
Theorem: Usa2023P4.halve_even
Proof state before:
case mk.intro
x : ℕ
hx : 0 < x
t : ℕ
ht : ↑⟨x, hx⟩ = t + t
⊢ 0 < ↑⟨x, hx⟩ / 2
Tactic:
dsimp at *
Proof state after:
case mk.intro
x : ℕ
hx : 0 < x
t : ℕ
ht : x = t + t
⊢ 0 < x / 2
Theorem: Usa2023P4.halve_even
Proof state before:
case mk.intro
x : ℕ
hx : 0 < x
t : ℕ
ht : x = t + t
⊢ 0 < x / 2
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
⊢ x ≤ y
Tactic:
by_contra! hxy
Proof state after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
⊢ False
Tactic:
have hxmy : 0 < x - y := sub_pos.mpr hxy
Proof state after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
⊢ False
Tactic:
have hn : ∀ n : ℕ, (x - y) * (n : ℝ) ≤ x^n - y^n := fun n ↦ by
  have hterm : ∀ i : ℕ, i ∈ Finset.range n → 1 ≤ x^i * y^(n - 1 - i) := by
    intro i _
    calc 1 ≤ x^i             := one_le_pow_of_one_le hx.le i
         _ = x^i * 1         := (mul_one _).symm
         _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow_of_one_le hy.le
  calc (x - y) * (n : ℝ)
      = (n : ℝ) * (x - y) := mul_comm _ _
    _ = (∑ _i in Finset.range n, (1 : ℝ)) * (x - y) :=
                               by simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
                                  Finset.card_range]
    _ ≤ (∑ i in Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x-y) :=
                                (mul_le_mul_right hxmy).mpr (Finset.sum_le_sum hterm)
    _ = x^n - y^n         := geom_sum₂_mul x y n
Proof state after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
⊢ False
Tactic:
obtain ⟨N, hN⟩ := exists_nat_gt (1 / (x - y))
Proof state after:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
⊢ False
Tactic:
have hNp : 0 < N := by exact_mod_cast (one_div_pos.mpr hxmy).trans hN
Proof state after:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
⊢ False
Tactic:
have h1 := calc 1 = (x - y) * (1 / (x - y)) := by field_simp
             _ < (x - y) * N             := (mul_lt_mul_left hxmy).mpr hN
             _ ≤ x^N - y^N               := hn N
Proof state after:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
h1 : 1 < x ^ N - y ^ N
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
h1 : 1 < x ^ N - y ^ N
⊢ False
Tactic:
linarith only [h1, h N hNp]
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
⊢ (x - y) * ↑n ≤ x ^ n - y ^ n
Tactic:
have hterm : ∀ i : ℕ, i ∈ Finset.range n → 1 ≤ x^i * y^(n - 1 - i) := by
  intro i _
  calc 1 ≤ x^i             := one_le_pow_of_one_le hx.le i
       _ = x^i * 1         := (mul_one _).symm
       _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow_of_one_le hy.le
Proof state after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
hterm : ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
⊢ (x - y) * ↑n ≤ x ^ n - y ^ n
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
hterm : ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
⊢ (x - y) * ↑n ≤ x ^ n - y ^ n
Tactic:
calc (x - y) * (n : ℝ)
    = (n : ℝ) * (x - y) := mul_comm _ _
  _ = (∑ _i in Finset.range n, (1 : ℝ)) * (x - y) :=
                             by simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
                                Finset.card_range]
  _ ≤ (∑ i in Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x-y) :=
                              (mul_le_mul_right hxmy).mpr (Finset.sum_le_sum hterm)
  _ = x^n - y^n         := geom_sum₂_mul x y n
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
Tactic:
intro i _
Proof state after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ x ^ i * y ^ (n - 1 - i)
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ x ^ i * y ^ (n - 1 - i)
Tactic:
calc 1 ≤ x^i             := one_le_pow_of_one_le hx.le i
     _ = x^i * 1         := (mul_one _).symm
     _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow_of_one_le hy.le
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ x ^ i * 1 ≤ x ^ i * y ^ (n - 1 - i)
Tactic:
gcongr
Proof state after:
case h
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ y ^ (n - 1 - i)
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
case h
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ y ^ (n - 1 - i)
Tactic:
apply one_le_pow_of_one_le hy.le
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
hterm : ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
⊢ ↑n * (x - y) = (∑ _i ∈ Finset.range n, 1) * (x - y)
Tactic:
simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
Finset.card_range]
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
⊢ 0 < N
Tactic:
exact_mod_cast (one_div_pos.mpr hxmy).trans hN
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ
Proof state before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
⊢ 1 = (x - y) * (1 / (x - y))
Tactic:
field_simp
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ'
Proof state before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
⊢ x ≤ y
Tactic:
refine le_of_all_pow_lt_succ hx ?_ h
Proof state after:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
⊢ 1 < y
Theorem: Imo2013P5.le_of_all_pow_lt_succ'
Proof state before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
⊢ 1 < y
Tactic:
by_contra! hy''
Proof state after:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ'
Proof state before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
⊢ False
Tactic:
obtain ⟨y', h1_lt_y', h_y'_lt_x⟩ := exists_between hx
Proof state after:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ'
Proof state before:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
⊢ False
Tactic:
have h_y_lt_y' : y < y' := hy''.trans_lt h1_lt_y'
Proof state after:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ'
Proof state before:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
⊢ False
Tactic:
have hh : ∀ n, 0 < n → x^n - 1 < y'^n := by
  intro n hn
  calc x^n - 1 < y^n  := h n hn
       _  ≤ y'^n := pow_le_pow_left hy.le h_y_lt_y'.le n
Proof state after:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
hh : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y' ^ n
⊢ False
Theorem: Imo2013P5.le_of_all_pow_lt_succ'
Proof state before:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
hh : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y' ^ n
⊢ False
Tactic:
exact h_y'_lt_x.not_le (le_of_all_pow_lt_succ hx h1_lt_y' hh)
Proof state after:
no goals
Theorem: Imo2013P5.le_of_all_pow_lt_succ'
Proof state before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
⊢ ∀ (n : ℕ), 0 < n → x ^ n - 1 < y' ^ n
Tactic:
intro n hn
Proof state after:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
n : ℕ
hn : 0 < n
⊢ x ^ n - 1 < y' ^ n