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

State before:
case nil
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs : List α
i : [].Index
j : (List.dedup s []).Index
h : Setoid.r i.val j.val
⊢ dedup s i = j
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r head.val j.val
⊢ dedup s head = j
Tactic:
rw [val_head] at h
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
⊢ dedup s head = j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
⊢ dedup s head = j
Tactic:
rw [dedup]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
⊢ (if h : Logic.Any (List.map (Setoid.r x) xs) then
      let_fun this := ⋯;
      ⋯ ▸ dedup s (unmap (Setoid.r x) h.get)
    else
      let_fun this := ⋯;
      ⋯ ▸ head) =
    j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
⊢ (if h : Logic.Any (List.map (Setoid.r x) xs) then
      let_fun this := ⋯;
      ⋯ ▸ dedup s (unmap (Setoid.r x) h.get)
    else
      let_fun this := ⋯;
      ⋯ ▸ head) =
    j
Tactic:
split
State after:
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ dedup s (unmap (Setoid.r x) h✝.get)) =
    j

case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ head) =
    j

State before:
case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ head) =
    j
Tactic:
next ha =>
  have : (x :: xs).dedup s = x :: xs.dedup s := if_neg ha
  rw [eqNdrec_symm]
  match hj : this ▸ j with
  | head =>
    rw [←hj]
  | tail j =>
    rw [eqNdrec_symm] at hj
    rw [hj, val_ndrec, val_tail] at h
    absurd ha
    apply Logic.Any.of_index ((j.undedup s).map (s.r x))
    rw [val_map, val_undedup]
    exact h
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ dedup s (unmap (Setoid.r x) ha.get)) =
    j
Tactic:
rw [eqNdrec_symm]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s (unmap (Setoid.r x) ha.get) = ⋯ ▸ j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s (unmap (Setoid.r x) ha.get) = ⋯ ▸ j
Tactic:
apply ih
State after:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) ha.get).val (⋯ ▸ j).val

State before:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) ha.get).val (⋯ ▸ j).val
Tactic:
rw [val_ndrec]
State after:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) ha.get).val j.val

State before:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) ha.get).val j.val
Tactic:
transitivity x
State after:
case h.left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) ha.get).val x

case h.right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r x j.val

State before:
case h.left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) ha.get).val x
Tactic:
symmetry
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r x (unmap (Setoid.r x) ha.get).val

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r x (unmap (Setoid.r x) ha.get).val
Tactic:
rw [←val_unmap (s.r x)]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ ha.get.val

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ ha.get.val
Tactic:
exact Logic.Any.get_prop ..
State after:
no goals

State before:
case h.right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r x j.val
Tactic:
exact h
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ head) =
    j
Tactic:
have : (x :: xs).dedup s = x :: xs.dedup s := if_neg ha
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (let_fun this := ⋯;
    ⋯ ▸ head) =
    j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (let_fun this := ⋯;
    ⋯ ▸ head) =
    j
Tactic:
rw [eqNdrec_symm]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ head = ⋯ ▸ j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ head = ⋯ ▸ j
Tactic:
match hj : this ▸ j with
| head =>
  rw [←hj]
| tail j =>
  rw [eqNdrec_symm] at hj
  rw [hj, val_ndrec, val_tail] at h
  absurd ha
  apply Logic.Any.of_index ((j.undedup s).map (s.r x))
  rw [val_map, val_undedup]
  exact h
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
h : Setoid.r x j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
hj : this ▸ j = head
⊢ head = ⋯ ▸ j
Tactic:
rw [←hj]
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
h : Setoid.r x j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : this ▸ j✝ = j.tail
⊢ head = ⋯ ▸ j✝
Tactic:
rw [eqNdrec_symm] at hj
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
h : Setoid.r x j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : j✝ = ⋯ ▸ j.tail
⊢ head = ⋯ ▸ j✝

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
h : Setoid.r x j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : j✝ = ⋯ ▸ j.tail
⊢ head = ⋯ ▸ j✝
Tactic:
rw [hj, val_ndrec, val_tail] at h
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r x j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ head = ⋯ ▸ j✝

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r x j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ head = ⋯ ▸ j✝
Tactic:
absurd ha
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r x j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ Logic.Any (List.map (Setoid.r x) xs)

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r x j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ Logic.Any (List.map (Setoid.r x) xs)
Tactic:
apply Logic.Any.of_index ((j.undedup s).map (s.r x))
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r x j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ (map (Setoid.r x) (undedup s j)).val

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r x j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ (map (Setoid.r x) (undedup s j)).val
Tactic:
rw [val_map, val_undedup]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r x j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ Setoid.r x j.val

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r x j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ Setoid.r x j.val
Tactic:
exact h
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.tail.val j.val
⊢ dedup s i.tail = j
Tactic:
rw [val_tail] at h
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
⊢ dedup s i.tail = j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
⊢ dedup s i.tail = j
Tactic:
rw [dedup]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
⊢ (if h : Logic.Any (List.map (Setoid.r x) xs) then
      let_fun this := ⋯;
      ⋯ ▸ dedup s i
    else
      let_fun this := ⋯;
      ⋯ ▸ (dedup s i).tail) =
    j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
