awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
l_ih : dlookup (β := β) a (tail.dedupKeys (β := β)) = dlookup (β := β) a tail
b : β a
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
have pos : dlookup (β := β) a
    (kinsert (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) ((Sigma.mk (β := β) a b).snd (β := β))
      (tail.dedupKeys (β := β))) =
  dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
Tactic: rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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)
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
have pos₁ : some ((Sigma.mk (β := β) a b).snd (β := β)) = dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
Tactic: rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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)
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
have pos₂ : some ((Sigma.mk (β := β) a b).snd (β := β)) = some b
Tactic: rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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'
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
have neg : a ≠ (Sigma.mk (β := β) a' b).fst (β := β)
Tactic: rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
⊢ dlookup (β := β) a (l.dedupKeys (β := β)) = dlookup (β := β) a l
have nil : Eq.{v + 1} (α := Option (β a)) (dlookup (β := β) a (dedupKeys (β := β) [])) (dlookup (β := β) a [])
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
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nil : Eq.{v + 1} (α := Option (β a)) (dlookup (β := β) a (dedupKeys (β := β) [])) (dlookup (β := β) a [])
⊢ dlookup (β := β) a (l.dedupKeys (β := β)) = dlookup (β := β) a l
have 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)
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
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
xs : List (Sigma β)
⊢ sizeOf (xs.dedupKeys (β := β)) ≤ sizeOf xs
have 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 :
    ℕ)
Tactic: simp only [SizeOf.sizeOf, _sizeOf_1]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 :
      ℕ)
⊢ 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) :
      ℕ)
have 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 :
    ℕ)
Tactic: simp only [dedupKeys_cons, kinsert_def, Nat.add_le_add_iff_left, Sigma.eta]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 :
      ℕ)
⊢ 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 :
      ℕ)
have 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 (β := β))
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β))
⊢ 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 :
      ℕ)
have 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
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ 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 :
      ℕ)
have trans₂ : ℕ
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (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 :
      ℕ)
have 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) [] :
    ℕ)
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
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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) [] :
      ℕ)
⊢ 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 :
      ℕ)
have 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) :
        ℕ)
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
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
head : Sigma β
l : List (Sigma β)
⊢ (head :: l).kunion (β := β) [] = head :: l
have rw : head :: l.kunion (β := β) (kerase (β := β) (head.fst (β := β)) []) = head :: l
Tactic: rw [kunion, kerase_nil, kunion_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
head : Sigma β
l : List (Sigma β)
rw : head :: l.kunion (β := β) (kerase (β := β) (head.fst (β := β)) []) = head :: l
⊢ (head :: l).kunion (β := β) [] = head :: l
have rw₁ : head :: l.kunion (β := β) [] = head :: l
Tactic: rw [kunion, kerase_nil, kunion_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ (head :: l).kunion (β := β) [] = head :: l
have rw₂ : head :: l = head :: l
Tactic: rw [kunion, kerase_nil, kunion_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 β)
⊢ a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
have pos : ∀ (h : a = s.fst (β := β)),
  a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
Tactic: by_cases h : a = s.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β)
⊢ a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
have neg : ∀ (h : ¬a = s.fst (β := β)),
  a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
Tactic: by_cases h : a = s.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 β)
⊢ a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
have pos : ∀ (h : a = s.fst (β := β)),
  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]]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β)
⊢ a ∈ ((s :: l₁).kunion (β := β) l₂).keys (β := β) ↔ a ∈ (s :: l₁).keys (β := β) ∨ a ∈ l₂.keys (β := β)
have neg : ∀ (h : ¬a = s.fst (β := β)),
  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]]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
⊢ a ∈ (l₁.kunion (β := β) l₂).keys (β := β) ↔ a ∈ l₁.keys (β := β) ∨ a ∈ l₂.keys (β := β)
have nil : ∀ {l₂ : List (Sigma β)},
  a ∈ (kunion (β := β) [] l₂).keys (β := β) ↔ Membership.mem (γ := List α) (keys (β := β) []) a ∨ 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]]
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β)
⊢ a ∈ (l₁.kunion (β := β) l₂).keys (β := β) ↔ a ∈ l₁.keys (β := β) ∨ a ∈ l₂.keys (β := β)
have 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 (β := β)
Tactic: induction l₁ generalizing l₂ with
  | nil => simp
  | cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
l : List (Sigma β)
⊢ (kerase (β := β) a (s :: tail)).kunion (β := β) (kerase (β := β) a l) =
    kerase (β := β) a ((s :: tail).kunion (β := β) l)
have pos : ∀ (h : a = s.fst (β := β)),
  (kerase (β := β) a (s :: tail)).kunion (β := β) (kerase (β := β) a l) =
    kerase (β := β) a ((s :: tail).kunion (β := β) l)
Tactic: by_cases h : a = s.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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)
⊢ (kerase (β := β) a (s :: tail)).kunion (β := β) (kerase (β := β) a l) =
    kerase (β := β) a ((s :: tail).kunion (β := β) l)
have neg : ∀ (h : ¬a = s.fst (β := β)),
  (kerase (β := β) a (s :: tail)).kunion (β := β) (kerase (β := β) a l) =
    kerase (β := β) a ((s :: tail).kunion (β := β) l)
Tactic: by_cases h : a = s.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
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 :: l₁).kunion (β := β) l₂).NodupKeys (β := β)
have nd₃ : ¬s.fst (β := β) ∈ l₁.keys (β := β) ∧ l₁.NodupKeys (β := β)
Tactic: simp only [nodupKeys_cons] at nd₁
Cleared hypotheses: nd₁
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
inst : DecidableEq α
nd₁ : l₁.NodupKeys (β := β)
nd₂ : l₂.NodupKeys (β := β)
⊢ (l₁.kunion (β := β) l₂).NodupKeys (β := β)
have nil : ∀ {l₂ : List (Sigma β)} (nd₁ : NodupKeys (β := β) []) (nd₂ : l₂.NodupKeys (β := β)),
  (List.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)]
Cleared hypotheses: l₁, l₂, nd₁, nd₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β)
⊢ (l₁.kunion (β := β) l₂).NodupKeys (β := β)
have 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 (β := β)
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)]
Cleared hypotheses: l₁, l₂, nd₁, nd₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
p : l₁ ~ l₂
l : List (Sigma β)
⊢ l₁.kunion (β := β) l ~ l₂.kunion (β := β) l
have nil : ∀ (l : List (Sigma β)), kunion (β := β) [] 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)
Cleared hypotheses: p, l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ l₁.kunion (β := β) l ~ l₂.kunion (β := β) l
have 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
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)
Cleared hypotheses: p, l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ l₁.kunion (β := β) l ~ l₂.kunion (β := β) l
have swap : ∀ (s₁ s₂ : Sigma β) (l : List (Sigma β)) (l_1 : List (Sigma β)),
  (s₂ :: s₁ :: l).kunion (β := β) l_1 ~ (s₁ :: s₂ :: l).kunion (β := β) l_1
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)
Cleared hypotheses: p, l