Theorem: List.Index.sublist_eq_iff_eq_unsublist (GMLInit/Data/Index/Sublist.lean)

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
State after:
no goals

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]
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

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
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

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
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

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]
State after:
no goals

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
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

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
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

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
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

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]
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

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
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

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
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

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
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

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]
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

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
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)

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]
State after:
no goals

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
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

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
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

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 =
    match ⋯ ▸ j with
    | head => head
    | i.tail => (unsublist p i).tail
⊢ ⋯ ▸ (sublist p i hi).tail = j
Tactic:
split at h
State after:
case tail.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
i : xs.Index
hi : p i.tail.val
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ j = head
h : i.tail = head
⊢ ⋯ ▸ (sublist p i hi).tail = j

case tail.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
i : xs.Index
hi : p i.tail.val
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h : i.tail = (unsublist p i✝).tail
⊢ ⋯ ▸ (sublist p i hi).tail = j

State before:
case tail.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
i : xs.Index
hi : p i.tail.val
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ j = head
h : i.tail = head
⊢ ⋯ ▸ (sublist p i hi).tail = j

case tail.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
i : xs.Index
hi : p i.tail.val
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h : i.tail = (unsublist p i✝).tail
⊢ ⋯ ▸ (sublist p i hi).tail = j
Tactic:
next => contradiction
State after:
case tail.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
i : xs.Index
hi : p i.tail.val
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h : i.tail = (unsublist p i✝).tail
⊢ ⋯ ▸ (sublist p i hi).tail = j

State before:
case tail.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
i : xs.Index
hi : p i.tail.val
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ j = i✝.tail
h : i.tail = (unsublist p i✝).tail
⊢ ⋯ ▸ (sublist p i hi).tail = j
Tactic:
next j ht =>
  cases h
  rw [eqNdrec_symm] at ht
  cases ht
  elim_casts
  apply congrArg
  rw [ih]
State after:
no goals

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
i : xs.Index
hi : p i.tail.val
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ j = head
h : i.tail = head
⊢ ⋯ ▸ (sublist p i hi).tail = j
Tactic:
contradiction
State after:
no goals

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
i : xs.Index
hi : p i.tail.val
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
ht : ⋯ ▸ j✝ = j.tail
h : i.tail = (unsublist p j).tail
⊢ ⋯ ▸ (sublist p i hi).tail = j✝
Tactic:
cases h
State after:
case refl
α : 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
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
ht : ⋯ ▸ j✝ = j.tail
hi : p (unsublist p j).tail.val
⊢ ⋯ ▸ (sublist p (unsublist p j) hi).tail = j✝

State before:
case refl
α : 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
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
ht : ⋯ ▸ j✝ = j.tail
hi : p (unsublist p j).tail.val
⊢ ⋯ ▸ (sublist p (unsublist p j) hi).tail = j✝
Tactic:
rw [eqNdrec_symm] at ht
State after:
case refl
α : 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
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
ht : j✝ = ⋯ ▸ j.tail
hi : p (unsublist p j).tail.val
⊢ ⋯ ▸ (sublist p (unsublist p j) hi).tail = j✝

State before:
case refl
α : 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
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
ht : j✝ = ⋯ ▸ j.tail
hi : p (unsublist p j).tail.val
⊢ ⋯ ▸ (sublist p (unsublist p j) hi).tail = j✝
Tactic:
cases ht
State after:
case refl.refl
α : 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
hx : p x
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
hi : p (unsublist p j).tail.val
⊢ ⋯ ▸ (sublist p (unsublist p j) hi).tail = ⋯ ▸ j.tail

State before:
case refl.refl
α : 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
hx : p x
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
hi : p (unsublist p j).tail.val
⊢ ⋯ ▸ (sublist p (unsublist p j) hi).tail = ⋯ ▸ j.tail
Tactic:
elim_casts
State after:
case refl.refl
α : 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
hx : p x
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
hi : p (unsublist p j).tail.val
⊢ (sublist p (unsublist p j) hi).tail = j.tail

