awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
z w : Sigma β
h_2 : ¬a = x.fst (β := β)
h₁ : Membership.mem (γ := Option (Sigma β)) none z
h_1 : ¬a = y.fst (β := β)
h₂ : Membership.mem (γ := Option (Sigma β)) none w
⊢ x = y ∧ z = w

Tactic:
cases h₁
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
w : Sigma β
h_2 : a = x.fst (β := β)
h_1 : a = y.fst (β := β)
h₂ : w ∈ some (Sigma.mk (β := β) a b)
pos : x = y ∧ Sigma.mk (β := β) a b = Sigma.mk (β := β) a b
⊢ x = y ∧ Sigma.mk (β := β) a b = w

Tactic:
cases h₂
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
w : Sigma β
h_2 : a = x.fst (β := β)
h_1 : ¬a = y.fst (β := β)
h₂ : Membership.mem (γ := Option (Sigma β)) none w
⊢ x = y ∧ Sigma.mk (β := β) a b = w

Tactic:
cases h₂
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
h_2 : a = x.fst (β := β)
h_1 : a = y.fst (β := β)
⊢ x = y ∧ Sigma.mk (β := β) a b = Sigma.mk (β := β) a b

Tactic:
(h (h_2.symm.trans h_1)).elim

Premises used: False.elim, Eq.symm, Eq.trans
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
h_2 : a = x.fst (β := β)
h_1 : a = y.fst (β := β)
⊢ x = y ∧ Sigma.mk (β := β) a b = Sigma.mk (β := β) a b

Tactic:
exact (h (h_2.symm.trans h_1)).elim

Premises used: False.elim, Eq.symm, Eq.trans
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq (α := List (Sigma β)) (kerase (β := β) a []) []

Tactic:
rfl

Premises used: List.kerase, List.eraseP, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l : List (Sigma β)
h : a = s.fst (β := β)
⊢ kerase (β := β) a (s :: l) = l

Tactic:
simp [kerase, h]

Premises used: List.kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l : List (Sigma β)
h : a ≠ s.fst (β := β)
⊢ kerase (β := β) a (s :: l) = s :: kerase (β := β) a l

Tactic:
simp [kerase, h]

Premises used: List.kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
h : ¬Membership.mem (γ := List α) (keys (β := β) []) a
⊢ Eq (α := List (Sigma β)) (kerase (β := β) a []) []

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
head : Sigma β
tail : List (Sigma β)
ih : ∀ (h : ¬a ∈ tail.keys (β := β)), kerase (β := β) a tail = tail
h : ¬a ∈ (head :: tail).keys (β := β)
⊢ ¬a = head.fst (β := β) ∧ ¬a ∈ tail.keys (β := β)

Tactic:
simp [not_or] at h

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

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

Premises used: And.right, And.left
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : ¬a ∈ l.keys (β := β)
nil : ∀ (h : ¬Membership.mem (γ := List α) (keys (β := β) []) a), Eq (α := List (Sigma β)) (kerase (β := β) a []) []
cons :
  ∀ (head : Sigma β) (tail : List (Sigma β)) (ih : ∀ (h : ¬a ∈ tail.keys (β := β)), kerase (β := β) a tail = tail)
    (h : ¬a ∈ (head :: tail).keys (β := β)), kerase (β := β) a (head :: tail) = head :: tail
⊢ kerase (β := β) a l = l

Tactic:
induction l with
  | nil => rfl
  | cons _ _ ih => simp [not_or] at h; simp [h.1, ih h.2]

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

Tactic:
eraseP_sublist

Premises used: List.eraseP_sublist, List.kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
⊢ (kerase (β := β) a l).keys (β := β) ⊆ l.keys (β := β)

Tactic:
((kerase_sublist a l).map _).subset

Premises used: List.keys, List.Sublist.map, List.kerase_sublist, List.Sublist.subset
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
⊢ a₁ ∈ (kerase (β := β) a₂ l).keys (β := β) → a₁ ∈ l.keys (β := β)

Tactic:
@kerase_keys_subset _ _ _ _ _ _

Premises used: List.kerase_keys_subset
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
h : Membership.mem (γ := List α) (keys (β := β) []) a
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ [] = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a [] = l₁ ++ l₂

