Theorem: IMOSL.Extra.exists_map_eq_seqMax (IMOSLLean4/Extra/NatSequence/SeqMax.lean)

State before:
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Tactic:
rcases le_total (seqMax f n) (f n.succ) with h | h
State after:
case inl
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : seqMax f n ≤ f n.succ
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)

case inr
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : f n.succ ≤ seqMax f n
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)

State before:
case inl
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : seqMax f n ≤ f n.succ
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Tactic:
exact ⟨n + 1, le_refl (n + 1), (max_eq_right h).symm⟩
State after:
no goals

State before:
case inr
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : f n.succ ≤ seqMax f n
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Tactic:
rcases exists_map_eq_seqMax n with ⟨k, h0, h1⟩
State after:
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : f n.succ ≤ seqMax f n
k : ℕ
h0 : k ≤ n
h1 : f k = seqMax f n
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)

State before:
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : f n.succ ≤ seqMax f n
k : ℕ
h0 : k ≤ n
h1 : f k = seqMax f n
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Tactic:
exact ⟨k, n.le_succ.trans' h0, h1.trans (max_eq_left h).symm⟩
State after:
no goals