mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ map✝ = fun {α β} ↦ Equiv.map eqv

Tactic:
ext

Goal state after:
case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = Equiv.map eqv x✝¹ x✝
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ mapConst✝ = fun {α β} ↦ Equiv.map eqv ∘ Function.const β

Tactic:
ext

Goal state after:
case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³
x✝ : t' x✝²
⊢ mapConst✝ x✝¹ x✝ = (Equiv.map eqv ∘ Function.const x✝²) x✝¹ x✝
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
⊢ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } =
    { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
      { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
ext

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ↔
    s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ↔
    s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
constructor

Goal state after:
case mk.mk.mp
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

case mk.mk.mpr
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
        { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case neg
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
h2 : ¬Even l.length
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
rcases l with - | ⟨x, l⟩
    · exact (h2 .zero).elim
    grind [hl.tail.two_mul_count_bool_of_even]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ DFinsupp.toMultiset.comp toDFinsupp = AddMonoidHom.id (Multiset α)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ a✝ : α
⊢ count a✝ ((DFinsupp.toMultiset.comp toDFinsupp) {x✝}) = count a✝ ((AddMonoidHom.id (Multiset α)) {x✝})
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp.comp DFinsupp.toMultiset = AddMonoidHom.id (Π₀ (x : α), ℕ)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ i✝ : α
⊢ (((toDFinsupp.comp DFinsupp.toMultiset).comp (DFinsupp.singleAddHom (fun i ↦ ℕ) x✝)) 1) i✝ =
    (((AddMonoidHom.id (Π₀ (x : α), ℕ)).comp (DFinsupp.singleAddHom (fun i ↦ ℕ) x✝)) 1) i✝
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → DecidableEq (α i)
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), IsBotZeroClass (α i)
inst✝¹ : (i : ι) → OrderBot (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1

Tactic:
card_Iio_eq_card_Iic_sub_one,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → DecidableEq (α i)
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), IsBotZeroClass (α i)
inst✝¹ : (i : ι) → OrderBot (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iic f) - 1 = ∏ i ∈ f.support, #(Iic (f i)) - 1
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

Tactic:
ext

Goal state after:
α✝ β✝ : Type u_1
x✝¹ : α✝
x✝ : Erased β✝
⊢ (Functor.mapConst x✝¹ x✝).out = ((Functor.map ∘ Function.const β✝) x✝¹ x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ : Type u_1
x✝ : Erased α✝
⊢ id <$> x✝ = x✝

Tactic:
ext

Goal state after:
α✝ : Type u_1
x✝ : Erased α✝
⊢ (id <$> x✝).out = x✝.out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ x✝ <* y✝ = Function.const β✝ <$> x✝ <*> y✝

Tactic:
ext

Goal state after:
α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (x✝ <* y✝).out = (Function.const β✝ <$> x✝ <*> y✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ x✝ *> y✝ = Function.const α✝ id <$> x✝ <*> y✝

Tactic:
ext

Goal state after:
α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (x✝ *> y✝).out = (Function.const α✝ id <$> x✝ <*> y✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ pure g✝ <*> x✝ = g✝ <$> x✝

Tactic:
ext

Goal state after:
α✝ β✝ : Type u_1
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (pure g✝ <*> x✝).out = (g✝ <$> x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝

Tactic:
ext

Goal state after:
α✝ β✝ : Type u_1
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
        let a ← x✝
        pure (f✝ a)).out =
    (f✝ <$> x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    f✝ <*> x✝

Tactic:
ext

Goal state after:
α✝ β✝ : Type u_1
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
        let x ← f✝
        x <$> x✝).out =
    (f✝ <*> x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ pure x✝ >>= f✝ = f✝ x✝

Tactic:
ext

Goal state after:
α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ (pure x✝ >>= f✝).out = (f✝ x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ γ✝ : Type u_1
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝

Tactic:
ext

Goal state after:
α✝ β✝ γ✝ : Type u_1
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ (x✝ >>= f✝ >>= g✝).out = (x✝ >>= fun x ↦ f✝ x >>= g✝).out
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
⊢ a ∈ q ↔ a ∈ pure (q.get p)

Tactic:
by simpa using ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ i = 0

Tactic:
ext

Goal state after:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ ↑i = ↑0
Module: Mathlib.Data.Fin.Tuple.Curry

Goal state before:
pp: n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
⊢ (curry f).uncurry = f

Tactic:
by
  ext args
  induction n with
  | zero => exact congrArg f (Subsingleton.allEq _ _)
  | succ n ih => exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))

Goal state after:
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    congr x✝ inst✝ ⋯ empty

Tactic:
exact Nat.noConfusion <| h.symm.trans ‹_›

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
i : Fin xs.length
⊢ (fun x ↦ ⟨List.idxOf x xs, ⋯⟩) (xs.get i) = i

Tactic:
ext

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
i : Fin xs.length
⊢ ↑((fun x ↦ ⟨List.idxOf x xs, ⋯⟩) (xs.get i)) = ↑i
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
⊢ insertRec H0 IH { entries := [], nodupKeys := ⋯ } = H0

Tactic:
rw [insertRec]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ insertRec H0 IH { entries := c :: l, nodupKeys := ⋯ } ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })

Tactic:
rw [insertRec]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ ⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (insertRec H0 IH { entries := l, nodupKeys := ⋯ })) ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s ∧ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s

Tactic:
constructor

Goal state after:
case left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s

case right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂

Tactic:
ext

Goal state after:
α : 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✝
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝ ↔
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝ →
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝ →
    dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
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₂
⊢ dlookup a l₁ = dlookup a l₂

Tactic:
have nd₂ := (perm_nodupKeys p).mp nd₁
  ext b; simp only [← Option.mem_def, mem_dlookup_iff nd₁, mem_dlookup_iff nd₂, p.mem_iff]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
⊢ (fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
      ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩) =
    ⟨(s, f), hf⟩

Tactic:
ext

Goal state after:
case fst
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
a✝ : α
⊢ a✝ ∈
      (↑((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
            ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩))).1 ↔
    a✝ ∈ (↑⟨(s, f), hf⟩).1

case snd
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
x✝ : α
a✝ : β x✝
⊢ (↑((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
              ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩))).2
        x✝ =
      some a✝ ↔
    (↑⟨(s, f), hf⟩).2 x✝ = some a✝
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
b' : β a
h' : ⟨a, b'⟩ ∈ l
h✝ : decide (a = a) = true
⊢ some ⟨a, b⟩ = some ⟨a, b'⟩

Tactic:
simp [nd.eq_of_mk_mem h h']

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

Goal state after:
inst✝ : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
a✝ : γ
⊢ a✝ ∈ image₂ f s t ↔ a✝ ∈ f <$> s <*> t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ i ∈ u, ∃ a_1, (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = a) ↔
    ∃ i, (∃ i_1, (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = a

Tactic:
constructor

Goal state after:
case mp
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ i ∈ u, ∃ a_1, (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = a) →
    ∃ i, (∃ i_1, (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_2 ∈ s, i a_2 = a

case mpr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ i, (∃ i_1, (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = a) →
    ∃ i ∈ u, ∃ a_2, (∃ i ∈ t, ∃ a ∈ s, i a = a_2) ∧ i a_2 = a
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons.mk
α : 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 ∧
    (kerase fst✝ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs)).NodupKeys

Tactic:
constructor

Goal state after:
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

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: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
⊢ a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys

Tactic:
induction l₁ generalizing l₂ with
  | nil => simp
  | cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
⊢ pimage (fun x ↦ Part.some (f x)) s = image f s

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
a✝ : β
⊢ a✝ ∈ pimage (fun x ↦ Part.some (f x)) s ↔ a✝ ∈ image f s
Module: Mathlib.Data.Finset.PImage

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
a✝ : β
⊢ a✝ ∈ pimage f ∅ ↔ a✝ ∈ ∅
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : f b = m ∧ ¬m = 0
n : M
hc : f b = n ∧ ¬n = 0
⊢ (b, m) = (b, n)

Tactic:
← hc.1,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : f b = m ∧ ¬m = 0
n : M
hc : f b = n ∧ ¬n = 0
⊢ (b, m) = (b, f b)
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ f.toAList.keys.toFinset = f.support

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a✝ : α
⊢ a✝ ∈ f.toAList.keys.toFinset ↔ a✝ ∈ f.support
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
⊢ (s.sum id).support = s.sup Finsupp.support

Tactic:
suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! Multiset.support_sum_eq s.1 this
    exact (Finset.sum_val _).symm

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ ↑(f.neLocus g) = {x | f x ≠ g x}

Tactic:
ext

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
x✝ : α
⊢ x✝ ∈ ↑(f.neLocus g) ↔ x✝ ∈ {x | f x ≠ g x}
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
⊢ f.neLocus 0 = f.support

Tactic:
ext

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g ↦ F f g
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g ↦ F f g
a✝ : α
⊢ a✝ ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a✝ ∈ g₁.neLocus g₂
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f ↦ F f g
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f ↦ F f g
a✝ : α
⊢ a✝ ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a✝ ∈ f₁.neLocus f₂
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
a✝ : α
⊢ a✝ ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a✝ ∈ f.neLocus g
Module: Mathlib.Data.Finsupp.Pointwise

Goal state before:
pp: α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
r : β
f : α → β
m : α →₀ β
⊢ (r • f) • m = r • f • m

Tactic:
ext

Goal state after:
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
r : β
f : α → β
m : α →₀ β
a✝ : α
⊢ ((r • f) • m) a✝ = (r • f • m) a✝