awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
h : ¬a = x.fst (β := β)
tail_ih :
  kerase (β := β) a (kerase (β := β) (x.fst (β := β)) xs) = kerase (β := β) (x.fst (β := β)) (kerase (β := β) a xs)
⊢ kerase (β := β) a (kerase (β := β) (x.fst (β := β)) (x :: xs)) =
    kerase (β := β) (x.fst (β := β)) (kerase (β := β) a (x :: xs))

Tactic:
simp [kerase_cons_ne h, kerase_cons_eq rfl]

Premises used: List.kerase_cons_ne, List.kerase_cons_eq, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih : kerase (β := β) a (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) a xs)
h_1 : ¬a' = x.fst (β := β)
pos :
  ∀ (h' : a = x.fst (β := β)),
    kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
neg :
  ∀ (h' : ¬a = x.fst (β := β)),
    kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))

Tactic:
by_cases h' : a = x.1

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih : kerase (β := β) a (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) a xs)
h_1 : ¬a' = x.fst (β := β)
h' : a = x.fst (β := β)
pos :
  ∀ (h : ¬x.fst (β := β) = a'),
    kerase (β := β) (x.fst (β := β)) (kerase (β := β) a' xs) =
        kerase (β := β) a' (kerase (β := β) (x.fst (β := β)) xs) →
      kerase (β := β) (x.fst (β := β)) (kerase (β := β) a' (x :: xs)) =
        kerase (β := β) a' (kerase (β := β) (x.fst (β := β)) (x :: xs))
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))

Tactic:
subst a
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a' : α
x : Sigma β
xs : List (Sigma β)
h_1 : ¬a' = x.fst (β := β)
h : ¬x.fst (β := β) = a'
tail_ih :
  kerase (β := β) (x.fst (β := β)) (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) (x.fst (β := β)) xs)
⊢ kerase (β := β) (x.fst (β := β)) (kerase (β := β) a' (x :: xs)) =
    kerase (β := β) a' (kerase (β := β) (x.fst (β := β)) (x :: xs))

Tactic:
simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]

Premises used: List.kerase_cons_ne, Ne.symm, List.kerase_cons_eq, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih : kerase (β := β) a (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) a xs)
h_1 : ¬a' = x.fst (β := β)
h' : ¬a = x.fst (β := β)
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))

Tactic:
simp [kerase_cons_ne, *]

Premises used: List.kerase_cons_ne
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
l : List (Sigma β)
h : ¬a = a'
neg : Eq (α := List (Sigma β)) (kerase (β := β) a (kerase (β := β) a' [])) (kerase (β := β) a' (kerase (β := β) a []))
neg₁ :
  ∀ (x : Sigma β) (xs : List (Sigma β)),
    kerase (β := β) a (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) a xs) →
      kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
⊢ kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)

Tactic:
induction l with
  | nil => rfl
  | cons x xs =>
    by_cases a' = x.1
    · subst a'
      simp [kerase_cons_ne h, kerase_cons_eq rfl]
    by_cases h' : a = x.1
    · subst a
      simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]
    · simp [kerase_cons_ne, *]

Premises used: List.kerase_cons_ne, Ne.symm, List.kerase_cons_eq, List.cons, rfl, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
inst : DecidableEq α
a : α
⊢ l.NodupKeys (β := β) → (List.kerase (β := β) a l).NodupKeys (β := β)

Tactic:
NodupKeys.sublist <| kerase_sublist _ _

Premises used: List.NodupKeys.sublist, List.kerase_sublist
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
H :
  Pairwise (fun (a_1 b : Sigma β) ↦ decide (a = a_1.fst (β := β)) = true → decide (a = b.fst (β := β)) = true → False)
    l₁
⊢ l₁ ~ l₂ → List.kerase (β := β) a l₁ ~ List.kerase (β := β) a l₂

Tactic:
apply Perm.eraseP

