Theorem: IMOSL.IMO2011A4.main_step (IMOSLLean4/IMO2011/A4/A4.lean)

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
⊢ f = id
Tactic:
have h1 : ∀ t n, n ≤ f^[t] n :=
  Nat.rec Nat.le_refl λ t h1 n ↦ (h0 n).trans (h1 _)
State after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
⊢ f = id

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
⊢ f = id
Tactic:
have h2 : StrictMono f :=
  strictMono_nat_of_lt_succ λ n ↦ (h1 _ (f n)).trans_lt (h n)
State after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
⊢ f = id

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
⊢ f = id
Tactic:
refine funext λ n ↦ (h0 n).antisymm' ?_
State after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
n : ℕ
⊢ f n ≤ n

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
n : ℕ
⊢ f n ≤ n
Tactic:
rw [← Nat.lt_succ_iff, ← h2.lt_iff_lt]
State after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
n : ℕ
⊢ f (f n) < f n.succ

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
n : ℕ
⊢ f (f n) < f n.succ
Tactic:
exact (h1 _ _).trans_lt (h n)
State after:
no goals

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
⊢ ∀ (n : ℕ), n ≤ f n
Tactic:
suffices ∀ k n : ℕ, k ≤ n → k ≤ f n from λ n ↦ this n n n.le_refl
State after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
⊢ ∀ (k n : ℕ), k ≤ n → k ≤ f n

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
⊢ ∀ (k n : ℕ), k ≤ n → k ≤ f n
Tactic:
refine Nat.rec (λ k _ ↦ (f k).zero_le) (λ k h0 n h1 ↦ ?_)
State after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n
⊢ k.succ ≤ f n

State before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n
⊢ k.succ ≤ f n
Tactic:
rcases n with _ | n
State after:
case zero
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
h1 : k.succ ≤ 0
⊢ k.succ ≤ f 0

case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
⊢ k.succ ≤ f (n + 1)

State before:
case zero
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
h1 : k.succ ≤ 0
⊢ k.succ ≤ f 0
Tactic:
exact absurd k.succ_pos h1.not_lt
State after:
no goals

State before:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
⊢ k.succ ≤ f (n + 1)
Tactic:
refine (h n).trans_le' ?_
State after:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
⊢ k ≤ f^[g n + 2] n

State before:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
⊢ k ≤ f^[g n + 2] n
Tactic:
generalize g n + 2 = t
State after:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
t : ℕ
⊢ k ≤ f^[t] n

State before:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
t : ℕ
⊢ k ≤ f^[t] n
Tactic:
exact t.rec (Nat.succ_le_succ_iff.mp h1)
  (λ t h2 ↦ (h0 _ h2).trans_eq (f.iterate_succ_apply' _ _).symm)
State after:
no goals