awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 }
i : α
x : β i
left :
  (Sigma.mk (β := fun (a : α) ↦ β a) i x).fst (β := fun (i : α) ↦ β i) ∈ (↑f : Finset α × ((a : α) → Option (β a))).1
hx :
  (↑f : Finset α × ((a : α) → Option (β a))).2 ((Sigma.mk (β := fun (a : α) ↦ β a) i x).fst (β := fun (i : α) ↦ β i)) =
    some ((Sigma.mk (β := fun (a : α) ↦ β a) i x).snd (β := fun (i : α) ↦ β i))
y : β i
left_1 :
  (Sigma.mk (β := fun (a : α) ↦ β a) i y).fst (β := fun (i : α) ↦ β i) ∈ (↑f : Finset α × ((a : α) → Option (β a))).1
hy :
  (↑f : Finset α × ((a : α) → Option (β a))).2 ((Sigma.mk (β := fun (a : α) ↦ β a) i y).fst (β := fun (i : α) ↦ β i)) =
    some ((Sigma.mk (β := fun (a : α) ↦ β a) i y).snd (β := fun (i : α) ↦ β i))
⊢ Sigma.mk (β := fun (a : α) ↦ β a) i x = Sigma.mk (β := fun (a : α) ↦ β a) i y

Tactic:
simpa using hx.symm.trans hy

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
f : Finmap β
⊢ entries (β := β)
      ((fun (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) ↦
          mk (β := β)
            (Finset.val
              ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
            ⋯)
        ((fun (s : Finmap β) ↦
            (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s.keys (β := β), fun (i : α) ↦ lookup (β := β) i s) ⋯ :
              { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }))
          f)) =
    f.entries (β := β)

Tactic:
simp
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
a : α
⊢ Membership.mem (γ := Finset α)
      (↑((fun (s : Finmap β) ↦
                (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                    ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s.keys (β := β), fun (i : α) ↦ lookup (β := β) i s) ⋯ :
                  { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }))
              ((fun (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) ↦
                  mk (β := β)
                    (Finset.val
                      ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                        ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
                    ⋯)
                (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                  ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s, f) hf))) :
          Finset α × ((a : α) → Option (β a))).1
      a ↔
    a ∈
      (↑(Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
              (s, f) hf) :
          Finset α × ((a : α) → Option (β a))).1

Tactic:
simp [keys, Multiset.keys, ← hf, Option.isSome_iff_exists]

Premises used: Option.isSome_iff_exists, Multiset.keys, Finmap.keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
x_1 : α
a : β x_1
⊢ (↑((fun (s : Finmap β) ↦
                  (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                      ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s.keys (β := β), fun (i : α) ↦ lookup (β := β) i s)
                      ⋯ :
                    { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }))
                ((fun (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) ↦
                    mk (β := β)
                      (Finset.val
                        ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                          ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
                      ⋯)
                  (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                    ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s, f) hf))) :
            Finset α × ((a : α) → Option (β a))).2
        x_1 =
      some a ↔
    (↑(Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
                (s, f) hf) :
            Finset α × ((a : α) → Option (β a))).2
        x_1 =
      some a

Tactic:
simp +contextual [lookup_eq_some_iff, ← hf]

Premises used: Finmap.lookup_eq_some_iff
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x : Finmap β
⊢ Eq.{u + 1} (α := Finset α)
    (keys (β := β)
      ((Equiv.symm (keysLookupEquiv (β := β)) :
          (a : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) → Finmap β)
        ((keysLookupEquiv (β := β) :
            (a : Finmap β) → { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 })
          x)))
    (↑((keysLookupEquiv (β := β) :
              (a : Finmap β) →
                { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 })
            x) :
        Finset α × ((a : α) → Option (β a))).1

Tactic:
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_fst]

Premises used: Equiv.symm_apply_apply, Finmap.keysLookupEquiv_apply_coe_fst
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x : Finmap β
x_1 : α
⊢ Eq.{v + 1} (α := Option (β x_1))
    (lookup (β := β) x_1
      ((Equiv.symm (keysLookupEquiv (β := β)) :
          (a : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) → Finmap β)
        ((keysLookupEquiv (β := β) :
            (a : Finmap β) → { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 })
          x)))
    ((↑((keysLookupEquiv (β := β) :
                (a : Finmap β) →
                  { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 })
              x) :
          Finset α × ((a : α) → Option (β a))).2
      x_1)