State before:
case refl.refl
α : 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
hx : p x
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
hi : p (unsublist p j).tail.val
⊢ (sublist p (unsublist p j) hi).tail = j.tail
Tactic:
apply congrArg
State after:
case refl.refl.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
hx : p x
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
hi : p (unsublist p j).tail.val
⊢ sublist p (unsublist p j) hi = j

State before:
case refl.refl.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
hx : p x
x✝ : (⟨x, ⋯⟩ :: List.sublist p xs).Index
j : (List.sublist p xs).Index
hi : p (unsublist p j).tail.val
⊢ sublist p (unsublist p j) hi = j
Tactic:
rw [ih]
State after:
no goals

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:
absurd hx
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
⊢ p x

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
⊢ p x
Tactic:
exact hi
State after:
no goals

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_neg_tail hx]
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 = j ↔ i.tail = unsublist p j

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 = j ↔ i.tail = unsublist p j
Tactic:
constructor
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 = 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 = j

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 = j → i.tail = unsublist p j
Tactic:
intro heq
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
heq : ⋯ ▸ sublist p i hi = j
⊢ i.tail = unsublist p j

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
heq : ⋯ ▸ sublist p i hi = j
⊢ i.tail = unsublist p j
Tactic:
cases heq
State after:
case tail.mp.refl
α : 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
hx : ¬p x
i : xs.Index
hi : p i.tail.val
⊢ i.tail = unsublist p (⋯ ▸ sublist p i hi)

State before:
case tail.mp.refl
α : 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
hx : ¬p x
i : xs.Index
hi : p i.tail.val
⊢ i.tail = unsublist p (⋯ ▸ sublist p i hi)
Tactic:
rw [unsublist_neg_tail hx]
State after:
case tail.mp.refl
α : 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
hx : ¬p x
i : xs.Index
hi : p i.tail.val
⊢ i.tail = (unsublist p (sublist p i hi)).tail

State before:
case tail.mp.refl
α : 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
hx : ¬p x
i : xs.Index
hi : p i.tail.val
⊢ i.tail = (unsublist p (sublist p i hi)).tail
Tactic:
apply congrArg
State after:
case tail.mp.refl.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
hx : ¬p x
i : xs.Index
hi : p i.tail.val
⊢ i = unsublist p (sublist p i hi)

State before:
case tail.mp.refl.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
hx : ¬p x
i : xs.Index
hi : p i.tail.val
⊢ i = unsublist p (sublist p i hi)
Tactic:
rw [←ih]
State after:
no goals

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 = j
Tactic:
intro heq
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
heq : i.tail = unsublist p j
⊢ ⋯ ▸ sublist p i hi = j

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
heq : i.tail = unsublist p j
⊢ ⋯ ▸ sublist p i hi = j
Tactic:
simp [unsublist, hx] at heq
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
heq : i = unsublist p (⋯ ▸ j)
⊢ ⋯ ▸ sublist p i hi = j

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
heq : i = unsublist p (⋯ ▸ j)
⊢ ⋯ ▸ sublist p i hi = j
Tactic:
cases heq
State after:
case tail.mpr.refl
α : 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 (unsublist p (⋯ ▸ j)).tail.val
⊢ ⋯ ▸ sublist p (unsublist p (⋯ ▸ j)) hi = j

State before:
case tail.mpr.refl
α : 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 (unsublist p (⋯ ▸ j)).tail.val
⊢ ⋯ ▸ sublist p (unsublist p (⋯ ▸ j)) hi = j
Tactic:
rw [eqNdrec_symm]
State after:
case tail.mpr.refl
α : 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 (unsublist p (⋯ ▸ j)).tail.val
⊢ sublist p (unsublist p (⋯ ▸ j)) hi = ⋯ ▸ j

State before:
case tail.mpr.refl
α : 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 (unsublist p (⋯ ▸ j)).tail.val
⊢ sublist p (unsublist p (⋯ ▸ j)) hi = ⋯ ▸ j
Tactic:
rw [ih]
State after:
no goals