awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih :
  LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (kerase (β := β) x ys) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) ys :
      ℕ)
h : x = y.fst (β := β)
⊢ LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (kerase (β := β) x (y :: ys)) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) (y :: ys) :
      ℕ)

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih :
  LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (kerase (β := β) x ys) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) ys :
      ℕ)
h : ¬x = y.fst (β := β)
⊢ LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (kerase (β := β) x (y :: ys)) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) (y :: ys) :
      ℕ)

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
x : α
xs : List (Sigma β)
nil :
  LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (kerase (β := β) x []) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) [] :
      ℕ)
cons :
  ∀ (y : Sigma β) (ys : List (Sigma β)),
    LE.le (α := ℕ)
        (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
            (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
            (kerase (β := β) x ys) :
          ℕ)
        (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
            (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) ys :
          ℕ) →
      LE.le (α := ℕ)
        (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
            (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
            (kerase (β := β) x (y :: ys)) :
          ℕ)
        (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
            (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) (y :: ys) :
          ℕ)
⊢ LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (kerase (β := β) x xs) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) xs :
      ℕ)

Tactic:
induction xs with
  | nil => simp
  | cons y ys => by_cases x = y.1 <;> simp [*]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ kinsert (β := β) a b l = Sigma.mk (β := β) a b :: kerase (β := β) a l

Tactic:
rfl