Tactic:
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_snd]

Premises used: Equiv.symm_apply_apply, Finmap.keysLookupEquiv_apply_coe_snd
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
⊢ replace (β := β) a b (s.toFinmap (β := β)) = (AList.replace (β := β) a b s).toFinmap (β := β)

Tactic:
simp [replace]

Premises used: Finmap.replace
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s_1 : Finmap β
s : AList β
⊢ (replace (β := β) a b (s.toFinmap (β := β))).keys (β := β) = s.toFinmap (β := β).keys (β := β)

Tactic:
simp
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
s_1 : Finmap β
s : AList β
⊢ a' ∈ replace (β := β) a b (s.toFinmap (β := β)) ↔ a' ∈ s.toFinmap (β := β)

Tactic:
simp
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x : Bool
x_1 : α
x_2 : β x_1
x_3 : α
simp_rw simp_rw₁ : ∀ (b₂ : β x_3), (x || f x_1 x_2 || f x_3 b₂) = (x || f x_3 b₂ || f x_1 x_2)
simp_rw₂ : ∀ (b₂ : β x_3), (x || (f x_1 x_2 || f x_3 b₂)) = (x || (f x_3 b₂ || f x_1 x_2))
simp_rw₃ : ∀ (b₂ : β x_3), True
⊢ ∀ (b₂ : β x_3),
    Eq (α := Bool)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) x x_1 x_2) x_3
        b₂)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) x x_3 b₂) x_1
        x_2)

Tactic:
simp_rw [Bool.or_assoc, Bool.or_comm, imp_true_iff]

Premises used: Bool.or_comm, Bool.or_assoc, imp_true_iff
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x : Bool
x_1 : α
x_2 : β x_1
x_3 : α
simp_rw simp_rw₁ : ∀ (b₂ : β x_3), (x && f x_1 x_2 && f x_3 b₂) = (x && f x_3 b₂ && f x_1 x_2)
simp_rw₂ : ∀ (b₂ : β x_3), (x && (f x_1 x_2 && f x_3 b₂)) = (x && (f x_3 b₂ && f x_1 x_2))
simp_rw₃ : ∀ (b₂ : β x_3), True
⊢ ∀ (b₂ : β x_3),
    Eq (α := Bool)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) x x_1 x_2) x_3
        b₂)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) x x_3 b₂) x_1
        x_2)

Tactic:
simp_rw [Bool.and_assoc, Bool.and_comm, imp_true_iff]

Premises used: Bool.and_assoc, imp_true_iff, Bool.and_comm
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : AList β
⊢ erase (β := β) a (s.toFinmap (β := β)) = (AList.erase (β := β) a s).toFinmap (β := β)

Tactic:
simp [erase]

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

Tactic:
simp [Finset.erase, keys, AList.erase, keys_kerase]

Premises used: List.keys_kerase, AList.erase, Finset.erase, Finmap.keys
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s_1 : Finmap β
s : AList β
⊢ (erase (β := β) a (s.toFinmap (β := β))).keys (β := β) = s.toFinmap (β := β).keys (β := β).erase a

Tactic:
simp
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s_1 : Finmap β
s : AList β
⊢ a' ∈ erase (β := β) a (s.toFinmap (β := β)) ↔ a' ≠ a ∧ a' ∈ s.toFinmap (β := β)

Tactic:
simp
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
rw : a = a ∨ a ∉ s
⊢ a ∉ erase (β := β) a s

Tactic:
rw [mem_erase, not_and_or, not_not]

Premises used: Finmap.mem_erase, Classical.not_not, not_and_or
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
h : a = a
⊢ a = a ∨ a ∉ s

Tactic:
left
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
⊢ lookup (β := β) a (erase (β := β) a s) = none

Tactic:
induction_on s <| AList.lookup_erase a

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

