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

State before:
case nil
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs : List α
i : [].Index
⊢ Setoid.r i.val (dedup s i).val
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), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
⊢ Setoid.r head.val (dedup s head).val
Tactic:
unfold dedup
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
⊢ Setoid.r head.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).val

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
⊢ Setoid.r head.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).val
Tactic:
split
State after:
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val
    (let_fun this := ⋯;
      ⋯ ▸ dedup s (unmap (Setoid.r x) h✝.get)).val

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

State before:
case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val
    (let_fun this := ⋯;
      ⋯ ▸ head).val
Tactic:
next => rw [val_ndrec]; reflexivity using s.r
State after:
no goals

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

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

case right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r (unmap (Setoid.r x) h.get).val (dedup s (unmap (Setoid.r x) h.get)).val

State before:
case left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val (unmap (Setoid.r x) h.get).val
Tactic:
rw [val_head, ←val_unmap (s.r x)]
State after:
case left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h : Logic.Any (List.map (Setoid.r x) xs)
⊢ h.get.val

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

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

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

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val head.val
Tactic:
reflexivity using s.r
State after:
no goals

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
⊢ Setoid.r i.tail.val (dedup s i.tail).val
Tactic:
unfold dedup
State after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
⊢ Setoid.r i.tail.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).val

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
⊢ Setoid.r i.tail.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).val
Tactic:
split
State after:
case isTrue
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val
    (let_fun this := ⋯;
      ⋯ ▸ dedup s i).val

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

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

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

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

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

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

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

State before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i✝ : (x :: xs).Index
i : xs.Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.tail.val (dedup s i).tail.val
Tactic:
exact ih ..
State after:
no goals