Theorem: Denumerable.lt_of_mem_list (Logic/Vorspiel/Vorspiel.lean)

State before:
⊢ ∀ i ∈ ofNat (List ℕ) 0, i < 0
Tactic:
simp
State after:
no goals

State before:
n : ℕ
this : n.unpair.2 < n + 1
⊢ ∀ i ∈ ofNat (List ℕ) (n + 1), i < n + 1
Tactic:
simp
State after:
n : ℕ
this : n.unpair.2 < n + 1
⊢ n.unpair.1 < n + 1 ∧ ∀ a ∈ ofNat (List ℕ) n.unpair.2, a < n + 1

State before:
n : ℕ
this : n.unpair.2 < n + 1
⊢ n.unpair.1 < n + 1 ∧ ∀ a ∈ ofNat (List ℕ) n.unpair.2, a < n + 1
Tactic:
exact ⟨Nat.lt_succ_of_le (Nat.unpair_left_le n),
  by { intro i hi
       have : i < n.unpair.2 := lt_of_mem_list n.unpair.2 i hi
       exact lt_trans this (Nat.lt_succ_of_le $ Nat.unpair_right_le n) }⟩
State after:
no goals

State before:
n : ℕ
this : n.unpair.2 < n + 1
⊢ ∀ a ∈ ofNat (List ℕ) n.unpair.2, a < n + 1
Tactic:
intro i hi
State after:
n : ℕ
this : n.unpair.2 < n + 1
i : ℕ
hi : i ∈ ofNat (List ℕ) n.unpair.2
⊢ i < n + 1

State before:
n : ℕ
this : n.unpair.2 < n + 1
i : ℕ
hi : i ∈ ofNat (List ℕ) n.unpair.2
⊢ i < n + 1
Tactic:
have : i < n.unpair.2 := lt_of_mem_list n.unpair.2 i hi
State after:
n : ℕ
this✝ : n.unpair.2 < n + 1
i : ℕ
hi : i ∈ ofNat (List ℕ) n.unpair.2
this : i < n.unpair.2
⊢ i < n + 1

State before:
n : ℕ
this✝ : n.unpair.2 < n + 1
i : ℕ
hi : i ∈ ofNat (List ℕ) n.unpair.2
this : i < n.unpair.2
⊢ i < n + 1
Tactic:
exact lt_trans this (Nat.lt_succ_of_le $ Nat.unpair_right_le n)
State after:
no goals