internlm/Lean-Github huggingface dataset:
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
have h6 : d / (a + c + d) < d / (c + d) :=
   div_lt_div_of_pos_left hd (add_pos hc hd) (by linarith)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
h6 : d / (a + c + d) < d / (c + d)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
h6 : d / (a + c + d) < d / (c + d)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
calc
  _ < a / (a + b) + b / (a + b) + c / (c + d) + d / (c + d) := by gcongr
  _ = 2 := by field_simp; ring
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
⊢ c + d < b + c + d
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
⊢ c + d < a + c + d
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
h6 : d / (a + c + d) < d / (c + d)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) <
    a / (a + b) + b / (a + b) + c / (c + d) + d / (c + d)
Tactic:
gcongr
Proof state after:
no goals
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
h6 : d / (a + c + d) < d / (c + d)
⊢ a / (a + b) + b / (a + b) + c / (c + d) + d / (c + d) = 2
Tactic:
field_simp
Proof state after:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
h6 : d / (a + c + d) < d / (c + d)
⊢ c + d + c + d = 2 * (c + d)
Theorem: Imo1974P5.condition_implies_solution_set
Proof state before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
h6 : d / (a + c + d) < d / (c + d)
⊢ c + d + c + d = 2 * (c + d)
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1974P5.T_continuous
Proof state before:
⊢ ContinuousOn T (Set.Icc 0 1)
Tactic:
unfold T S
Proof state after:
⊢ ContinuousOn
    (fun t =>
      1 / (1 + (1 - t) + t * (1 - t)) + (1 - t) / (1 + (1 - t) + t) + t / (1 - t + t + t * (1 - t)) +
        t * (1 - t) / (1 + t + t * (1 - t)))
    (Set.Icc 0 1)
Theorem: Imo1974P5.T_continuous
Proof state before:
⊢ ContinuousOn
    (fun t =>
      1 / (1 + (1 - t) + t * (1 - t)) + (1 - t) / (1 + (1 - t) + t) + t / (1 - t + t + t * (1 - t)) +
        t * (1 - t) / (1 + t + t * (1 - t)))
    (Set.Icc 0 1)
Tactic:
fun_prop (disch := (rintro x ⟨a,b⟩; nlinarith))
Proof state after:
no goals
Theorem: Imo1974P5.T_continuous
Proof state before:
case funProp.discharger

⊢ ∀ x ∈ Set.Icc 0 1, 1 + x + x * (1 - x) ≠ 0
Tactic:
(rintro x ⟨a,b⟩; nlinarith)
Proof state after:
no goals
Theorem: Imo1974P5.T_continuous
Proof state before:
case funProp.discharger

⊢ ∀ x ∈ Set.Icc 0 1, 1 + x + x * (1 - x) ≠ 0
Tactic:
rintro x ⟨a,b⟩
Proof state after:
case funProp.discharger.intro
x : ℝ
a : 0 ≤ x
b : x ≤ 1
⊢ 1 + x + x * (1 - x) ≠ 0
Theorem: Imo1974P5.T_continuous
Proof state before:
case funProp.discharger.intro
x : ℝ
a : 0 ≤ x
b : x ≤ 1
⊢ 1 + x + x * (1 - x) ≠ 0
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Imo1974P5.T0
Proof state before:
⊢ T 0 = 1
Tactic:
norm_num [T, S]
Proof state after:
no goals
Theorem: Imo1974P5.T1
Proof state before:
⊢ T 1 = 2
Tactic:
norm_num [T, S]
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
wlog Hcb : c ≤ b with h1
Proof state after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
wlog Hba : b ≤ a with h2
Proof state after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) =
          (a - b) * (a * (a - c) - b * (b - c)) := by ring
