Theorem: Nat.unvector_le (Logic/Vorspiel/Vorspiel.lean)

State before:
n e : ℕ
i : Fin n
⊢ unvector e i ≤ e
Tactic:
induction' n with n ih generalizing e <;> simp[*, unvector]
State after:
case zero
n e : ℕ
i : Fin 0
⊢ ![] ≤ e

case succ
n✝ n : ℕ
ih : ∀ (e : ℕ) (i : Fin n), unvector e i ≤ e
e : ℕ
i : Fin (n + 1)
⊢ (e.unpair.1 :> unvector e.unpair.2) i ≤ e

State before:
case zero
n e : ℕ
i : Fin 0
⊢ ![] ≤ e
Tactic:
have := i.isLt
State after:
case zero
n e : ℕ
i : Fin 0
this : ↑i < 0
⊢ ![] ≤ e

State before:
case zero
n e : ℕ
i : Fin 0
this : ↑i < 0
⊢ ![] ≤ e
Tactic:
contradiction
State after:
no goals

State before:
case succ
n✝ n : ℕ
ih : ∀ (e : ℕ) (i : Fin n), unvector e i ≤ e
e : ℕ
i : Fin (n + 1)
⊢ (e.unpair.1 :> unvector e.unpair.2) i ≤ e
Tactic:
exact Fin.cases (by simpa using Nat.unpair_left_le _) (fun i => le_trans (ih e.unpair.2 i) (Nat.unpair_right_le _)) i
State after:
no goals

State before:
n✝ n : ℕ
ih : ∀ (e : ℕ) (i : Fin n), unvector e i ≤ e
e : ℕ
i : Fin (n + 1)
⊢ (e.unpair.1 :> unvector e.unpair.2) 0 ≤ e
Tactic:
simpa using Nat.unpair_left_le _
State after:
no goals