awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : AList β
h : ¬a ∈ l
h_1 : True
⊢ True

Tactic:
trivial
-- Module: Mathlib.Data.List.AList
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)
change : insertRec (β := β) (C := C) H0 IH (mk (β := β) [] ⋯) = H0
⊢ insertRec (β := β) (C := C) H0 IH ∅ = H0

Tactic:
change @insertRec α β _ C H0 IH ⟨[], _⟩ = H0

Premises used: AList.mk, AList.insertRec, List.nil
-- Module: Mathlib.Data.List.AList
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)
rw rw₁ : H0 = H0
⊢ insertRec (β := β) (C := C) H0 IH (mk (β := β) [] ⋯) = H0

Tactic:
rw [insertRec]
-- Module: Mathlib.Data.List.AList
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
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))
⊢ insertRec (β := β) (C := C) H0 IH (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) l) =
    IH (c.fst (β := β)) (c.snd (β := β)) l h (insertRec (β := β) (C := C) H0 IH l)

Tactic:
obtain ⟨l, hl⟩ := l
-- Module: Mathlib.Data.List.AList
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 (β := β) ∈ AList.mk (β := β) l hl
this :
  HEq (α := C (AList.mk (β := β) (c :: l) ⋯)) (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) (c :: l) ⋯))
    (IH (c.fst (β := β)) (c.snd (β := β)) (AList.mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) l hl)))
mk :
  ∀ (fst : α) (snd : β fst) (h : ¬(Sigma.mk (β := β) fst snd).fst (β := β) ∈ AList.mk (β := β) l hl)
    (this :
      HEq (α := C (AList.mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
        (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
        (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
          (AList.mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) l hl)))),
    insertRec (β := β) (C := C) H0 IH
        (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
          (AList.mk (β := β) l hl)) =
      IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (AList.mk (β := β) l hl)
        h (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) l hl))
⊢ insertRec (β := β) (C := C) H0 IH (insert (β := β) (c.fst (β := β)) (c.snd (β := β)) (AList.mk (β := β) l hl)) =
    IH (c.fst (β := β)) (c.snd (β := β)) (AList.mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) l hl))

Tactic:
cases c
-- Module: Mathlib.Data.List.AList
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 (β := β) ∈ AList.mk (β := β) l hl
this :
  HEq (α := C (AList.mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) (Sigma.mk (β := β) fst snd :: l) ⋯))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (AList.mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) l hl)))
mk :
  HEq (α :=
    C
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (AList.mk (β := β) l hl)))
    (insertRec (β := β) (C := C) H0 IH
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (AList.mk (β := β) l hl)))
    (IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (AList.mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) l hl)))
⊢ insertRec (β := β) (C := C) H0 IH
      (insert (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β))
        (AList.mk (β := β) l hl)) =
    IH ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) (AList.mk (β := β) l hl) h
      (insertRec (β := β) (C := C) H0 IH (AList.mk (β := β) l hl))

Tactic:
apply eq_of_heq

Premises used: eq_of_heq
-- Module: Mathlib.Data.List.AList
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 (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)))

Tactic:
this
-- Module: Mathlib.Data.List.AList
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
h₂ :
  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
⊢ 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:
convert! this
-- Module: Mathlib.Data.List.AList
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₁ h₂ :
  (mk (β := β)
          (Sigma.mk (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) ::
            (mk (β := β) l hl).entries (β := β))
          ⋯).entries
      (β := β) =
    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

Tactic:
rw [insert_of_notMem h]

Premises used: AList.insert_of_notMem
-- Module: Mathlib.Data.List.AList
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) ⋯)
h₁ h₂ :
  (mk (β := β)
          (Sigma.mk (β := β) ((Sigma.mk (β := β) fst snd).fst (β := β)) ((Sigma.mk (β := β) fst snd).snd (β := β)) ::
            (mk (β := β) l hl).entries (β := β))
          ⋯).entries
      (β := β) =
    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

Tactic:
rw [insert_of_notMem h]

