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

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

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

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