awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
rw :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
rw₁ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
have rw₂ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
Tactic: rw [kerase_cons_ne, kerase_cons_ne, kerase_comm]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
have rw : Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
  Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
Tactic: rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
    [apply Perm.swap; exact h; exact h.symm]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
rw :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
have rw₁ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
Tactic: rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
    [apply Perm.swap; exact h; exact h.symm]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
rw :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
rw₁ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
have rw₂ : Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
  Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
Tactic: rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
    [apply Perm.swap; exact h; exact h.symm]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
rw :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
rw₁ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
rw₂ :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
have rw₃ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
Tactic: rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
    [apply Perm.swap; exact h; exact h.symm]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
rw :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
rw₁ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
rw₂ :
  Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a' (kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
rw₃ : a ≠ (Sigma.mk (β := β) a' b').fst (β := β)
rw₄ : a' ≠ (Sigma.mk (β := β) a b).fst (β := β)
⊢ Sigma.mk (β := β) a' b' :: kerase (β := β) a' (Sigma.mk (β := β) a b :: kerase (β := β) a (s.entries (β := β))) ~
    Sigma.mk (β := β) a b :: kerase (β := β) a (Sigma.mk (β := β) a' b' :: kerase (β := β) a' (s.entries (β := β)))
have rw₅ : Sigma.mk (β := β) a' b' :: Sigma.mk (β := β) a b :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β))) ~
  Sigma.mk (β := β) a b :: Sigma.mk (β := β) a' b' :: kerase (β := β) a (kerase (β := β) a' (s.entries (β := β)))
Tactic: rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
    [apply Perm.swap; exact h; exact h.symm]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys (β := β)
⊢ C (mk (β := β) (c :: l) h)
have rw : C (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l sorry))
Tactic: rw [mk_cons_eq_insert]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys (β := β)
⊢ C (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l ⋯))
have refine : ¬c.fst (β := β) ∈ mk (β := β) l sorry
Tactic: refine IH _ _ _ ?_ (insertRec H0 IH _)
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : AList β
H0 : True
⊢ True
have IH : ∀ (a : α) (b : β a) (l : AList β), ¬a ∈ l → True → True
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
⊢ insertRec (β := β) (C := C) H0 IH ∅ = H0
have change : insertRec (β := β) (C := C) H0 IH (mk (β := β) [] sorry) = H0
Tactic: change @insertRec α β _ C H0 IH ⟨[], _⟩ = H0
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
⊢ insertRec (β := β) (C := C) H0 IH (mk (β := β) [] ⋯) = H0
have rw : H0 = H0
Tactic: rw [insertRec]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : AList β
h : ¬c.fst (β := β) ∈ l
⊢ insertRec (β := β) (C := C) H0 IH (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) l) =
    IH (c.fst (β := β)) (c.snd (β := β)) l h (insertRec (β := β) (C := C) H0 IH l)
have obtain : ∀ (l : List (Sigma β)) (hl : l.NodupKeys (β := β)) (h : ¬c.fst (β := β) ∈ mk (β := β) l hl),
  insertRec (β := β) (C := C) H0 IH (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl)) =
    IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl))
Tactic: obtain ⟨l, hl⟩ := l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys (β := β)
h : ¬c.fst (β := β) ∈ mk (β := β) l hl
this :
  HEq (α := C (mk (β := β) (c :: l) ⋯)) (insertRec (β := β) (C := C) H0 IH (mk (β := β) (c :: l) ⋯))
    (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
⊢ insertRec (β := β) (C := C) H0 IH (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl)) =
    IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl))
have mk : ∀ (fst : α) (snd : β fst) (h : ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ mk (β := β) l hl)
  (this :
    HEq (α := C (mk (β := β) (Sigma.mk (β := β) fst snd :: l) sorry))
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) (Sigma.mk (β := β) fst snd :: l) sorry))
      (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
        (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))),
  insertRec (β := β) (C := C) H0 IH
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)) =
    IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl))
Tactic: cases c
Cleared hypotheses: c, h, this
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
l : List (Sigma β)
hl : l.NodupKeys (β := β)
fst : α
snd : β fst
h : ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ mk (β := β) l hl
this :
  HEq (α := C (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (insertRec (β := β) (C := C) H0 IH (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
⊢ insertRec (β := β) (C := C) H0 IH
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)) =
    IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl))