Tactic:
induction_on s fun _ => AList.lookup_erase_ne h

Premises used: Finmap.induction_on
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
s_1 : Finmap β
s : AList β
⊢ (erase (β := β) a (erase (β := β) a' (s.toFinmap (β := β)))).entries (β := β) =
    (erase (β := β) a' (erase (β := β) a (s.toFinmap (β := β)))).entries (β := β)

Tactic:
simp only [AList.erase_erase, erase_toFinmap]

Premises used: AList.erase_erase, Finmap.erase_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : AList β
⊢ insert (β := β) a b (s.toFinmap (β := β)) = (AList.insert (β := β) a b s).toFinmap (β := β)

Tactic:
simp [insert]

Premises used: Finmap.insert
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s_1 : Finmap β
s : AList β
h : a ∉ s.toFinmap (β := β)
⊢ (insert (β := β) a b (s.toFinmap (β := β))).entries (β := β) =
    Sigma.mk (β := β) a b ::ₘ s.toFinmap (β := β).entries (β := β)

Tactic:
simp [AList.entries_insert_of_notMem (mt mem_toFinmap.1 h), -entries_insert]

Premises used: mt, AList.entries_insert, Iff.mp, AList.entries_insert_of_notMem, Finmap.mem_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
s : Finmap β
⊢ a ∈ insert (β := β) a' b' s ↔ a = a' ∨ a ∈ s

Tactic:
induction_on s AList.mem_insert

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

Tactic:
simp only [insert_toFinmap, lookup_toFinmap, AList.lookup_insert]

Premises used: AList.lookup_insert, Finmap.insert_toFinmap, Finmap.lookup_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
s_1 : Finmap β
h : a' ≠ a
s : AList β
⊢ lookup (β := β) a' (insert (β := β) a b (s.toFinmap (β := β))) = lookup (β := β) a' (s.toFinmap (β := β))

Tactic:
simp only [insert_toFinmap, lookup_toFinmap, lookup_insert_ne h]

Premises used: AList.lookup_insert_ne, Finmap.insert_toFinmap, Finmap.lookup_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b b' : β a
s_1 : Finmap β
s : AList β
⊢ insert (β := β) a b' (insert (β := β) a b (s.toFinmap (β := β))) = insert (β := β) a b' (s.toFinmap (β := β))

Tactic:
simp only [insert_toFinmap, AList.insert_insert]

Premises used: AList.insert_insert, Finmap.insert_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a
b' : β a'
s_1 : Finmap β
h : a ≠ a'
s : AList β
⊢ insert (β := β) a' b' (insert (β := β) a b (s.toFinmap (β := β))) =
    insert (β := β) a b (insert (β := β) a' b' (s.toFinmap (β := β)))

Tactic:
simp only [insert_toFinmap, AList.toFinmap_eq, AList.insert_insert_of_ne _ h]

Premises used: AList.toFinmap_eq, Finmap.insert_toFinmap, AList.insert_insert_of_ne
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
xs : List (Sigma β)
⊢ (Sigma.mk (β := β) a b :: xs).toFinmap (β := β) = insert (β := β) a b (xs.toFinmap (β := β))

Tactic:
rfl

Premises used: List.toFinmap, Finmap.liftOn, Finmap.insert, List.kinsert, List.dedupKeys, List.foldr, AList.toFinmap, rfl
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Membership.mem (γ := Finmap β) (List.toFinmap (β := β) []) a ↔
    ∃ (b : β a), Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)

Tactic:
simp only [toFinmap_nil, notMem_empty, not_mem_nil, exists_false]

Premises used: Finmap.notMem_empty, exists_false, Finmap.toFinmap_nil, List.not_mem_nil
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
tail_ih : a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
cons :
  ∀ (fst_i : α) (snd_i : β fst_i),
    a ∈ (Sigma.mk (β := β) fst_i snd_i :: xs).toFinmap (β := β) ↔
      ∃ (b : β a), Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) fst_i snd_i :: xs
⊢ a ∈ (x :: xs).toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ x :: xs

Tactic:
obtain ⟨fst_i, snd_i⟩ := x
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih : a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
fst_i : α
snd_i : β fst_i
cons :
  (a = fst_i ∨ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs) ↔
    (a = fst_i ∧ ∃ (x : β a), x ≍ snd_i) ∨ ∃ (x : β a), Sigma.mk (β := β) a x ∈ xs
⊢ a ∈ (Sigma.mk (β := β) fst_i snd_i :: xs).toFinmap (β := β) ↔
    ∃ (b : β a), Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) fst_i snd_i :: xs

