internlm/Lean-Github huggingface dataset:
Theorem: List.Index.unsublist_pos_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
⊢ (match ⋯ ▸ ⋯ ▸ i.tail with
    | head => head
    | i.tail => (unsublist p i).tail) =
    (unsublist p i).tail
Tactic:
split
Proof state after:
case h_1
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ i.tail = head
⊢ head = (unsublist p i).tail

case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ i.tail = i✝.tail
⊢ (unsublist p i✝).tail = (unsublist p i).tail
Theorem: List.Index.unsublist_pos_tail
Proof state before:
case h_1
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ i.tail = head
⊢ head = (unsublist p i).tail

case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ i.tail = i✝.tail
⊢ (unsublist p i✝).tail = (unsublist p i).tail
Tactic:
next i hh => elim_casts at hh; cases hh
Proof state after:
case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ i.tail = i✝.tail
⊢ (unsublist p i✝).tail = (unsublist p i).tail
Theorem: List.Index.unsublist_pos_tail
Proof state before:
case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ i.tail = i✝.tail
⊢ (unsublist p i✝).tail = (unsublist p i).tail
Tactic:
next i hh => elim_casts at hh; cases hh; rfl
Proof state after:
no goals
Theorem: List.Index.unsublist_pos_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i✝ : (List.sublist p xs).Index
i : (⟨x, ⋯⟩ :: List.sublist p xs).Index
hh : ⋯ ▸ ⋯ ▸ i✝.tail = head
⊢ head = (unsublist p i✝).tail
Tactic:
elim_casts at hh
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i✝ : (List.sublist p xs).Index
i : (⟨x, ⋯⟩ :: List.sublist p xs).Index
hh : i✝.tail = head
⊢ head = (unsublist p i✝).tail
Theorem: List.Index.unsublist_pos_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i✝ : (List.sublist p xs).Index
i : (⟨x, ⋯⟩ :: List.sublist p xs).Index
hh : i✝.tail = head
⊢ head = (unsublist p i✝).tail
Tactic:
cases hh
Proof state after:
no goals
Theorem: List.Index.unsublist_pos_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i✝ : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : ⋯ ▸ ⋯ ▸ i✝.tail = i.tail
⊢ (unsublist p i).tail = (unsublist p i✝).tail
Tactic:
elim_casts at hh
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i✝ : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : i✝.tail = i.tail
⊢ (unsublist p i).tail = (unsublist p i✝).tail
Theorem: List.Index.unsublist_pos_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i✝ : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : i✝.tail = i.tail
⊢ (unsublist p i).tail = (unsublist p i✝).tail
Tactic:
cases hh
Proof state after:
case refl
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
⊢ (unsublist p i).tail = (unsublist p i).tail
Theorem: List.Index.unsublist_pos_tail
Proof state before:
case refl
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
⊢ (unsublist p i).tail = (unsublist p i).tail
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.unsublist_neg_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ unsublist p (⋯ ▸ i) = (unsublist p i).tail
Tactic:
simp only [unsublist]
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ (if h_1 : p x then
      match ⋯ ▸ ⋯ ▸ i with
      | head => head
      | i.tail => (unsublist p i).tail
    else (unsublist p (⋯ ▸ ⋯ ▸ i)).tail) =
    (unsublist p i).tail
Theorem: List.Index.unsublist_neg_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ (if h_1 : p x then
      match ⋯ ▸ ⋯ ▸ i with
      | head => head
      | i.tail => (unsublist p i).tail
    else (unsublist p (⋯ ▸ ⋯ ▸ i)).tail) =
    (unsublist p i).tail
Tactic:
rw [dif_neg h]
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ (unsublist p (⋯ ▸ ⋯ ▸ i)).tail = (unsublist p i).tail
Theorem: List.Index.unsublist_neg_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ (unsublist p (⋯ ▸ ⋯ ▸ i)).tail = (unsublist p i).tail
Tactic:
congr
Proof state after:
case e_a.e_i
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ ⋯ ▸ ⋯ ▸ i = i
Theorem: List.Index.unsublist_neg_tail
Proof state before:
case e_a.e_i
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : ¬p x
i : (List.sublist p xs).Index
⊢ ⋯ ▸ ⋯ ▸ i = i
Tactic:
elim_casts
Proof state after:
no goals
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case nil
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
i : [].Index
hi : p i.val
j : (List.sublist p []).Index
⊢ sublist p i hi = j ↔ i = unsublist p j
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
⊢ sublist p head hi = j ↔ head = unsublist p j
Tactic:
rw [sublist_pos_head hx]
Proof state after:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
⊢ ⋯ ▸ head = j ↔ head = unsublist p j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
⊢ ⋯ ▸ head = j ↔ head = unsublist p j
Tactic:
constructor
Proof state after:
case head.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
⊢ ⋯ ▸ head = j → head = unsublist p j

