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

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ dedup s i = j ↔ Setoid.r i.val j.val
Tactic:
constructor
State after:
case mp
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ dedup s i = j → Setoid.r i.val j.val

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

State before:
case mp
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ dedup s i = j → Setoid.r i.val j.val
Tactic:
intro | rfl => exact val_dedup ..
State after:
no goals

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

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