Tactic:
simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]

Premises used: exists_or, Finmap.toFinmap_cons, exists_and_left, Sigma.mk.inj_iff, List.mem_cons, Finmap.mem_insert
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih : a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
fst_i : α
snd_i : β fst_i
⊢ (a = fst_i ∨ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs) ↔
    (a = fst_i ∧ ∃ (x : β a), x ≍ snd_i) ∨ ∃ (x : β a), Sigma.mk (β := β) a x ∈ xs

Tactic:
(or_congr_left <| and_iff_left_of_imp ?_).symm

Premises used: and_iff_left_of_imp, or_congr_left, Iff.symm
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih : a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
fst_i : α
snd_i : β fst_i
cons : a = fst_i → ∃ (x : β a), x ≍ snd_i
⊢ (a = fst_i ∨ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs) ↔
    (a = fst_i ∧ ∃ (x : β a), x ≍ snd_i) ∨ ∃ (x : β a), Sigma.mk (β := β) a x ∈ xs

Tactic:
refine (or_congr_left <| and_iff_left_of_imp ?_).symm

Premises used: and_iff_left_of_imp, or_congr_left, Iff.symm
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih : a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
snd_i : β a
⊢ ∃ (x : β a), x ≍ snd_i

Tactic:
simp only [exists_eq, heq_iff_eq]

Premises used: heq_iff_eq, exists_eq
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
nil :
  Membership.mem (γ := Finmap β) (List.toFinmap (β := β) []) a ↔
    ∃ (b : β a), Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)
cons :
  ∀ (x : Sigma β) (xs : List (Sigma β)),
    (a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs) →
      (a ∈ (x :: xs).toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ x :: xs)
⊢ a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs

Tactic:
induction xs with
  | nil => simp only [toFinmap_nil, notMem_empty, not_mem_nil, exists_false]
  | cons x xs =>
    obtain ⟨fst_i, snd_i⟩ := x
    simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]
    refine (or_congr_left <| and_iff_left_of_imp ?_).symm
    rintro rfl
    simp only [exists_eq, heq_iff_eq]

Premises used: exists_or, and_iff_left_of_imp, Finmap.toFinmap_cons, heq_iff_eq, exists_eq, exists_and_left, List.cons, Finmap.notMem_empty, or_congr_left, exists_false, Finmap.toFinmap_nil, Sigma.mk.inj_iff, List.mem_cons, Iff.symm, List.not_mem_nil, Finmap.mem_insert, rfl, List.nil
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b b' : β a
⊢ insert (β := β) a b (singleton (β := β) a b') = singleton (β := β) a b

Tactic:
simp only [singleton, Finmap.insert_toFinmap, AList.insert_singleton_eq]

Premises used: AList.insert_singleton_eq, Finmap.singleton, Finmap.insert_toFinmap
-- Module: Mathlib.Data.Finmap
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₂)

Tactic:
simp [perm_lookup p, toFinmap_eq, perm_erase p]

Premises used: AList.toFinmap_eq, AList.perm_erase, AList.perm_lookup
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s_1 : Finmap β
s : AList β
⊢ extract (β := β) a (s.toFinmap (β := β)) =
    (lookup (β := β) a (s.toFinmap (β := β)), erase (β := β) a (s.toFinmap (β := β)))

Tactic:
simp [extract]

Premises used: Finmap.extract
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
⊢ a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂

Tactic:
induction_on₂ s₁ s₂ fun _ _ => AList.mem_union

