internlm/Lean-Github huggingface dataset:
Theorem: List.Index.unappend_append
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (i : xs.Index ⊕ ys.Index), (append i).unappend = i
ys : List α✝
i : (x :: xs).Index ⊕ ys.Index
j : ys.Index
⊢ (append (Sum.inr j)).unappend = Sum.inr j
Tactic:
simp only [append, unappend, ih]
Proof state after:
no goals
Theorem: List.Index.append_unappend
Proof state before:
α✝ : Type u_1
xs ys : List α✝
k : (xs ++ ys).Index
⊢ append k.unappend = k
Tactic:
induction xs generalizing ys with
| nil => rfl
| cons x xs ih =>
  match k with
  | .head => rfl
  | .tail k =>
    simp only [unappend]
    split
    next h => rw [append, ←h, ih]
    next h => rw [append, ←h, ih]
Proof state after:
no goals
Theorem: List.Index.append_unappend
Proof state before:
case nil
α✝ : Type u_1
ys : List α✝
k : ([] ++ ys).Index
⊢ append k.unappend = k
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.append_unappend
Proof state before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k : (x :: xs ++ ys).Index
⊢ append k.unappend = k
Tactic:
match k with
| .head => rfl
| .tail k =>
  simp only [unappend]
  split
  next h => rw [append, ←h, ih]
  next h => rw [append, ←h, ih]
Proof state after:
no goals
Theorem: List.Index.append_unappend
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k : (x :: xs ++ ys).Index
⊢ append head.unappend = head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.append_unappend
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
⊢ append k.tail.unappend = k.tail
Tactic:
simp only [unappend]
Proof state after:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
⊢ append
      (match k.unappend with
      | Sum.inl i => Sum.inl i.tail
      | Sum.inr i => Sum.inr i) =
    k.tail
Theorem: List.Index.append_unappend
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
⊢ append
      (match k.unappend with
      | Sum.inl i => Sum.inl i.tail
      | Sum.inr i => Sum.inr i) =
    k.tail
Tactic:
split
Proof state after:
case h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : xs.Index
heq✝ : k.unappend = Sum.inl i✝
⊢ append (Sum.inl i✝.tail) = k.tail

case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
heq✝ : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail
Theorem: List.Index.append_unappend
Proof state before:
case h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : xs.Index
heq✝ : k.unappend = Sum.inl i✝
⊢ append (Sum.inl i✝.tail) = k.tail

case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
heq✝ : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail
Tactic:
next h => rw [append, ←h, ih]
Proof state after:
case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
heq✝ : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail
Theorem: List.Index.append_unappend
Proof state before:
case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
heq✝ : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail
Tactic:
next h => rw [append, ←h, ih]
Proof state after:
no goals
Theorem: List.Index.append_unappend
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : xs.Index
h : k.unappend = Sum.inl i✝
⊢ append (Sum.inl i✝.tail) = k.tail
Tactic:
rw [append, ←h, ih]
Proof state after:
no goals
Theorem: List.Index.append_unappend
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
h : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail
Tactic:
rw [append, ←h, ih]
Proof state after:
no goals
Theorem: List.Index.append_eq_iff_eq_unappend
Proof state before:
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ append i = j ↔ i = j.unappend
Tactic:
constructor
Proof state after:
case mp
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ append i = j → i = j.unappend

case mpr
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ i = j.unappend → append i = j
Theorem: List.Index.append_eq_iff_eq_unappend
Proof state before:
case mp
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ append i = j → i = j.unappend
Tactic:
intro h
Proof state after:
case mp
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
h : append i = j
⊢ i = j.unappend
Theorem: List.Index.append_eq_iff_eq_unappend
Proof state before:
case mp
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
h : append i = j
⊢ i = j.unappend
Tactic:
rw [←h, unappend_append]
Proof state after:
no goals
Theorem: List.Index.append_eq_iff_eq_unappend
Proof state before:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ i = j.unappend → append i = j
Tactic:
intro h
Proof state after:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
h : i = j.unappend
⊢ append i = j
Theorem: List.Index.append_eq_iff_eq_unappend
Proof state before:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
h : i = j.unappend
⊢ append i = j
Tactic:
rw [h, append_unappend]
Proof state after:
no goals
Theorem: List.Index.unappend_eq_iff_eq_append
Proof state before:
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
⊢ i.unappend = j ↔ i = append j
Tactic:
constructor
Proof state after:
case mp
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
⊢ i.unappend = j → i = append j