⊢ (if h : Logic.Any (List.map (Setoid.r x) xs) then
      let_fun this := ⋯;
      ⋯ ▸ dedup s i
    else
      let_fun this := ⋯;
      ⋯ ▸ (dedup s i).tail) =
    j
Tactic:
split
State after:
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ dedup s i) =
    j

case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j

State before:
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ dedup s i) =
    j

case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j
Tactic:
next ha =>
  rw [eqNdrec_symm]
  apply ih
  rw [val_ndrec]
  exact h
State after:
case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j

State before:
case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j
Tactic:
next ha =>
  have : (x :: xs).dedup s = x :: xs.dedup s := if_neg ha
  rw [eqNdrec_symm]
  match hj : this ▸ j with
  | head =>
    rw [eqNdrec_symm] at hj
    rw [hj, val_ndrec, val_head] at h
    absurd ha
    apply Logic.Any.of_index (i.map (s.r x))
    rw [val_map]
    symmetry
    exact h
  | tail j =>
    rw [eqNdrec_symm] at hj
    rw [hj, val_ndrec, val_tail] at h
    rw [hj, ih h]
    elim_casts
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ dedup s i) =
    j
Tactic:
rw [eqNdrec_symm]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s i = ⋯ ▸ j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s i = ⋯ ▸ j
Tactic:
apply ih
State after:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.val (⋯ ▸ j).val

State before:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.val (⋯ ▸ j).val
Tactic:
rw [val_ndrec]
State after:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.val j.val

State before:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.val j.val
Tactic:
exact h
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j
Tactic:
have : (x :: xs).dedup s = x :: xs.dedup s := if_neg ha
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j
Tactic:
rw [eqNdrec_symm]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (dedup s i).tail = ⋯ ▸ j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (dedup s i).tail = ⋯ ▸ j
Tactic:
match hj : this ▸ j with
| head =>
  rw [eqNdrec_symm] at hj
  rw [hj, val_ndrec, val_head] at h
  absurd ha
  apply Logic.Any.of_index (i.map (s.r x))
  rw [val_map]
  symmetry
  exact h
| tail j =>
  rw [eqNdrec_symm] at hj
  rw [hj, val_ndrec, val_tail] at h
  rw [hj, ih h]
  elim_casts
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
hj : this ▸ j = head
⊢ (dedup s i).tail = ⋯ ▸ j
Tactic:
rw [eqNdrec_symm] at hj
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
hj : j = ⋯ ▸ head
⊢ (dedup s i).tail = ⋯ ▸ j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
hj : j = ⋯ ▸ head
⊢ (dedup s i).tail = ⋯ ▸ j
Tactic:
rw [hj, val_ndrec, val_head] at h
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ (dedup s i).tail = ⋯ ▸ j

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ (dedup s i).tail = ⋯ ▸ j
Tactic:
absurd ha
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Logic.Any (List.map (Setoid.r x) xs)

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Logic.Any (List.map (Setoid.r x) xs)
Tactic:
apply Logic.Any.of_index (i.map (s.r x))
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ (map (Setoid.r x) i).val

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ (map (Setoid.r x) i).val
Tactic:
rw [val_map]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Setoid.r x i.val

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Setoid.r x i.val
Tactic:
symmetry
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Setoid.r i.val x

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Setoid.r i.val x
Tactic:
exact h
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : this ▸ j✝ = j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝
Tactic:
rw [eqNdrec_symm] at hj
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : j✝ = ⋯ ▸ j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : j✝ = ⋯ ▸ j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝
Tactic:
rw [hj, val_ndrec, val_tail] at h
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r i.val j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r i.val j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝
Tactic:
rw [hj, ih h]
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r i.val j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ j.tail = ⋯ ▸ ⋯ ▸ j.tail

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r i.val j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ j.tail = ⋯ ▸ ⋯ ▸ j.tail
Tactic:
elim_casts
State after:
no goals