awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
      ℕ)
trans :
  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 (β := β))) ≤
    sizeOf (xs.dedupKeys (β := β))
trans₁ :
  sizeOf (xs.dedupKeys (β := β)) ≤
    rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
      (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) xs
trans₂ : ℕ
⊢ 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 :
      ℕ)

Tactic:
trans
-- 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 :
      ℕ)
⊢ 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 (β := β))) ≤
    sizeOf (xs.dedupKeys (β := β))

Tactic:
apply sizeOf_kerase

Premises used: List.sizeOf_kerase
-- 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 :
      ℕ)
⊢ sizeOf (xs.dedupKeys (β := β)) ≤
    rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
      (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) xs

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

Tactic:
induction xs with
  | nil => simp [dedupKeys]
  | cons x xs =>
    simp only [dedupKeys_cons, kinsert_def, Nat.add_le_add_iff_left, Sigma.eta]
    trans
    · apply sizeOf_kerase
    · assumption

Premises used: List.dedupKeys_cons, Sigma.eta, List.kinsert_def, List.cons, List.sizeOf_kerase, Nat.add_le_add_iff_left, List.dedupKeys, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
⊢ kunion (β := β) [] l = l

Tactic:
rfl

Premises used: List.kunion, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
head : Sigma β
l : List (Sigma β)
rw : head :: l.kunion (β := β) (kerase (β := β) (head.fst (β := β)) []) = head :: l
rw₁ : head :: l.kunion (β := β) [] = head :: l
rw₂ rw₃ : head :: l = head :: l
⊢ (head :: l).kunion (β := β) [] = head :: l

Tactic:
rw [kunion, kerase_nil, kunion_nil]

Premises used: List.kerase_nil, List.kunion
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Sigma β
l₁ l₂ : List (Sigma β)
⊢ (s :: l₁).kunion (β := β) l₂ = s :: l₁.kunion (β := β) (kerase (β := β) (s.fst (β := β)) l₂)

Tactic:
rfl

Premises used: List.kunion, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₂ : List (Sigma β)
⊢ a ∈ (kunion (β := β) [] l₂).keys (β := β) ↔ Membership.mem (γ := List α) (keys (β := β) []) a ∨ a ∈ l₂.keys (β := β)

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion (β := β) l₂).keys (β := β) ↔ a ∈ l₁.keys (β := β) ∨ a ∈ l₂.keys (β := β)
l₂ : List (Sigma β)
pos :
  ∀ (h : a = s.fst (β := β)),
    a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
neg :
  ∀ (h : ¬a = s.fst (β := β)),
    a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
⊢ a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)

Tactic:
by_cases h : a = s.1

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion (β := β) l₂).keys (β := β) ↔ a ∈ l₁.keys (β := β) ∨ a ∈ l₂.keys (β := β)
l₂ : List (Sigma β)
h : a = s.fst (β := β)
⊢ a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion (β := β) l₂).keys (β := β) ↔ a ∈ l₁.keys (β := β) ∨ a ∈ l₂.keys (β := β)
l₂ : List (Sigma β)
h : ¬a = s.fst (β := β)
⊢ a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)

Tactic:
simp [h, ih]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion (β := β) l₂).keys (β := β) ↔ a ∈ l₁.keys (β := β) ∨ a ∈ l₂.keys (β := β)
l₂ : List (Sigma β)
pos :
  ∀ (h : a = s.fst (β := β)),
    a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
neg :
  ∀ (h : ¬a = s.fst (β := β)),
    a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
pos₁ :
  ∀ (h : a = s.fst (β := β)),
    a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
neg₁ :
  ∀ (h : ¬a = s.fst (β := β)),
    a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
⊢ a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)

Tactic:
by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nil :
  ∀ {l₂ : List (Sigma β)},
    a ∈ (kunion (β := β) [] l₂).keys (β := β) ↔ Membership.mem (γ := List α) (keys (β := β) []) a ∨ a ∈ l₂.keys (β := β)
cons :
  ∀ (s : Sigma β) (l₁ : List (Sigma β))
    (ih :
      ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion (β := β) l₂).keys (β := β) ↔ a ∈ l₁.keys (β := β) ∨ a ∈ l₂.keys (β := β))
    {l₂ : List (Sigma β)},
    a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