case mpr
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
⊢ i = append j → i.unappend = j
Theorem: List.Index.unappend_eq_iff_eq_append
Proof state before:
case mp
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
⊢ i.unappend = j → i = append j
Tactic:
intro h
Proof state after:
case mp
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
h : i.unappend = j
⊢ i = append j
Theorem: List.Index.unappend_eq_iff_eq_append
Proof state before:
case mp
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
h : i.unappend = j
⊢ i = append j
Tactic:
rw [←h, append_unappend]
Proof state after:
no goals
Theorem: List.Index.unappend_eq_iff_eq_append
Proof state before:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
⊢ i = append j → i.unappend = j
Tactic:
intro h
Proof state after:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
h : i = append j
⊢ i.unappend = j
Theorem: List.Index.unappend_eq_iff_eq_append
Proof state before:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : (xs ++ ys).Index
j : xs.Index ⊕ ys.Index
h : i = append j
⊢ i.unappend = j
Tactic:
rw [h, unappend_append]
Proof state after:
no goals
Theorem: List.Index.val_append_inl
Proof state before:
α✝ : Type u_1
xs ys : List α✝
i : xs.Index
⊢ i.append_inl.val = i.val
Tactic:
induction i with
| head => rfl
| tail _ ih => exact ih
Proof state after:
no goals
Theorem: List.Index.val_append_inl
Proof state before:
case head
α✝ : Type u_1
xs ys : List α✝
x✝ : α✝
xs✝ : List α✝
⊢ head.append_inl.val = head.val
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.val_append_inl
Proof state before:
case tail
α✝ : Type u_1
xs ys xs✝ : List α✝
x✝ : α✝
a✝ : xs✝.Index
ih : a✝.append_inl.val = a✝.val
⊢ a✝.tail.append_inl.val = a✝.tail.val
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.Index.val_append_inr
Proof state before:
α✝ : Type u_1
ys xs : List α✝
j : ys.Index
⊢ j.append_inr.val = j.val
Tactic:
induction xs with
| nil => rfl
| cons _ _ ih => exact ih
Proof state after:
no goals
Theorem: List.Index.val_append_inr
Proof state before:
case nil
α✝ : Type u_1
ys : List α✝
j : ys.Index
⊢ j.append_inr.val = j.val
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.val_append_inr
Proof state before:
case cons
α✝ : Type u_1
ys : List α✝
j : ys.Index
head✝ : α✝
tail✝ : List α✝
ih : j.append_inr.val = j.val
⊢ j.append_inr.val = j.val
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.Index.val_append
Proof state before:
α : Type u_1
xs ys : List α
i : xs.Index ⊕ ys.Index
⊢ (append i).val =
    match i with
    | Sum.inl i => i.val
    | Sum.inr j => j.val
Tactic:
match i with
| .inl _ => exact val_append_inl ..
| .inr _ => exact val_append_inr ..
Proof state after:
no goals
Theorem: List.Index.val_append
Proof state before:
α : Type u_1
xs ys : List α
i : xs.Index ⊕ ys.Index
val✝ : xs.Index
⊢ (append (Sum.inl val✝)).val =
    match Sum.inl val✝ with
    | Sum.inl i => i.val
    | Sum.inr j => j.val