Tactic:
cases h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys (β := β)
pos :
  ∀ (e : a = hd.fst (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
neg :
  ∀ (e : ¬a = hd.fst (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂

Tactic:
by_cases e : 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 :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys (β := β)
e : a = hd.fst (β := β)
pos :
  ∀
    (ih :
      ∀ (h : hd.fst (β := β) ∈ tl.keys (β := β)),
        ∃ (b : β (hd.fst (β := β))),
          ∃ (l₁ : List (Sigma β)),
            ∃ (l₂ : List (Sigma β)),
              ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
                tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧
                  kerase (β := β) (hd.fst (β := β)) tl = l₁ ++ l₂)
    (h : hd.fst (β := β) ∈ (hd :: tl).keys (β := β)),
    ∃ (b : β (hd.fst (β := β))),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
            hd :: tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧
              kerase (β := β) (hd.fst (β := β)) (hd :: tl) = l₁ ++ l₂
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂

Tactic:
subst e
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : hd.fst (β := β) ∈ tl.keys (β := β)),
    ∃ (b : β (hd.fst (β := β))),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
            tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧ kerase (β := β) (hd.fst (β := β)) tl = l₁ ++ l₂
h : hd.fst (β := β) ∈ (hd :: tl).keys (β := β)
⊢ ¬Membership.mem (γ := List α) (keys (β := β) []) (hd.fst (β := β))

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : hd.fst (β := β) ∈ tl.keys (β := β)),
    ∃ (b : β (hd.fst (β := β))),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
            tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧ kerase (β := β) (hd.fst (β := β)) tl = l₁ ++ l₂
h : hd.fst (β := β) ∈ (hd :: tl).keys (β := β)
mk :
  ∀ (fst : α) (snd : β fst)
    (ih :
      ∀ (h : (Sigma.mk (β := β) fst snd).fst (β := β) ∈ tl.keys (β := β)),
        ∃ (b : β ((Sigma.mk (β := β) fst snd).fst (β := β))),
          ∃ (l₁ : List (Sigma β)),
            ∃ (l₂ : List (Sigma β)),
              ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ l₁.keys (β := β) ∧
                tl = l₁ ++ Sigma.mk (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) b :: l₂ ∧
                  kerase (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) tl = l₁ ++ l₂)
    (h : (Sigma.mk (β := β) fst snd).fst (β := β) ∈ (Sigma.mk (β := β) fst snd :: tl).keys (β := β)),
    Sigma.mk (β := β) fst snd :: tl =
      [] ++
        Sigma.mk (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) :: tl
⊢ hd :: tl = [] ++ Sigma.mk (β := β) (hd.fst (β := β)) (hd.snd (β := β)) :: tl

Tactic:
cases hd
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
tl : List (Sigma β)
fst : α
snd : β fst
ih :
  ∀ (h : (Sigma.mk (β := β) fst snd).fst (β := β) ∈ tl.keys (β := β)),
    ∃ (b : β ((Sigma.mk (β := β) fst snd).fst (β := β))),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ l₁.keys (β := β) ∧
            tl = l₁ ++ Sigma.mk (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) b :: l₂ ∧
              kerase (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) tl = l₁ ++ l₂
h : (Sigma.mk (β := β) fst snd).fst (β := β) ∈ (Sigma.mk (β := β) fst snd :: tl).keys (β := β)
⊢ Sigma.mk (β := β) fst snd :: tl =
    [] ++ Sigma.mk (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) :: tl

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : hd.fst (β := β) ∈ tl.keys (β := β)),
    ∃ (b : β (hd.fst (β := β))),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
            tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧ kerase (β := β) (hd.fst (β := β)) tl = l₁ ++ l₂
h : hd.fst (β := β) ∈ (hd :: tl).keys (β := β)
⊢ kerase (β := β) (hd.fst (β := β)) (hd :: tl) = [] ++ tl

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : hd.fst (β := β) ∈ tl.keys (β := β)),
    ∃ (b : β (hd.fst (β := β))),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
            tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧ kerase (β := β) (hd.fst (β := β)) tl = l₁ ++ l₂
h : hd.fst (β := β) ∈ (hd :: tl).keys (β := β)
⊢ ∃ (b : β (hd.fst (β := β))),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
          hd :: tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧
            kerase (β := β) (hd.fst (β := β)) (hd :: tl) = l₁ ++ l₂

Tactic:
exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys (β := β)
e : ¬a = hd.fst (β := β)
⊢ a = hd.fst (β := β) ∨ a ∈ tl.keys (β := β)

Tactic:
simp only [keys_cons, mem_cons] at h

