[GOAL]
α : Type u
β : α → Type v
l₁ : List (Sigma β)
h₁ : NodupKeys l₁
l₂ : List (Sigma β)
nodupKeys✝ : NodupKeys l₂
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs = ys)
[PROOFSTEP]
rw [ext_iff]
[GOAL]
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs.entries = ys.entries)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
⊢ keys s₁ ⊆ keys s₂
[PROOFSTEP]
intro k hk
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
⊢ k ∈ keys s₂
[PROOFSTEP]
letI : DecidableEq α := Classical.decEq α
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
this : DecidableEq α := Classical.decEq α
⊢ k ∈ keys s₂
[PROOFSTEP]
have := h (mem_lookup_iff.1 (Option.get_mem (lookup_isSome.2 hk)))
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
this✝ : DecidableEq α := Classical.decEq α
this : { fst := k, snd := Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true) } ∈ s₂.entries
⊢ k ∈ keys s₂
[PROOFSTEP]
rw [← mem_lookup_iff, Option.mem_def] at this 
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
this✝¹ : DecidableEq α := Classical.decEq α
this✝ : { fst := k, snd := Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true) } ∈ s₂.entries
this : lookup k s₂ = some (Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true))
⊢ k ∈ keys s₂
[PROOFSTEP]
rw [← mem_keys, ← lookup_isSome, this]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
this✝¹ : DecidableEq α := Classical.decEq α
this✝ : { fst := k, snd := Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true) } ∈ s₂.entries
this : lookup k s₂ = some (Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true))
⊢ Option.isSome (some (Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true))) = true
[PROOFSTEP]
exact Option.isSome_some
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ replace a b s ↔ a' ∈ s
[PROOFSTEP]
rw [mem_keys, keys_replace, ← mem_keys]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s : AList β
⊢ a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s
[PROOFSTEP]
rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ (insert a b s).entries = { fst := a, snd := b } :: s.entries
[PROOFSTEP]
rw [insert_entries, kerase_of_not_mem_keys h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ keys (insert a b s) = a :: List.erase (keys s) a
[PROOFSTEP]
simp [insert, keys, keys_kerase]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ (insert a b s₁).entries ~ (insert a b s₂).entries
[PROOFSTEP]
simp only [insert_entries]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ { fst := a, snd := b } :: kerase a s₁.entries ~ { fst := a, snd := b } :: kerase a s₂.entries
[PROOFSTEP]
exact p.kinsert s₁.nodupKeys
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ lookup a (insert a b s) = some b
[PROOFSTEP]
simp only [lookup, insert, dlookup_kinsert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a (toAList s) = dlookup a s
[PROOFSTEP]
rw [List.toAList, lookup, dlookup_dedupKeys]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ insert a b' (insert a b s) = insert a b' s
[PROOFSTEP]
ext : 1
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries
[PROOFSTEP]
simp only [AList.insert_entries, List.kerase_cons_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ (insert a' b' (insert a b s)).entries ~ (insert a b (insert a' b' s)).entries
[PROOFSTEP]
simp only [insert_entries]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ { fst := a', snd := b' } :: kerase a' ({ fst := a, snd := b } :: kerase a s.entries) ~
    { fst := a, snd := b } :: kerase a ({ fst := a', snd := b' } :: kerase a' s.entries)
[PROOFSTEP]
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;> [apply Perm.swap; exact h; exact h.symm]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ { fst := a', snd := b' } :: kerase a' ({ fst := a, snd := b } :: kerase a s.entries) ~
    { fst := a, snd := b } :: kerase a ({ fst := a', snd := b' } :: kerase a' s.entries)
[PROOFSTEP]
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ { fst := a', snd := b' } :: { fst := a, snd := b } :: kerase a (kerase a' s.entries) ~
    { fst := a, snd := b } :: { fst := a', snd := b' } :: kerase a (kerase a' s.entries)
[PROOFSTEP]
apply Perm.swap
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a ≠ { fst := a', snd := b' }.fst
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a' ≠ { fst := a, snd := b }.fst
[PROOFSTEP]
exact h.symm
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ (insert a b (singleton a b')).entries = (singleton a b).entries
[PROOFSTEP]
simp only [AList.insert_entries, List.kerase_cons_eq, and_self_iff, AList.singleton_entries, heq_iff_eq,
  eq_self_iff_true]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : NodupKeys (c :: l)
⊢ { entries := c :: l, nodupKeys := h } = insert c.fst c.snd { entries := l, nodupKeys := (_ : NodupKeys l) }
[PROOFSTEP]
simpa [insert] using (kerase_of_not_mem_keys <| not_mem_keys_of_nodupKeys_cons h).symm
[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 : NodupKeys (c :: l)
⊢ C { entries := c :: l, nodupKeys := h }
[PROOFSTEP]
rw [mk_cons_eq_insert]
[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 : NodupKeys (c :: l)
⊢ C (insert c.fst c.snd { entries := l, nodupKeys := (_ : NodupKeys l) })
[PROOFSTEP]
refine' IH _ _ _ _ (insertRec H0 IH _)
[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 : NodupKeys (c :: l)
⊢ ¬c.fst ∈ { entries := l, nodupKeys := (_ : NodupKeys l) }
[PROOFSTEP]
exact not_mem_keys_of_nodupKeys_cons h
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
⊢ True
[PROOFSTEP]
induction l using AList.insertRec
[GOAL]
case H0
α : Type u
β : α → Type v
inst✝ : DecidableEq α
⊢ True
[PROOFSTEP]
trivial
[GOAL]
case IH
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a✝² : α
b✝ : β a✝²
l✝ : AList β
a✝¹ : ¬a✝² ∈ l✝
a✝ : True
⊢ True
[PROOFSTEP]
trivial
[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 H0 IH ∅ = H0
[PROOFSTEP]
change @insertRec α β _ C H0 IH ⟨[], _⟩ = H0
[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 H0 IH { entries := [], nodupKeys := (_ : NodupKeys []) } = H0
[PROOFSTEP]
rw [insertRec]
[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 H0 IH (insert c.fst c.snd l) = IH c.fst c.snd l h (insertRec H0 IH l)
[PROOFSTEP]
cases' l with l hl
[GOAL]
case mk
α : 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 : NodupKeys l
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ insertRec H0 IH (insert c.fst c.snd { entries := l, nodupKeys := hl }) =
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
[PROOFSTEP]
suffices
  HEq (@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_neg h]
[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 : NodupKeys l
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq (insertRec H0 IH { entries := c :: l, nodupKeys := (_ : NodupKeys (c :: l)) })
    (IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl }))
⊢ insertRec H0 IH (insert c.fst c.snd { entries := l, nodupKeys := hl }) =
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
[PROOFSTEP]
cases c
[GOAL]
case mk
α : 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 : NodupKeys l
fst✝ : α
snd✝ : β fst✝
h : ¬{ fst := fst✝, snd := snd✝ }.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq
    (insertRec H0 IH
      { entries := { fst := fst✝, snd := snd✝ } :: l,
        nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) })
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
⊢ insertRec H0 IH
      (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }) =
    IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
[PROOFSTEP]
apply eq_of_heq
[GOAL]
case mk.h
α : 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 : NodupKeys l
fst✝ : α
snd✝ : β fst✝
h : ¬{ fst := fst✝, snd := snd✝ }.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq
    (insertRec H0 IH
      { entries := { fst := fst✝, snd := snd✝ } :: l,
        nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) })
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
⊢ HEq
    (insertRec H0 IH
      (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }))
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
[PROOFSTEP]
convert this
[GOAL]
case h.e'_1.h.e'_1.h.e'_3.h
α : 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 : NodupKeys l
fst✝ : α
snd✝ : β fst✝
h : ¬{ fst := fst✝, snd := snd✝ }.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq
    (insertRec H0 IH
      { entries := { fst := fst✝, snd := snd✝ } :: l,
        nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) })
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
⊢ (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }).entries =
    { fst := fst✝, snd := snd✝ } :: l
[PROOFSTEP]
rw [insert_of_neg h]
[GOAL]
case h.e'_2.e'_7.h.e'_3.h
α : 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 : NodupKeys l
fst✝ : α
snd✝ : β fst✝
h : ¬{ fst := fst✝, snd := snd✝ }.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq
    (insertRec H0 IH
      { entries := { fst := fst✝, snd := snd✝ } :: l,
        nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) })
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
e_1✝ :
  C (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }) =
    C { entries := { fst := fst✝, snd := snd✝ } :: l, nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) }
⊢ (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }).entries =
    { fst := fst✝, snd := snd✝ } :: l
[PROOFSTEP]
rw [insert_of_neg h]
[GOAL]
case mk
α : 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 : NodupKeys l
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ HEq (insertRec H0 IH { entries := c :: l, nodupKeys := (_ : NodupKeys (c :: l)) })
    (IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl }))
[PROOFSTEP]
rw [insertRec]
[GOAL]
case mk
α : 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 : NodupKeys l
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ HEq
    (Eq.mpr
      (_ :
        C { entries := c :: l, nodupKeys := (_ : NodupKeys (c :: l)) } =
          C (insert c.fst c.snd { entries := l, nodupKeys := (_ : NodupKeys l) }))
      (IH c.fst c.snd { entries := l, nodupKeys := (_ : NodupKeys l) }
        (_ : ¬c.fst ∈ List.keys { entries := l, nodupKeys := (_ : NodupKeys l) }.entries)
        (insertRec H0 IH { entries := l, nodupKeys := (_ : NodupKeys l) })))
    (IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl }))