Tactic:
exact val_append_inl ..
Proof state after:
no goals
Theorem: List.Index.val_append
Proof state before:
α : Type u_1
xs ys : List α
i : xs.Index ⊕ ys.Index
val✝ : ys.Index
⊢ (append (Sum.inr val✝)).val =
    match Sum.inr val✝ with
    | Sum.inl i => i.val
    | Sum.inr j => j.val
Tactic:
exact val_append_inr ..
Proof state after:
no goals
Theorem: List.Index.val_unappend
Proof state before:
α : Type u_1
xs ys : List α
k : (xs ++ ys).Index
⊢ (match k.unappend with
    | Sum.inl i => i.val
    | Sum.inr j => j.val) =
    k.val
Tactic:
rw [←append_unappend k, val_append, unappend_append]
Proof state after:
no goals
Theorem: List.Index.unsum_sum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
val✝ : xs.Index
⊢ (sum (Sum.inl val✝)).unsum = Sum.inl val✝
Tactic:
simp only [unsum, sum, unappend_append, unmap_map]
Proof state after:
no goals
Theorem: List.Index.unsum_sum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
val✝ : ys.Index
⊢ (sum (Sum.inr val✝)).unsum = Sum.inr val✝
Tactic:
simp only [unsum, sum, unappend_append, unmap_map]
Proof state after:
no goals
Theorem: List.Index.sum_unsum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
⊢ sum k.unsum = k
Tactic:
match h : unappend k with
| .inl i => rw [unappend_eq_iff_eq_append] at h; simp only [h, unsum, unappend_append, sum, map_unmap]
| .inr j => rw [unappend_eq_iff_eq_append] at h; simp only [h, unsum, unappend_append, sum, map_unmap]
Proof state after:
no goals
Theorem: List.Index.sum_unsum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : (List.map Sum.inl xs).Index
h : k.unappend = Sum.inl i
⊢ sum k.unsum = k
Tactic:
rw [unappend_eq_iff_eq_append] at h
Proof state after:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : (List.map Sum.inl xs).Index
h : k = append (Sum.inl i)
⊢ sum k.unsum = k
Theorem: List.Index.sum_unsum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : (List.map Sum.inl xs).Index
h : k = append (Sum.inl i)
⊢ sum k.unsum = k
Tactic:
simp only [h, unsum, unappend_append, sum, map_unmap]
Proof state after:
no goals
Theorem: List.Index.sum_unsum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
j : (List.map Sum.inr ys).Index
h : k.unappend = Sum.inr j
⊢ sum k.unsum = k
Tactic:
rw [unappend_eq_iff_eq_append] at h
Proof state after:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
j : (List.map Sum.inr ys).Index
h : k = append (Sum.inr j)
⊢ sum k.unsum = k
Theorem: List.Index.sum_unsum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
j : (List.map Sum.inr ys).Index
h : k = append (Sum.inr j)
⊢ sum k.unsum = k
Tactic:
simp only [h, unsum, unappend_append, sum, map_unmap]
Proof state after:
no goals
Theorem: List.Index.sum_eq_iff_eq_unsum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
⊢ sum i = k ↔ i = k.unsum
Tactic:
constructor
Proof state after:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
⊢ sum i = k → i = k.unsum

case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
⊢ i = k.unsum → sum i = k
Theorem: List.Index.sum_eq_iff_eq_unsum
Proof state before:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
⊢ sum i = k → i = k.unsum
Tactic:
intro h
Proof state after:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
h : sum i = k
⊢ i = k.unsum
Theorem: List.Index.sum_eq_iff_eq_unsum
Proof state before:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
h : sum i = k
⊢ i = k.unsum
Tactic:
rw [←h, unsum_sum]
Proof state after:
no goals
Theorem: List.Index.sum_eq_iff_eq_unsum
Proof state before:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
⊢ i = k.unsum → sum i = k
Tactic:
intro h
Proof state after:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
h : i = k.unsum
⊢ sum i = k
Theorem: List.Index.sum_eq_iff_eq_unsum
Proof state before:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
i : xs.Index ⊕ ys.Index
k : (xs.sum ys).Index
h : i = k.unsum
⊢ sum i = k
Tactic:
rw [h, sum_unsum]
Proof state after:
no goals
Theorem: List.Index.unsum_eq_iff_eq_sum
Proof state before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k.unsum = i ↔ k = sum i
Tactic:
constructor
Proof state after:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k.unsum = i → k = sum i

