Theorem: IMOSL.IMO2007A1.final_solution_part1 (IMOSLLean4/IMO2007/A1/A1.lean)

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ a k - a m ≤ 2 • seqMax (fun i => |x i - a i|) n
Tactic:
apply (le_add_of_nonneg_left (sub_nonneg_of_le (h h0))).trans
State after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ x m - x k + (a k - a m) ≤ 2 • seqMax (fun i => |x i - a i|) n

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ x m - x k + (a k - a m) ≤ 2 • seqMax (fun i => |x i - a i|) n
Tactic:
rw [← add_comm_sub, sub_add, sub_sub_sub_comm, two_nsmul]
State after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ x m - a m - (x k - a k) ≤ seqMax (fun i => |x i - a i|) n + seqMax (fun i => |x i - a i|) n

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ x m - a m - (x k - a k) ≤ seqMax (fun i => |x i - a i|) n + seqMax (fun i => |x i - a i|) n
Tactic:
have X {i} : i ≤ n → |x i - a i| ≤ seqMax (λ i ↦ |x i - a i|) n :=
  le_seqMax_of_le (λ i ↦ |x i - a i|)
State after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
X : ∀ {i : ℕ}, i ≤ n → |x i - a i| ≤ seqMax (fun i => |x i - a i|) n
⊢ x m - a m - (x k - a k) ≤ seqMax (fun i => |x i - a i|) n + seqMax (fun i => |x i - a i|) n

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
X : ∀ {i : ℕ}, i ≤ n → |x i - a i| ≤ seqMax (fun i => |x i - a i|) n
⊢ x m - a m - (x k - a k) ≤ seqMax (fun i => |x i - a i|) n + seqMax (fun i => |x i - a i|) n
Tactic:
exact (le_abs_self _).trans <| (abs_sub _ _).trans <|
  add_le_add (X h1) (X (h0.trans h1))
State after:
no goals