Theorem: Imo2009P5.exists_sup_fn_fin (Compfiles/Imo2009P5.lean)

State before:
f : ℕ → ℕ
c : ℕ
⊢ ∃ K, ∀ n < c, f n ≤ K
Tactic:
induction' c with c ih
State after:
case zero
f : ℕ → ℕ
⊢ ∃ K, ∀ n < 0, f n ≤ K

case succ
f : ℕ → ℕ
c : ℕ
ih : ∃ K, ∀ n < c, f n ≤ K
⊢ ∃ K, ∀ n < c + 1, f n ≤ K

State before:
case zero
f : ℕ → ℕ
⊢ ∃ K, ∀ n < 0, f n ≤ K
Tactic:
simp
State after:
no goals

State before:
case succ
f : ℕ → ℕ
c : ℕ
ih : ∃ K, ∀ n < c, f n ≤ K
⊢ ∃ K, ∀ n < c + 1, f n ≤ K
Tactic:
obtain ⟨k, hk⟩ := ih
State after:
case succ.intro
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
⊢ ∃ K, ∀ n < c + 1, f n ≤ K

State before:
case succ.intro
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
⊢ ∃ K, ∀ n < c + 1, f n ≤ K
Tactic:
use max k (f c)
State after:
case h
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
⊢ ∀ n < c + 1, f n ≤ max k (f c)

State before:
case h
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
⊢ ∀ n < c + 1, f n ≤ max k (f c)
Tactic:
intro n hn
State after:
case h
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
n : ℕ
hn : n < c + 1
⊢ f n ≤ max k (f c)

State before:
case h
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
n : ℕ
hn : n < c + 1
⊢ f n ≤ max k (f c)
Tactic:
obtain hlt | rfl := Nat.lt_succ_iff_lt_or_eq.mp hn <;> aesop
State after:
no goals