Premises used: List.keys_cons, List.mem_cons
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
e : ¬a = hd.fst (β := β)
h : a = hd.fst (β := β) ∨ a ∈ tl.keys (β := β)
neg :
  ∀ (h : a = hd.fst (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
neg₁ :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂

Tactic:
rcases h with h | h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
e : ¬a = hd.fst (β := β)
h : a = hd.fst (β := β)
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂

Tactic:
absurd h e

Premises used: absurd
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
e : ¬a = hd.fst (β := β)
h : a = hd.fst (β := β)
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂

Tactic:
exact absurd h e

Premises used: absurd
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
e : ¬a = hd.fst (β := β)
h : a ∈ tl.keys (β := β)
neg :
  ∀ (b : β a) (tl₁ tl₂ : List (Sigma β)) (h₁ : ¬a ∈ tl₁.keys (β := β)) (h₂ : tl = tl₁ ++ Sigma.mk (β := β) a b :: tl₂)
    (h₃ : kerase (β := β) a tl = tl₁ ++ tl₂),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂

Tactic:
rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
e : ¬a = hd.fst (β := β)
h : a ∈ tl.keys (β := β)
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys (β := β)
h₂ : tl = tl₁ ++ Sigma.mk (β := β) a b :: tl₂
h₃ : kerase (β := β) a tl = tl₁ ++ tl₂
rw : hd :: (tl₁ ++ Sigma.mk (β := β) a b :: tl₂) = hd :: tl₁ ++ Sigma.mk (β := β) a b :: tl₂
⊢ hd :: tl = hd :: tl₁ ++ Sigma.mk (β := β) a b :: tl₂

Tactic:
rw [h₂]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
e : ¬a = hd.fst (β := β)
h : a ∈ tl.keys (β := β)
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys (β := β)
h₂ : tl = tl₁ ++ Sigma.mk (β := β) a b :: tl₂
h₃ : kerase (β := β) a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ Sigma.mk (β := β) a b :: tl₂) = hd :: tl₁ ++ Sigma.mk (β := β) a b :: tl₂

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
e : ¬a = hd.fst (β := β)
h : a ∈ tl.keys (β := β)
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys (β := β)
h₂ : tl = tl₁ ++ Sigma.mk (β := β) a b :: tl₂
h₃ : kerase (β := β) a tl = tl₁ ++ tl₂
⊢ kerase (β := β) a (hd :: tl) = hd :: tl₁ ++ tl₂

Tactic:
simp [e, h₃]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
e : ¬a = hd.fst (β := β)
h : a ∈ tl.keys (β := β)
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys (β := β)
h₂ : tl = tl₁ ++ Sigma.mk (β := β) a b :: tl₂
h₃ : kerase (β := β) a tl = tl₁ ++ tl₂
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂

Tactic:
exact ⟨b, hd :: tl₁, tl₂, not_mem_cons_of_ne_of_not_mem e h₁, by (rw [h₂]; rfl), by
            simp [e, h₃]⟩
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : a ∈ l.keys (β := β)
nil :
  ∀ (h : Membership.mem (γ := List α) (keys (β := β) []) a),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ [] = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a [] = l₁ ++ l₂
cons :
  ∀ (hd : Sigma β) (tl : List (Sigma β))
    (ih :
      ∀ (h : a ∈ tl.keys (β := β)),
        ∃ (b : β a),
          ∃ (l₁ : List (Sigma β)),
            ∃ (l₂ : List (Sigma β)),
              ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂)
    (h : a ∈ (hd :: tl).keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ l = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a l = l₁ ++ l₂

Tactic:
induction l with
  | nil => cases h
  | cons hd tl ih =>
    by_cases e : a = hd.1
    · subst e
      exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩
    · simp only [keys_cons, mem_cons] at h
      rcases h with h | h
      · exact absurd h e
      rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩
      exact ⟨b, hd :: tl₁, tl₂, not_mem_cons_of_ne_of_not_mem e h₁, by (rw [h₂]; rfl), by
            simp [e, h₃]⟩

Premises used: List.keys_cons, List.cons, List.mem_cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p_1 : a₁ ∈ l.keys (β := β)
w : β a₂
w_1 w_2 : List (Sigma β)
left : ¬a₂ ∈ w_1.keys (β := β)
p : a₁ ∈ (w_1 ++ Sigma.mk (β := β) a₂ w :: w_2).keys (β := β)
q : a₂ ∈ (w_1 ++ Sigma.mk (β := β) a₂ w :: w_2).keys (β := β)
⊢ a₁ ∈ (w_1 ++ w_2).keys (β := β)

Tactic:
simpa [keys, h] using p

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

Tactic:
simp [q, p]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
rw :
  map (Sigma.fst (β := β)) (eraseP (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) l) =
    map (Sigma.fst (β := β)) (eraseP (fun (x : Sigma β) ↦ a == x.fst (β := β)) l)
⊢ (kerase (β := β) a l).keys (β := β) = l.keys (β := β).erase a

Tactic:
rw [keys, kerase, erase_eq_eraseP, eraseP_map, Function.comp_def]

Premises used: List.keys, List.erase_eq_eraseP, List.eraseP_map, List.kerase, Function.comp_def
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
⊢ map (Sigma.fst (β := β)) (eraseP (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) l) =
    map (Sigma.fst (β := β)) (eraseP (fun (x : Sigma β) ↦ a == x.fst (β := β)) l)

Tactic:
congr
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
l : List (Sigma β)
pos : ∀ (h : a = a'), kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
neg : ∀ (h : ¬a = a'), kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
⊢ kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)

Tactic:
by_cases h : a = a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
l : List (Sigma β)
h : a = a'
pos : kerase (β := β) a (kerase (β := β) a l) = kerase (β := β) a (kerase (β := β) a l)
⊢ kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)

Tactic:
subst a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
⊢ kerase (β := β) a (kerase (β := β) a l) = kerase (β := β) a (kerase (β := β) a l)

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : ¬a = a'
⊢ Eq (α := List (Sigma β)) (kerase (β := β) a (kerase (β := β) a' [])) (kerase (β := β) a' (kerase (β := β) a []))

Tactic:
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)
pos :
  a' = x.fst (β := β) →
    kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
neg :
  ¬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 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 (β := β)
pos :
  ∀ (h : ¬a = x.fst (β := β)),
    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))
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))

Tactic:
subst a'