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 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)
have 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)
Tactic: substs h₁ h₂
Cleared hypotheses: a, h, ih, ah, bh, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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)
have neg : ∀ (bh : β a) (h₂ : ¬a' = a),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) a bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) a bh :: tl)
Tactic: subst h₁
Cleared hypotheses: ah, bh, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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)
have pos : ∀ (bh : β a') (h₁ : ¬a = a'),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) a' bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' bh :: tl)
Tactic: subst h₂
Cleared hypotheses: ah, bh, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
l : List (Sigma β)
h : a ≠ a'
⊢ dlookup (β := β) a (kerase (β := β) a' l) = dlookup (β := β) a l
have nil : Eq.{v + 1} (α := Option (β a)) (dlookup (β := β) a (kerase (β := β) a' [])) (dlookup (β := β) a [])
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 [])
⊢ dlookup (β := β) a (kerase (β := β) a' l) = dlookup (β := β) a l
have 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)
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys (β := β)
⊢ kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂
have if : ∀ (h₂ : a = s.fst (β := β)), 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]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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₂
⊢ kerase (β := β) a (s :: l₁ ++ l₂) = kerase (β := β) a (s :: l₁) ++ l₂
have if₁ : ∀ (h₂ : ¬a = s.fst (β := β)), 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]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
head : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a ∈ (head :: l₁).keys (β := β)
⊢ kerase (β := β) a (head :: l₁ ++ l₂) = head :: l₁ ++ kerase (β := β) a l₂
have h₁ : ¬a = head.fst (β := β) ∧ ¬a ∈ l₁.keys (β := β)
Tactic: simp only [keys_cons, mem_cons, not_or] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
x : α
xs : List (Sigma β)
⊢ sizeOf (kerase (β := β) x xs) ≤ 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) (kerase (β := β) x xs) :
    ℕ)
  (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
      (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) xs :
    ℕ)
Tactic: 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 : α
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 :
      ℕ)
⊢ 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) :
      ℕ)
have 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) :
      ℕ)
Tactic: by_cases x = y.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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) :
        ℕ)
⊢ 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) :
      ℕ)
have 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) :
      ℕ)
Tactic: by_cases x = y.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
x : α
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)
        (kerase (β := β) x xs) :
      ℕ)
    (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) (kerase (β := β) x []) :
    ℕ)
  (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
  | cons y ys => by_cases x = y.1 <;> simp [*]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
inst_1 : SizeOf (Sigma β)
x : α
xs : List (Sigma β)
nil :
  LE.le (α := ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
        (kerase (β := β) x []) :
      ℕ)
    (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
        (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) [] :
      ℕ)
⊢ 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 :
      ℕ)
have cons : ∀ (y : Sigma β) (ys : List (Sigma β)),
  LE.le (α := ℕ)
      (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
          (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
          (kerase (β := β) x ys) :
        ℕ)
      (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
          (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) ys :
        ℕ) →
    LE.le (α := ℕ)
      (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
          (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih)
          (kerase (β := β) x (y :: ys)) :
        ℕ)
      (rec (motive := fun (t : List (Sigma β)) ↦ ℕ) 1
          (fun (head : Sigma β) (tail : List (Sigma β)) (tail_ih : ℕ) ↦ 1 + sizeOf head + tail_ih) (y :: ys) :
        ℕ)
Tactic: induction xs with
  | nil => simp
  | cons y ys => by_cases x = y.1 <;> simp [*]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)