case head.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
⊢ head = unsublist p j → ⋯ ▸ head = j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
⊢ ⋯ ▸ head = j → head = unsublist p j
Tactic:
intro h
Proof state after:
case head.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
h : ⋯ ▸ head = j
⊢ head = unsublist p j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
h : ⋯ ▸ head = j
⊢ head = unsublist p j
Tactic:
rw [←h, unsublist_pos_head]
Proof state after:
no goals
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
⊢ head = unsublist p j → ⋯ ▸ head = j
Tactic:
intro h
Proof state after:
case head.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
h : head = unsublist p j
⊢ ⋯ ▸ head = j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
h : head = unsublist p j
⊢ ⋯ ▸ head = j
Tactic:
rw [unsublist, dif_pos hx] at h
Proof state after:
case head.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
h :
  head =
    let_fun this := ⋯;
    match ⋯ ▸ j with
    | head => head
    | i.tail => (unsublist p i).tail
⊢ ⋯ ▸ head = j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
h :
  head =
    let_fun this := ⋯;
    match ⋯ ▸ j with
    | head => head
    | i.tail => (unsublist p i).tail
⊢ ⋯ ▸ head = j
Tactic:
split at h
Proof state after:
case head.mpr.h_1
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ j = head
h :
  head =
    let_fun this := ⋯;
    head
⊢ ⋯ ▸ head = j

case head.mpr.h_2
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h :
  head =
    let_fun this := ⋯;
    (unsublist p i✝).tail
⊢ ⋯ ▸ head = j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head.mpr.h_1
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ j = head
h :
  head =
    let_fun this := ⋯;
    head
⊢ ⋯ ▸ head = j

case head.mpr.h_2
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h :
  head =
    let_fun this := ⋯;
    (unsublist p i✝).tail
⊢ ⋯ ▸ head = j
Tactic:
next hh => rw [←hh, eqNdrec_symm]
Proof state after:
case head.mpr.h_2
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h :
  head =
    let_fun this := ⋯;
    (unsublist p i✝).tail
⊢ ⋯ ▸ head = j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case head.mpr.h_2
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h :
  head =
    let_fun this := ⋯;
    (unsublist p i✝).tail
⊢ ⋯ ▸ head = j
Tactic:
next => contradiction
Proof state after:
no goals
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
hh : ⋯ ▸ j = head
h :
  head =
    let_fun this := ⋯;
    head
⊢ ⋯ ▸ head = j
Tactic:
rw [←hh, eqNdrec_symm]
Proof state after:
no goals
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
hi : p head.val
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h :
  head =
    let_fun this := ⋯;
    (unsublist p i✝).tail
⊢ ⋯ ▸ head = j
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case tail
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
⊢ sublist p i.tail hi = j ↔ i.tail = unsublist p j
Tactic:
rw [sublist_pos_tail hx]
Proof state after:
case tail
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
⊢ ⋯ ▸ (sublist p i hi).tail = j ↔ i.tail = unsublist p j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case tail
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
⊢ ⋯ ▸ (sublist p i hi).tail = j ↔ i.tail = unsublist p j
Tactic:
constructor
Proof state after:
case tail.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
⊢ ⋯ ▸ (sublist p i hi).tail = j → i.tail = unsublist p j

case tail.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
⊢ i.tail = unsublist p j → ⋯ ▸ (sublist p i hi).tail = j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case tail.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
⊢ ⋯ ▸ (sublist p i hi).tail = j → i.tail = unsublist p j
Tactic:
intro h
Proof state after:
case tail.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h : ⋯ ▸ (sublist p i hi).tail = j
⊢ i.tail = unsublist p j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case tail.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h : ⋯ ▸ (sublist p i hi).tail = j
⊢ i.tail = unsublist p j
Tactic:
rw [←h, unsublist_pos_tail]
Proof state after:
case tail.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h : ⋯ ▸ (sublist p i hi).tail = j
⊢ i.tail = (unsublist p (sublist p i hi)).tail
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case tail.mp
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h : ⋯ ▸ (sublist p i hi).tail = j
⊢ i.tail = (unsublist p (sublist p i hi)).tail
Tactic:
apply congrArg
Proof state after:
case tail.mp.h
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h : ⋯ ▸ (sublist p i hi).tail = j
⊢ i = unsublist p (sublist p i hi)
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case tail.mp.h
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h : ⋯ ▸ (sublist p i hi).tail = j
⊢ i = unsublist p (sublist p i hi)
Tactic:
rw [←ih]
Proof state after:
no goals
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case tail.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
⊢ i.tail = unsublist p j → ⋯ ▸ (sublist p i hi).tail = j
Tactic:
intro h
Proof state after:
case tail.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h : i.tail = unsublist p j
⊢ ⋯ ▸ (sublist p i hi).tail = j
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof state before:
case tail.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h : i.tail = unsublist p j
⊢ ⋯ ▸ (sublist p i hi).tail = j
Tactic:
simp [unsublist, hx] at h
Proof state after:
case tail.mpr
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : xs.Index) (hi : p i.val) (j : (List.sublist p xs).Index), sublist p i hi = j ↔ i = unsublist p j
j : (List.sublist p (x :: xs)).Index
hx : p x
i : xs.Index
hi : p i.tail.val
h :
  i.tail =
    match ⋯ ▸ j with
    | head => head
    | i.tail => (unsublist p i).tail
⊢ ⋯ ▸ (sublist p i hi).tail = j