internlm/Lean-Github huggingface dataset:
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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]
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof 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]
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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]
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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)]
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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 ..
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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]
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof 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]
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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✝
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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✝
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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)
Theorem: List.Index.dedup_eq_of_rel
Proof 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))
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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]
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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]
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof 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]
Proof 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
Theorem: List.Index.dedup_eq_of_rel
Proof 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
Proof 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