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

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
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), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
⊢ (undedup s i).val = i.val
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), (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

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

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]
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), (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
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

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

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

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

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 ..
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), (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
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

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

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]
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), (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
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

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]
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), (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
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

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