Theorem: IMOSL.IMO2017A4.good1_bdd_above (IMOSLLean4/IMO2017/A4/A4.lean)

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n
Tactic:
rcases Extra.exists_map_eq_seqMax a n with ⟨i, h2, h1⟩
State after:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
i : ℕ
h2 : i ≤ n
h1 : a i = Extra.seqMax a n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n

State before:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
i : ℕ
h2 : i ≤ n
h1 : a i = Extra.seqMax a n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n
Tactic:
rw [le_iff_exists_add] at h2
State after:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
i : ℕ
h2 : ∃ c, n = i + c
h1 : a i = Extra.seqMax a n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n

State before:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
i : ℕ
h2 : ∃ c, n = i + c
h1 : a i = Extra.seqMax a n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n
Tactic:
rcases h2 with ⟨j, rfl⟩
State after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ a (i + j + 1) ≤ Extra.seqMax (-a) (i + j) - Extra.seqMax a (i + j)

State before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ a (i + j + 1) ≤ Extra.seqMax (-a) (i + j) - Extra.seqMax a (i + j)
Tactic:
apply (h i j h0).trans
State after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ -(a i + a j) ≤ Extra.seqMax (-a) (i + j) - Extra.seqMax a (i + j)

State before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ -(a i + a j) ≤ Extra.seqMax (-a) (i + j) - Extra.seqMax a (i + j)
Tactic:
rw [← h1, neg_add_rev, ← sub_eq_add_neg]
State after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ -a j - a i ≤ Extra.seqMax (-a) (i + j) - a i

State before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ -a j - a i ≤ Extra.seqMax (-a) (i + j) - a i
Tactic:
exact sub_le_sub_right (Extra.le_seqMax_of_le (-a) (j.le_add_left i)) (a i)
State after:
no goals