mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
X✝ Y✝ : Profiniteᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : CostructuredArrow toProfinite.op X✝
⊢ colimit.ι (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F)
          { pt := colimit (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F),
            ι :=
              {
                app := fun g ↦
                  colimit.ι (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F)
                    ((CostructuredArrow.map x✝¹).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op Y✝ ⋙ toProfinite.op ⋙ F)
          (Profinite.Extend.cocone F (Opposite.unop Y✝)) =
    colimit.ι (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toProfinite.op X✝ ⋙ toProfinite.op ⋙ F)
          (Profinite.Extend.cocone F (Opposite.unop X✝)) ≫
        F.map x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ (∀ (X_1 : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op X_1))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op X'))) x =
              (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y) ↔
    ∀ (S : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
simp_rw [LightProfinite.effectiveEpi_iff_surjective]

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X✝ Y✝ : LightProfiniteᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : CostructuredArrow toLightProfinite.op X✝
⊢ colimit.ι (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F)
          { pt := colimit (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F),
            ι :=
              {
                app := fun g ↦
                  colimit.ι (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F)
                    ((CostructuredArrow.map x✝¹).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F)
          (LightProfinite.Extend.cocone F (Opposite.unop Y✝)) =
    colimit.ι (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F) x✝ ≫
      colimit.desc (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F)
          (LightProfinite.Extend.cocone F (Opposite.unop X✝)) ≫
        F.map x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: n✝ : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
n : ℕ
⊢ lim.map f ≫ limit.π Y✝ { as := n } =
    ((Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom) ≫ limit.π Y✝ { as := n }

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ i ∈ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ j ∈ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
x✝ : ↑(condensedSetToTopCat.obj Y)
⊢ (ConcreteCategory.hom (Y.obj.map (𝟙 (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))) x✝ =
    (ConcreteCategory.hom (𝟙 (condensedSetToTopCat.obj Y))) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
β γ : Type u
f : β → γ
⊢ traverse (pure ∘ f) = pure ∘ map f

Tactic:
ext
  exact traverse_eq_map_id _ _

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.3
x✝¹ : Perm α
x✝ : α
⊢ (((Equiv.refl α).symm.trans x✝¹).trans (Equiv.refl α)) x✝ = (id x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α✝ β✝ γ✝ : Type ?u.3
x✝³ : α✝ ≃ β✝
x✝² : β✝ ≃ γ✝
x✝¹ : Perm α✝
x✝ : γ✝
⊢ (((x✝³.trans x✝²).symm.trans x✝¹).trans (x✝³.trans x✝²)) x✝ =
    (((fun p ↦ (x✝².symm.trans p).trans x✝²) ∘ fun p ↦ (x✝³.symm.trans p).trans x✝³) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.4
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ Finset.map (Equiv.refl α).toEmbedding x✝ ↔ a✝ ∈ id x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
⊢ [] ∈ traverse f [] ↔ Forall₂ (fun b a ↦ b ∈ f a) [] []

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
⊢ [] ∈ traverse f (a :: as) ↔ Forall₂ (fun b a ↦ b ∈ f a) [] (a :: as)

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f [] ↔ Forall₂ (fun b a ↦ b ∈ f a) (b :: bs) []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ fz ∉ Finset.map { toFun := fs, inj' := ⋯ } elems

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ FreeMonoid.toList (foldMap FreeMonoid.of xs).reverse.reverse =
    (List.foldr cons [] (FreeMonoid.toList (foldMap FreeMonoid.of xs)).reverse).reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: case nil
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
n : ℕ
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := n } []).down = [].length + n

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ : Type u
x✝ : WriterT ω M α✝
⊢ (id <$> x✝).run = x✝.run

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝
x✝ : α✝ → WriterT ω M β✝
⊢ (pure x✝¹ >>= x✝).run = (x✝ x✝¹).run

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : WriterT ω M α✝
⊢ (do
        let y ← x✝
        pure (x✝¹ y)).run =
    (x✝¹ <$> x✝).run

Tactic:
simp

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'

Tactic:
simp

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : TypeVec.{?u.30} (n + 1) → Sort u_1
f : (t : Type ?u.30) → (v : TypeVec.{?u.30} n) → β (v ::: t)
v : TypeVec.{?u.30} (n + 1)
⊢ β (v.drop ::: v.last) = β v

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : StateT σ m α), (callCC fun x ↦ dummy) = dummy

Tactic:
by
    intros
    simp only [callCC, StateT.callCC, @callCC_dummy m _]
    ext; rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
r : α₁ → m₁ r₁
⊢ (fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) ((fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) f) r = f r

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
r : α₂ → m₂ r₂
⊢ (fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) ((fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) f) r = f r

Tactic:
simp

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case none
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) none) = none

Tactic:
simp

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case some
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
val✝ : α✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) (some val✝)) = some val✝

Tactic:
simp

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case none
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) none) = none

Tactic:
simp

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case some
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
val✝ : β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) (some val✝)) = some val✝

