Theorem: List.get_pmap (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
i : Fin (length (pmap f l h))
⊢ get (pmap f l h) i =
    f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
      (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
Tactic:
induction l with
| nil => exact i.elim0
| cons a l IH =>
  let ⟨i,hi⟩ := i
  cases i <;> dsimp; rfl
  exact IH _ _
State after:
no goals

State before:
case nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ [] → p a
i : Fin (length (pmap f [] h))
⊢ get (pmap f [] h) i =
    f (get [] (Fin.cast (_ : length (pmap f [] h) = length []) i))
      (_ : p (get [] (Fin.cast (_ : length (pmap f [] h) = length []) i)))
Tactic:
exact i.elim0
State after:
no goals

State before:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
⊢ get (pmap f (a :: l) h) i =
    f (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) i))
      (_ : p (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) i)))
Tactic:
let ⟨i,hi⟩ := i
State after:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i✝ : Fin (length (pmap f (a :: l) h))
i : Nat
hi : i < length (pmap f (a :: l) h)
⊢ get (pmap f (a :: l) h) { val := i, isLt := hi } =
    f (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) { val := i, isLt := hi }))
      (_ : p (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) { val := i, isLt := hi })))

State before:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i✝ : Fin (length (pmap f (a :: l) h))
i : Nat
hi : i < length (pmap f (a :: l) h)
⊢ get (pmap f (a :: l) h) { val := i, isLt := hi } =
    f (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) { val := i, isLt := hi }))
      (_ : p (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) { val := i, isLt := hi })))
Tactic:
cases i <;> dsimp
State after:
case cons.zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
hi : Nat.zero < length (pmap f (a :: l) h)
⊢ f a (_ : p a) = f a (_ : p a)

case cons.succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
n✝ : Nat
hi : Nat.succ n✝ < length (pmap f (a :: l) h)
⊢ get (pmap f l (_ : ∀ (x : α), x ∈ l → p x))
      { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) } =
    f (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) })
      (_ : p (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }))

State before:
case cons.zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
hi : Nat.zero < length (pmap f (a :: l) h)
⊢ f a (_ : p a) = f a (_ : p a)

case cons.succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
n✝ : Nat
hi : Nat.succ n✝ < length (pmap f (a :: l) h)
⊢ get (pmap f l (_ : ∀ (x : α), x ∈ l → p x))
      { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) } =
    f (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) })
      (_ : p (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }))
Tactic:
rfl
State after:
case cons.succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
n✝ : Nat
hi : Nat.succ n✝ < length (pmap f (a :: l) h)
⊢ get (pmap f l (_ : ∀ (x : α), x ∈ l → p x))
      { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) } =
    f (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) })
      (_ : p (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }))

State before:
case cons.succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
n✝ : Nat
hi : Nat.succ n✝ < length (pmap f (a :: l) h)
⊢ get (pmap f l (_ : ∀ (x : α), x ∈ l → p x))
      { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) } =
    f (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) })
      (_ : p (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }))
Tactic:
exact IH _ _
State after:
no goals