Premises used: AList.insert_of_notMem
-- Module: Mathlib.Data.List.AList
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
suffices :
  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))

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]
-- Module: Mathlib.Data.List.AList
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
rw :
  HEq (α := C (mk (β := β) (c :: l) ⋯))
    (Eq.mpr ⋯
      (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l ⋯) ⋯ (insertRec (β := β) (C := C) H0 IH (mk (β := β) l ⋯))))
    (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (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)))

Tactic:
rw [insertRec]
-- Module: Mathlib.Data.List.AList
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) ⋯))
    (Eq.mpr ⋯
      (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l ⋯) ⋯ (insertRec (β := β) (C := C) H0 IH (mk (β := β) l ⋯))))
    (IH (c.fst (β := β)) (c.snd (β := β)) (mk (β := β) l hl) h (insertRec (β := β) (C := C) H0 IH (mk (β := β) l hl)))

Tactic:
apply cast_heq

Premises used: cast_heq
-- Module: Mathlib.Data.List.AList
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)
a : α
b : β a
l : AList β
h : ¬a ∈ l
⊢ insertRec (β := β) (C := C) H0 IH (insert (β := β) a b l) = IH a b l h (insertRec (β := β) (C := C) H0 IH l)

Tactic:
@insertRec_insert α β _ C H0 IH ⟨a, b⟩ l h

Premises used: AList.insertRec_insert
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
rw : (dlookup (β := β) a (s.entries (β := β)), kerase (β := β) a (s.entries (β := β))).snd.NodupKeys (β := β)
⊢ (kextract (β := β) a (s.entries (β := β))).snd.NodupKeys (β := β)

Tactic:
rw [kextract_eq_dlookup_kerase]

Premises used: List.kextract_eq_dlookup_kerase
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ (dlookup (β := β) a (s.entries (β := β)), kerase (β := β) a (s.entries (β := β))).snd.NodupKeys (β := β)

Tactic:
s.nodupKeys.kerase _

Premises used: List.kerase, List.NodupKeys.kerase, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ (dlookup (β := β) a (s.entries (β := β)), kerase (β := β) a (s.entries (β := β))).snd.NodupKeys (β := β)

Tactic:
exact s.nodupKeys.kerase _

Premises used: List.NodupKeys.kerase, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
simp :
  dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s ∧
    mk (β := β) (kerase (β := β) a (s.entries (β := β))) ⋯ = erase (β := β) a s
⊢ extract (β := β) a s = (lookup (β := β) a s, erase (β := β) a s)

Tactic:
simp [extract]

Premises used: AList.extract
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
left : dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s
right : mk (β := β) (kerase (β := β) a (s.entries (β := β))) ⋯ = erase (β := β) a s
⊢ dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s ∧
    mk (β := β) (kerase (β := β) a (s.entries (β := β))) ⋯ = erase (β := β) a s

Tactic:
constructor
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ dlookup (β := β) a (s.entries (β := β)) = lookup (β := β) a s

Tactic:
rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ mk (β := β) (kerase (β := β) a (s.entries (β := β))) ⋯ = erase (β := β) a s