Tactic:
simp

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (OnePoint.some ⁻¹' {↑i})

Tactic:
simp

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ σ (Option.some x) s ∈ fibres π σ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ toSubtype p ⊚ ofSubtype p = id

Tactic:
ext i x
  induction i <;> simp only [id, toSubtype, comp, ofSubtype] at *
  simp [*]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f

Tactic:
simp

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ 2 ^ (w + 1) = ↑(2 ^ (w + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: case zero
w : ℕ
x : BitVec w
⊢ (x ^ 0).toFin = x.toFin ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Bool.AllAny

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (l.all fun a ↦ decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Bool.AllAny

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (l.any fun a ↦ decide (p a)) = true ↔ ∃ a, a ∈ l ∧ p a

Tactic:
simp

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ 𝟙 T ≫ π = 𝟙 T ≫ π

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ }.F.f s = F.F.f (E.symm s)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : DecidableEq α
x✝ : Set α
h : x✝ ∈ cofinite.sets
⊢ { f := fun s ↦ {a | a ∉ s}, pt := ∅, inf := fun x1 x2 ↦ x1 ∪ x2, inf_le_left := ⋯, inf_le_right := ⋯ }.f
      (Finite.toFinset h) ⊆
    x✝

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : 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✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∩ t)) i = (toDFinsupp s ⊓ toDFinsupp t) i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∪ t)) i = (toDFinsupp s ⊔ toDFinsupp t) i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset (f ⊓ g)) = Multiset.toDFinsupp (toMultiset f ∩ toMultiset g)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset (f ⊔ g)) = Multiset.toDFinsupp (toMultiset f ∪ toMultiset g)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Erased

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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Erased

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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Erased

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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Erased

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

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ ∑ a ∈ ∅, ⨆ i, f a i = ⨆ i, ∑ a ∈ ∅, f a i

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
q : Semiquot α
⊢ ∀ (a : α), a ∈ id <$> q ↔ a ∈ q

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β : Type u_3
x : α
f : α → Semiquot β
⊢ ∀ (a : β), a ∈ pure x >>= f ↔ a ∈ f x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β γ : Type u_3
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), (∃ a_1, (∃ a ∈ s, a_1 ∈ f a) ∧ a ∈ g a_1) ↔ ∃ a_1 ∈ s, ∃ a_2 ∈ f a_1, a ∈ g a_2

Tactic:
exact fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩,
      fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩

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:
simp

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

Goal state before:
pp: case succ.cast
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝¹ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
i : Fin (m + 1)
a✝ : take (m + 1).succ h v i.succ = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.succ
⊢ take (m + 1).succ h v i.castSucc = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.castSucc

Tactic:
simp

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
x : α
⊢ xs.get ((fun x ↦ ⟨List.idxOf x xs, ⋯⟩) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
x : α
⊢ equiv.symm (equiv x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : PUnit.{?u.8 + 1}
⊢ x ∈ [PUnit.unit]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case mk
α : Type u
β✝ : α → Type v
β : Type ?u.23
inst✝¹ : FinEnum α
inst✝ : FinEnum β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ∈ toList α ×ˢ toList β

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case inl
α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : α
⊢ Sum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case inr
α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : β
⊢ Sum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ ∀ (x : Fin n), x ∈ List.finRange n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case nil
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ s ∈ enum [] ↔ ∀ x ∈ s, x ∈ []

Tactic:
simp [enum, eq_empty_iff_forall_notMem]

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

Goal state before:
pp: n✝ : ℕ
α : Type u_2
m : ℕ
h : m ≤ n✝
v : Fin n✝ → α
n : ℕ
h1 : n < (List.ofFn (take m h v)).length
h2 : n < (List.take m (List.ofFn v)).length
⊢ (List.ofFn (take m h v)).get ⟨n, h1⟩ = (List.take m (List.ofFn v)).get ⟨n, h2⟩

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
n : ℕ
h1 : n < (List.ofFn (take m h l.get)).length
h2 : n < (List.take m l).length
⊢ (List.ofFn (take m h l.get)).get ⟨n, h1⟩ = (List.take m l).get ⟨n, h2⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : Finset α), x ∈ enum (toList α)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case mk
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
fst✝ : α
snd✝ : β fst✝
⊢ ⟨fst✝, snd✝⟩ ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Type v
inst✝¹ : (a : α) → FinEnum (β a)
inst✝ : Decidable α
h : α
x✝ : (a : α) ×' β a
a : α
Ba : β a
⊢ ⟨a, Ba⟩ ∈ List.map (PSigma.mk h) (toList (β h))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ (a : α), β a
⊢ ∀ (x : (a : α) ×' β a), x ∈ [⟨⋯, ⋯⟩]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
⊢ ∀ (x : { x // x ∈ xs }), x ∈ xs.attach

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : FinEnum α
x✝ : α
⊢ x✝ ∈ map equiv.symm.toEmbedding univ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : UInt8
⊢ UInt8.ofFin x.toFin = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : UInt16
⊢ UInt16.ofFin x.toFin = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : UInt32
⊢ UInt32.ofFin x.toFin = x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : UInt64
⊢ UInt64.ofFin x.toFin = x

Tactic:
simp

Goal state after: