mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 64)
⊢ (UInt64.ofFin x).toFin = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Int8
⊢ (Int8.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int8.toBitVec) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 8)
⊢ (BitVec.toFin ∘ Int8.toBitVec) ((Int8.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Int16
⊢ (Int16.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int16.toBitVec) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 16)
⊢ (BitVec.toFin ∘ Int16.toBitVec) ((Int16.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Int32
⊢ (Int32.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int32.toBitVec) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 32)
⊢ (BitVec.toFin ∘ Int32.toBitVec) ((Int32.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Int64
⊢ (Int64.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int64.toBitVec) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 64)
⊢ (BitVec.toFin ∘ Int64.toBitVec) ((Int64.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
x : BitVec n
⊢ { toFin := x.toFin } = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
x : Fin (2 ^ n)
⊢ { toFin := x }.toFin = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case cons.some
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
a : α
⊢ (match some a with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match some a with
      | some b => #[].toListAppend (b :: tl)
      | none => go f tl (#[].push hd))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match none with
    | some b => b :: l
    | none => (#[].push a).toListAppend (lookmap.go f l #[])) =
    a :: lookmap.go f l #[]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case some
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
b : α
h : g a = some b
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
simp [lookmap_cons_some _ _ h, lookmap_cons_some _ _ (H₁.trans h)]

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case h
α : Type u_1
f : α → Option α
l : List α
⊢ ∀ (a b : α), b ∈ f a → () = ()

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case nil
α : Type u_1
f : α → Option α
l₁ l₂ : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) []
⊢ lookmap f [] ~ lookmap f []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k' : α
v : β k'
⊢ lookup k' (insert k' v l) = none ↔ k' ≠ k' ∧ lookup k' l = none

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : AList β
⊢ (s ∪ ∅).entries = s.entries

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
i✝ : ℕ
a✝ : Sigma β
⊢ (insert a b (s₁ ∪ s₂)).entries[i✝]? = some a✝ ↔ (insert a b s₁ ∪ s₂).entries[i✝]? = some a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ (dlookup a []).isSome = true ↔ a ∈ [].keys

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
nd₂ : l₂.NodupKeys
⊢ dlookup a l₁ = dlookup a l₂

Tactic:
ext b

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
nd₂ : l₂.NodupKeys
b : β a
⊢ dlookup a l₁ = some b ↔ dlookup a l₂ = some b
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ lookupAll a [] = [] ↔ ∀ (b : β a), ¬⟨a, b⟩ ∈ []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ¬b = b → ⟨a, b⟩ ∈ l

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ (lookupAll a []).head? = dlookup a []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (lookupAll a (⟨a, b⟩ :: l)).head? = dlookup a (⟨a, b⟩ :: l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: case e'_1
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
x✝ : α
⊢ (∀ x ∈ s, x < x✝) ↔ s.max' hs < x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
x✝ : α
⊢ (∀ y ∈ t, x✝ < y) ↔ x✝ < t.min' ht

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ b ∈ lookupAll a [] ↔ ⟨a, b⟩ ∈ []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ ∀ (x : (a : α) × β a),
    x.fst ∈ (↑f).1 ∧ (↑f).2 x.fst = some x.snd →
      ∀ (y : (a : α) × β a), y.fst ∈ (↑f).1 ∧ (↑f).2 y.fst = some y.snd → x.fst = y.fst → x = y

Tactic:
rintro ⟨i, x⟩ ⟨_, hx⟩ ⟨j, y⟩ ⟨_, hy⟩ (rfl : i = j)

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
i : α
x : β i
left✝¹ : ⟨i, x⟩.fst ∈ (↑f).1
hx : (↑f).2 ⟨i, x⟩.fst = some ⟨i, x⟩.snd
y : β i
left✝ : ⟨i, y⟩.fst ∈ (↑f).1
hy : (↑f).2 ⟨i, y⟩.fst = some ⟨i, y⟩.snd
⊢ ⟨i, x⟩ = ⟨i, y⟩
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ map (Sigma.mk a) (lookupAll a []) <+ []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : Finmap β
⊢ ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ })
        ((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩) f)).entries =
    f.entries

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ (fun b ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) = fun b ↦ (∀ x ∈ hsf.toFinset, x < b) ∧ ∀ y ∈ htf.toFinset, b < y

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ (fun b ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) = fun b ↦ (∀ x ∈ hs.toFinset, x < b) ∧ ∀ y ∈ ht.toFinset, b < y

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: ⊢ ∀ {α : Type u_1} (x : Multiset α), id <$> x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: ⊢ ∀ {α β γ : Type u_1} (g : α → β) (h : β → γ) (x : Multiset α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ (replace a b ⟦s⟧).keys = ⟦s⟧.keys

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
s : AList β
⊢ a' ∈ replace a b ⟦s⟧ ↔ a' ∈ ⟦s⟧

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ (erase a ⟦s⟧).keys = ⟦s⟧.keys.erase a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ a' ∈ erase a ⟦s⟧ ↔ a' ≠ a ∧ a' ∈ ⟦s⟧

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ ¬(b :: c :: l).length ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case refine_2
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s ↦ decide (a = s.fst)) a_1 → a_1 = b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: inst✝ : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
⊢ image₂ f s t = f <$> s <*> t

Tactic:
ext
  simp [mem_sup]

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s <* t = (const β✝ <$> s).sup fun f ↦ image f t

Tactic:
fmap_def,

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s <* t = (image (const β✝) s).sup fun f ↦ image f t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih : hd.fst ∈ tl.keys → ∃ b l₁ l₂, ¬hd.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨hd.fst, b⟩ :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ (hd :: tl).keys
⊢ ¬hd.fst ∈ [].keys

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih : hd.fst ∈ tl.keys → ∃ b l₁ l₂, ¬hd.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨hd.fst, b⟩ :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ (hd :: tl).keys
⊢ kerase hd.fst (hd :: tl) = [] ++ tl

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s *> t = (const α✝ id <$> s).sup fun f ↦ image f t

Tactic:
fmap_def,

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s *> t = (image (const α✝ id) s).sup fun f ↦ image f t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p✝ : a₁ ∈ l.keys
w✝² : β a₂
w✝¹ w✝ : List (Sigma β)
left✝ : ¬a₂ ∈ w✝¹.keys
p : a₁ ∈ (w✝¹ ++ ⟨a₂, w✝²⟩ :: w✝).keys
q : a₂ ∈ (w✝¹ ++ ⟨a₂, w✝²⟩ :: w✝).keys
⊢ a₁ ∈ (w✝¹ ++ w✝).keys

Tactic:
by simpa [keys, h] using p

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ (∅.inf fun i ↦ (t i).sup (f i)) = (∅.pi t).sup fun g ↦ ∅.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ ((Prod.mk <$> s).sup fun f ↦ image f t) = ((fun b a ↦ (a, b)) <$> t).sup fun f ↦ image f s

Tactic:
fmap_def,

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ ((image Prod.mk s).sup fun f ↦ image f t) = (image (fun b a ↦ (a, b)) t).sup fun f ↦ image f s
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ l₁ ~ l₂ → List.kerase a l₁ ~ List.kerase a l₂

Tactic:
apply Perm.eraseP

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ Pairwise (fun a_1 b ↦ decide (a = a_1.fst) = true → decide (a = b.fst) = true → False) l₁
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s ×ˢ t = t.biUnion fun b ↦ image (fun a ↦ (a, b)) s

Tactic:
rw [product_eq_biUnion_right]

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
nd : [].NodupKeys
⊢ ¬a ∈ (kerase a []).keys

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
⊢ sizeOf (kerase x []) ≤ sizeOf []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ (kerase fst✝ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs)).keys

pp: case cons.mk.right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ (kerase fst✝ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs)).NodupKeys

Tactic:
· simp only [keys_kerase]
      apply l_ih.not_mem_erase

Goal state after:
case cons.mk.right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ (kerase fst✝ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs)).NodupKeys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
⊢ a ∈ ([].kunion l₂).keys ↔ a ∈ [].keys ∨ a ∈ l₂.keys

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
tail✝ : List (Sigma β)
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
ih :
  ∀ {l₂ : List (Sigma β)},
    ⟨a', snd✝⟩.fst ∈ tail✝.keys → dlookup ⟨a', snd✝⟩.fst (tail✝.kunion l₂) = dlookup ⟨a', snd✝⟩.fst tail✝
⊢ dlookup ⟨a', snd✝⟩.fst ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup ⟨a', snd✝⟩.fst (⟨a', snd✝⟩ :: tail✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
snd✝ : β a
⊢ dlookup a (⟨a, snd✝⟩ :: tail✝.kunion (kerase ⟨a, snd✝⟩.fst l₂)) = dlookup a (⟨a, snd✝⟩ :: tail✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
h : ¬a ∈ [].keys
⊢ dlookup a ([].kunion l₂) = dlookup a l₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₂ : List (Sigma β)
⊢ b ∈ dlookup a ([].kunion l₂) ↔ b ∈ dlookup a [] ∨ ¬a ∈ [].keys ∧ b ∈ dlookup a l₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
snd✝ : β a
⊢ b ∈ dlookup a ((⟨a, snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a, snd✝⟩ :: tail✝) ∨ ¬a ∈ (⟨a, snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.PImage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
a✝ : β
⊢ a✝ ∈ pimage f ∅ ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ (∃ b ∈ none, decide (b ≠ 0) = true) ↔ none.getD 0 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case some
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
val✝ : M
⊢ (∃ b ∈ some val✝, decide (b ≠ 0) = true) ↔ (some val✝).getD 0 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
⊢ [].sum.support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ (lookup a l).getD 0 = x ↔ x ∈ lookup a l

Tactic:
rcases lookup a l with - | m

Goal state after:
case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ none.getD 0 = x ↔ x ∈ none

case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
m : M
⊢ (some m).getD 0 = x ↔ x ∈ some m
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ s.sum id = s.val.sum

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ (lookup a l).getD 0 = 0 ↔ lookup a l = none ∨ 0 ∈ lookup a l

Tactic:
rcases lookup a l with - | m

Goal state after:
case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ none.getD 0 = 0 ↔ none = none ∨ 0 ∈ none

case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
⊢ (some m).getD 0 = 0 ↔ some m = none ∨ 0 ∈ some m
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ∪ x2) ∅ [] ↔ ∃ f ∈ [], f x ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ none.getD 0 = 0 ↔ none = none ∨ 0 ∈ none

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
⊢ (some m).getD 0 = 0 ↔ some m = none ∨ 0 ∈ some m

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
⊢ (insert a m l).lookupFinsupp = l.lookupFinsupp.update a m

Tactic:
ext b

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
b : α
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hl : Pairwise (_root_.Disjoint on Finsupp.support) []
⊢ [].sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ ⟨i, x⟩.snd ∈ update g i (insert x (g i)) ⟨i, x⟩.fst

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
⊢ f ∈ (map Finsupp.support tl).toFinset → _root_.Disjoint hd.support (id f)

Tactic:
hf

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : f ∈ (map Finsupp.support tl).toFinset
⊢ _root_.Disjoint hd.support (id f)
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) s
⊢ s.sum.support = (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn with

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a : List (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M))) a = ↑l
hd : List.Pairwise (Disjoint on Finsupp.support) l
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup

Tactic:
suffices a.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! List.support_sum_eq a this
    simp only [quot_mk_to_coe'', map_coe, sup_coe,
      Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M))) a = ↑l
hd : List.Pairwise (Disjoint on Finsupp.support) l
⊢ List.Pairwise (Disjoint on Finsupp.support) a