Theorem: Fin.restrict_of_not_mem_last (Fifteen/Data/Fin/Basic.lean)

State before:
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∃ l', l = List.map castSucc l'
Tactic:
refine .intro (l.pmap (fun i (hi : i.1 < n) => ⟨i.1,hi⟩) ?_) ?_
State after:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (a : Fin (n + 1)), a ∈ l → ↑a < n

case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l ?refine_1)

State before:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (a : Fin (n + 1)), a ∈ l → ↑a < n

case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l ?refine_1)
Tactic:
. intro i hi
  cases Nat.eq_or_lt_of_le i.2 with
  | inl heq => cases i; cases heq; exact absurd hi h
  | inr hlt => exact Nat.lt_of_succ_lt_succ hlt
State after:
case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))

State before:
case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))
Tactic:
. apply List.ext_get
  . rw [List.length_map, List.length_pmap]
  . intro i hi _
    rewrite [List.get_map, List.get_pmap]
    rfl
State after:
no goals

State before:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (a : Fin (n + 1)), a ∈ l → ↑a < n
Tactic:
intro i hi
State after:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
⊢ ↑i < n

State before:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
⊢ ↑i < n
Tactic:
cases Nat.eq_or_lt_of_le i.2 with
| inl heq => cases i; cases heq; exact absurd hi h
| inr hlt => exact Nat.lt_of_succ_lt_succ hlt
State after:
no goals

State before:
case refine_1.inl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
heq : Nat.succ ↑i = n + 1
⊢ ↑i < n
Tactic:
cases i
State after:
case refine_1.inl.mk
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
val✝ : Nat
isLt✝ : val✝ < n + 1
hi : { val := val✝, isLt := isLt✝ } ∈ l
heq : Nat.succ ↑{ val := val✝, isLt := isLt✝ } = n + 1
⊢ ↑{ val := val✝, isLt := isLt✝ } < n

State before:
case refine_1.inl.mk
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
val✝ : Nat
isLt✝ : val✝ < n + 1
hi : { val := val✝, isLt := isLt✝ } ∈ l
heq : Nat.succ ↑{ val := val✝, isLt := isLt✝ } = n + 1
⊢ ↑{ val := val✝, isLt := isLt✝ } < n
Tactic:
cases heq
State after:
case refine_1.inl.mk.refl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
isLt✝ : n < n + 1
hi : { val := n, isLt := isLt✝ } ∈ l
⊢ ↑{ val := n, isLt := isLt✝ } < n

State before:
case refine_1.inl.mk.refl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
isLt✝ : n < n + 1
hi : { val := n, isLt := isLt✝ } ∈ l
⊢ ↑{ val := n, isLt := isLt✝ } < n
Tactic:
exact absurd hi h
State after:
no goals

State before:
case refine_1.inr
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
hlt : Nat.succ ↑i < n + 1
⊢ ↑i < n
Tactic:
exact Nat.lt_of_succ_lt_succ hlt
State after:
no goals

State before:
case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))
Tactic:
apply List.ext_get
State after:
case refine_2.hl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ List.length l =
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))

case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }

State before:
case refine_2.hl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ List.length l =
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))

case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }
Tactic:
. rw [List.length_map, List.length_pmap]
State after:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }

State before:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }
Tactic:
. intro i hi _
  rewrite [List.get_map, List.get_pmap]
  rfl
State after:
no goals

State before:
case refine_2.hl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ List.length l =
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
Tactic:
rw [List.length_map, List.length_pmap]
State after:
no goals

State before:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }
Tactic:
intro i hi _
State after:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Nat
hi : i < List.length l
h₂✝ :
  i <
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
⊢ List.get l { val := i, isLt := hi } =
    List.get
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
      { val := i, isLt := h₂✝ }

State before:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Nat
hi : i < List.length l
h₂✝ :
  i <
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
⊢ List.get l { val := i, isLt := hi } =
    List.get
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
      { val := i, isLt := h₂✝ }
Tactic:
rewrite [List.get_map, List.get_pmap]
State after:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Nat
hi : i < List.length l
h₂✝ :
  i <
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
⊢ List.get l { val := i, isLt := hi } =
    castSucc
      {
        val :=
          ↑(List.get l
              (cast
                (_ :
                  List.length
                      (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)) =
                    List.length l)
                { val := ↑{ val := i, isLt := h₂✝ },
                  isLt :=
                    (_ :
                      ↑{ val := i, isLt := h₂✝ } <
                        List.length
                          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                            (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))) })),
        isLt :=
          (_ :
            ↑(List.get l
                  (cast
                    (_ :
                      List.length
                          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                            (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)) =
                        List.length l)
                    { val := ↑{ val := i, isLt := h₂✝ },
                      isLt :=
                        (_ :
                          ↑{ val := i, isLt := h₂✝ } <
                            List.length
                              (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                                (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))) })) <
              n) }

State before:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Nat
hi : i < List.length l
h₂✝ :
  i <
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
⊢ List.get l { val := i, isLt := hi } =
    castSucc
      {
        val :=
          ↑(List.get l
              (cast
                (_ :
                  List.length
                      (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)) =
                    List.length l)
                { val := ↑{ val := i, isLt := h₂✝ },
                  isLt :=
                    (_ :
                      ↑{ val := i, isLt := h₂✝ } <
                        List.length
                          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                            (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))) })),
        isLt :=
          (_ :
            ↑(List.get l
                  (cast
                    (_ :
                      List.length
                          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                            (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)) =
                        List.length l)
                    { val := ↑{ val := i, isLt := h₂✝ },
                      isLt :=
                        (_ :
                          ↑{ val := i, isLt := h₂✝ } <
                            List.length
                              (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                                (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))) })) <
              n) }
Tactic:
rfl
State after:
no goals