have mk : HEq (α :=
  C
    (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
      (mk (β := β) l hl)))
  (insertRec (β := β) (C := C) H0 IH
    (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
      (mk (β := β) l hl)))
  (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
    (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
Tactic: apply eq_of_heq
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
l : List (Sigma β)
hl : l.NodupKeys (β := β)
fst : α
snd : β fst
h : ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ mk (β := β) l hl
this :
  HEq (α := C (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (insertRec (β := β) (C := C) H0 IH (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
⊢ HEq (α :=
    C
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)))
    (insertRec (β := β) (C := C) H0 IH
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
have h₁ : (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)).entries
    (β := β) =
  Sigma.mk (β := β) fst snd :: l
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
l : List (Sigma β)
hl : l.NodupKeys (β := β)
fst : α
snd : β fst
h : ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ mk (β := β) l hl
this :
  HEq (α := C (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (insertRec (β := β) (C := C) H0 IH (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
h₁ :
  (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
          (mk (β := β) l hl)).entries
      (β := β) =
    Sigma.mk (β := β) fst snd :: l
⊢ HEq (α :=
    C
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)))
    (insertRec (β := β) (C := C) H0 IH
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
have h₂ : C
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)) =
    C (mk (β := β) (Sigma.mk (β := β) fst snd :: l) sorry) →
  (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
          (mk (β := β) l hl)).entries
      (β := β) =
    Sigma.mk (β := β) fst snd :: l
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
l : List (Sigma β)
hl : l.NodupKeys (β := β)
fst : α
snd : β fst
h : ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ mk (β := β) l hl
this :
  HEq (α := C (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (insertRec (β := β) (C := C) H0 IH (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
⊢ (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
          (mk (β := β) l hl)).entries
      (β := β) =
    Sigma.mk (β := β) fst snd :: l
have h₁ : (mk (β := β)
        (Sigma.mk (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) ::
          (mk (β := β) l hl).entries (β := β))
        sorry).entries
    (β := β) =
  Sigma.mk (β := β) fst snd :: l
Tactic: rw [insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
l : List (Sigma β)
hl : l.NodupKeys (β := β)
fst : α
snd : β fst
h : ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ mk (β := β) l hl
this :
  HEq (α := C (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (insertRec (β := β) (C := C) H0 IH (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
e_1 :
  C
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (mk (β := β) l hl)) =
    C (mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯)
⊢ (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
          (mk (β := β) l hl)).entries
      (β := β) =
    Sigma.mk (β := β) fst snd :: l
have h₁ : (mk (β := β)
        (Sigma.mk (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) ::
          (mk (β := β) l hl).entries (β := β))
        sorry).entries
    (β := β) =
  Sigma.mk (β := β) fst snd :: l
Tactic: rw [insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys (β := β)
h : ¬c.fst (β := β) ∈ mk (β := β) l hl
⊢ insertRec (β := β) (C := C) H0 IH (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl)) =
    IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl))
have suffices : HEq (α := C (mk (β := β) (c :: l) sorry)) (insertRec (β := β) (C := C) H0 IH (mk (β := β) (c :: l) sorry))
  (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
Tactic: suffices @insertRec α β _ C H0 IH ⟨c :: l, nodupKeys_cons.2 ⟨h, hl⟩⟩ ≍
      IH c.1 c.2 ⟨l, hl⟩ h (@insertRec α β _ C H0 IH ⟨l, hl⟩) by
    cases c
    apply eq_of_heq
    convert! this <;> rw [insert_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert (β := β) a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys (β := β)
h : ¬c.fst (β := β) ∈ mk (β := β) l hl
⊢ HEq (α := C (mk (β := β) (c :: l) ⋯)) (insertRec (β := β) (C := C) H0 IH (mk (β := β) (c :: l) ⋯))
    (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
have rw : HEq (α := C (mk (β := β) (c :: l) sorry))
  (Eq.mpr sorry
    (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l sorry) sorry (insertRec (β := β) (C := C) H0 IH (mk (β := β) l sorry))))
  (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))
Tactic: rw [insertRec]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ (kextract (β := β) a (s.entries (β := β))).snd.NodupKeys (β := β)
have rw : (dlookup (β := β) a (s.entries (β := β)), kerase (β := β) a (s.entries (β := β))).snd.NodupKeys (β := β)
Tactic: rw [kextract_eq_dlookup_kerase]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ extract (β := β) a s = (lookup (β := β) a s, erase (β := β) a s)
have simp : dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s ∧
  mk (β := β) (kerase (β := β) a (s.entries (β := β))) sorry = erase (β := β) a s
Tactic: simp [extract]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s ∧
    mk (β := β) (kerase (β := β) a (s.entries (β := β))) ⋯ = erase (β := β) a s
have left : dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
left : dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s
⊢ dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s ∧
    mk (β := β) (kerase (β := β) a (s.entries (β := β))) ⋯ = erase (β := β) a s
have right : mk (β := β) (kerase (β := β) a (s.entries (β := β))) sorry = erase (β := β) a s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ insert (β := β) a b (s₁ ∪ s₂) = insert (β := β) a b s₁ ∪ s₂
have a₁ : ∀ (i : ℕ) (a_1 : Sigma β),
  getElem? (valid := fun (as : List (Sigma β)) (i : ℕ) ↦ i < as.length)
        ((insert (β := β) a b (s₁ ∪ s₂)).entries (β := β)) i =
      some a_1 ↔
    getElem? (valid := fun (as : List (Sigma β)) (i : ℕ) ↦ i < as.length)
        ((insert (β := β) a b s₁ ∪ s₂).entries (β := β)) i =
      some a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
⊢ y ∈ dlookup (β := β) x ((s₁ ∪ s₂).entries (β := β)) ↔ y ∈ dlookup (β := β) x ((s₂ ∪ s₁).entries (β := β))
have simp : dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y ↔
  dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
Tactic: simp only [union_entries, Option.mem_def, dlookup_kunion_eq_some]
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
      ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y ↔
    dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
      ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
have mp : dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y →
  dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.AList (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
mp :
  dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
      ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y →
    dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
      ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
      ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y ↔
    dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
      ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
have mpr : dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
    ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y →
  dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
Tactic: constructor