Premises used: List.Perm.eraseP
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
H :
  ∀ {a_1 b : Sigma β},
    a_1.fst (β := β) ≠ b.fst (β := β) →
      decide (a = a_1.fst (β := β)) = true → decide (a = b.fst (β := β)) = true → False
⊢ Pairwise (fun (a_1 b : Sigma β) ↦ decide (a = a_1.fst (β := β)) = true → decide (a = b.fst (β := β)) = true → False)
    l₁

Tactic:
apply (nodupKeys_iff_pairwise.1 nd).imp

Premises used: List.nodupKeys_iff_pairwise, Iff.mp, List.Pairwise.imp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
a_1 b : Sigma β
h : a_1.fst (β := β) ≠ b.fst (β := β)
h_1 : decide (a = a_1.fst (β := β)) = true
h_2 : decide (a = b.fst (β := β)) = true
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
nd : NodupKeys (β := β) []
⊢ ¬a ∈ keys (β := β) (kerase (β := β) a [])

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β)
nd : (hd :: tl).NodupKeys (β := β)
⊢ ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.NodupKeys (β := β)

Tactic:
simp only [nodupKeys_cons] at nd

Premises used: List.nodupKeys_cons
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β)
nd : ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.NodupKeys (β := β)
pos : ∀ (h : a = hd.fst (β := β)), ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
neg : ∀ (h : ¬a = hd.fst (β := β)), ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
⊢ ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)

Tactic:
by_cases h : a = hd.1

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β)
nd : ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.NodupKeys (β := β)
h : a = hd.fst (β := β)
pos :
  ∀ (ih : ∀ (nd : tl.NodupKeys (β := β)), ¬hd.fst (β := β) ∈ (kerase (β := β) (hd.fst (β := β)) tl).keys (β := β)),
    ¬hd.fst (β := β) ∈ (kerase (β := β) (hd.fst (β := β)) (hd :: tl)).keys (β := β)
⊢ ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)

Tactic:
subst h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
nd : ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.NodupKeys (β := β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬hd.fst (β := β) ∈ (kerase (β := β) (hd.fst (β := β)) tl).keys (β := β)
⊢ ¬hd.fst (β := β) ∈ (kerase (β := β) (hd.fst (β := β)) (hd :: tl)).keys (β := β)

Tactic:
simp [nd.1]

Premises used: And.left
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β)
nd : ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.NodupKeys (β := β)
h : ¬a = hd.fst (β := β)
⊢ ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)

Tactic:
simp [h, ih nd.2]