Premises used: Finmap.induction_on₂
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁ s₂ : AList β
⊢ s₁.toFinmap (β := β) ∪ s₂.toFinmap (β := β) = (s₁ ∪ s₂).toFinmap (β := β)

Tactic:
simp [(· ∪ ·), union]

Premises used: Finmap.union, Union.union
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 : Finmap β
s₁ s₂ : AList β
⊢ ∀ (a : α),
    a ∈ (s₁.toFinmap (β := β) ∪ s₂.toFinmap (β := β)).keys (β := β) ↔
      a ∈ s₁.toFinmap (β := β).keys (β := β) ∪ s₂.toFinmap (β := β).keys (β := β)

Tactic:
simp [keys]

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

Tactic:
induction_on₂ s₁ s₂ fun _ _ => AList.lookup_union_left

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

Tactic:
induction_on₂ s₁ s₂ fun _ _ => AList.lookup_union_right

Premises used: Finmap.induction_on₂
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
pos : ∀ (h' : a ∈ s₁), lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
neg : ∀ (h' : a ∉ s₁), lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁

Tactic:
by_cases h' : a ∈ s₁
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∈ s₁
pos pos₁ : lookup (β := β) a s₁ = lookup (β := β) a s₁
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁

Tactic:
rw [lookup_union_left h']

Premises used: Finmap.lookup_union_left
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
neg : lookup (β := β) a s₂ = lookup (β := β) a s₁
neg₁ : none = lookup (β := β) a s₁
neg₂ neg₃ : Eq.{v + 1} (α := Option (β a)) none none
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁

Tactic:
rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']

Premises used: Iff.mpr, Finmap.lookup_eq_none, Finmap.lookup_union_right
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : Finmap β
⊢ lookup (β := β) a (s₁ ∪ s₂) = some b ↔ b ∈ lookup (β := β) a s₁ ∨ a ∉ s₁ ∧ b ∈ lookup (β := β) a s₂

Tactic:
induction_on₂ s₁ s₂ fun _ _ => AList.mem_lookup_union

Premises used: Finmap.induction_on₂
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : Finmap β
⊢ b ∈ lookup (β := β) a (s₁ ∪ s₂) ↔ b ∈ lookup (β := β) a s₁ ∨ a ∉ s₁ ∧ b ∈ lookup (β := β) a s₂

Tactic:
induction_on₂ s₁ s₂ fun _ _ => AList.mem_lookup_union

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

Tactic:
induction_on₃ s₁ s₂ s₃ fun _ _ _ => AList.mem_lookup_union_middle

Premises used: Finmap.induction_on₃
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s₁ s₂ : Finmap β
a₁ a₂ : AList β
⊢ insert (β := β) a b (a₁.toFinmap (β := β) ∪ a₂.toFinmap (β := β)) =
    insert (β := β) a b (a₁.toFinmap (β := β)) ∪ a₂.toFinmap (β := β)

Tactic:
simp [AList.insert_union]

Premises used: AList.insert_union
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 s₃_1 : Finmap β
s₁ s₂ s₃ : AList β
⊢ s₁.toFinmap (β := β) ∪ s₂.toFinmap (β := β) ∪ s₃.toFinmap (β := β) =
    s₁.toFinmap (β := β) ∪ (s₂.toFinmap (β := β) ∪ s₃.toFinmap (β := β))

Tactic:
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

Premises used: AList.toFinmap_eq, AList.union_assoc, Finmap.union_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 : Finmap β
s₁ : AList β
⊢ AList.toFinmap (β := β) ∅ ∪ s₁.toFinmap (β := β) = s₁.toFinmap (β := β)

Tactic:
simp [-empty_toFinmap, union_toFinmap]

Premises used: Finmap.empty_toFinmap, Finmap.union_toFinmap
-- Module: Mathlib.Data.Finmap
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 : Finmap β
s₁ : AList β
⊢ s₁.toFinmap (β := β) ∪ AList.toFinmap (β := β) ∅ = s₁.toFinmap (β := β)

Tactic:
simp [-empty_toFinmap, union_toFinmap]

Premises used: Finmap.empty_toFinmap, Finmap.union_toFinmap