case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k = sum i → k.unsum = i
Theorem: List.Index.unsum_eq_iff_eq_sum
Proof state before:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k.unsum = i → k = sum i
Tactic:
intro h
Proof state after:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
h : k.unsum = i
⊢ k = sum i
Theorem: List.Index.unsum_eq_iff_eq_sum
Proof state before:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
h : k.unsum = i
⊢ k = sum i
Tactic:
rw [←h, sum_unsum]
Proof state after:
no goals
Theorem: List.Index.unsum_eq_iff_eq_sum
Proof state before:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k = sum i → k.unsum = i
Tactic:
intro h
Proof state after:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
h : k = sum i
⊢ k.unsum = i
Theorem: List.Index.unsum_eq_iff_eq_sum
Proof state before:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
h : k = sum i
⊢ k.unsum = i
Tactic:
rw [h, unsum_sum]
Proof state after:
no goals
Theorem: List.Index.val_sum
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index ⊕ ys.Index
⊢ (match i with
    | Sum.inl i => Sum.inl i.val
    | Sum.inr j => Sum.inr j.val) =
    (sum i).val
Tactic:
match i with
| .inl i => simp only [sum, val_append, val_map]
| .inr j => simp only [sum, val_append, val_map]
Proof state after:
no goals
Theorem: List.Index.val_sum
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i✝ : xs.Index ⊕ ys.Index
i : xs.Index
⊢ (match Sum.inl i with
    | Sum.inl i => Sum.inl i.val
    | Sum.inr j => Sum.inr j.val) =
    (sum (Sum.inl i)).val
Tactic:
simp only [sum, val_append, val_map]
Proof state after:
no goals
Theorem: List.Index.val_sum
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index ⊕ ys.Index
j : ys.Index
⊢ (match Sum.inr j with
    | Sum.inl i => Sum.inl i.val
    | Sum.inr j => Sum.inr j.val) =
    (sum (Sum.inr j)).val
Tactic:
simp only [sum, val_append, val_map]
Proof state after:
no goals
Theorem: List.Index.val_unsum
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.sum ys).Index
⊢ k.val =
    match k.unsum with
    | Sum.inl i => Sum.inl i.val
    | Sum.inr j => Sum.inr j.val
Tactic:
rw [←sum_unsum k, val_sum, unsum_sum]
Proof state after:
no goals
Theorem: List.Index.unsigma_sigma
Proof state before:
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
⊢ (sigma i).unsigma = i
Tactic:
induction xs with
| nil => cases i; contradiction
| cons x xs ih =>
  match i with
  | ⟨head, j⟩ => simp only [sigma, unsigma, unappend_append, unmap_map]
  | ⟨tail i, j⟩ => simp only [sigma, unsigma, unappend_append]; rw [ih]
