awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
l₁ l₂ : List (Sigma β)
p : l₁ ≈ l₂
⊢ ∀
    (h₁ :
      Part.Dom.{u_1} (α := γ)
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₁))
    (h₂ :
      Part.Dom.{u_1} (α := γ)
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₂)),
    Part.get
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₁)
        h₁ =
      Part.get
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₂)
        h₂

Tactic:
fun h1 h2 => H _ _ p

Premises used: AList.mk
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
l₁ l₂ : List (Sigma β)
p : l₁ ≈ l₂
⊢ ∀
    (h₁ :
      Part.Dom.{u_1} (α := γ)
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₁))
    (h₂ :
      Part.Dom.{u_1} (α := γ)
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₂)),
    Part.get
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₁)
        h₁ =
      Part.get
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₂)
        h₂

Tactic:
exact fun h1 h2 => H _ _ p
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
⊢ s.entries (β := β).NodupKeys (β := β)

Tactic:
have := s.nodupKeys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
this : s.entries (β := β).NodupKeys (β := β)
refine_2 :
  ∀ (this : s.entries (β := β).NodupKeys (β := β)),
    Part.Dom.{u_1} (α := γ)
      (Quotient.liftOn (s.entries (β := β))
        (fun (l : List (Sigma β)) ↦
          { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
        ⋯)
⊢ Part.Dom.{u_1} (α := γ)
    (Quotient.liftOn (s.entries (β := β))
      (fun (l : List (Sigma β)) ↦
        { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
      ⋯)

Tactic:
revert this
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
refine_2 :
  ∀ (x : Multiset (Sigma β)) (l : List (Sigma β))
    (this : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)),
    Part.Dom.{u_1} (α := γ)
      (Quotient.liftOn (s := isSetoid (Sigma β))
        (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)
        (fun (l : List (Sigma β)) ↦
          { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
        ⋯)
⊢ ∀ (this : s.entries (β := β).NodupKeys (β := β)),
    Part.Dom.{u_1} (α := γ)
      (Quotient.liftOn (s.entries (β := β))
        (fun (l : List (Sigma β)) ↦
          { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
        ⋯)

Tactic:
rcases s.entries with ⟨l⟩

Premises used: Finmap.entries
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
x : Multiset (Sigma β)
l : List (Sigma β)
⊢ ∀ (this : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)),
    Part.Dom.{u_1} (α := γ)
      (Quotient.liftOn (s := isSetoid (Sigma β))
        (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)
        (fun (l : List (Sigma β)) ↦
          { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
        ⋯)

Tactic:
id

Premises used: id, Multiset.NodupKeys, List.Nodup, List.NodupKeys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
x : Multiset (Sigma β)
l : List (Sigma β)
⊢ ∀ (this : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)),
    Part.Dom.{u_1} (α := γ)
      (Quotient.liftOn (s := isSetoid (Sigma β))
        (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)
        (fun (l : List (Sigma β)) ↦
          { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
        ⋯)

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
mk :
  ∀ (entries : List (Sigma β)) (nodupKeys : entries.NodupKeys (β := β)),
    (AList.mk (β := β) entries nodupKeys).toFinmap (β := β).liftOn (β := β) f H =
      f (AList.mk (β := β) entries nodupKeys)
⊢ s.toFinmap (β := β).liftOn (β := β) f H = f s

Tactic:
cases s
-- Module: Mathlib.Data.Finmap
Goal:
α : 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 : entries.NodupKeys (β := β)
⊢ (AList.mk (β := β) entries nodupKeys).toFinmap (β := β).liftOn (β := β) f H = f (AList.mk (β := β) entries nodupKeys)

Tactic:
rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
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 (β := β)
⊢ f a₁ = f a₂

Tactic:
have H' : f a₁ = f a₂ := funext fun _ => H _ _ _ _ p (Perm.refl _)
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
γ : Type u_1
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₂
⊢ Eq.{u_1 + 1} (α := γ) ((fun (l₁ : AList β) ↦ s₂.liftOn (β := β) (f l₁) ⋯) a₁)
    ((fun (l₁ : AList β) ↦ s₂.liftOn (β := β) (f l₁) ⋯) a₂)

Tactic:
simp only [H']
-- Module: Mathlib.Data.Finmap
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₂
⊢ s₁.toFinmap (β := β).liftOn₂ (β := β) (s₂.toFinmap (β := β)) f H = f s₁ s₂

Tactic:
rfl

Premises used: Finmap.liftOn, Finmap.liftOn₂, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C (a.toFinmap (β := β))
mk :
  ∀ (entries : Multiset (Sigma β)) (a : List (Sigma β))
    (h : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) a)),
    C (Finmap.mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) a) h)
⊢ C s

Tactic:
rcases s with ⟨⟨a⟩, h⟩
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C (a.toFinmap (β := β))
entries : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) a)
⊢ C (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) a) h)

Tactic:
H ⟨a, h⟩

Premises used: AList.mk, Multiset.ofList, AList.toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C (a.toFinmap (β := β))
entries : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) a)
⊢ C (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) a) h)