⊢ a ∈ (l₁.kunion (β := β) l₂).keys (β := β) ↔ a ∈ l₁.keys (β := β) ∨ a ∈ l₂.keys (β := β)

Tactic:
induction l₁ generalizing l₂ with
  | nil => simp
  | cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
l : List (Sigma β)
pos :
  ∀ (h : a = s.fst (β := β)),
    (kerase (β := β) a (s :: tail)).kunion (β := β) (kerase (β := β) a l) =
      kerase (β := β) a ((s :: tail).kunion (β := β) l)
neg :
  ∀ (h : ¬a = s.fst (β := β)),
    (kerase (β := β) a (s :: tail)).kunion (β := β) (kerase (β := β) a l) =
      kerase (β := β) a ((s :: tail).kunion (β := β) l)
⊢ (kerase (β := β) a (s :: tail)).kunion (β := β) (kerase (β := β) a l) =
    kerase (β := β) a ((s :: tail).kunion (β := β) l)

Tactic:
by_cases h : a = s.1

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

Tactic:
simp [h, kerase_comm a s.1 l, kunion_kerase]

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

Tactic:
simp [h, kerase_comm a s.1 l, kunion_kerase]

Premises used: List.kerase_comm, Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₂ : List (Sigma β)
nd₁ : NodupKeys (β := β) []
nd₂ : l₂.NodupKeys (β := β)
⊢ (List.kunion (β := β) [] l₂).NodupKeys (β := β)

Tactic:
simp only [nil_kunion, nd₂]

Premises used: List.nil_kunion
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys (β := β)) (nd₂ : l₂.NodupKeys (β := β)),
    (l₁.kunion (β := β) l₂).NodupKeys (β := β)
l₂ : List (Sigma β)
nd₁ : (s :: l₁).NodupKeys (β := β)
nd₂ : l₂.NodupKeys (β := β)
⊢ ¬s.fst (β := β) ∈ l₁.keys (β := β) ∧ l₁.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 α
s : Sigma β
l₁ : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys (β := β)) (nd₂ : l₂.NodupKeys (β := β)),
    (l₁.kunion (β := β) l₂).NodupKeys (β := β)
l₂ : List (Sigma β)
nd₂ : l₂.NodupKeys (β := β)
nd₁ : ¬s.fst (β := β) ∈ l₁.keys (β := β) ∧ l₁.NodupKeys (β := β)
⊢ ((s :: l₁).kunion (β := β) l₂).NodupKeys (β := β)

Tactic:
simp [nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]

Premises used: Sigma.fst, List.NodupKeys.kerase, And.right, And.left
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
inst : DecidableEq α
nd₁ : l₁.NodupKeys (β := β)
nd₂ : l₂.NodupKeys (β := β)
nil :
  ∀ {l₂ : List (Sigma β)} (nd₁ : NodupKeys (β := β) []) (nd₂ : l₂.NodupKeys (β := β)),
    (List.kunion (β := β) [] l₂).NodupKeys (β := β)
cons :
  ∀ (s : Sigma β) (l₁ : List (Sigma β))
    (ih :
      ∀ {l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys (β := β)) (nd₂ : l₂.NodupKeys (β := β)),
        (l₁.kunion (β := β) l₂).NodupKeys (β := β))
    {l₂ : List (Sigma β)} (nd₁ : (s :: l₁).NodupKeys (β := β)) (nd₂ : l₂.NodupKeys (β := β)),
    ((s :: l₁).kunion (β := β) l₂).NodupKeys (β := β)
⊢ (l₁.kunion (β := β) l₂).NodupKeys (β := β)

Tactic:
induction l₁ generalizing l₂ with
  | nil => simp only [nil_kunion, nd₂]
  | cons s l₁ ih =>
    simp only [nodupKeys_cons] at nd₁
    simp [nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]