have pos : ∀ (h : a = a'), a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)
Tactic: by_cases h : a = a'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
pos : ∀ (h : a = a'), a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)
⊢ a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)
have neg : ∀ (h : ¬a = a'), a ∈ (kinsert (β := β) a' b' l).keys (β := β) ↔ a = a' ∨ a ∈ l.keys (β := β)
Tactic: by_cases h : a = a'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ kextract (β := β) a (Sigma.mk (β := β) a' b :: l) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
have simp : (if h : a' = a then (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b sorry), l)
  else ((kextract (β := β) a l).fst, Sigma.mk (β := β) a' b :: (kextract (β := β) a l).snd)) =
  (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
Tactic: simp only [kextract]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (if h : a' = a then (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b ⋯), l)
    else ((kextract (β := β) a l).fst, Sigma.mk (β := β) a' b :: (kextract (β := β) a l).snd)) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
have pos : ∀ (h : a' = a),
  (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b sorry), l) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
pos :
  ∀ (h : a' = a),
    (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b ⋯), l) =
      (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
⊢ (if h : a' = a then (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b ⋯), l)
    else ((kextract (β := β) a l).fst, Sigma.mk (β := β) a' b :: (kextract (β := β) a l).snd)) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
have neg : ∀ (h : ¬a' = a),
  ((kextract (β := β) a l).fst, Sigma.mk (β := β) a' b :: (kextract (β := β) a l).snd) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a' = a
⊢ (some (Eq.rec (motive := fun (x : α) (x_1 : a' = x) ↦ β x) b ⋯), l) =
    (dlookup (β := β) a (Sigma.mk (β := β) a' b :: l), kerase (β := β) a (Sigma.mk (β := β) a' b :: l))
have pos : ∀ (b : β a),
  (some (Eq.rec (motive := fun (x : α) (x_1 : a = x) ↦ β x) b sorry), l) =
    (dlookup (β := β) a (Sigma.mk (β := β) a b :: l), kerase (β := β) a (Sigma.mk (β := β) a b :: l))
Tactic: subst a'
Cleared hypotheses: a', b, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
⊢ NodupKeys (β := β) (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) [] l)
have generalize : ∀ (l' : List (Sigma β)) (hl : [] = l'),
  (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' l).NodupKeys (β := β)
Tactic: generalize hl : nil = l'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ l'.NodupKeys (β := β)
have rw : NodupKeys (β := β) []
Tactic: rw [← hl]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' l).NodupKeys (β := β)
have this : l'.NodupKeys (β := β)
Tactic: have : NodupKeys l' := by
    rw [← hl]
    apply nodup_nil
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
x : Sigma β
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' (x :: xs)).NodupKeys (β := β)
have cons : ∀ (fst : α) (snd : β fst),
  (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l'
        (Sigma.mk (β := β) fst snd :: xs)).NodupKeys
    (β := β)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l'
        (Sigma.mk (β := β) fst snd :: xs)).NodupKeys
    (β := β)
have cons : ¬fst ∈
      (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
        (β := β) ∧
  (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
    (β := β)
Tactic: simp only [foldr_cons, kinsert_def, nodupKeys_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
⊢ ¬fst ∈
        (kerase (β := β) fst
              (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
          (β := β) ∧
    (kerase (β := β) fst
          (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
      (β := β)
have cons : ¬fst ∈
    (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
      (β := β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
cons :
  ¬fst ∈
      (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
        (β := β)
⊢ ¬fst ∈
        (kerase (β := β) fst
              (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
          (β := β) ∧
    (kerase (β := β) fst
          (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
      (β := β)
have cons₁ : (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).NodupKeys
  (β := β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
xs : List (Sigma β)
l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)
fst : α
snd : β fst
⊢ ¬fst ∈
      (kerase (β := β) fst (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs)).keys
        (β := β)
have cons : ¬fst ∈ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).keys (β := β).erase fst
Tactic: simp only [keys_kerase]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' l).NodupKeys (β := β)
have nil : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' []).NodupKeys (β := β)
Tactic: induction l with
  | nil => apply this
  | cons x xs l_ih =>
    cases x
    simp only [foldr_cons, kinsert_def, nodupKeys_cons]
    constructor
    · simp only [keys_kerase]
      apply l_ih.not_mem_erase
    · exact l_ih.kerase _
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
this : l'.NodupKeys (β := β)
nil : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' []).NodupKeys (β := β)
⊢ (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' l).NodupKeys (β := β)
have cons : ∀ (x : Sigma β) (xs : List (Sigma β))
  (l_ih : (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' xs).NodupKeys (β := β)),
  (foldr (fun (x : Sigma β) ↦ kinsert (β := β) (x.fst (β := β)) (x.snd (β := β))) l' (x :: xs)).NodupKeys (β := β)
Tactic: induction l with
  | nil => apply this
  | cons x xs l_ih =>
    cases x
    simp only [foldr_cons, kinsert_def, nodupKeys_cons]
    constructor
    · simp only [keys_kerase]
      apply l_ih.not_mem_erase
    · exact l_ih.kerase _
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
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)
have cons : ∀ (a' : α) (b : β a'),
  dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
Tactic: obtain ⟨a', b⟩ := l_hd
Cleared hypotheses: l_hd
-- 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'
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
have pos : ∀ (h : a = a'),
  dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
Tactic: by_cases h : a = a'
-- 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'
pos :
  ∀ (h : a = a'),
    dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
      dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
⊢ dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
have neg : ∀ (h : ¬a = a'),
  dlookup (β := β) a ((Sigma.mk (β := β) a' b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' b :: tail)
Tactic: by_cases h : a = a'
-- 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 pos : ∀ (b : β a),
  dlookup (β := β) a ((Sigma.mk (β := β) a b :: tail).dedupKeys (β := β)) =
    dlookup (β := β) a (Sigma.mk (β := β) a b :: tail)
Tactic: subst a'
Cleared hypotheses: a', b, h