Tactic:
exact H ⟨a, h⟩

Premises used: AList.mk
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
C : Finmap β → Finmap β → Prop
s₁ s₂ : Finmap β
H : ∀ (a₁ a₂ : AList β), C (a₁.toFinmap (β := β)) (a₂.toFinmap (β := β))
⊢ C s₁ s₂

Tactic:
induction_on s₁ fun l₁ => induction_on s₂ fun l₂ => H l₁ l₂

Premises used: Finmap.induction_on
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
C : Finmap β → Finmap β → Finmap β → Prop
s₁ s₂ s₃ : Finmap β
H : ∀ (a₁ a₂ a₃ : AList β), C (a₁.toFinmap (β := β)) (a₂.toFinmap (β := β)) (a₃.toFinmap (β := β))
⊢ C s₁ s₂ s₃

Tactic:
induction_on₂ s₁ s₂ fun l₁ l₂ => induction_on s₃ fun l₃ => H l₁ l₂ l₃

Premises used: Finmap.induction_on₂
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
l₁ : Multiset (Sigma β)
h₁ : l₁.NodupKeys (β := β)
l₂ : Multiset (Sigma β)
nodupKeys : l₂.NodupKeys (β := β)
H : (mk (β := β) l₁ h₁).entries (β := β) = (mk (β := β) l₂ nodupKeys).entries (β := β)
⊢ mk (β := β) l₁ h₁ = mk (β := β) l₂ nodupKeys

Tactic:
congr
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
s t : Finmap β
⊢ s.entries (β := β) = t.entries (β := β) ↔ s = t

Tactic:
Finmap.ext_iff.symm

Premises used: Finmap.ext_iff, Iff.symm
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
a : α
s : Finmap β
⊢ a ∈ s ↔ a ∈ s.entries (β := β).keys (β := β)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
a : α
s : AList β
⊢ a ∈ s.toFinmap (β := β) ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, List.keys, Multiset.Mem, AList.keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
s : AList β
⊢ s.toFinmap (β := β).keys (β := β).val = (↑(s.keys (β := β)) : Multiset α)

Tactic:
rfl

Premises used: Multiset.map, List.keys, Multiset.ofList, AList.keys, Multiset.keys, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ s₁.toFinmap (β := β).keys (β := β) = s₂.toFinmap (β := β).keys (β := β) ↔ s₁.keys (β := β) ~ s₂.keys (β := β)

Tactic:
simp [keys, AList.keys]

Premises used: AList.keys, Finmap.keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
a : α
s : Finmap β
⊢ a ∈ s.keys (β := β) ↔ a ∈ s

Tactic:
induction_on s fun _ => AList.mem_keys

Premises used: Finmap.induction_on
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
⊢ Eq (α := Finmap β) (AList.toFinmap (β := β) ∅) ∅

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, AList.toFinmap, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
⊢ Eq (α := Finmap β) (List.toFinmap (β := β) []) ∅

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, List.toFinmap, List.dedupKeys, List.foldr, AList.toFinmap, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
a : α
⊢ a ∉ ∅

Tactic:
Multiset.notMem_zero a

Premises used: Multiset.notMem_zero, Multiset.map, List.map, Multiset.zero, Multiset.ofList, Multiset.keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
⊢ Eq.{u + 1} (α := Finset α) (keys (β := β) ∅) ∅

Tactic:
rfl

Premises used: Multiset.map, List.map, Multiset.zero, Finset.empty, Multiset.ofList, Multiset.keys, rfl, Finmap.keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
a : α
b : β a
⊢ (singleton (β := β) a b).keys (β := β) = {a}

Tactic:
rfl

Premises used: Multiset.map, List.map, Multiset.cons, Multiset.ofList, Multiset.keys, rfl, Finmap.keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ singleton (β := β) y b ↔ x = y

Tactic:
simp [singleton, mem_def]

Premises used: Finmap.mem_def, Finmap.singleton
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ lookup (β := β) a (s.toFinmap (β := β)) = AList.lookup (β := β) a s

Tactic:
rfl