Premises used: List.nodupKeys_cons, List.cons, List.nil_kunion, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ l : List (Sigma β)
⊢ kunion (β := β) [] l ~ kunion (β := β) [] l

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
hd : Sigma β
l₁_1 l₂_1 : List (Sigma β)
h : l₁_1 ~ l₂_1
ih : ∀ (l : List (Sigma β)), l₁_1.kunion (β := β) l ~ l₂_1.kunion (β := β) l
l : List (Sigma β)
⊢ (hd :: l₁_1).kunion (β := β) l ~ (hd :: l₂_1).kunion (β := β) l

Tactic:
simp [ih (List.kerase _ _)]

Premises used: List.kerase
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
s₁ s₂ : Sigma β
l_1 : List (Sigma β)
l : List (Sigma β)
⊢ (s₂ :: s₁ :: l_1).kunion (β := β) l ~ (s₁ :: s₂ :: l_1).kunion (β := β) l

Tactic:
simp [kerase_comm, Perm.swap]

Premises used: List.kerase_comm, List.Perm.swap
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
l₁_1 l₂_1 l₃ : List (Sigma β)
h : l₁_1 ~ l₂_1
h_1 : l₂_1 ~ l₃
ih₁₂ : ∀ (l : List (Sigma β)), l₁_1.kunion (β := β) l ~ l₂_1.kunion (β := β) l
ih₂₃ : ∀ (l : List (Sigma β)), l₂_1.kunion (β := β) l ~ l₃.kunion (β := β) l
l : List (Sigma β)
⊢ l₁_1.kunion (β := β) l ~ l₃.kunion (β := β) l

Tactic:
Perm.trans (ih₁₂ l) (ih₂₃ l)

Premises used: List.Perm.trans
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
l₁_1 l₂_1 l₃ : List (Sigma β)
h : l₁_1 ~ l₂_1
h_1 : l₂_1 ~ l₃
ih₁₂ : ∀ (l : List (Sigma β)), l₁_1.kunion (β := β) l ~ l₂_1.kunion (β := β) l
ih₂₃ : ∀ (l : List (Sigma β)), l₂_1.kunion (β := β) l ~ l₃.kunion (β := β) l
l : List (Sigma β)
⊢ l₁_1.kunion (β := β) l ~ l₃.kunion (β := β) l

Tactic:
exact Perm.trans (ih₁₂ l) (ih₂₃ l)

Premises used: List.Perm.trans
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
p : l₁ ~ l₂
l : List (Sigma β)
nil : ∀ (l : List (Sigma β)), kunion (β := β) [] l ~ kunion (β := β) [] l
cons :
  ∀ (hd : Sigma β) {l₁ l₂ : List (Sigma β)},
    l₁ ~ l₂ →
      ∀ (ih : ∀ (l : List (Sigma β)), l₁.kunion (β := β) l ~ l₂.kunion (β := β) l) (l : List (Sigma β)),
        (hd :: l₁).kunion (β := β) l ~ (hd :: l₂).kunion (β := β) l
swap :
  ∀ (s₁ s₂ : Sigma β) (l : List (Sigma β)) (l_1 : List (Sigma β)),
    (s₂ :: s₁ :: l).kunion (β := β) l_1 ~ (s₁ :: s₂ :: l).kunion (β := β) l_1
trans :
  ∀ {l₁ l₂ l₃ : List (Sigma β)},
    l₁ ~ l₂ →
      l₂ ~ l₃ →
        ∀ (ih₁₂ : ∀ (l : List (Sigma β)), l₁.kunion (β := β) l ~ l₂.kunion (β := β) l)
          (ih₂₃ : ∀ (l : List (Sigma β)), l₂.kunion (β := β) l ~ l₃.kunion (β := β) l) (l : List (Sigma β)),
          l₁.kunion (β := β) l ~ l₃.kunion (β := β) l
⊢ l₁.kunion (β := β) l ~ l₂.kunion (β := β) l

Tactic:
induction p generalizing l with
  | nil => rfl
  | cons hd _ ih =>
    simp [ih (List.kerase _ _)]
  | swap s₁ s₂ l => simp [kerase_comm, Perm.swap]
  | trans _ _ ih₁₂ ih₂₃ => exact Perm.trans (ih₁₂ l) (ih₂₃ l)