Tactic:
rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
⊢ (s₁ ∪ s₂).entries (β := β) = s₁.entries (β := β).kunion (β := β) (s₂.entries (β := β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : AList β
⊢ ∅ ∪ s = s

Tactic:
ext rfl

Premises used: AList.ext, rfl
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : AList β
⊢ (s ∪ ∅).entries (β := β) = s.entries (β := β)

Tactic:
simp
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : AList β
⊢ a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂

Tactic:
mem_keys_kunion

Premises used: List.mem_keys_kunion, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ s₄ : AList β
p₁₂ : s₁.entries (β := β) ~ s₂.entries (β := β)
p₃₄ : s₃.entries (β := β) ~ s₄.entries (β := β)
⊢ (s₁ ∪ s₃).entries (β := β) ~ (s₂ ∪ s₄).entries (β := β)

Tactic:
simp [p₁₂.kunion s₃.nodupKeys p₃₄]

Premises used: List.Perm.kunion, AList.nodupKeys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : AList β
⊢ erase (β := β) a (s₁ ∪ s₂) = erase (β := β) a s₁ ∪ erase (β := β) a s₂

Tactic:
ext kunion_kerase.symm

Premises used: List.kunion_kerase, AList.ext, Eq.symm
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : AList β
⊢ a ∈ s₁ → lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁

Tactic:
dlookup_kunion_left

Premises used: List.dlookup_kunion_left, AList.lookup, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : AList β
⊢ ¬a ∈ s₁ → lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₂

Tactic:
dlookup_kunion_right

Premises used: AList.lookup, List.dlookup_kunion_right, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ b ∈ lookup (β := β) a (s₁ ∪ s₂) ↔ b ∈ lookup (β := β) a s₁ ∨ ¬a ∈ s₁ ∧ b ∈ lookup (β := β) a s₂

Tactic:
mem_dlookup_kunion

Premises used: List.mem_dlookup_kunion, AList.lookup, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ lookup (β := β) a (s₁ ∪ s₂) = some b ↔ lookup (β := β) a s₁ = some b ∨ ¬a ∈ s₁ ∧ lookup (β := β) a s₂ = some b

Tactic:
mem_dlookup_kunion

Premises used: List.mem_dlookup_kunion, AList.lookup, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ s₃ : AList β
⊢ b ∈ lookup (β := β) a (s₁ ∪ s₃) → ¬a ∈ s₂ → b ∈ lookup (β := β) a (s₁ ∪ s₂ ∪ s₃)

Tactic:
mem_dlookup_kunion_middle

Premises used: List.mem_dlookup_kunion_middle, AList.lookup, AList.keys
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
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
⊢ insert (β := β) a b (s₁ ∪ s₂) = insert (β := β) a b s₁ ∪ s₂

Tactic:
ext
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
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:
simp
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ s₃ : AList β
⊢ ∀ (x : α) (y : β x),
    y ∈ dlookup (β := β) x ((s₁ ∪ s₂ ∪ s₃).entries (β := β)) ↔
      y ∈ dlookup (β := β) x ((s₁ ∪ (s₂ ∪ s₃)).entries (β := β))

Tactic:
simp [not_or, or_assoc, and_or_left, and_assoc]

Premises used: and_or_left, not_or, and_assoc, or_assoc
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
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
⊢ y ∈ dlookup (β := β) x ((s₁ ∪ s₂).entries (β := β)) ↔ y ∈ dlookup (β := β) x ((s₂ ∪ s₁).entries (β := β))

Tactic:
simp only [union_entries, Option.mem_def, dlookup_kunion_eq_some]

Premises used: List.dlookup_kunion_eq_some, AList.union_entries, Option.mem_def
-- Module: Mathlib.Data.List.AList
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
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
⊢ 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
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' :
  dlookup (β := β) x (s₁.entries (β := β)) = some y ∨
    ¬x ∈ s₁.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₂.entries (β := β)) = some y
mp :
  ∀ (h' : dlookup (β := β) x (s₁.entries (β := β)) = some y),
    dlookup (β := β) x (s₂.entries (β := β)) = some y ∨
      ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y
mp₁ :
  ∀ (h' : ¬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

Tactic:
rcases h' with h' | h'
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
mp : ¬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:
right
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
⊢ ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y

Tactic:
⟨?_, h'⟩

Premises used: And.intro
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
mp : ¬x ∈ s₂.entries (β := β).keys (β := β)
⊢ ¬x ∈ s₂.entries (β := β).keys (β := β) ∧ dlookup (β := β) x (s₁.entries (β := β)) = some y

Tactic:
refine ⟨?_, h'⟩
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
mp : x ∈ s₁.keys (β := β)
⊢ ¬x ∈ s₂.entries (β := β).keys (β := β)

Tactic:
apply h
-- Module: Mathlib.Data.List.AList
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint (β := β) s₂
x : α
y : β x
h' : dlookup (β := β) x (s₁.entries (β := β)) = some y
mp : (some y).isSome = true
⊢ x ∈ s₁.keys (β := β)

Tactic:
rw [keys, ← List.dlookup_isSome, h']

Premises used: List.dlookup_isSome, AList.keys