Premises used: Finmap.lookup, AList.lookup, Finmap.liftOn, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : List (Sigma β)
rw : lookup (β := β) a (s.toAList (β := β).toFinmap (β := β)) = dlookup (β := β) a s
rw₁ : AList.lookup (β := β) a (s.toAList (β := β)) = dlookup (β := β) a s
rw₂ rw₃ : dlookup (β := β) a s = dlookup (β := β) a s
⊢ lookup (β := β) a (s.toFinmap (β := β)) = dlookup (β := β) a s

Tactic:
rw [List.toFinmap, lookup_toFinmap, lookup_to_alist]

Premises used: AList.lookup_to_alist, List.toFinmap, Finmap.lookup_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq.{v + 1} (α := Option (β a)) (lookup (β := β) a ∅) none

Tactic:
rfl

Premises used: Finmap.lookup, AList.lookup, Finmap.liftOn, List.dlookup, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
⊢ (lookup (β := β) a s).isSome = true ↔ a ∈ s

Tactic:
induction_on s fun _ => AList.lookup_isSome

Premises used: Finmap.induction_on
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
⊢ lookup (β := β) a s = none ↔ a ∉ s

Tactic:
induction_on s fun _ => AList.lookup_eq_none

Premises used: Finmap.induction_on
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
a : α
b : β a
mk :
  ∀ (entries : Multiset (Sigma β)) (l : List (Sigma β))
    (hl : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)),
    b ∈
        lookup (β := β) a
          (Finmap.mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l) hl) ↔
      Sigma.mk (β := β) a b ∈
        (Finmap.mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l) hl).entries
          (β := β)
⊢ b ∈ lookup (β := β) a s ↔ Sigma.mk (β := β) a b ∈ s.entries (β := β)

Tactic:
rcases s with ⟨⟨l⟩, hl⟩
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
entries : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)
⊢ b ∈ lookup (β := β) a (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l) hl) ↔
    Sigma.mk (β := β) a b ∈
      (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l) hl).entries (β := β)

Tactic:
List.mem_dlookup_iff hl

Premises used: Finmap.lookup, Multiset.Mem, AList.lookup, List.mem_dlookup_iff, Finmap.liftOn
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
entries : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)
⊢ b ∈ lookup (β := β) a (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l) hl) ↔
    Sigma.mk (β := β) a b ∈
      (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l) hl).entries (β := β)

Tactic:
exact List.mem_dlookup_iff hl

Premises used: List.mem_dlookup_iff
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
a : α
b : β a
⊢ lookup (β := β) a s = some b ↔ Sigma.mk (β := β) a b ∈ s.entries (β := β)

Tactic:
mem_lookup_iff

Premises used: Finmap.mem_lookup_iff
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
h :
  ∀ (x : (i : α) × β i),
    Membership.mem (γ := Finset ((i : α) × β i))
        (s.keys (β := β).sigma (α := β) fun (i : α) ↦ (lookup (β := β) i s).toFinset) x ↔
      x ∈ { val := s.entries (β := β), nodup := ⋯ : Finset ((i : α) × β i) }
⊢ (s.keys (β := β).sigma (α := β) fun (i : α) ↦ (lookup (β := β) i s).toFinset) =
    { val := s.entries (β := β), nodup := ⋯ : Finset ((i : α) × β i) }

Tactic:
ext x
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
x : (i : α) × β i
⊢ x ∈ s.entries (β := β) → x.fst (β := fun (i : α) ↦ β i) ∈ s.keys (β := β)

Tactic:
have : x ∈ s.entries → x.1 ∈ s.keys := Multiset.mem_map_of_mem _
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
x : (i : α) × β i
this : x ∈ s.entries (β := β) → x.fst (β := fun (i : α) ↦ β i) ∈ s.keys (β := β)
⊢ Membership.mem (γ := Finset ((i : α) × β i))
      (s.keys (β := β).sigma (α := β) fun (i : α) ↦ (lookup (β := β) i s).toFinset) x ↔
    x ∈ { val := s.entries (β := β), nodup := ⋯ : Finset ((i : α) × β i) }

Tactic:
simpa [lookup_eq_some_iff]

Premises used: Finmap.lookup_eq_some_iff
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
rw : lookup (β := β) a ((AList.singleton (β := β) a b).toFinmap (β := β)) = some b
rw₁ : AList.lookup (β := β) a (AList.singleton (β := β) a b) = some b
rw₂ : AList.lookup (β := β) a (AList.mk (β := β) [Sigma.mk (β := β) a b] ⋯) = some b
rw₃ : dlookup (β := β) a ((AList.mk (β := β) [Sigma.mk (β := β) a b] ⋯).entries (β := β)) = some b
rw₄ rw₅ : some b = some b
⊢ lookup (β := β) a (singleton (β := β) a b) = some b

Tactic:
rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]