Premises used: List.kinsert, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
pos : ∀ (h : a = a'), a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)
neg : ∀ (h : ¬a = a'), a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)
⊢ a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)

Tactic:
by_cases h : a = a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
⊢ (kinsert (β := β) a b l).NodupKeys (β := β)

Tactic:
nodupKeys_cons.mpr ⟨notMem_keys_kerase a nd, nd.kerase a⟩

Premises used: Iff.mpr, List.nodupKeys_cons, List.NodupKeys.kerase, And.intro, List.kinsert, List.notMem_keys_kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys (β := β)
p : l₁ ~ l₂
⊢ List.kinsert (β := β) a b l₁ ~ List.kinsert (β := β) a b l₂

Tactic:
(p.kerase nd₁).cons _

Premises used: List.Perm.kerase, List.Perm.cons, List.kinsert
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ dlookup (β := β) a (kinsert (β := β) a b l) = some b

Tactic:
simp only [kinsert, dlookup_cons_eq]

Premises used: List.dlookup_cons_eq, List.kinsert
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a ≠ a'
⊢ dlookup (β := β) a (kinsert (β := β) a' b' l) = dlookup (β := β) a l

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
simp :
  (if h : a' = a then (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b ⋯), l)
    else ((kextract (β := β) a l).fst, Sigma.mk (β := β) a' b :: (kextract (β := β) a l).snd)) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
⊢ kextract (β := β) a (Sigma.mk (β := β) a' b :: l) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))

Tactic:
simp only [kextract]

Premises used: List.kextract
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
pos :
  ∀ (h : a' = a),
    (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b ⋯), l) =
      (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
neg :
  ∀ (h : ¬a' = a),
    ((kextract (β := β) a l).fst, Sigma.mk (β := β) a' b :: (kextract (β := β) a l).snd) =
      (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
⊢ (if h : a' = a then (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b ⋯), l)
    else ((kextract (β := β) a l).fst, Sigma.mk (β := β) a' b :: (kextract (β := β) a l).snd)) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))

Tactic:
split_ifs with h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a' = a
pos :
  ∀ (b : β a),
    (some (Eq.rec (motive := fun (x : α) (x_1 : a = x) ↦ β x) b ⋯), l) =
      (dlookup (β := β) a (Sigma.mk (β := β) a b :: l), kerase (β := β) a (Sigma.mk (β := β) a b :: l))
⊢ (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b ⋯), l) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))

Tactic:
subst a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (some (Eq.rec (motive := fun (x : α) (x_1 : a = x) ↦ β x) b ⋯), l) =
    (dlookup (β := β) a (Sigma.mk (β := β) a b :: l), kerase (β := β) a (Sigma.mk (β := β) a b :: l))

Tactic:
simp [kerase]

Premises used: List.kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract (β := β) a l).fst, Sigma.mk (β := β) a' b :: (kextract (β := β) a l).snd) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))

Tactic:
simp [Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]

Premises used: Ne.symm, List.kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x : Sigma β
l : List (Sigma β)
⊢ (x :: l).dedupKeys (β := β) = kinsert (β := β) (x.fst (β := β)) (x.snd (β := β)) (l.dedupKeys (β := β))

Tactic:
rfl

Premises used: List.kinsert, List.dedupKeys, List.foldr, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
generalize :
  ∀ (l' : List (Sigma β)) (hl : [] = l'),
    (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' l).NodupKeys (β := β)
⊢ NodupKeys (β := β) (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) [] l)

Tactic:
generalize hl : nil = l'

Premises used: List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
rw : NodupKeys (β := β) []
⊢ l'.NodupKeys (β := β)

Tactic:
rw [← hl]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ NodupKeys (β := β) []

Tactic:
apply nodup_nil

Premises used: List.nodup_nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ l'.NodupKeys (β := β)

Tactic:
have : NodupKeys l' := by
    rw [← hl]
    apply nodup_nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' []).NodupKeys (β := β)

Tactic:
apply this
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
x : Sigma β
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
cons :
  ∀ (fst : α) (snd : β fst),
    (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l'
          (Sigma.mk (β := β) fst snd :: xs)).NodupKeys
      (β := β)
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' (x :: xs)).NodupKeys (β := β)

Tactic:
cases x
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
cons :
  ¬fst ∈
        (kerase (β := β) fst
              (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
          (β := β) ∧
    (kerase (β := β) fst
          (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
      (β := β)
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l'
        (Sigma.mk (β := β) fst snd :: xs)).NodupKeys
    (β := β)

Tactic:
simp only [foldr_cons, kinsert_def, nodupKeys_cons]

Premises used: List.foldr_cons, List.nodupKeys_cons, List.kinsert_def
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
cons :
  ¬fst ∈
      (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
        (β := β)
cons₁ :
  (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
    (β := β)
⊢ ¬fst ∈
        (kerase (β := β) fst
              (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
          (β := β) ∧
    (kerase (β := β) fst
          (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
      (β := β)

Tactic:
constructor
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
cons :
  ¬fst ∈ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).keys (β := β).erase fst
⊢ ¬fst ∈
      (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
        (β := β)

Tactic:
simp only [keys_kerase]

Premises used: List.keys_kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
⊢ ¬fst ∈ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).keys (β := β).erase fst

Tactic:
apply l_ih.not_mem_erase

Premises used: List.Nodup.not_mem_erase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
⊢ (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
    (β := β)

Tactic:
l_ih.kerase _

Premises used: List.NodupKeys.kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
⊢ (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
    (β := β)

Tactic:
exact l_ih.kerase _

Premises used: List.NodupKeys.kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
nil : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' []).NodupKeys (β := β)
cons :
  ∀ (x : Sigma β) (xs : List (Sigma β))
    (l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)),
    (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' (x :: xs)).NodupKeys (β := β)
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' l).NodupKeys (β := β)

Tactic:
induction l with
  | nil => apply this
  | cons x xs l_ih =>
    cases x
    simp only [foldr_cons, kinsert_def, nodupKeys_cons]
    constructor
    · simp only [keys_kerase]
      apply l_ih.not_mem_erase
    · exact l_ih.kerase _

Premises used: List.foldr_cons, List.nodupKeys_cons, List.kinsert_def, List.cons, List.keys_kerase, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq.{v + 1} (α := Option (β a)) (dlookup (β := β) a (dedupKeys (β := β) [])) (dlookup (β := β) a [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l_hd : Sigma β
tail : List (Sigma β)
l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail
cons :
  ∀ (a' : α) (b : β a'),
    dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
      dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
⊢ dlookup (β := β) a ((l_hd :: tail).dedupKeys (β := β)) = dlookup (β := β) a (l_hd :: tail)

Tactic:
obtain ⟨a', b⟩ := l_hd
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail
a' : α
b : β a'
pos :
  ∀ (h : a = a'),
    dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
      dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
neg :
  ∀ (h : ¬a = a'),
    dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
      dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)

Tactic:
by_cases h : a = a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail
a' : α
b : β a'
h : a = a'
pos :
  ∀ (b : β a),
    dlookup (β := β) a ((Sigma.mk (β := β) a b :: tail).dedupKeys (β := β)) =
      dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)

Tactic:
subst a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail
b : β a
pos :
  dlookup (β := β) a
      (kinsert (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) ((Sigma.mk (β := β) a b).snd (β := β))
        (tail.dedupKeys (β := β))) =
    dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
pos₁ : some ((Sigma.mk (β := β) a b).snd (β := β)) = dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
pos₂ pos₃ : some ((Sigma.mk (β := β) a b).snd (β := β)) = some b
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)

Tactic:
rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]

Premises used: List.dedupKeys_cons, List.dlookup_cons_eq, List.dlookup_kinsert
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail
a' : α
b : β a'
h : ¬a = a'
neg : a ≠ (Sigma.mk (β := β) a' b).fst (β := β)
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)

Tactic:
rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]

Premises used: List.dedupKeys_cons, List.dlookup_cons_ne, List.dlookup_kinsert_ne
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail
a' : α
b : β a'
h : ¬a = a'
⊢ a ≠ (Sigma.mk (β := β) a' b).fst (β := β)

Tactic:
h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail
a' : α
b : β a'
h : ¬a = a'
⊢ a ≠ (Sigma.mk (β := β) a' b).fst (β := β)

Tactic:
exact h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nil : Eq.{v + 1} (α := Option (β a)) (dlookup (β := β) a (dedupKeys (β := β) [])) (dlookup (β := β) a [])
cons :
  ∀ (l_hd : Sigma β) (tail : List (Sigma β))
    (l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail),
    dlookup (β := β) a ((l_hd :: tail).dedupKeys (β := β)) = dlookup (β := β) a (l_hd :: tail)
⊢ dlookup (β := β) a (l.dedupKeys (β := β)) = dlookup (β := β) a l

Tactic:
induction l with
  | nil => rfl
  | cons l_hd _ l_ih =>
    obtain ⟨a', b⟩ := l_hd
    by_cases h : a = a'
    · subst a'
      rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]
    · rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
      exact h

Premises used: List.dedupKeys_cons, List.dlookup_cons_ne, List.cons, List.dlookup_cons_eq, List.dlookup_kinsert, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
xs : List (Sigma β)
simp :
  LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (xs.dedupKeys (β := β)) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) xs :
      ℕ)
⊢ sizeOf (xs.dedupKeys (β := β)) ≤ sizeOf xs

Tactic:
simp only [SizeOf.sizeOf, _sizeOf_1]

Premises used: List._sizeOf_1, SizeOf.sizeOf
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
⊢ LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (dedupKeys (β := β) []) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) [] :
      ℕ)

Tactic:
simp [dedupKeys]

Premises used: List.dedupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih :
  LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (xs.dedupKeys (β := β)) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) xs :
      ℕ)
cons :
  LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (kerase (β := β) (x.fst (β := β)) (xs.dedupKeys (β := β))) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) xs :
      ℕ)
⊢ LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        ((x :: xs).dedupKeys (β := β)) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) (x :: xs) :
      ℕ)

Tactic:
simp only [dedupKeys_cons, kinsert_def, Nat.add_le_add_iff_left, Sigma.eta]

Premises used: List.dedupKeys_cons, Sigma.eta, List.kinsert_def, Nat.add_le_add_iff_left