Theorem: List.Index.dedup_undedup (GMLInit/Data/Index/Dedup.lean)

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

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

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

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

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

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

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

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

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

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

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

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