Premises used: Finmap.singleton, AList.singleton, AList.lookup, List.dlookup_cons_eq, Finmap.lookup_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
⊢ a ∈ s ↔ ∃ (b : β a), lookup (β := β) a s = some b

Tactic:
induction_on s fun s =>
    Iff.trans List.mem_keys <| exists_congr fun _ => (mem_dlookup_iff s.nodupKeys).symm

Premises used: Finmap.induction_on
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup (β := β) a s = some b
⊢ a ∈ s

Tactic:
mem_iff.mpr ⟨_, h⟩

Premises used: Iff.mpr, Finmap.mem_iff, Exists.intro
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup (β := β) x (s₁.entries (β := β)) = dlookup (β := β) x (s₂.entries (β := β))
rw : s₁.entries (β := β) ~ s₂.entries (β := β)
⊢ s₁.toFinmap (β := β) = s₂.toFinmap (β := β)

Tactic:
rw [AList.toFinmap_eq]

Premises used: AList.toFinmap_eq
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup (β := β) x (s₁.entries (β := β)) = dlookup (β := β) x (s₂.entries (β := β))
apply : ∀ (x : α) (y : β x), y ∈ dlookup (β := β) x (s₁.entries (β := β)) ↔ y ∈ dlookup (β := β) x (s₂.entries (β := β))
⊢ s₁.entries (β := β) ~ s₂.entries (β := β)

Tactic:
apply lookup_ext s₁.nodupKeys s₂.nodupKeys

Premises used: List.lookup_ext, AList.nodupKeys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup (β := β) x (s₁.entries (β := β)) = dlookup (β := β) x (s₂.entries (β := β))
x : α
y : β x
rw rw₁ : y ∈ dlookup (β := β) x (s₂.entries (β := β)) ↔ y ∈ dlookup (β := β) x (s₂.entries (β := β))
⊢ y ∈ dlookup (β := β) x (s₁.entries (β := β)) ↔ y ∈ dlookup (β := β) x (s₂.entries (β := β))

Tactic:
rw [h]
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ Multiset.NodupKeys (β := β)
    (Finset.val
      ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
        ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))

Tactic:
Multiset.nodup_keys.1 ((Finset.nodup _).map_on ?_)

Premises used: Multiset.nodup_keys, Finset.nodup, Iff.mp, Multiset.Nodup.map_on
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
refine :
  ∀ (x : (a : α) × β a),
    Membership.mem (γ := Multiset ((a : α) × β a))
        (Finset.val
          ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
            ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
        x →
      ∀ (y : (a : α) × β a),
        Membership.mem (γ := Multiset ((a : α) × β a))
            (Finset.val
              ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
            y →
          x.fst (β := fun (a : α) ↦ β a) = y.fst (β := fun (a : α) ↦ β a) → x = y
⊢ Multiset.NodupKeys (β := β)
    (Finset.val
      ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
        ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))

Tactic:
refine Multiset.nodup_keys.1 ((Finset.nodup _).map_on ?_)

Premises used: Multiset.nodup_keys, Finset.nodup, Iff.mp, Multiset.Nodup.map_on
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
simp :
  ∀ (x : (a : α) × β a),
    x.fst (β := fun (i : α) ↦ β i) ∈ (↑f : Finset α × ((a : α) → Option (β a))).1 ∧
        (↑f : Finset α × ((a : α) → Option (β a))).2 (x.fst (β := fun (i : α) ↦ β i)) =
          some (x.snd (β := fun (i : α) ↦ β i)) →
      ∀ (y : (a : α) × β a),
        y.fst (β := fun (i : α) ↦ β i) ∈ (↑f : Finset α × ((a : α) → Option (β a))).1 ∧
            (↑f : Finset α × ((a : α) → Option (β a))).2 (y.fst (β := fun (i : α) ↦ β i)) =
              some (y.snd (β := fun (i : α) ↦ β i)) →
          x.fst (β := fun (i : α) ↦ β i) = y.fst (β := fun (i : α) ↦ β i) → x = y
⊢ ∀ (x : (a : α) × β a),
    Membership.mem (γ := Multiset ((a : α) × β a))
        (Finset.val
          ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
            ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
        x →
      ∀ (y : (a : α) × β a),
        Membership.mem (γ := Multiset ((a : α) × β a))
            (Finset.val
              ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
            y →
          x.fst (β := fun (a : α) ↦ β a) = y.fst (β := fun (a : α) ↦ β a) → x = y

Tactic:
simp only [Finset.mem_val, Finset.mem_sigma, Option.mem_toFinset, Option.mem_def]

Premises used: Finset.mem_sigma, Option.mem_toFinset, Finset.mem_val, Option.mem_def