Theorem: IMOSL.IMO2011A6.final_solution (IMOSLLean4/IMO2011/A6/A6.lean)

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
have h0 : ∀ t x : R, f (f t) - f (f x) ≤ (f t - x) * f x := λ t x ↦ by
  rw [sub_le_iff_le_add]
  apply (h _ _).trans_eq'
  rw [add_sub_cancel]
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
⊢ ∀ (x : R), x ≤ 0 → f x = 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
replace h0 : ∀ t x : R, 0 ≤ (f t - x) * f x + (f x - t) * f t := λ t x ↦ by
  rw [← sub_self (f (f t)), ← sub_add_sub_cancel _ (f (f x))]
  exact add_le_add (h0 t x) (h0 x t)
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
⊢ ∀ (x : R), x ≤ 0 → f x = 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
replace h0 : ∀ x : R, x * f x ≤ 0 := λ x ↦ by
  have h1 := h0 x (f x + f x)
  rwa [sub_add_cancel_left, sub_mul, neg_mul, mul_comm,
    ← add_sub_assoc, neg_add_self, zero_sub, neg_nonneg] at h1
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
have h1 : ∀ x : R, f x ≤ f (f x) := λ x ↦ by
  have h1 := h x 0
  rwa [add_zero, zero_mul, zero_add] at h1
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
h1 : ∀ (x : R), f x ≤ f (f x)
⊢ ∀ (x : R), x ≤ 0 → f x = 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
h1 : ∀ (x : R), f x ≤ f (f x)
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
replace h1 : ∀ x : R, f x ≤ 0 := λ x ↦
  le_of_not_lt λ h2 ↦ (h0 (f x)).not_lt <| mul_pos h2 (h2.trans_le (h1 x))
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
h1 : ∀ (x : R), f x ≤ 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
h1 : ∀ (x : R), f x ≤ 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
replace h0 : ∀ x : R, x < 0 → f x = 0 := λ x h2 ↦
  (h1 x).antisymm (nonneg_of_mul_nonpos_right (h0 x) h2)
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
intros x h2
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
x : R
h2 : x ≤ 0
⊢ f x = 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
x : R
h2 : x ≤ 0
⊢ f x = 0
Tactic:
rcases h2.lt_or_eq with h2 | rfl
State after:
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
x : R
h2✝ : x ≤ 0
h2 : x < 0
⊢ f x = 0

case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
⊢ f 0 = 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) - f (f x) ≤ (f t - x) * f x
Tactic:
rw [sub_le_iff_le_add]
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) ≤ (f t - x) * f x + f (f x)

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) ≤ (f t - x) * f x + f (f x)
Tactic:
apply (h _ _).trans_eq'
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) = f (x + (f t - x))

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) = f (x + (f t - x))
Tactic:
rw [add_sub_cancel]
State after:
no goals

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
t x : R
⊢ 0 ≤ (f t - x) * f x + (f x - t) * f t
Tactic:
rw [← sub_self (f (f t)), ← sub_add_sub_cancel _ (f (f x))]
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
t x : R
⊢ f (f t) - f (f x) + (f (f x) - f (f t)) ≤ (f t - x) * f x + (f x - t) * f t

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
t x : R
⊢ f (f t) - f (f x) + (f (f x) - f (f t)) ≤ (f t - x) * f x + (f x - t) * f t
Tactic:
exact add_le_add (h0 t x) (h0 x t)
State after:
no goals

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
x : R
⊢ x * f x ≤ 0
Tactic:
have h1 := h0 x (f x + f x)
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
x : R
h1 : 0 ≤ (f x - (f x + f x)) * f (f x + f x) + (f (f x + f x) - x) * f x
⊢ x * f x ≤ 0

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
x : R
h1 : 0 ≤ (f x - (f x + f x)) * f (f x + f x) + (f (f x + f x) - x) * f x
⊢ x * f x ≤ 0
Tactic:
rwa [sub_add_cancel_left, sub_mul, neg_mul, mul_comm,
  ← add_sub_assoc, neg_add_self, zero_sub, neg_nonneg] at h1
State after:
no goals

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
x : R
⊢ f x ≤ f (f x)
Tactic:
have h1 := h x 0
State after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
x : R
h1 : f (x + 0) ≤ 0 * f x + f (f x)
⊢ f x ≤ f (f x)

State before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
x : R
h1 : f (x + 0) ≤ 0 * f x + f (f x)
⊢ f x ≤ f (f x)
Tactic:
rwa [add_zero, zero_mul, zero_add] at h1
State after:
no goals

State before:
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
x : R
h2✝ : x ≤ 0
h2 : x < 0
⊢ f x = 0
Tactic:
exact h0 x h2
State after:
no goals

State before:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
⊢ f 0 = 0
Tactic:
apply (h1 0).antisymm
State after:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
⊢ 0 ≤ f 0

State before:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
⊢ 0 ≤ f 0
Tactic:
specialize h (-1) 0
State after:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
h : f (-1 + 0) ≤ 0 * f (-1) + f (f (-1))
⊢ 0 ≤ f 0

State before:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
h : f (-1 + 0) ≤ 0 * f (-1) + f (f (-1))
⊢ 0 ≤ f 0
Tactic:
rwa [add_zero, zero_mul, zero_add, h0 _ neg_one_lt_zero] at h
State after:
no goals