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

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ dedup s i = dedup s j
Tactic:
apply dedup_eq_of_rel
State after:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val (dedup s j).val

State before:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val (dedup s j).val
Tactic:
transitivity j.val
State after:
case h.left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val j.val

case h.right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r j.val (dedup s j).val

State before:
case h.left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val j.val
Tactic:
exact h
State after:
no goals

State before:
case h.right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r j.val (dedup s j).val
Tactic:
exact val_dedup ..
State after:
no goals