internlm/Lean-Github huggingface dataset:
Theorem: List.Index.val_dedup
Proof state before:
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ dedup s i).val

case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ (dedup s i).tail).val
Tactic:
next => rw [val_ndrec]; exact ih ..
Proof state after:
case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ (dedup s i).tail).val
Theorem: List.Index.val_dedup
Proof state before:
case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ (dedup s i).tail).val
Tactic:
next => rw [val_ndrec]; exact ih ..
Proof state after:
no goals
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ dedup s i).val
Tactic:
rw [val_ndrec]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val (dedup s i).val
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val (dedup s i).val
Tactic:
exact ih ..
Proof state after:
no goals
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ (dedup s i).tail).val
Tactic:
rw [val_ndrec]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val (dedup s i).tail.val
Theorem: List.Index.val_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val (dedup s i).tail.val
Tactic:
exact ih ..
Proof state after:
no goals
Theorem: List.Index.val_undedup
Proof state before:
case nil
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs : List α
i : (List.dedup s []).Index
⊢ (undedup s i).val = i.val
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.val_undedup
Proof state before:
case cons
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
⊢ (undedup s i).val = i.val
Tactic:
simp only [undedup]
Proof state after:
case cons
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
⊢ (if h : Logic.Any (List.map (Setoid.r x) xs) then (undedup s (⋯ ▸ i)).tail
      else
        match ⋯ ▸ i with
        | head => head
        | i.tail => (undedup s i).tail).val =
    i.val
Theorem: List.Index.val_undedup
Proof state before:
case cons
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
⊢ (if h : Logic.Any (List.map (Setoid.r x) xs) then (undedup s (⋯ ▸ i)).tail
      else
        match ⋯ ▸ i with
        | head => head
        | i.tail => (undedup s i).tail).val =
    i.val
Tactic:
split
Proof state after:
case cons.isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ (undedup s (⋯ ▸ i)).tail.val = i.val

case cons.isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail).val =
    i.val
Theorem: List.Index.val_undedup
Proof state before:
case cons.isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail).val =
    i.val
Tactic:
next ha =>
  split
  next h =>
    rw [eqNdrec_symm] at h
    rw [h, val_ndrec]
  next h =>
    rw [eqNdrec_symm] at h
    rw [h, val_ndrec, val_tail, val_tail, ih]
Proof state after:
no goals
Theorem: List.Index.val_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ (undedup s (⋯ ▸ i)).tail.val = i.val
Tactic:
have : (x :: xs).dedup s = xs.dedup s := if_pos ha
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (undedup s (⋯ ▸ i)).tail.val = i.val
Theorem: List.Index.val_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (undedup s (⋯ ▸ i)).tail.val = i.val
Tactic:
rw [val_tail]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (undedup s (⋯ ▸ i)).val = i.val
Theorem: List.Index.val_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (undedup s (⋯ ▸ i)).val = i.val
Tactic:
transitivity (this ▸ i).val
Proof state after:
case left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (undedup s (⋯ ▸ i)).val = (this ▸ i).val

case right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (this ▸ i).val = i.val
Theorem: List.Index.val_undedup
Proof state before:
case left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (undedup s (⋯ ▸ i)).val = (this ▸ i).val
Tactic:
exact ih ..
Proof state after:
no goals
Theorem: List.Index.val_undedup
Proof state before:
case right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (this ▸ i).val = i.val
Tactic:
exact val_ndrec ..
Proof state after:
no goals
Theorem: List.Index.val_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail).val =
    i.val
Tactic:
split
Proof state after:
case h_1
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
heq✝ : ⋯ ▸ i = head
⊢ head.val = i.val

case h_2
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ (undedup s i✝).tail.val = i.val
Theorem: List.Index.val_undedup
Proof state before:
case h_1
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
heq✝ : ⋯ ▸ i = head
⊢ head.val = i.val

case h_2
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ (undedup s i✝).tail.val = i.val
Tactic:
next h =>
  rw [eqNdrec_symm] at h
  rw [h, val_ndrec]
Proof state after:
case h_2
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ (undedup s i✝).tail.val = i.val
Theorem: List.Index.val_undedup
Proof state before:
case h_2
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ (undedup s i✝).tail.val = i.val
Tactic:
next h =>
  rw [eqNdrec_symm] at h
  rw [h, val_ndrec, val_tail, val_tail, ih]
