Theorem: Imo1974P5.condition_implies_solution_set (Compfiles/Imo1974P5.lean)

State before:
s : ℝ
h : ∃ a b c d, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
⊢ s ∈ solution_set
Tactic:
rw [Set.mem_Ioo]
State after:
s : ℝ
h : ∃ a b c d, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
⊢ 1 < s ∧ s < 2

State before:
s : ℝ
h : ∃ a b c d, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
⊢ 1 < s ∧ s < 2
Tactic:
obtain ⟨a, b, c, d, ha, hb, hc, hd, rfl⟩ := h
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) ∧
    a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) ∧
    a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)

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
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
have h8 : a / (a + b + c + d) < a / (a + b + d) :=
   div_lt_div_of_pos_left ha (by linarith) (by linarith)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
have h9 : b / (a + b + c + d) < b / (a + b + c) :=
   div_lt_div_of_pos_left hb (by linarith) (lt_add_of_pos_right _ hd)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
have h10 : c / (a + b + c + d) < c / (b + c + d) :=
   div_lt_div_of_pos_left hc (by linarith) (by linarith)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
have h11 : d / (a + b + c + d) < d / (a + c + d) :=
   div_lt_div_of_pos_left hd (by linarith) (by linarith)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
h11 : d / (a + b + c + d) < d / (a + c + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
h11 : d / (a + b + c + d) < d / (a + c + d)
⊢ 1 < a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
calc 1 = a / (a + b + c + d) + b / (a + b + c + d) +
         c / (a + b + c + d) + d / (a + b + c + d) := by field_simp
     _ < _ := by gcongr
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ 0 < a + b + d
Tactic:
linarith
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
⊢ a + b + d < a + b + c + d
Tactic:
linarith
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
⊢ 0 < a + b + c
Tactic:
linarith
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
⊢ 0 < b + c + d
Tactic:
linarith
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
⊢ b + c + d < a + b + c + d
Tactic:
linarith
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
⊢ 0 < a + c + d
Tactic:
linarith
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
⊢ a + c + d < a + b + c + d
Tactic:
linarith
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
h11 : d / (a + b + c + d) < d / (a + c + d)
⊢ 1 = a / (a + b + c + d) + b / (a + b + c + d) + c / (a + b + c + d) + d / (a + b + c + d)
Tactic:
field_simp
State after:
no goals

State before:
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h8 : a / (a + b + c + d) < a / (a + b + d)
h9 : b / (a + b + c + d) < b / (a + b + c)
h10 : c / (a + b + c + d) < c / (b + c + d)
h11 : d / (a + b + c + d) < d / (a + c + d)
⊢ a / (a + b + c + d) + b / (a + b + c + d) + c / (a + b + c + d) + d / (a + b + c + d) <
    a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
Tactic:
gcongr
State after:
no goals

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
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
have h3 : a / (a + b + d) < a / (a + b) :=
   div_lt_div_of_pos_left ha (add_pos ha hb) (lt_add_of_pos_right _ hd)
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)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2

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)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
have h4 : b / (a + b + c) < b / (a + b) :=
   div_lt_div_of_pos_left hb (add_pos ha hb) (lt_add_of_pos_right _ hc)
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)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2

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)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
Tactic:
have h5 : c / (b + c + d) < c / (c + d) :=
   div_lt_div_of_pos_left hc (add_pos hc hd) (by linarith)
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)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2

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)
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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)

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
State after:
no goals