[GOAL]
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
⊢ Nodup (keys m) ↔ NodupKeys m
[PROOFSTEP]
rcases m with ⟨l⟩
[GOAL]
case mk
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
l : List ((a : α) × β a)
⊢ Nodup (keys (Quot.mk Setoid.r l)) ↔ NodupKeys (Quot.mk Setoid.r l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ ⟦s₁⟧ = ⟦s₂⟧ ↔ s₁.entries ~ s₂.entries
[PROOFSTEP]
cases s₁
[GOAL]
case mk
α : Type u
β : α → Type v
s₂ : AList β
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ = ⟦s₂⟧ ↔
    { entries := entries✝, nodupKeys := nodupKeys✝ }.entries ~ s₂.entries
[PROOFSTEP]
cases s₂
[GOAL]
case mk.mk
α : Type u
β : α → Type v
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : NodupKeys entries✝¹
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧ = ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ ↔
    { entries := entries✝¹, nodupKeys := nodupKeys✝¹ }.entries ~
      { entries := entries✝, nodupKeys := nodupKeys✝ }.entries
[PROOFSTEP]
simp [AList.toFinmap]
[GOAL]
α : Type u
β : α → Type v
γ : Sort ?u.11051
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ γ
[PROOFSTEP]
refine'
  (Quotient.liftOn s.entries (fun (l : List (Sigma β)) => (⟨_, fun nd => f ⟨l, nd⟩⟩ : Part γ))
          (fun l₁ l₂ p => Part.ext' (perm_nodupKeys p) _) :
        Part γ).get
    _
[GOAL]
case refine'_1
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
l₁ l₂ : List (Sigma β)
p : l₁ ≈ l₂
⊢ ∀ (h₁ : ((fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁).Dom)
    (h₂ : ((fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂).Dom),
    Part.get ((fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁) h₁ =
      Part.get ((fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂) h₂
[PROOFSTEP]
exact fun h1 h2 => H _ _ p
[GOAL]
case refine'_2
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ (Quotient.liftOn s.entries (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } })
      (_ :
        ∀ (l₁ l₂ : List (Sigma β)),
          l₁ ≈ l₂ →
            (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁ =
              (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂)).Dom
[PROOFSTEP]
have := s.nodupKeys
[GOAL]
case refine'_2
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
this : Multiset.NodupKeys s.entries
⊢ (Quotient.liftOn s.entries (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } })
      (_ :
        ∀ (l₁ l₂ : List (Sigma β)),
          l₁ ≈ l₂ →
            (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁ =
              (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂)).Dom
[PROOFSTEP]
revert this
[GOAL]
case refine'_2
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ Multiset.NodupKeys s.entries →
    (Quotient.liftOn s.entries (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } })
        (_ :
          ∀ (l₁ l₂ : List (Sigma β)),
            l₁ ≈ l₂ →
              (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁ =
                (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂)).Dom
[PROOFSTEP]
rcases s.entries with ⟨l⟩
[GOAL]
case refine'_2.mk
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
x✝ : Multiset (Sigma β)
l : List (Sigma β)
⊢ Multiset.NodupKeys (Quot.mk Setoid.r l) →
    (Quotient.liftOn (Quot.mk Setoid.r l)
        (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } })
        (_ :
          ∀ (l₁ l₂ : List (Sigma β)),
            l₁ ≈ l₂ →
              (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁ =
                (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂)).Dom
[PROOFSTEP]
exact id
[GOAL]
α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ liftOn ⟦s⟧ f H = f s
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ f H = f { entries := entries✝, nodupKeys := nodupKeys✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
γ : Type ?u.20104
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
⊢ (fun l₁ => liftOn s₂ (f l₁) (_ : ∀ (b₁ b₂ : AList β), b₁.entries ~ b₂.entries → f l₁ b₁ = f l₁ b₂)) a₁ =
    (fun l₁ => liftOn s₂ (f l₁) (_ : ∀ (b₁ b₂ : AList β), b₁.entries ~ b₂.entries → f l₁ b₁ = f l₁ b₂)) a₂
[PROOFSTEP]
have H' : f a₁ = f a₂ := funext fun _ => H _ _ _ _ p (Perm.refl _)
[GOAL]
α : Type u
β : α → Type v
γ : Type ?u.20104
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
H' : f a₁ = f a₂
⊢ (fun l₁ => liftOn s₂ (f l₁) (_ : ∀ (b₁ b₂ : AList β), b₁.entries ~ b₂.entries → f l₁ b₁ = f l₁ b₂)) a₁ =
    (fun l₁ => liftOn s₂ (f l₁) (_ : ∀ (b₁ b₂ : AList β), b₁.entries ~ b₂.entries → f l₁ b₁ = f l₁ b₂)) a₂
[PROOFSTEP]
simp only [H']
[GOAL]
α : Type u
β : α → Type v
γ : Type u_1
s₁ s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
⊢ liftOn₂ ⟦s₁⟧ ⟦s₂⟧ f H = f s₁ s₂
[PROOFSTEP]
cases s₁
[GOAL]
case mk
α : Type u
β : α → Type v
γ : Type u_1
s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn₂ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ ⟦s₂⟧ f H =
    f { entries := entries✝, nodupKeys := nodupKeys✝ } s₂
[PROOFSTEP]
cases s₂
[GOAL]
case mk.mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : NodupKeys entries✝¹
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn₂ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ f H =
    f { entries := entries✝¹, nodupKeys := nodupKeys✝¹ } { entries := entries✝, nodupKeys := nodupKeys✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C ⟦a⟧
⊢ C s
[PROOFSTEP]
rcases s with ⟨⟨a⟩, h⟩
[GOAL]
case mk.mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk Setoid.r a)
⊢ C { entries := Quot.mk Setoid.r a, nodupKeys := h }
[PROOFSTEP]
exact H ⟨a, h⟩
[GOAL]
α : Type u
β : α → Type v
l₁ : Multiset (Sigma β)
h₁ : Multiset.NodupKeys l₁
l₂ : Multiset (Sigma β)
nodupKeys✝ : Multiset.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
s₁ s₂ : AList β
⊢ keys ⟦s₁⟧ = keys ⟦s₂⟧ ↔ AList.keys s₁ ~ AList.keys s₂
[PROOFSTEP]
simp [keys, AList.keys]
[GOAL]
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ singleton y b ↔ x = y
[PROOFSTEP]
simp only [singleton]
[GOAL]
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ ⟦AList.singleton y b⟧ ↔ x = y
[PROOFSTEP]
erw [mem_cons, mem_nil_iff, or_false_iff]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a (List.toFinmap s) = dlookup a s
[PROOFSTEP]
rw [List.toFinmap, lookup_toFinmap, lookup_to_alist]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
a : α
b : β a
⊢ b ∈ lookup a s ↔ { fst := a, snd := b } ∈ s.entries
[PROOFSTEP]
rcases s with ⟨⟨l⟩, hl⟩
[GOAL]
case mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
entries✝ : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (Quot.mk Setoid.r l)
⊢ b ∈ lookup a { entries := Quot.mk Setoid.r l, nodupKeys := hl } ↔
    { fst := a, snd := b } ∈ { entries := Quot.mk Setoid.r l, nodupKeys := hl }.entries
[PROOFSTEP]
exact List.mem_dlookup_iff hl
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
⊢ (Finset.sigma (keys s) fun i => Option.toFinset (lookup i s)) =
    { val := s.entries, nodup := (_ : Multiset.Nodup s.entries) }
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
⊢ (x ∈ Finset.sigma (keys s) fun i => Option.toFinset (lookup i s)) ↔
    x ∈ { val := s.entries, nodup := (_ : Multiset.Nodup s.entries) }
[PROOFSTEP]
have : x ∈ s.entries → x.1 ∈ s.keys := Multiset.mem_map_of_mem _
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
this : x ∈ s.entries → x.fst ∈ keys s
⊢ (x ∈ Finset.sigma (keys s) fun i => Option.toFinset (lookup i s)) ↔
    x ∈ { val := s.entries, nodup := (_ : Multiset.Nodup s.entries) }
[PROOFSTEP]
simpa [lookup_eq_some_iff]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ lookup a (singleton a b) = some b
[PROOFSTEP]
rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), lookup x ⟦s₁⟧ = lookup x ⟦s₂⟧
⊢ ⟦s₁⟧ = ⟦s₂⟧
[PROOFSTEP]
simp only [AList.lookup, lookup_toFinmap] at h 
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ⟦s₁⟧ = ⟦s₂⟧
[PROOFSTEP]
rw [AList.toFinmap_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ s₁.entries ~ s₂.entries
[PROOFSTEP]
apply lookup_ext s₁.nodupKeys s₂.nodupKeys
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
[PROOFSTEP]
intro x y
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
x : α
y : β x
⊢ y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
⊢ Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val
[PROOFSTEP]
refine Multiset.nodup_keys.1 ((Finset.nodup _).map_on ?_)
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
⊢ ∀ (x : (a : α) × β a),
    x ∈ (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val →
      ∀ (y : (a : α) × β a),
        y ∈ (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val → x.fst = y.fst → x = y
[PROOFSTEP]
simp only [Finset.mem_val, Finset.mem_sigma, Option.mem_toFinset, Option.mem_def]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
⊢ ∀ (x : (a : α) × β a),
    x.fst ∈ (↑f).fst ∧ Prod.snd (↑f) x.fst = some x.snd →
      ∀ (y : (a : α) × β a), y.fst ∈ (↑f).fst ∧ Prod.snd (↑f) y.fst = some y.snd → x.fst = y.fst → x = y
[PROOFSTEP]
rintro ⟨i, x⟩ ⟨_, hx⟩ ⟨j, y⟩ ⟨_, hy⟩ (rfl : i = j)
[GOAL]
case mk.intro.mk.intro
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
i : α
x : β i
left✝¹ : { fst := i, snd := x }.fst ∈ (↑f).fst
hx : Prod.snd ↑f { fst := i, snd := x }.fst = some { fst := i, snd := x }.snd
y : β i
left✝ : { fst := i, snd := y }.fst ∈ (↑f).fst
hy : Prod.snd ↑f { fst := i, snd := y }.fst = some { fst := i, snd := y }.snd
⊢ { fst := i, snd := x } = { fst := i, snd := y }
[PROOFSTEP]
simpa using hx.symm.trans hy
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : Finmap β
⊢ ((fun f =>
          { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
            nodupKeys :=
              (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
        ((fun s =>
            { val := (keys s, fun i => lookup i s),
              property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
          f)).entries =
    f.entries
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), Option.isSome (Prod.snd (s, f) i) = true ↔ i ∈ (s, f).fst
⊢ (fun s =>
        { val := (keys s, fun i => lookup i s),
          property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
      ((fun f =>
          { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
            nodupKeys :=
              (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
        { val := (s, f), property := hf }) =
    { val := (s, f), property := hf }
[PROOFSTEP]
dsimp only at hf 
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), Option.isSome (f i) = true ↔ i ∈ s
⊢ (fun s =>
        { val := (keys s, fun i => lookup i s),
          property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
      ((fun f =>
          { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
            nodupKeys :=
              (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
        { val := (s, f), property := hf }) =
    { val := (s, f), property := hf }
[PROOFSTEP]
ext
[GOAL]
case a.h₁.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), Option.isSome (f i) = true ↔ i ∈ s
a✝ : α
⊢ a✝ ∈
      (↑((fun s =>
              { val := (keys s, fun i => lookup i s),
                property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
            ((fun f =>
                { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
                  nodupKeys :=
                    (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
              { val := (s, f), property := hf }))).fst ↔
    a✝ ∈ (↑{ val := (s, f), property := hf }).fst
[PROOFSTEP]
simp [keys, Multiset.keys, ← hf, Option.isSome_iff_exists]
[GOAL]
case a.h₂.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), Option.isSome (f i) = true ↔ i ∈ s
x✝ : α
a✝ : β x✝
⊢ a✝ ∈
      Prod.snd
        (↑((fun s =>
              { val := (keys s, fun i => lookup i s),
                property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
            ((fun f =>
                { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
                  nodupKeys :=
                    (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
              { val := (s, f), property := hf })))
        x✝ ↔
    a✝ ∈ Prod.snd (↑{ val := (s, f), property := hf }) x✝
[PROOFSTEP]
simp (config := { contextual := true }) [lookup_eq_some_iff, ← hf]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : Finmap fun a => β a
⊢ keys (↑keysLookupEquiv.symm (↑keysLookupEquiv x✝)) = (↑(↑keysLookupEquiv x✝)).fst
[PROOFSTEP]
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_fst]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : Finmap fun a => β a
x✝ : α
⊢ lookup x✝ (↑keysLookupEquiv.symm (↑keysLookupEquiv x✝¹)) = Prod.snd (↑(↑keysLookupEquiv x✝¹)) x✝
[PROOFSTEP]
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_snd]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ replace a b ⟦s⟧ = ⟦AList.replace a b s⟧
[PROOFSTEP]
simp [replace]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ keys (replace a b ⟦s⟧) = keys ⟦s⟧
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
s : AList β
⊢ a' ∈ replace a b ⟦s⟧ ↔ a' ∈ ⟦s⟧
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝),
    (fun x y z => x || f y z) ((fun x y z => x || f y z) x✝³ x✝² x✝¹) x✝ b₂ =
      (fun x y z => x || f y z) ((fun x y z => x || f y z) x✝³ x✝ b₂) x✝² x✝¹
[PROOFSTEP]
simp_rw [Bool.or_assoc, Bool.or_comm, imp_true_iff]
[GOAL]
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝),
    (fun x y z => x && f y z) ((fun x y z => x && f y z) x✝³ x✝² x✝¹) x✝ b₂ =
      (fun x y z => x && f y z) ((fun x y z => x && f y z) x✝³ x✝ b₂) x✝² x✝¹
[PROOFSTEP]
simp_rw [Bool.and_assoc, Bool.and_comm, imp_true_iff]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ erase a ⟦s⟧ = ⟦AList.erase a s⟧
[PROOFSTEP]
simp [erase]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ keys ⟦AList.erase a s⟧ = Finset.erase (keys ⟦s⟧) a
[PROOFSTEP]
simp [Finset.erase, keys, AList.erase, keys_kerase]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ keys (erase a ⟦s⟧) = Finset.erase (keys ⟦s⟧) a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ a' ∈ erase a ⟦s⟧ ↔ a' ≠ a ∧ a' ∈ ⟦s⟧
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ ¬a ∈ erase a s
[PROOFSTEP]
rw [mem_erase, not_and_or, not_not]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a ∨ ¬a ∈ s
[PROOFSTEP]
left
[GOAL]
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ (erase a (erase a' ⟦s⟧)).entries = (erase a' (erase a ⟦s⟧)).entries
[PROOFSTEP]
simp only [AList.erase_erase, erase_toFinmap]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ insert a b ⟦s⟧ = ⟦AList.insert a b s⟧
[PROOFSTEP]
simp [insert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
h : ¬a ∈ ⟦s⟧
⊢ (insert a b ⟦s⟧).entries = { fst := a, snd := b } ::ₘ ⟦s⟧.entries
[PROOFSTEP]
simp [AList.insert_entries_of_neg (mt mem_toFinmap.1 h), -insert_entries]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ lookup a (insert a b ⟦s⟧) = some b
[PROOFSTEP]
simp only [insert_toFinmap, lookup_toFinmap, AList.lookup_insert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
h : a' ≠ a
s : AList β
⊢ lookup a' (insert a b ⟦s⟧) = lookup a' ⟦s⟧
[PROOFSTEP]
simp only [insert_toFinmap, lookup_toFinmap, lookup_insert_ne h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s✝ : Finmap β
s : AList β
⊢ insert a b' (insert a b ⟦s⟧) = insert a b' ⟦s⟧
[PROOFSTEP]
simp only [insert_toFinmap, AList.insert_insert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s✝ : Finmap β
h : a ≠ a'
s : AList β
⊢ insert a' b' (insert a b ⟦s⟧) = insert a b (insert a' b' ⟦s⟧)
[PROOFSTEP]
simp only [insert_toFinmap, AList.toFinmap_eq, AList.insert_insert_of_ne _ h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
⊢ a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
[PROOFSTEP]
induction' xs with x xs
[GOAL]
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ a ∈ List.toFinmap [] ↔ ∃ b, { fst := a, snd := b } ∈ []
[PROOFSTEP]
simp only [toFinmap_nil, not_mem_empty, find?, not_mem_nil, exists_false]
[GOAL]
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
⊢ a ∈ List.toFinmap (x :: xs) ↔ ∃ b, { fst := a, snd := b } ∈ x :: xs
[PROOFSTEP]
cases' x with fst_i snd_i
[GOAL]
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a ∈ List.toFinmap ({ fst := fst_i, snd := snd_i } :: xs) ↔
    ∃ b, { fst := a, snd := b } ∈ { fst := fst_i, snd := snd_i } :: xs
[PROOFSTEP]
simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]
[GOAL]
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
fst_i : α
snd_i : β fst_i
⊢ (a = fst_i ∨ ∃ b, { fst := a, snd := b } ∈ xs) ↔ (a = fst_i ∧ ∃ x, HEq x snd_i) ∨ ∃ x, { fst := a, snd := x } ∈ xs
[PROOFSTEP]
refine (or_congr_left <| and_iff_left_of_imp ?_).symm
[GOAL]
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a = fst_i → ∃ x, HEq x snd_i
[PROOFSTEP]
rintro rfl
[GOAL]
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
snd_i : β a
⊢ ∃ x, HEq x snd_i
[PROOFSTEP]
simp only [exists_eq, heq_iff_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ insert a b (singleton a b') = singleton a b
[PROOFSTEP]
simp only [singleton, Finmap.insert_toFinmap, AList.insert_singleton_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ Prod.map id AList.toFinmap (AList.extract a s₁) = Prod.map id AList.toFinmap (AList.extract a s₂)
[PROOFSTEP]
simp [perm_lookup p, toFinmap_eq, perm_erase p]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ extract a ⟦s⟧ = (lookup a ⟦s⟧, erase a ⟦s⟧)
[PROOFSTEP]
simp [extract]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₁ ∪ s₂⟧
[PROOFSTEP]
simp [(· ∪ ·), union]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ∀ (a : α), a ∈ keys (⟦s₁⟧ ∪ ⟦s₂⟧) ↔ a ∈ keys ⟦s₁⟧ ∪ keys ⟦s₂⟧
[PROOFSTEP]
simp [keys]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
[PROOFSTEP]
by_cases h' : a ∈ s₁
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
h' : a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
[PROOFSTEP]
rw [lookup_union_left h']
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
h' : ¬a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
[PROOFSTEP]
rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : Finmap β
a₁ a₂ : AList β
⊢ insert a b (⟦a₁⟧ ∪ ⟦a₂⟧) = insert a b ⟦a₁⟧ ∪ ⟦a₂⟧
[PROOFSTEP]
simp [AList.insert_union]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ s₃✝ : Finmap β
s₁ s₂ s₃ : AList β
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ ∪ ⟦s₃⟧ = ⟦s₁⟧ ∪ (⟦s₂⟧ ∪ ⟦s₃⟧)
[PROOFSTEP]
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_assoc]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ∅ ∪ ⟦s₁⟧ = ⟦s₁⟧
[PROOFSTEP]
rw [← empty_toFinmap]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧
[PROOFSTEP]
simp [-empty_toFinmap, AList.toFinmap_eq, union_toFinmap, AList.union_assoc]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ∅ = ⟦s₁⟧
[PROOFSTEP]
rw [← empty_toFinmap]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧
[PROOFSTEP]
simp [-empty_toFinmap, AList.toFinmap_eq, union_toFinmap, AList.union_assoc]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
[PROOFSTEP]
by_cases h' : x = a
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
[PROOFSTEP]
subst a
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ lookup x (erase x s ∪ singleton x b) = lookup x s
[PROOFSTEP]
rw [lookup_union_right not_mem_erase_self, lookup_singleton_eq, h]
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
[PROOFSTEP]
have : x ∉ singleton a b := by rwa [mem_singleton]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ ¬x ∈ singleton a b
[PROOFSTEP]
rwa [mem_singleton]
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : ¬x ∈ singleton a b
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
[PROOFSTEP]
rw [lookup_union_left_of_not_in this, lookup_erase_ne h']
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y : Finmap β
⊢ Decidable (Disjoint x y)
[PROOFSTEP]
dsimp only [Disjoint]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y : Finmap β
⊢ Decidable (∀ (x_1 : α), x_1 ∈ x → ¬x_1 ∈ y)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ Disjoint (x ∪ y) z ↔ Disjoint x z ∧ Disjoint y z
[PROOFSTEP]
simp [Disjoint, Finmap.mem_union, or_imp, forall_and]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ Disjoint x (y ∪ z) ↔ Disjoint x y ∧ Disjoint x z
[PROOFSTEP]
rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ Disjoint ⟦s₁⟧ ⟦s₂⟧ → ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : Disjoint ⟦s₁⟧ ⟦s₂⟧
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧
[PROOFSTEP]
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_comm_of_disjoint h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
⊢ s₁ = s₂
[PROOFSTEP]
apply ext_lookup
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
⊢ ∀ (x : α), lookup x s₁ = lookup x s₂
[PROOFSTEP]
intro x
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
have : (s₁ ∪ s₃).lookup x = (s₂ ∪ s₃).lookup x := h'' ▸ rfl
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
by_cases hs₁ : x ∈ s₁
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∈ s₁
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
rwa [lookup_union_left hs₁, lookup_union_left_of_not_in (h _ hs₁)] at this 
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : ¬x ∈ s₁
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
by_cases hs₂ : x ∈ s₂
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : ¬x ∈ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
rwa [lookup_union_left_of_not_in (h' _ hs₂), lookup_union_left hs₂] at this 
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : ¬x ∈ s₁
hs₂ : ¬x ∈ s₂
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
rw [lookup_eq_none.mpr hs₁, lookup_eq_none.mpr hs₂]