Proof state after:
no goals
Theorem: List.Index.val_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
h : ⋯ ▸ i = head
⊢ head.val = i.val
Tactic:
rw [eqNdrec_symm] at h
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
h : i = ⋯ ▸ head
⊢ head.val = i.val
Theorem: List.Index.val_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
h : i = ⋯ ▸ head
⊢ head.val = i.val
Tactic:
rw [h, val_ndrec]
Proof state after:
no goals
Theorem: List.Index.val_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
h : ⋯ ▸ i = i✝.tail
⊢ (undedup s i✝).tail.val = i.val
Tactic:
rw [eqNdrec_symm] at h
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
h : i = ⋯ ▸ i✝.tail
⊢ (undedup s i✝).tail.val = i.val
Theorem: List.Index.val_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
h : i = ⋯ ▸ i✝.tail
⊢ (undedup s i✝).tail.val = i.val
Tactic:
rw [h, val_ndrec, val_tail, val_tail, ih]
Proof state after:
no goals
Theorem: List.Index.dedup_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : (List.dedup s xs).Index
⊢ dedup s (undedup s i) = i
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  simp only [undedup]
  split
  next ha => rw [dedup, dif_pos ha, ih, eqNdrec_symm]
  next ha =>
    split
    next h => rw [dedup, dif_neg ha, eqNdrec_symm, ←h]
    next h => rw [dedup, dif_neg ha, eqNdrec_symm, ih, ←h]
Proof state after:
no goals
Theorem: List.Index.dedup_undedup
Proof state before:
case nil
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs : List α
i : (List.dedup s []).Index
⊢ dedup s (undedup s i) = i
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.dedup_undedup
Proof state before:
case cons
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
⊢ dedup s (undedup s i) = i
Tactic:
simp only [undedup]
Proof state after:
case cons
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
⊢ dedup s
      (if h : Logic.Any (List.map (Setoid.r x) xs) then (undedup s (⋯ ▸ i)).tail
      else
        match ⋯ ▸ i with
        | head => head
        | i.tail => (undedup s i).tail) =
    i
Theorem: List.Index.dedup_undedup
Proof state before:
case cons
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
⊢ dedup s
      (if h : Logic.Any (List.map (Setoid.r x) xs) then (undedup s (⋯ ▸ i)).tail
      else
        match ⋯ ▸ i with
        | head => head
        | i.tail => (undedup s i).tail) =
    i
Tactic:
split
Proof state after:
case cons.isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s (undedup s (⋯ ▸ i)).tail = i

case cons.isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s
      (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail) =
    i
Theorem: List.Index.dedup_undedup
Proof state before:
case cons.isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s (undedup s (⋯ ▸ i)).tail = i

case cons.isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s
      (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail) =
    i
Tactic:
next ha => rw [dedup, dif_pos ha, ih, eqNdrec_symm]
Proof state after:
case cons.isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s
      (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail) =
    i
Theorem: List.Index.dedup_undedup
Proof state before:
case cons.isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s
      (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail) =
    i
Tactic:
next ha =>
  split
  next h => rw [dedup, dif_neg ha, eqNdrec_symm, ←h]
  next h => rw [dedup, dif_neg ha, eqNdrec_symm, ih, ←h]
Proof state after:
no goals
Theorem: List.Index.dedup_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s (undedup s (⋯ ▸ i)).tail = i
Tactic:
rw [dedup, dif_pos ha, ih, eqNdrec_symm]
Proof state after:
no goals
Theorem: List.Index.dedup_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s
      (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail) =
    i
Tactic:
split
Proof state after:
case h_1
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
heq✝ : ⋯ ▸ i = head
⊢ dedup s head = i

case h_2
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ dedup s (undedup s i✝).tail = i
Theorem: List.Index.dedup_undedup
Proof state before:
case h_1
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
heq✝ : ⋯ ▸ i = head
⊢ dedup s head = i

case h_2
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ dedup s (undedup s i✝).tail = i
Tactic:
next h => rw [dedup, dif_neg ha, eqNdrec_symm, ←h]
Proof state after:
case h_2
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ dedup s (undedup s i✝).tail = i
Theorem: List.Index.dedup_undedup
Proof state before:
case h_2
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ dedup s (undedup s i✝).tail = i
Tactic:
next h => rw [dedup, dif_neg ha, eqNdrec_symm, ih, ←h]
Proof state after:
no goals
Theorem: List.Index.dedup_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
h : ⋯ ▸ i = head
⊢ dedup s head = i
Tactic:
rw [dedup, dif_neg ha, eqNdrec_symm, ←h]
Proof state after:
no goals
Theorem: List.Index.dedup_undedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
h : ⋯ ▸ i = i✝.tail
⊢ dedup s (undedup s i✝).tail = i
Tactic:
rw [dedup, dif_neg ha, eqNdrec_symm, ih, ←h]
Proof state after:
no goals
Theorem: List.Index.undedup_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
⊢ Setoid.r (undedup s (dedup s i)).val i.val
Tactic:
symmetry
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
⊢ Setoid.r i.val (undedup s (dedup s i)).val
Theorem: List.Index.undedup_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
⊢ Setoid.r i.val (undedup s (dedup s i)).val
Tactic:
rw [val_undedup]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
⊢ Setoid.r i.val (dedup s i).val
Theorem: List.Index.undedup_dedup
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
⊢ Setoid.r i.val (dedup s i).val
Tactic:
exact val_dedup ..
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
case nil
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs : List α
i : [].Index
j : (List.dedup s []).Index
h : Setoid.r i.val j.val
⊢ dedup s i = j
Tactic:
contradiction
Proof state after:
no goals