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

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
⊢ |a n| ≤ max (Extra.seqMax (-a) n) (2 • Extra.seqMax a n)
Tactic:
rw [le_max_iff]
State after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
⊢ |a n| ≤ Extra.seqMax (-a) n ∨ |a n| ≤ 2 • Extra.seqMax a n

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
⊢ |a n| ≤ Extra.seqMax (-a) n ∨ |a n| ≤ 2 • Extra.seqMax a n
Tactic:
refine (le_total (a n) 0).imp (λ h ↦ ?_) (λ h ↦ ?_)
State after:
case refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : a n ≤ 0
⊢ |a n| ≤ Extra.seqMax (-a) n

case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
⊢ |a n| ≤ 2 • Extra.seqMax a n

State before:
case refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : a n ≤ 0
⊢ |a n| ≤ Extra.seqMax (-a) n
Tactic:
rw [abs_of_nonpos h]
State after:
case refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : a n ≤ 0
⊢ -a n ≤ Extra.seqMax (-a) n

State before:
case refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : a n ≤ 0
⊢ -a n ≤ Extra.seqMax (-a) n
Tactic:
exact Extra.le_seqMax_self (-a) n
State after:
no goals

State before:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
⊢ |a n| ≤ 2 • Extra.seqMax a n
Tactic:
rw [abs_of_nonneg h, two_nsmul]
State after:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
⊢ a n ≤ Extra.seqMax a n + Extra.seqMax a n

State before:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
⊢ a n ≤ Extra.seqMax a n + Extra.seqMax a n
Tactic:
have h0 := Extra.le_seqMax_self a n
State after:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
h0 : a n ≤ Extra.seqMax a n
⊢ a n ≤ Extra.seqMax a n + Extra.seqMax a n

State before:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
h0 : a n ≤ Extra.seqMax a n
⊢ a n ≤ Extra.seqMax a n + Extra.seqMax a n
Tactic:
exact le_add_of_le_of_nonneg h0 (h.trans h0)
State after:
no goals