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

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n = g
Tactic:
apply le_antisymm
State after:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n ≤ g

case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n

State before:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n ≤ g
Tactic:
rcases exists_map_eq_seqMax (λ i ↦ |seqMax a i - g - a i|) n with ⟨i, h0, h1⟩
State after:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
h1 : |seqMax a i - g - a i| = seqMax (fun i => |seqMax a i - g - a i|) n
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n ≤ g

State before:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
h1 : |seqMax a i - g - a i| = seqMax (fun i => |seqMax a i - g - a i|) n
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n ≤ g
Tactic:
rw [← h1, sub_right_comm, abs_le]
State after:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
h1 : |seqMax a i - g - a i| = seqMax (fun i => |seqMax a i - g - a i|) n
⊢ -g ≤ seqMax a i - a i - g ∧ seqMax a i - a i - g ≤ g

State before:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
h1 : |seqMax a i - g - a i| = seqMax (fun i => |seqMax a i - g - a i|) n
⊢ -g ≤ seqMax a i - a i - g ∧ seqMax a i - a i - g ≤ g
Tactic:
clear h1
State after:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ -g ≤ seqMax a i - a i - g ∧ seqMax a i - a i - g ≤ g

State before:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ -g ≤ seqMax a i - a i - g ∧ seqMax a i - a i - g ≤ g
Tactic:
refine ⟨?_, ?_⟩
State after:
case a.intro.intro.refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ -g ≤ seqMax a i - a i - g

case a.intro.intro.refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ seqMax a i - a i - g ≤ g

State before:
case a.intro.intro.refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ -g ≤ seqMax a i - a i - g
Tactic:
rw [le_sub_iff_add_le, neg_add_self, sub_nonneg]
State after:
case a.intro.intro.refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ a i ≤ seqMax a i

State before:
case a.intro.intro.refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ a i ≤ seqMax a i
Tactic:
exact le_seqMax_self a i
State after:
no goals

State before:
case a.intro.intro.refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ seqMax a i - a i - g ≤ g
Tactic:
rcases exists_map_eq_seqMax a i with ⟨j, h1, h2⟩
State after:
case a.intro.intro.refine_2.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
j : ℕ
h1 : j ≤ i
h2 : a j = seqMax a i
⊢ seqMax a i - a i - g ≤ g

State before:
case a.intro.intro.refine_2.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
j : ℕ
h1 : j ≤ i
h2 : a j = seqMax a i
⊢ seqMax a i - a i - g ≤ g
Tactic:
rw [← h2, sub_le_iff_le_add, ← two_nsmul]
State after:
case a.intro.intro.refine_2.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
j : ℕ
h1 : j ≤ i
h2 : a j = seqMax a i
⊢ a j - a i ≤ 2 • g

State before:
case a.intro.intro.refine_2.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
j : ℕ
h1 : j ≤ i
h2 : a j = seqMax a i
⊢ a j - a i ≤ 2 • g
Tactic:
exact h j i h1 h0
State after:
no goals

State before:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n
Tactic:
apply (le_seqMax_of_le _ n.zero_le).trans'
State after:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ |(fun i => seqMax a i - g) 0 - a 0|

State before:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ |(fun i => seqMax a i - g) 0 - a 0|
Tactic:
rw [sub_sub, seqMax, sub_add_cancel_right, abs_neg]
State after:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ |g|

State before:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ |g|
Tactic:
exact le_abs_self g
State after:
no goals