Proof state after:
no goals
Theorem: List.Index.unsigma_sigma
Proof state before:
case nil
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : [].Index) × (f i.val).Index
⊢ (sigma i).unsigma = i
Tactic:
cases i
Proof state after:
case nil.mk
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
fst✝ : [].Index
snd✝ : (f fst✝.val).Index
⊢ (sigma ⟨fst✝, snd✝⟩).unsigma = ⟨fst✝, snd✝⟩
Theorem: List.Index.unsigma_sigma
Proof state before:
case nil.mk
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
fst✝ : [].Index
snd✝ : (f fst✝.val).Index
⊢ (sigma ⟨fst✝, snd✝⟩).unsigma = ⟨fst✝, snd✝⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.unsigma_sigma
Proof state before:
case cons
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).unsigma = i
i : (i : (x :: xs).Index) × (f i.val).Index
⊢ (sigma i).unsigma = i
Tactic:
match i with
| ⟨head, j⟩ => simp only [sigma, unsigma, unappend_append, unmap_map]
| ⟨tail i, j⟩ => simp only [sigma, unsigma, unappend_append]; rw [ih]
Proof state after:
no goals
Theorem: List.Index.unsigma_sigma
Proof state before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).unsigma = i
i : (i : (x :: xs).Index) × (f i.val).Index
j : (f head.val).Index
⊢ (sigma ⟨head, j⟩).unsigma = ⟨head, j⟩
Tactic:
simp only [sigma, unsigma, unappend_append, unmap_map]
Proof state after:
no goals
Theorem: List.Index.unsigma_sigma
Proof state before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).unsigma = i
i✝ : (i : (x :: xs).Index) × (f i.val).Index
i : xs.Index
j : (f i.tail.val).Index
⊢ (sigma ⟨i.tail, j⟩).unsigma = ⟨i.tail, j⟩
Tactic:
simp only [sigma, unsigma, unappend_append]
Proof state after:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).unsigma = i
i✝ : (i : (x :: xs).Index) × (f i.val).Index
i : xs.Index
j : (f i.tail.val).Index
⊢ ⟨(sigma ⟨i, j⟩).unsigma.fst.tail, (sigma ⟨i, j⟩).unsigma.snd⟩ = ⟨i.tail, j⟩
Theorem: List.Index.unsigma_sigma
Proof state before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).unsigma = i
i✝ : (i : (x :: xs).Index) × (f i.val).Index
i : xs.Index
j : (f i.tail.val).Index
⊢ ⟨(sigma ⟨i, j⟩).unsigma.fst.tail, (sigma ⟨i, j⟩).unsigma.snd⟩ = ⟨i.tail, j⟩
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: List.Index.sigma_unsigma
Proof state before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
xs : List α
k : (xs.sigma f).Index
⊢ sigma k.unsigma = k
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  match h : unappend k with
  | .inl j => rw [unappend_eq_iff_eq_append] at h; cases h; rw [unsigma, unappend_append, sigma, map_unmap]
  | .inr k => rw [unappend_eq_iff_eq_append] at h; cases h; rw [unsigma, unappend_append, sigma, ih]
Proof state after:
no goals
Theorem: List.Index.sigma_unsigma
Proof state before:
case nil
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
k : ([].sigma f).Index
⊢ sigma k.unsigma = k
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.sigma_unsigma
Proof state before:
case cons
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : ((x :: xs).sigma f).Index
⊢ sigma k.unsigma = k
Tactic:
match h : unappend k with
| .inl j => rw [unappend_eq_iff_eq_append] at h; cases h; rw [unsigma, unappend_append, sigma, map_unmap]
| .inr k => rw [unappend_eq_iff_eq_append] at h; cases h; rw [unsigma, unappend_append, sigma, ih]
Proof state after:
no goals
Theorem: List.Index.sigma_unsigma
Proof state before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : ((x :: xs).sigma f).Index
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
h : k.unappend = Sum.inl j
⊢ sigma k.unsigma = k
Tactic:
rw [unappend_eq_iff_eq_append] at h
Proof state after:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : ((x :: xs).sigma f).Index
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
h : k = append (Sum.inl j)
⊢ sigma k.unsigma = k
Theorem: List.Index.sigma_unsigma
Proof state before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : ((x :: xs).sigma f).Index
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
h : k = append (Sum.inl j)
⊢ sigma k.unsigma = k
Tactic:
cases h
Proof state after:
case refl
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
⊢ sigma (append (Sum.inl j)).unsigma = append (Sum.inl j)
Theorem: List.Index.sigma_unsigma
Proof state before:
case refl
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
⊢ sigma (append (Sum.inl j)).unsigma = append (Sum.inl j)
Tactic:
rw [unsigma, unappend_append, sigma, map_unmap]
Proof state after:
no goals