Proof state after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ (a - b) * (a * (a - c) - b * (b - c))
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
rw [← h5] at h6
Proof state after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h12 : 0 ≤ (c - a) * (c - b) := by nlinarith only [Hba, Hcb]
Proof state after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h13 : 0 ≤ c * (c - a) * (c - b) := by nlinarith only [hc, h12]
Proof state after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
h13 : 0 ≤ c * (c - a) * (c - b)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
h13 : 0 ≤ c * (c - a) * (c - b)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h3 : b ≤ c := le_of_not_le Hcb
Proof state after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
linarith [h1 a c b ha hc hb h3]
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h4 : a ≤ b := le_of_not_le Hba
Proof state after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
obtain hca | hac : c ≤ a ∨ a ≤ c := le_total c a
Proof state after:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have := h2 b a c hb ha hc hca h4
Proof state after:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : b ^ 2 * a + b ^ 2 * c + a ^ 2 * b + a ^ 2 * c + c ^ 2 * b + c ^ 2 * a ≤ b ^ 3 + a ^ 3 + c ^ 3 + 3 * b * a * c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : b ^ 2 * a + b ^ 2 * c + a ^ 2 * b + a ^ 2 * c + c ^ 2 * b + c ^ 2 * a ≤ b ^ 3 + a ^ 3 + c ^ 3 + 3 * b * a * c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
linarith only [this]
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have := h2 b c a hb hc ha hac Hcb
Proof state after:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
this : b ^ 2 * c + b ^ 2 * a + c ^ 2 * b + c ^ 2 * a + a ^ 2 * b + a ^ 2 * c ≤ b ^ 3 + c ^ 3 + a ^ 3 + 3 * b * c * a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Theorem: Imo2000P2.schur
Proof state before:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
this : b ^ 2 * c + b ^ 2 * a + c ^ 2 * b + c ^ 2 * a + a ^ 2 * b + a ^ 2 * c ≤ b ^ 3 + c ^ 3 + a ^ 3 + 3 * b * c * a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
linarith only [this]
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
⊢ a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ (a - b) * (a * (a - c) - b * (b - c))
Tactic:
apply mul_nonneg
Proof state after:
case ha
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a - b

case hb
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a * (a - c) - b * (b - c)
Theorem: Imo2000P2.schur
Proof state before:
case ha
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a - b
Tactic:
exact sub_nonneg_of_le Hba
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
case hb
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a * (a - c) - b * (b - c)
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ 0 ≤ (c - a) * (c - b)
Tactic:
nlinarith only [Hba, Hcb]
Proof state after:
no goals
Theorem: Imo2000P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ 0 ≤ c * (c - a) * (c - b)
Tactic:
nlinarith only [hc, h12]
Proof state after:
no goals
Theorem: Imo2000P2.lemma1
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 0 < z
⊢ (-x + y + z) * (x - y + z) * (x + y - z) ≤ x * y * z
Tactic:
linarith [schur x y z (le_of_lt hx) (le_of_lt hy) (le_of_lt hz)]
Proof state after:
no goals
Theorem: Imo2000P2.lemma2
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ ∃ x y z, 0 < x ∧ 0 < y ∧ 0 < z ∧ a = x / y ∧ b = y / z ∧ c = z / x
Tactic:
refine ⟨a, 1, (1/b), ha, zero_lt_one, ?_, ?_, ?_, ?_⟩
Proof state after:
case refine_1
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ 0 < 1 / b

case refine_2
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ a = a / 1

case refine_3
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ b = 1 / (1 / b)

case refine_4
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ c = 1 / b / a
Theorem: Imo2000P2.lemma2
Proof state before:
case refine_1
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ 0 < 1 / b
Tactic:
exact one_div_pos.mpr hb
Proof state after:
no goals
Theorem: Imo2000P2.lemma2
Proof state before:
case refine_2
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ a = a / 1
Tactic:
exact (div_one a).symm
Proof state after:
no goals
Theorem: Imo2000P2.lemma2
Proof state before:
case refine_3
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ b = 1 / (1 / b)
Tactic:
exact (one_div_one_div b).symm
Proof state after:
no goals
Theorem: Imo2000P2.lemma2
Proof state before:
case refine_4
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ c = 1 / b / a
Tactic:
field_simp
Proof state after:
case refine_4
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ c * (b * a) = 1
Theorem: Imo2000P2.lemma2
Proof state before:
case refine_4
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ c * (b * a) = 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2022P2.lemma0
Proof state before:
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
⊢ ∀ (x : α), Classical.choose ⋯ = x
Tactic:
intro x
Proof state after:
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x : α
⊢ Classical.choose ⋯ = x
Theorem: Imo2022P2.lemma0
Proof state before:
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x : α
⊢ Classical.choose ⋯ = x
Tactic:
obtain ⟨y, h1e, h1u⟩ := h1 x
Proof state after:
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
⊢ Classical.choose ⋯ = x
Theorem: Imo2022P2.lemma0
Proof state before:
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
⊢ Classical.choose ⋯ = x
Tactic:
have h2' : Classical.choose (h1 x).exists = y :=
  h1u _ (Classical.choose_spec (h1 x).exists)
Proof state after:
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
⊢ Classical.choose ⋯ = x
Theorem: Imo2022P2.lemma0
Proof state before:
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
⊢ Classical.choose ⋯ = x
Tactic:
obtain ⟨w, h1e', h1u'⟩ := h1 y
Proof state after:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
⊢ Classical.choose ⋯ = x
Theorem: Imo2022P2.lemma0
Proof state before:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
⊢ Classical.choose ⋯ = x
Tactic:
have h4 := Classical.choose_spec (h1 y).exists
Proof state after:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ Classical.choose ⋯ = x