internlm/Lean-Github huggingface dataset:
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) = i.tail
Tactic:
rw [unsublist_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)).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.sublist_unsublist
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
i : (List.sublist p xs).Index
hi : p (unsublist p i).val
⊢ sublist p (unsublist p i) hi = i
Tactic:
rw [sublist_eq_iff_eq_unsublist]
Proof state after:
no goals
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
i : (List.sublist p xs).Index
⊢ (unsublist p i).val = i.val.val
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  by_cases p x with
  | isTrue hx =>
    unfold unsublist
    rw [dif_pos hx]
    split
    next h =>
      rw [eqNdrec_symm] at h
      cases h
      rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
    next h =>
      rw [eqNdrec_symm] at h
      cases h
      rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
      rw [val_tail, val_tail]
      apply ih
  | isFalse hx =>
    unfold unsublist
    rw [dif_neg hx]
    rw [val_tail]
    rw [ih]
    apply congrArg
    rw [val_ndrec]
Proof state after:
no goals
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
case nil
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
i : (List.sublist p []).Index
⊢ (unsublist p i).val = i.val.val
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
case cons
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
⊢ (unsublist p i).val = i.val.val
Tactic:
by_cases p x with
| isTrue hx =>
  unfold unsublist
  rw [dif_pos hx]
  split
  next h =>
    rw [eqNdrec_symm] at h
    cases h
    rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
  next h =>
    rw [eqNdrec_symm] at h
    cases h
    rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
    rw [val_tail, val_tail]
    apply ih
| isFalse hx =>
  unfold unsublist
  rw [dif_neg hx]
  rw [val_tail]
  rw [ih]
  apply congrArg
  rw [val_ndrec]
Proof state after:
no goals
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
⊢ (unsublist p i).val = i.val.val
Tactic:
unfold unsublist
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
⊢ (if hh : p x then
        let_fun this := ⋯;
        match ⋯ ▸ i with
        | head => head
        | i.tail => (unsublist p i).tail
      else
        let_fun this := ⋯;
        (unsublist p (this ▸ i)).tail).val =
    i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
⊢ (if hh : p x then
        let_fun this := ⋯;
        match ⋯ ▸ i with
        | head => head
        | i.tail => (unsublist p i).tail
      else
        let_fun this := ⋯;
        (unsublist p (this ▸ i)).tail).val =
    i.val.val
Tactic:
rw [dif_pos hx]
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
⊢ (let_fun this := ⋯;
      match ⋯ ▸ i with
      | head => head
      | i.tail => (unsublist p i).tail).val =
    i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
⊢ (let_fun this := ⋯;
      match ⋯ ▸ i with
      | head => head
      | i.tail => (unsublist p i).tail).val =
    i.val.val
Tactic:
split
Proof state after:
case h_1
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ i = head
⊢ (let_fun this := ⋯;
      head).val =
    i.val.val

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

case h_2
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i.val.val
Tactic:
next h =>
  rw [eqNdrec_symm] at h
  cases h
  rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
Proof state after:
case h_2
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
case h_2
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i.val.val
Tactic:
next h =>
  rw [eqNdrec_symm] at h
  cases h
  rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
  rw [val_tail, val_tail]
  apply ih
Proof state after:
no goals
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
h : ⋯ ▸ i = head
⊢ (let_fun this := ⋯;
      head).val =
    i.val.val
Tactic:
rw [eqNdrec_symm] at h
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
h : i = ⋯ ▸ head
⊢ (let_fun this := ⋯;
      head).val =
    i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
h : i = ⋯ ▸ head
⊢ (let_fun this := ⋯;
      head).val =
    i.val.val
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 : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
⊢ (let_fun this := ⋯;
      head).val =
    (⋯ ▸ head).val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
case refl
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
⊢ (let_fun this := ⋯;
      head).val =
    (⋯ ▸ head).val.val
Tactic:
rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
Proof state after:
no goals
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
h : ⋯ ▸ i = i✝.tail
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i.val.val
Tactic:
rw [eqNdrec_symm] at h
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
h : i = ⋯ ▸ i✝.tail
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
h : i = ⋯ ▸ i✝.tail
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i.val.val
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 : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    (⋯ ▸ i✝.tail).val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
case refl
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    (⋯ ▸ i✝.tail).val.val
Tactic:
rw [val_ndrec _ (List.sublist_pos hx).symm.symm.symm]
Proof state after:
case refl
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i✝.tail.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
case refl
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
⊢ (let_fun this := ⋯;
      (unsublist p i✝).tail).val =
    i✝.tail.val.val