Premises used: And.right
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nd : l.NodupKeys (β := β)
nil : ∀ (nd : NodupKeys (β := β) []), ¬a ∈ keys (β := β) (kerase (β := β) a [])
cons :
  ∀ (hd : Sigma β) (tl : List (Sigma β))
    (ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β))
    (nd : (hd :: tl).NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
⊢ ¬a ∈ (kerase (β := β) a l).keys (β := β)

Tactic:
induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [nodupKeys_cons] at nd
    by_cases h : a = hd.1
    · subst h
      simp [nd.1]
    · simp [h, ih nd.2]

Premises used: List.nodupKeys_cons, List.cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nd : l.NodupKeys (β := β)
⊢ dlookup (β := β) a (kerase (β := β) a l) = none

Tactic:
dlookup_eq_none.mpr (notMem_keys_kerase a nd)

Premises used: Iff.mpr, List.dlookup_eq_none, List.notMem_keys_kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
⊢ Eq.{v + 1} (α := Option (β a)) (dlookup (β := β) a (kerase (β := β) a' [])) (dlookup (β := β) a [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
hd : Sigma β
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
cons :
  ∀ (ah : α) (bh : β ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (hd :: tl)) = dlookup (β := β) a (hd :: tl)

Tactic:
obtain ⟨ah, bh⟩ := hd
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
ah : α
bh : β ah
pos :
  ∀ (h₁ : a = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
neg :
  ∀ (h₁ : ¬a = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)

Tactic:
by_cases h₁ : a = ah
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
ah : α
bh : β ah
h₁ : a = ah
pos :
  ∀ (h₂ : a' = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
neg :
  ∀ (h₂ : ¬a' = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)

Tactic:
by_cases h₂ : a' = ah
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
ah : α
bh : β ah
h₁ : ¬a = ah
pos :
  ∀ (h₂ : a' = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
neg :
  ∀ (h₂ : ¬a' = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)

Tactic:
by_cases h₂ : a' = ah
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : a' = ah
pos :
  ∀ (h : a' ≠ a') (ih : dlookup (β := β) a' (kerase (β := β) a' tl) = dlookup (β := β) a' tl) (bh : β a'),
    dlookup (β := β) a' (kerase (β := β) a' (Sigma.mk (β := β) a' bh :: tl)) =
      dlookup (β := β) a' (Sigma.mk (β := β) a' bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)

Tactic:
substs h₁ h₂
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a' : α
tl : List (Sigma β)
h : a' ≠ a'
ih : dlookup (β := β) a' (kerase (β := β) a' tl) = dlookup (β := β) a' tl
bh : β a'
⊢ dlookup (β := β) a' (kerase (β := β) a' (Sigma.mk (β := β) a' bh :: tl)) =
    dlookup (β := β) a' (Sigma.mk (β := β) a' bh :: tl)

Tactic:
cases Ne.irrefl h

Premises used: Ne.irrefl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : ¬a' = ah
neg :
  ∀ (bh : β a) (h₂ : ¬a' = a),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) a bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) a bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)

Tactic:
subst h₁
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
bh : β a
h₂ : ¬a' = a
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) a bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) a bh :: tl)

Tactic:
simp [h₂]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : a' = ah
pos :
  ∀ (bh : β a') (h₁ : ¬a = a'),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) a' bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) a' bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)

Tactic:
subst h₂
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
bh : β a'
h₁ : ¬a = a'
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) a' bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' bh :: tl)

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)

