awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β)
⊢ hd :: tl = [] ++ Sigma.mk (β := β) (hd.fst (β := β)) (hd.snd (β := β)) :: tl
have 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
Tactic: cases hd
Cleared hypotheses: hd, ih, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
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 (β := β)
⊢ ∃ (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₂
have h₁ : a = hd.fst (β := β) ∨ a ∈ tl.keys (β := β)
Tactic: simp only [keys_cons, mem_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β)
⊢ ∃ (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₂
have 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₂
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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₂
⊢ ∃ (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₂
have 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₂
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
have 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₂
Tactic: rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 = hd :: tl₁ ++ Sigma.mk (β := β) a b :: tl₂
have rw : hd :: (tl₁ ++ Sigma.mk (β := β) a b :: tl₂) = hd :: tl₁ ++ Sigma.mk (β := β) a b :: tl₂
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : a ∈ l.keys (β := β)
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ l = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a l = l₁ ++ l₂
have 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₂
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₃]⟩
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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₂
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ l = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a l = l₁ ++ l₂
have 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₂
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₃]⟩
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
⊢ (kerase (β := β) a l).keys (β := β) = l.keys (β := β).erase a
have rw : map (Sigma.fst (β := β)) (eraseP (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) l) =
  map (Sigma.fst (β := β)) (eraseP (fun (x : Sigma β) ↦ a == x.fst (β := β)) l)
Tactic: rw [keys, kerase, erase_eq_eraseP, eraseP_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
l : List (Sigma β)
⊢ kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
have pos : ∀ (h : a = a'), kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
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' : α
l : List (Sigma β)
pos : ∀ (h : a = a'), kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
⊢ kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
have neg : ∀ (h : ¬a = a'), kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
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' : α
l : List (Sigma β)
h : a = a'
⊢ kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
have pos : kerase (β := β) a (kerase (β := β) a l) = kerase (β := β) a (kerase (β := β) a l)
Tactic: subst a'
Cleared hypotheses: a', h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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)
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
have pos : a' = x.fst (β := β) →
  kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
Tactic: by_cases a' = x.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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))
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
have neg : ¬a' = x.fst (β := β) →
  kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
Tactic: by_cases a' = x.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β)
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
have 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))
Tactic: subst a'
Cleared hypotheses: a', h, tail_ih, h_1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β)
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
have pos : ∀ (h' : a = x.fst (β := β)),
  kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
Tactic: by_cases h' : a = x.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih : kerase (β := β) a (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) a xs)
h_1 : ¬a' = x.fst (β := β)
pos :
  ∀ (h' : a = x.fst (β := β)),
    kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
have neg : ∀ (h' : ¬a = x.fst (β := β)),
  kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
Tactic: by_cases h' : a = x.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih : kerase (β := β) a (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) a xs)
h_1 : ¬a' = x.fst (β := β)
h' : a = x.fst (β := β)
⊢ kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
have pos : ∀ (h : ¬x.fst (β := β) = a'),
  kerase (β := β) (x.fst (β := β)) (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) (x.fst (β := β)) xs) →
    kerase (β := β) (x.fst (β := β)) (kerase (β := β) a' (x :: xs)) =
      kerase (β := β) a' (kerase (β := β) (x.fst (β := β)) (x :: xs))
Tactic: subst a
Cleared hypotheses: a, h, tail_ih, 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'
⊢ kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
have neg : Eq (α := List (Sigma β)) (kerase (β := β) a (kerase (β := β) a' [])) (kerase (β := β) a' (kerase (β := β) a []))
Tactic: induction l with
  | nil => rfl
  | cons x xs =>
    by_cases a' = x.1
    · subst a'
      simp [kerase_cons_ne h, kerase_cons_eq rfl]
    by_cases h' : a = x.1
    · subst a
      simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]
    · simp [kerase_cons_ne, *]
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'
neg : Eq (α := List (Sigma β)) (kerase (β := β) a (kerase (β := β) a' [])) (kerase (β := β) a' (kerase (β := β) a []))
⊢ kerase (β := β) a (kerase (β := β) a' l) = kerase (β := β) a' (kerase (β := β) a l)
have neg₁ : ∀ (x : Sigma β) (xs : List (Sigma β)),
  kerase (β := β) a (kerase (β := β) a' xs) = kerase (β := β) a' (kerase (β := β) a xs) →
    kerase (β := β) a (kerase (β := β) a' (x :: xs)) = kerase (β := β) a' (kerase (β := β) a (x :: xs))
Tactic: induction l with
  | nil => rfl
  | cons x xs =>
    by_cases a' = x.1
    · subst a'
      simp [kerase_cons_ne h, kerase_cons_eq rfl]
    by_cases h' : a = x.1
    · subst a
      simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]
    · simp [kerase_cons_ne, *]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
⊢ l₁ ~ l₂ → List.kerase (β := β) a l₁ ~ List.kerase (β := β) a l₂
have H : Pairwise (fun (a_1 b : Sigma β) ↦ decide (a = a_1.fst (β := β)) = true → decide (a = b.fst (β := β)) = true → False) l₁
Tactic: apply Perm.eraseP
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
⊢ Pairwise (fun (a_1 b : Sigma β) ↦ decide (a = a_1.fst (β := β)) = true → decide (a = b.fst (β := β)) = true → False)
    l₁
have H : ∀ {a_1 b : Sigma β},
  a_1.fst (β := β) ≠ b.fst (β := β) → decide (a = a_1.fst (β := β)) = true → decide (a = b.fst (β := β)) = true → False
Tactic: apply (nodupKeys_iff_pairwise.1 nd).imp
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β)
nd : (hd :: tl).NodupKeys (β := β)
⊢ ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
have nd₁ : ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.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
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β)
nd : ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.NodupKeys (β := β)
⊢ ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
have pos : ∀ (h : a = hd.fst (β := β)), ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
Tactic: by_cases h : a = hd.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β)
nd : ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.NodupKeys (β := β)
pos : ∀ (h : a = hd.fst (β := β)), ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
⊢ ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
have neg : ∀ (h : ¬a = hd.fst (β := β)), ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
Tactic: by_cases h : a = hd.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β)
nd : ¬hd.fst (β := β) ∈ tl.keys (β := β) ∧ tl.NodupKeys (β := β)
h : a = hd.fst (β := β)
⊢ ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
have pos : ∀ (ih : ∀ (nd : tl.NodupKeys (β := β)), ¬hd.fst (β := β) ∈ (kerase (β := β) (hd.fst (β := β)) tl).keys (β := β)),
  ¬hd.fst (β := β) ∈ (kerase (β := β) (hd.fst (β := β)) (hd :: tl)).keys (β := β)
Tactic: subst h
Cleared hypotheses: a, ih, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nd : l.NodupKeys (β := β)
⊢ ¬a ∈ (kerase (β := β) a l).keys (β := β)
have nil : ∀ (nd : NodupKeys (β := β) []), ¬a ∈ keys (β := β) (kerase (β := β) a [])
Tactic: induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [nodupKeys_cons] at nd
    by_cases h : a = hd.1
    · subst h
      simp [nd.1]
    · simp [h, ih nd.2]
Cleared hypotheses: l, nd
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nd : l.NodupKeys (β := β)
nil : ∀ (nd : NodupKeys (β := β) []), ¬a ∈ keys (β := β) (kerase (β := β) a [])
⊢ ¬a ∈ (kerase (β := β) a l).keys (β := β)
have cons : ∀ (hd : Sigma β) (tl : List (Sigma β)) (ih : ∀ (nd : tl.NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a tl).keys (β := β))
  (nd : (hd :: tl).NodupKeys (β := β)), ¬a ∈ (kerase (β := β) a (hd :: tl)).keys (β := β)
Tactic: induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [nodupKeys_cons] at nd
    by_cases h : a = hd.1
    · subst h
      simp [nd.1]
    · simp [h, ih nd.2]
Cleared hypotheses: l, nd
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
h : a ≠ a'
hd : Sigma β
tl : List (Sigma β)
ih : dlookup (β := β) a (kerase (β := β) a' tl) = dlookup (β := β) a tl
⊢ dlookup (β := β) a (kerase (β := β) a' (hd :: tl)) = dlookup (β := β) a (hd :: tl)
have cons : ∀ (ah : α) (bh : β ah),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
Tactic: obtain ⟨ah, bh⟩ := hd
Cleared hypotheses: hd
-- 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
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
have pos : ∀ (h₁ : a = ah),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
Tactic: by_cases h₁ : a = ah
-- 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
pos :
  ∀ (h₁ : a = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
have neg : ∀ (h₁ : ¬a = ah),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
Tactic: by_cases h₁ : a = ah
-- 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
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
have pos : ∀ (h₂ : a' = ah),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
Tactic: by_cases h₂ : a' = ah
-- 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
pos :
  ∀ (h₂ : a' = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
have neg : ∀ (h₂ : ¬a' = ah),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
Tactic: by_cases h₂ : a' = ah
-- 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
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
have pos : ∀ (h₂ : a' = ah),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
Tactic: by_cases h₂ : a' = ah
-- 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
pos :
  ∀ (h₂ : a' = ah),
    dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
      dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
⊢ dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
have neg : ∀ (h₂ : ¬a' = ah),
  dlookup (β := β) a (kerase (β := β) a' (Sigma.mk (β := β) ah bh :: tl)) =
    dlookup (β := β) a (Sigma.mk (β := β) ah bh :: tl)
Tactic: by_cases h₂ : a' = ah