Tactic:
rw [val_tail, val_tail]
Proof state after:
case refl
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
⊢ (unsublist p i✝).val = i✝.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
case refl
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
hx : p x
x✝ : (⟨x, hx⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
⊢ (unsublist p i✝).val = i✝.val.val
Tactic:
apply ih
Proof state after:
no goals
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (unsublist p i).val = i.val.val
Tactic:
unfold unsublist
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (if hh : p x then
        let_fun this := ⋯;
        match ⋯ ▸ i with
        | head => head
        | i.tail => (unsublist p i).tail
      else
        let_fun this := ⋯;
        (unsublist p (this ▸ i)).tail).val =
    i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (if hh : p x then
        let_fun this := ⋯;
        match ⋯ ▸ i with
        | head => head
        | i.tail => (unsublist p i).tail
      else
        let_fun this := ⋯;
        (unsublist p (this ▸ i)).tail).val =
    i.val.val
Tactic:
rw [dif_neg hx]
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (let_fun this := ⋯;
      (unsublist p (this ▸ i)).tail).val =
    i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (let_fun this := ⋯;
      (unsublist p (this ▸ i)).tail).val =
    i.val.val
Tactic:
rw [val_tail]
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (unsublist p (⋯ ▸ i)).val = i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (unsublist p (⋯ ▸ i)).val = i.val.val
Tactic:
rw [ih]
Proof state after:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (⋯ ▸ i).val.val = i.val.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (⋯ ▸ i).val.val = i.val.val
Tactic:
apply congrArg
Proof state after:
case h
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (⋯ ▸ i).val = i.val
Theorem: List.Index.val_unsublist_eq_val_val
Proof state before:
case h
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : ∀ (i : (List.sublist p xs).Index), (unsublist p i).val = i.val.val
i : (List.sublist p (x :: xs)).Index
hx : ¬p x
⊢ (⋯ ▸ i).val = i.val
Tactic:
rw [val_ndrec]
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ (IndView.pure x).toList1 = List1.cons y [] ↔ (List1.cons y []).toIndView = IndView.pure x
Tactic:
unfold IndView.toList1 toIndView
Proof state after:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] ↔ IndView.pure y = IndView.pure x
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] ↔ IndView.pure y = IndView.pure x
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] → IndView.pure y = IndView.pure x

case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ IndView.pure y = IndView.pure x → List1.cons x [] = List1.cons y []
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] → IndView.pure y = IndView.pure x
Tactic:
intro | rfl => rfl
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
x✝ : List1.cons x [] = List1.cons y []
⊢ IndView.pure x = IndView.pure x
Tactic:
rfl
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ IndView.pure y = IndView.pure x → List1.cons x [] = List1.cons y []
Tactic:
intro | rfl => rfl
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
x✝ : IndView.pure y = IndView.pure x
⊢ List1.cons y [] = List1.cons y []
Tactic:
rfl
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ (IndView.pure x).toList1 = List1.cons y (head✝ :: tail✝) ↔ (List1.cons y (head✝ :: tail✝)).toIndView = IndView.pure x
Tactic:
unfold IndView.toList1 toIndView
Proof state after:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝) ↔ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝) ↔ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝) → IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x

case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x → List1.cons x [] = List1.cons y (head✝ :: tail✝)
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝) → IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
h : List1.cons x [] = List1.cons y (head✝ :: tail✝)
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
h : List1.cons x [] = List1.cons y (head✝ :: tail✝)
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
injection h with h
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
h : [x] = y :: head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
h : [x] = y :: head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
injection h with hh ht
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
hh : x = y
ht : [] = head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
hh : x = y
ht : [] = head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
contradiction
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x → List1.cons x [] = List1.cons y (head✝ :: tail✝)
Tactic:
intro
Proof state after:
case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
a✝ : IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝)
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
a✝ : IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝)
Tactic:
contradiction
Proof state after:
no goals