internlm/Lean-Github huggingface dataset:
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 =
    match ⋯ ▸ j with
    | head => head
    | i.tail => (unsublist p i).tail
⊢ ⋯ ▸ (sublist p i hi).tail = j
Tactic:
split at h
Proof 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
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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
Proof 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
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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]
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
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
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
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
Proof 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✝
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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
Proof 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✝
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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
Proof 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
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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
Proof 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
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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
Proof 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
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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]
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:
absurd 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
⊢ p x
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
⊢ p x
Tactic:
exact hi
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_neg_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 = 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 = 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 = 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
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 = j → i.tail = unsublist p j
Tactic:
intro heq
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
heq : ⋯ ▸ sublist p i hi = 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
heq : ⋯ ▸ sublist p i hi = j
⊢ i.tail = unsublist p j
Tactic:
cases heq
Proof 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)
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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]
Proof 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
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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
Proof 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)
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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]
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 = j
Tactic:
intro heq
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
heq : i.tail = unsublist p j
⊢ ⋯ ▸ sublist p i hi = 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
heq : i.tail = unsublist p j
⊢ ⋯ ▸ sublist p i hi = j
Tactic:
simp [unsublist, hx] at heq
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
heq : i = unsublist p (⋯ ▸ j)
⊢ ⋯ ▸ sublist p i hi = 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
heq : i = unsublist p (⋯ ▸ j)
⊢ ⋯ ▸ sublist p i hi = j
Tactic:
cases heq
Proof 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
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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]
Proof 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
Theorem: List.Index.sublist_eq_iff_eq_unsublist
Proof 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]
Proof state after:
no goals
Theorem: List.Index.unsublist_sublist
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
i : xs.Index
hi : p i.val
⊢ unsublist p (sublist p i hi) = i
Tactic:
induction i with
| head =>
  rw [sublist_pos_head]
  rw [unsublist_pos_head]
| @tail xs x i ih =>
  by_cases p x with
  | isTrue hh =>
    rw [sublist_pos_tail hh]
    rw [unsublist_pos_tail hh]
    rw [ih]
  | isFalse hh =>
    rw [sublist_neg_tail hh]
    rw [unsublist_neg_tail hh]
    rw [ih]
Proof state after:
no goals
Theorem: List.Index.unsublist_sublist
Proof state before:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x✝ : α
xs✝ : List α
hi : p head.val
⊢ unsublist p (sublist p head hi) = head
Tactic:
rw [sublist_pos_head]
Proof state after:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x✝ : α
xs✝ : List α
hi : p head.val
⊢ unsublist p (⋯ ▸ head) = head
Theorem: List.Index.unsublist_sublist
Proof state before:
case head
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x✝ : α
xs✝ : List α
hi : p head.val
⊢ unsublist p (⋯ ▸ head) = head
Tactic:
rw [unsublist_pos_head]
Proof state after:
no goals
Theorem: List.Index.unsublist_sublist
Proof state before:
case tail
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
⊢ unsublist p (sublist p i.tail hi) = i.tail
Tactic:
by_cases p x with
| isTrue hh =>
  rw [sublist_pos_tail hh]
  rw [unsublist_pos_tail hh]
  rw [ih]
| isFalse hh =>
  rw [sublist_neg_tail hh]
  rw [unsublist_neg_tail hh]
  rw [ih]
Proof state after:
no goals
Theorem: List.Index.unsublist_sublist
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ unsublist p (sublist p i.tail hi) = i.tail
Tactic:
rw [sublist_pos_tail hh]
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ unsublist p (⋯ ▸ (sublist p i hi).tail) = i.tail
Theorem: List.Index.unsublist_sublist
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ unsublist p (⋯ ▸ (sublist p i hi).tail) = i.tail
Tactic:
rw [unsublist_pos_tail hh]
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ (unsublist p (sublist p i hi)).tail = i.tail
Theorem: List.Index.unsublist_sublist
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : p x
⊢ (unsublist p (sublist p i hi)).tail = i.tail
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: List.Index.unsublist_sublist
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : ¬p x
⊢ unsublist p (sublist p i.tail hi) = i.tail
Tactic:
rw [sublist_neg_tail hh]
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs✝ xs : List α
x : α
i : xs.Index
ih : ∀ (hi : p i.val), unsublist p (sublist p i hi) = i
hi : p i.tail.val
hh : ¬p x
⊢ unsublist p (⋯ ▸ sublist p i hi) = i.tail