Premises used: List.kerase_comm, List.Perm.cons, List.Perm.swap, List.Perm.trans, List.Perm.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ l₃ l₄ : List (Sigma β)
nd₃ : l₃.NodupKeys (β := β)
p₁₂ : l₁ ~ l₂
p₃₄ : l₃ ~ l₄
⊢ l₁.kunion (β := β) l₃ ~ l₂.kunion (β := β) l₄

Tactic:
(p₁₂.kunion_right l₃).trans (p₃₄.kunion_left l₂ nd₃)

Premises used: List.Perm.kunion_left, List.Perm.kunion_right, List.Perm.trans
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₂ : List (Sigma β)
h : Membership.mem (γ := List α) (keys (β := β) []) a
⊢ dlookup (β := β) a (kunion (β := β) [] l₂) = dlookup (β := β) a []

Tactic:
simp at h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ (s :: tail).keys (β := β)
⊢ a = s.fst (β := β) ∨ a ∈ tail.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 : α
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a = s.fst (β := β) ∨ a ∈ tail.keys (β := β)
cons :
  ∀
    (ih :
      ∀ {l₂ : List (Sigma β)} (h : s.fst (β := β) ∈ tail.keys (β := β)),
        dlookup (β := β) (s.fst (β := β)) (tail.kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) tail),
    dlookup (β := β) (s.fst (β := β)) ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) (s :: tail)
cons₁ :
  ∀ (h : a ∈ tail.keys (β := β)), dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)
⊢ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)

Tactic:
rcases h with rfl | h

Premises used: rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Sigma β
tail : List (Sigma β)
l₂ : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : s.fst (β := β) ∈ tail.keys (β := β)),
    dlookup (β := β) (s.fst (β := β)) (tail.kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) tail
cons :
  ∀ (a' : α) (snd : β a')
    (ih :
      ∀ {l₂ : List (Sigma β)} (h : (Sigma.mk (β := β) a' snd).fst (β := β) ∈ tail.keys (β := β)),
        dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) (tail.kunion (β := β) l₂) =
          dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) tail),
    dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) =
      dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) (Sigma.mk (β := β) a' snd :: tail)
⊢ dlookup (β := β) (s.fst (β := β)) ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) (s :: tail)

Tactic:
obtain ⟨a'⟩ := s
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
cons :
  ∀ (a' : α) (snd : β a'),
    dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) =
      dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
⊢ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)

Tactic:
obtain ⟨a'⟩ := s
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
tail : List (Sigma β)
l₂ : List (Sigma β)
a' : α
snd : β a'
ih :
  ∀ {l₂ : List (Sigma β)} (h : (Sigma.mk (β := β) a' snd).fst (β := β) ∈ tail.keys (β := β)),
    dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) (tail.kunion (β := β) l₂) =
      dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) tail
⊢ dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) =
    dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) (Sigma.mk (β := β) a' snd :: tail)

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
a' : α
snd : β a'
pos :
  ∀ (h' : a = a'),
    dlookup (β := β) a
        (Sigma.mk (β := β) a' snd ::
          tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
      dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
neg :
  ∀ (h' : ¬a = a'),
    dlookup (β := β) a
        (Sigma.mk (β := β) a' snd ::
          tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
      dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
⊢ dlookup (β := β) a
      (Sigma.mk (β := β) a' snd ::
        tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)

Tactic:
by_cases h' : a = a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
a' : α
snd : β a'
h' : a = a'
pos :
  ∀ (snd : β a),
    dlookup (β := β) a
        (Sigma.mk (β := β) a snd ::
          tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a snd).fst (β := β)) l₂)) =
      dlookup (β := β) a (Sigma.mk (β := β) a snd :: tail)
⊢ dlookup (β := β) a
      (Sigma.mk (β := β) a' snd ::
        tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)

Tactic:
subst h'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
snd : β a
⊢ dlookup (β := β) a
      (Sigma.mk (β := β) a snd :: tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a snd :: tail)

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
a' : α
snd : β a'
h' : ¬a = a'
⊢ dlookup (β := β) a
      (Sigma.mk (β := β) a' snd ::
        tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)

Tactic:
simp [h', ih h]