Tactic:
simp [h₁, h₂, ih]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
l : List (Sigma β)
h : a ≠ a'
nil : Eq.{v + 1} (α := Option (β a)) (dlookup (β := β) a (kerase (β := β) a' [])) (dlookup (β := β) a [])
cons :
  ∀ (hd : Sigma β) (tl : List (Sigma β)) (ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl),
    dlookup (β := β) a (kerase (β := β) a' (hd :: tl)) = dlookup (β := β) a (hd :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' l) = dlookup (β := β) a l

Tactic:
induction l with
  | nil => rfl
  | cons hd tl ih =>
    obtain ⟨ah, bh⟩ := hd
    by_cases h₁ : a = ah <;> by_cases h₂ : a' = ah
    · substs h₁ h₂
      cases Ne.irrefl h
    · subst h₁
      simp [h₂]
    · subst h₂
      simp [h]
    · simp [h₁, h₂, ih]

Premises used: Ne.irrefl, List.cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
x : List (Sigma β)
h : Membership.mem (γ := List α) (keys (β := β) []) a
⊢ kerase (β := β) a ([] ++ x) = kerase (β := β) a [] ++ x

Tactic:
cases h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys (β := β)
h₂ : a = s.fst (β := β)
⊢ kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂

Tactic:
simp [h₂]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys (β := β)
h₂ : ¬a = s.fst (β := β)
⊢ kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂

Tactic:
simp_all [kerase_append_left]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys (β := β)
if : ∀ (h₂ : a = s.fst (β := β)), kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂
if₁ : ∀ (h₂ : ¬a = s.fst (β := β)), kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂
if₂ : ∀ (h₂ : a = s.fst (β := β)), kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂
if₃ if₄ : ∀ (h₂ : ¬a = s.fst (β := β)), kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂
⊢ kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂

Tactic:
if h₂ : a = s.1 then simp [h₂]
    else simp_all [kerase_append_left]

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
head : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a ∈ (head :: l₁).keys (β := β)
⊢ ¬a = head.fst (β := β) ∧ ¬a ∈ l₁.keys (β := β)

Tactic:
simp only [keys_cons, mem_cons, not_or] at h

Premises used: List.keys_cons, not_or, List.mem_cons
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
head : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a = head.fst (β := β) ∧ ¬a ∈ l₁.keys (β := β)
⊢ kerase (β := β) a (head :: l₁ ++ l₂) = head :: l₁ ++ kerase (β := β) a l₂

Tactic:
simp [h.1, kerase_append_right h.2]

Premises used: And.right, And.left
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ = a₂
⊢ kerase (β := β) a₂ (kerase (β := β) a₁ l) = kerase (β := β) a₁ (kerase (β := β) a₂ l)

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₂ : a₂ ∈ l.keys (β := β)
b₁ : β a₁
l₁ l₂ : List (Sigma β)
a₁_nin_l₁ : ¬a₁ ∈ l₁.keys (β := β)
h_1 : a₂ ∈ (l₁ ++ Sigma.mk (β := β) a₁ b₁ :: l₂).keys (β := β)
ha₁ : a₁ ∈ (l₁ ++ Sigma.mk (β := β) a₁ b₁ :: l₂).keys (β := β)
h' : a₂ ∈ l₁.keys (β := β)
⊢ kerase (β := β) a₂ (l₁ ++ l₂) = kerase (β := β) a₁ (kerase (β := β) a₂ (l₁ ++ Sigma.mk (β := β) a₁ b₁ :: l₂))

Tactic:
simp [kerase_append_left h',
              kerase_append_right (mt (mem_keys_kerase_of_ne h).mp a₁_nin_l₁)]

Premises used: List.kerase_append_right, mt, List.mem_keys_kerase_of_ne, List.kerase_append_left, Iff.mp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₂ : a₂ ∈ l.keys (β := β)
b₁ : β a₁
l₁ l₂ : List (Sigma β)
a₁_nin_l₁ : ¬a₁ ∈ l₁.keys (β := β)
h_1 : a₂ ∈ (l₁ ++ Sigma.mk (β := β) a₁ b₁ :: l₂).keys (β := β)
ha₁ : a₁ ∈ (l₁ ++ Sigma.mk (β := β) a₁ b₁ :: l₂).keys (β := β)
h' : ¬a₂ ∈ l₁.keys (β := β)
⊢ kerase (β := β) a₂ (l₁ ++ l₂) = kerase (β := β) a₁ (kerase (β := β) a₂ (l₁ ++ Sigma.mk (β := β) a₁ b₁ :: l₂))

Tactic:
simp [kerase_append_right h', kerase_append_right a₁_nin_l₁,
              @kerase_cons_ne _ _ _ a₂ ⟨a₁, b₁⟩ _ (Ne.symm h)]

Premises used: List.kerase_append_right, List.kerase_cons_ne, Ne.symm
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₁ : a₁ ∈ l.keys (β := β)
ha₂ : ¬a₂ ∈ l.keys (β := β)
⊢ kerase (β := β) a₂ (kerase (β := β) a₁ l) = kerase (β := β) a₁ (kerase (β := β) a₂ l)

Tactic:
simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂]

Premises used: mt, List.mem_keys_of_mem_keys_kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₁ : ¬a₁ ∈ l.keys (β := β)
⊢ kerase (β := β) a₂ (kerase (β := β) a₁ l) = kerase (β := β) a₁ (kerase (β := β) a₂ l)

Tactic:
simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]

Premises used: mt, List.mem_keys_of_mem_keys_kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
x : α
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)
        (kerase (β := β) x xs) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) xs :
      ℕ)
⊢ sizeOf (kerase (β := β) x xs) ≤ 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 β)
x : α
⊢ 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) [] :
      ℕ)

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 :
      ℕ)
pos :
  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) :
        ℕ)
neg :
  ¬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) :
        ℕ)
⊢ 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:
by_cases x = y.1

Premises used: Sigma.fst