Theorem: Imo1977P6.imo1977_p6_nat (Compfiles/Imo1977P6.lean)

State before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
⊢ ∀ (n : ℕ), f n = n
Tactic:
have hf : ∀ n, n ≤ f n := fun n => h' n n rfl.le
State after:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
⊢ ∀ (n : ℕ), f n = n

State before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
⊢ ∀ (n : ℕ), f n = n
Tactic:
have hf_mono : StrictMono f := strictMono_nat_of_lt_succ fun _ => lt_of_le_of_lt (hf _) (h _)
State after:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
⊢ ∀ (n : ℕ), f n = n

State before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
⊢ ∀ (n : ℕ), f n = n
Tactic:
intro
State after:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
n✝ : ℕ
⊢ f n✝ = n✝

State before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
hf_mono : StrictMono f
n✝ : ℕ
⊢ f n✝ = n✝
Tactic:
exact Nat.eq_of_le_of_lt_succ (hf _) (hf_mono.lt_iff_lt.mp (h _))
State after:
no goals

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

State before:
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
⊢ ∀ (n : ℕ), k ≤ n → k ≤ f n
Tactic:
induction' k with k h_ind
State after:
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
⊢ ∀ (n : ℕ), 0 ≤ n → 0 ≤ f n

case succ
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
⊢ ∀ (n : ℕ), k + 1 ≤ n → k + 1 ≤ f n

State before:
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
⊢ ∀ (n : ℕ), 0 ≤ n → 0 ≤ f n
Tactic:
intros
State after:
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
n✝ : ℕ
a✝ : 0 ≤ n✝
⊢ 0 ≤ f n✝

State before:
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
n✝ : ℕ
a✝ : 0 ≤ n✝
⊢ 0 ≤ f n✝
Tactic:
exact Nat.zero_le _
State after:
no goals

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

State before:
case succ
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k + 1 ≤ f n
Tactic:
apply Nat.succ_le_of_lt
State after:
case succ.h
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k < f n

State before:
case succ.h
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k < f n
Tactic:
calc
  k ≤ f (f (n - 1)) := h_ind _ (h_ind (n - 1) (le_tsub_of_add_le_right hk))
  _ < f n := tsub_add_cancel_of_le (le_trans (Nat.succ_le_succ (Nat.zero_le _)) hk) ▸ h _
State after:
no goals