Theorem: Fin.mem_fin_list_range (src/Pre.lean)

State before:
n : ℕ
i : Fin n
⊢ i ∈ Nat.fin_list_range n
Tactic:
induction n with
| zero => exact i.elim0
| succ n ih =>
  match i with
  | 0 => exact List.mem_cons_self _ _
  | (mk (Nat.succ m) h) =>
    have : m < n := by omega
    let m' : Fin n := ⟨m, this⟩
    unfold Nat.fin_list_range
    apply List.mem_cons_of_mem
    simp only [List.mem_map]
    use m'
    use ih m'
    rfl
State after:
no goals

State before:
case zero
i : Fin Nat.zero
⊢ i ∈ Nat.fin_list_range Nat.zero
Tactic:
exact i.elim0
State after:
no goals

State before:
case succ
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
⊢ i ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
match i with
| 0 => exact List.mem_cons_self _ _
| (mk (Nat.succ m) h) =>
  have : m < n := by omega
  let m' : Fin n := ⟨m, this⟩
  unfold Nat.fin_list_range
  apply List.mem_cons_of_mem
  simp only [List.mem_map]
  use m'
  use ih m'
  rfl
State after:
no goals

State before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
⊢ 0 ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
exact List.mem_cons_self _ _
State after:
no goals

State before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
have : m < n := by omega
State after:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)

State before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
let m' : Fin n := ⟨m, this⟩
State after:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)

State before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
unfold Nat.fin_list_range
State after:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ 0 :: List.map succ (Nat.fin_list_range n)

State before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ 0 :: List.map succ (Nat.fin_list_range n)
Tactic:
apply List.mem_cons_of_mem
State after:
case a
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ List.map succ (Nat.fin_list_range n)

State before:
case a
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ List.map succ (Nat.fin_list_range n)
Tactic:
simp only [List.mem_map]
State after:
case a
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ ∃ a ∈ Nat.fin_list_range n, succ a = { val := Nat.succ m, isLt := h }

State before:
case a
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ ∃ a ∈ Nat.fin_list_range n, succ a = { val := Nat.succ m, isLt := h }
Tactic:
use m'
State after:
case h
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ m' ∈ Nat.fin_list_range n ∧ succ m' = { val := Nat.succ m, isLt := h }

State before:
case h
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ m' ∈ Nat.fin_list_range n ∧ succ m' = { val := Nat.succ m, isLt := h }
Tactic:
use ih m'
State after:
case right
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ succ m' = { val := Nat.succ m, isLt := h }

State before:
case right
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ succ m' = { val := Nat.succ m, isLt := h }
Tactic:
rfl
State after:
no goals

State before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
⊢ m < n
Tactic:
omega
State after:
no goals