[PROOFSTEP]
apply cast_heq
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ NodupKeys (kextract a s.entries).snd
[PROOFSTEP]
rw [kextract_eq_dlookup_kerase]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ NodupKeys (dlookup a s.entries, kerase a s.entries).snd
[PROOFSTEP]
exact s.nodupKeys.kerase _
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ extract a s = (lookup a s, erase a s)
[PROOFSTEP]
simp [extract]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s ∧
    { entries := kerase a s.entries, nodupKeys := (_ : NodupKeys (kerase a s.entries)) } = erase a s
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s
[PROOFSTEP]
rfl
[GOAL]
case right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ { entries := kerase a s.entries, nodupKeys := (_ : NodupKeys (kerase a s.entries)) } = erase a s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : AList β
⊢ (s ∪ ∅).entries = s.entries
[PROOFSTEP]
simp
[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
[PROOFSTEP]
simp [p₁₂.kunion s₃.nodupKeys p₃₄]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂
[PROOFSTEP]
ext
[GOAL]
case a.a.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
n✝ : ℕ
a✝ : Sigma β
⊢ a✝ ∈ get? (insert a b (s₁ ∪ s₂)).entries n✝ ↔ a✝ ∈ get? (insert a b s₁ ∪ s₂).entries n✝
[PROOFSTEP]
simp
[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
[PROOFSTEP]
simp [not_or, or_assoc, and_or_left, and_assoc]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂).entries ↔ y ∈ dlookup x (s₂ ∪ s₁).entries
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝ ↔
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝ →
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
intro h'
[GOAL]
case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝ →
    dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
intro h'
[GOAL]
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
cases' h' with h' h'
[GOAL]
case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
right
[GOAL]
case mp.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
refine' ⟨_, h'⟩
[GOAL]
case mp.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₂.entries
[PROOFSTEP]
apply h
[GOAL]
case mp.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ x✝ ∈ keys s₁
[PROOFSTEP]
rw [keys, ← List.dlookup_isSome, h']
[GOAL]
case mp.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ Option.isSome (some y✝) = true
[PROOFSTEP]
exact rfl
[GOAL]
case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
left
[GOAL]
case mp.inr.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
rw [h'.2]
[GOAL]
case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
cases' h' with h' h'
[GOAL]
case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
right
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
refine' ⟨_, h'⟩
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₁.entries
[PROOFSTEP]
intro h''
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ False
[PROOFSTEP]
apply h _ h''
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ x✝ ∈ keys s₂
[PROOFSTEP]
rw [keys, ← List.dlookup_isSome, h']
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ Option.isSome (some y✝) = true
[PROOFSTEP]
exact rfl
[GOAL]
case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
left
[GOAL]
case mpr.inr.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
rw [h'.2]
