mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'}
  [inst_1 : (L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {n : ℕ}
  {φ : (L.withConstants α).BoundedFormula β n} {v : β → M} {xs : Fin n → M},
  (FirstOrder.Language.BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) v) xs ↔
    φ.Realize v xs
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, (m₁ \ m₂).getKey! k = if k ∈ m₂ then default else m₁.getKey! k
-- Mathlib.LinearAlgebra.Prod
/-- The coprod function `x : M × M₂ ↦ f x.1 + g x.2` is a linear map.  -/
LinearMap.coprod : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R M₃] → (M →ₗ[R] M₃) → (M₂ →ₗ[R] M₃) → M × M₂ →ₗ[R] M₃
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_mem_unit : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.ExtTreeMap α Unit cmp}, (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁ = t₂
-- Mathlib.Algebra.Free
FreeMagma.toFreeSemigroup.eq_1 : ∀ {α : Type u}, FreeMagma.toFreeSemigroup = FreeMagma.lift FreeSemigroup.of
-- Mathlib.Data.Vector.Basic
/-- Define `C v` by induction on `v : Vector α n`.

This function has two arguments: `nil` handles the base case on `C nil`,
and `cons` defines the inductive step using `∀ x : α, C w → C (x ::ᵥ w)`.

It is used as the default induction principle for the `induction` tactic.
 -/
List.Vector.inductionOn : {α : Type u_1} →
  {C : {n : ℕ} → List.Vector α n → Sort u_6} →
    {n : ℕ} →
      (v : List.Vector α n) → C List.Vector.nil → ({n : ℕ} → {x : α} → {w : List.Vector α n} → C w → C (x ::ᵥ w)) → C v
-- Batteries.Recycling.MonadSatisfying.Array
Array.size_mapFinIdxM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (as : Array α)
  (f : (i : ℕ) → α → i < as.size → m β), SatisfiesM (fun arr => arr.size = as.size) (as.mapFinIdxM f)
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- A presieve is *regular* if it consists of a single effective epimorphism.  -/
CategoryTheory.Presieve.regular : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : C} → CategoryTheory.Presieve X → Prop
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnit_iff_isLeftRegular : ∀ {R : Type u_1} [inst : Semiring R] [IsArtinianRing Rᵐᵒᵖ] {x : R}, IsUnit x ↔ IsLeftRegular x
-- Lean.Data.Name
Lean.Name.quickCmp : Lean.Name → Lean.Name → Ordering
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.unfoldFun : Mathlib.Tactic.Translate.CastKind✝
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.diff_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ m₄ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ \ m₂).Equiv (m₃ \ m₄)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.allTR.loop : (n : ℕ) → ((i : ℕ) → i < n → Bool) → (i : ℕ) → i ≤ n → Bool
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.matched : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {l : List (String.Slice.Pattern.SearchStep s)} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos →
    String.Slice.Pattern.Model.IsValidSearchFrom pat endPos l →
      String.Slice.Pattern.Model.IsValidSearchFrom pat startPos
        (String.Slice.Pattern.SearchStep.matched startPos endPos :: l)
-- Mathlib.Algebra.Module.Equiv.Defs
RingEquiv.toSemilinearEquiv_symm_apply : ∀ {R : Type u_1} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S) (a : S),
  f.toSemilinearEquiv.symm a = f.invFun a
-- Mathlib.Topology.ContinuousMap.Weierstrass
bernstein.eq_1 : ∀ (n ν : ℕ), bernstein n ν = (bernsteinPolynomial ℝ n ν).toContinuousMapOn unitInterval
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.power_sum : ∀ {ι : Type u} (a : Cardinal.{max u v}) (f : ι → Cardinal.{max u v}),
  a ^ Cardinal.sum f = Cardinal.prod fun i => a ^ f i
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
/-- Turn a `CNF Nat`, that might contain `0` as a variable, to a `CNF PosFin`.
This representation is guaranteed to not have `0` and is limited to an upper bound of
variable indices.
 -/
Std.Tactic.BVDecide.LRAT.Internal.CNF.lift : (cnf : Std.Sat.CNF ℕ) → Std.Sat.CNF (Std.Tactic.BVDecide.LRAT.Internal.PosFin (cnf.numLiterals + 1))
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- To prove a property of a product, it suffices to prove that
the property is multiplicative and holds on factors.  -/
Finset.prod_induction_nonempty : ∀ {ι : Type u_1} {s : Finset ι} {M : Type u_7} [inst : CommMonoid M] (f : ι → M) (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a * b)) → s.Nonempty → (∀ x ∈ s, p (f x)) → p (∏ x ∈ s, f x)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_empty_injective : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  Function.Injective (s.touchpoint ∅)
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extendOfIsometry_eq : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : NormedField 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] [inst_6 : NormedAddCommGroup Eₗ] [inst_7 : NormedSpace 𝕜 Eₗ] [inst_8 : CompleteSpace Eₗ]
  [inst_9 : NormedAddCommGroup Fₗ] [inst_10 : NormedSpace 𝕜₂ Fₗ] [inst_11 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : E),
  (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm) (e₁ x) = e₂ (f x)
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ioo_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (b : α i), Pi.mulSingle i '' Set.Ioo 1 b = Set.Ioo 1 (Pi.mulSingle i b)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Mathlib.GroupTheory.Index
AddSubgroup.index_dvd_card : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.index ∣ Nat.card G
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_div : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Div F] [inst_2 : Div β]
  [IsDivApply F α β] (f g : F), ⇑(f / g) = ⇑f / ⇑g
-- Lean.Expr
Lean.mkBVarEx : ℕ → Lean.Expr
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.ConstructibleSetData.map_comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (f : S →+* T) (g : R →+* S) (s : PrimeSpectrum.ConstructibleSetData R),
  PrimeSpectrum.ConstructibleSetData.map (f.comp g) s =
    PrimeSpectrum.ConstructibleSetData.map f (PrimeSpectrum.ConstructibleSetData.map g s)
-- Init.Data.Fin.Basic
/-- The greatest value of `Fin (n+1)`, namely `n`.

Examples:
* `Fin.last 4 = (4 : Fin 5)`
* `(Fin.last 0).val = (0 : Nat)`
 -/
Fin.last : (n : ℕ) → Fin (n + 1)
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.topologicalSpaceFiber : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} → (Z : VectorBundleCore R B F ι) → (x : B) → TopologicalSpace (Z.Fiber x)
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A) {Z : ChainComplex A ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap X)
      (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap X) h
-- Mathlib.Data.List.Permutation
List.permutations_perm_permutations' : ∀ {α : Type u_1} (ts : List α), ts.permutations.Perm ts.permutations'
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
/-- When `F G H : C ⥤ Type max w v u`, we have `(G ⟶ F.functorHom H) ≃ (F ⊗ G ⟶ H)`.  -/
CategoryTheory.FunctorToTypes.functorHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G H : CategoryTheory.Functor C (Type (max w v u))) →
      (G ⟶ F.functorHom H) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorObj F G ⟶ H)
-- Mathlib.GroupTheory.DivisibleHull
ArchimedeanClass.liftOrderHom.congr_simp : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f f_1 : M → α) (e_f : f = f_1)
  (h : ∀ (a b : M), ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b → f a ≤ f b),
  ArchimedeanClass.liftOrderHom f h = ArchimedeanClass.liftOrderHom f_1 ⋯
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- A family of gluing data consists of
1. An index type `J`
2. A presheafed space `U i` for each `i : J`.
3. A presheafed space `V i j` for each `i j : J`.
   (Note that this is `J × J → PresheafedSpace C` rather than `J → J → PresheafedSpace C` to
   connect to the limits library more easily.)
4. An open immersion `f i j : V i j ⟶ U i` for each `i j : J`.
5. A transition map `t i j : V i j ⟶ V j i` for each `i j : J`.

such that
6. `f i i` is an isomorphism.
7. `t i i` is the identity.
8. `V i j ×[U i] V i k ⟶ V i j ⟶ V j i` factors through `V j k ×[U j] V j i ⟶ V j i` via some
   `t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i`.
9. `t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _`.

We can then glue the spaces `U i` together by identifying `V i j` with `V j i`, such
that the `U i`'s are open subspaces of the glued space.
 -/
AlgebraicGeometry.PresheafedSpace.GlueData : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u (v + 1))
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.hom_trans : ∀ {V : Type u} {G : SimpleGraph V} {K L M : Set V} (C : G.ComponentCompl L) (h : K ⊆ L) (h' : M ⊆ K),
  SimpleGraph.ComponentCompl.hom ⋯ C = SimpleGraph.ComponentCompl.hom h' (SimpleGraph.ComponentCompl.hom h C)
-- Std.Time.Format.Modifier
Std.Time.Modifier.u.sizeOf_spec : ∀ (presentation : Std.Time.Year), sizeOf (Std.Time.Modifier.u presentation) = 1 + sizeOf presentation
-- Lean.Util.Trace
Lean.checkEmoji : String
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of an `AddCommSemigroup` by an additive congruence relation is
an `AddCommSemigroup`.  -/
AddCon.addCommSemigroup : {M : Type u_4} → [inst : AddCommSemigroup M] → (c : AddCon M) → AddCommSemigroup c.Quotient
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
stronglyMeasurable_const_smul_iff₀ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {G₀ : Type u_7} [inst : TopologicalSpace β] [inst_1 : GroupWithZero G₀]
  [inst_2 : MulAction G₀ β] [ContinuousConstSMul G₀ β] {x : MeasurableSpace α} {c : G₀},
  c ≠ 0 → ((MeasureTheory.StronglyMeasurable fun x => c • f x) ↔ MeasureTheory.StronglyMeasurable f)
-- Lean.Meta.Tactic.Grind.CasesMatch
_private.Lean.Meta.Tactic.Grind.CasesMatch.0.Lean.Meta.Grind.isMatchCondCandidate.go : Lean.Expr → Bool
-- Init.Core
Std.LawfulCommIdentity.mk : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} [hc : Std.Commutative op] [toLawfulIdentity : Std.LawfulIdentity op o],
  Std.LawfulCommIdentity op o
-- Mathlib.Algebra.Group.Int.Units
Int.ofNat_isUnit : ∀ {n : ℕ}, IsUnit ↑n ↔ IsUnit n
-- Mathlib.CategoryTheory.FintypeCat
/-- Equivalences between finite types are the same as isomorphisms in `FintypeCat`.  -/
FintypeCat.equivEquivIso : {A B : FintypeCat} → A.obj ≃ B.obj ≃ (A ≅ B)
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_ofNatLT : ∀ (n : ℕ) (hn : n < 2 ^ 8), Int8.ofBitVec n#'hn = Int8.ofNat n
-- Lean.PrettyPrinter.Parenthesizer
/-- We need to store this `categoryParser` argument to deal with the implicit Pratt parser call in `trailingNode.parenthesizer`.  -/
Lean.PrettyPrinter.Parenthesizer.Context.cat : Lean.PrettyPrinter.Parenthesizer.Context → Lean.Name
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.Dep.exists_isCircuit_subset : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Dep X → ∃ C ⊆ X, M.IsCircuit C
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Polynomial evaluation on a pair is a pair of evaluations.  -/
Polynomial.aeval_prod_apply : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (x : A × B) (p : Polynomial R),
  (Polynomial.aeval x) p = ((Polynomial.aeval x.1) p, (Polynomial.aeval x.2) p)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsGLB.div : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G},
  IsGLB s a → IsLUB t b → IsGLB (s / t) (a / b)
-- Init.System.IO
/-- Runs an action with the specified stream `h` as standard error, restoring the original standard
error stream afterwards.
 -/
IO.withStderr : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadFinally m] → [MonadLiftT BaseIO m] → IO.FS.Stream → m α → m α
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X : D),
  (CategoryTheory.Functor.LaxMonoidal.ε
            (CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D)).unmop.app
      X =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).inv
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.smul_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {S : Type u_10}
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass R S N] (c : S) (m : ι → M),
  (c • f) m = c • f m
-- Mathlib.Tactic.FindSyntax
/-- The `#find_syntax` command takes as input a string `str` and retrieves from the environment
all the candidates for `syntax` terms that contain the string `str`.

It also makes a very crude effort at regenerating what the syntax looks like:
this is supposed to be just indicative of what the syntax may look like, but there is no
guarantee or expectation of correctness.

The optional trailing `approx`, as in `#find_syntax "∘" approx`, is only intended to make tests
more stable: rather than outputting the exact count of the overall number of existing syntax
declarations, it returns its round-down to the previous multiple of 100.
 -/
Mathlib.FindSyntax.«command#find_syntax_Approx» : Lean.ParserDescr
-- Mathlib.GroupTheory.Torsion
/-- The image of a quotient is torsion iff the additive group is torsion.  -/
IsAddTorsion.quotient_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : AddGroup H] {f : G →+ H},
  Function.Surjective ⇑f → N = f.ker → IsAddTorsion ↥N → (IsAddTorsion H ↔ IsAddTorsion G)
-- Init.Data.List.Lex
List.instIsLinearOrder : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α], Std.IsLinearOrder (List α)
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.RelevantArg.arg.inj : ∀ {n n_1 : ℕ}, Mathlib.Tactic.Translate.RelevantArg.arg n = Mathlib.Tactic.Translate.RelevantArg.arg n_1 → n = n_1
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.floor_map_map_zero_le : ∀ (f g : CircleDeg1Lift), ⌊f (g 0)⌋ ≤ ⌊f 0⌋ + ⌈g 0⌉
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.ι_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {X Y : CategoryTheory.MonoidalCategory.DayFunctor C V} (α : X ⟶ Y),
  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V
          (CategoryTheory.MonoidalCategory.DayFunctor C V)).map
      α =
    α.natTrans
-- Mathlib.RingTheory.Localization.Integer
/-- We can clear the denominators of a `Finset`-indexed family of fractions.  -/
IsLocalization.exist_integer_multiples : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {ι : Type u_4} (s : Finset ι) (f : ι → S),
  ∃ b, ∀ i ∈ s, IsLocalization.IsInteger R (↑b • f i)
-- Mathlib.Order.Filter.NAry
Filter.map₂_pure_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {g : Filter β} {a : α},
  Filter.map₂ m (pure a) g = Filter.map (m a) g
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A bounded subset has finite measure for a measure which is finite on compact sets, in a
proper space.  -/
Bornology.IsBounded.measure_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃s : Set α⦄, Bornology.IsBounded s → μ s < ⊤
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.IsNatPowModT.run : ∀ {a m : ℕ} {b c : ℕ}, Mathlib.Meta.NormNum.IsNatPowModT ((a.pow 1).mod m = a.mod m) a b m c → (a.pow b).mod m = c
-- Mathlib.Tactic.Translate.Attributes
/-- Attributes that generate new declarations when applied.  -/
Mathlib.Tactic.generatingAttrs : IO.Ref (Lean.NameMap (Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM (Array Lean.Name)))
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A}
  (H : g.IsWeierstrassFactorizationAt f h I) (hI : I ≠ ⊤),
  f.degree = ↑(((PowerSeries.map (Ideal.Quotient.mk I)) g).order.lift ⋯)
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv_zero : ∀ (a : ℤ), a / 0 = 0
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ_coeff_φ_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ →
    (algebraMap (Polynomial K) (RatFunc K)) ((RatFunc.Luroth.Φ✝ E).coeff (RatFunc.Luroth.φ✝ E).natDegree) =
      RatFunc.Luroth.c✝ E
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExceptSummand.eq_1 : ∀ (L : PeriodPair) (l₀ x : ℂ) (i : ℕ) (l : ↥L.lattice),
  L.weierstrassPExceptSummand l₀ x i l =
    if ↑l = l₀ then 0 else (↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.assoc : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y U V : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom U) (g : U.Hom V) (h : V.Hom Y),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.alter.congr_simp : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Hashable α] (m m_1 : Std.HashMap.Raw α β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → ∀ (f f_1 : Option β → Option β), f = f_1 → m.alter a f = m_1.alter a_1 f_1
-- Lean.Parser.Basic
/-- Succeeds if `s.lhsPrec >= prec`  -/
Lean.Parser.checkLhsPrecFn : ℕ → Lean.Parser.ParserFn
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.pi.eq_1 : ∀ {α : Type u} (β : α → ProfiniteAddGrp.{u_1}),
  ProfiniteAddGrp.pi β = ProfiniteAddGrp.ofProfinite (Profinite.pi fun a => (β a).toProfinite)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
ContDiff.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞},
  ContDiff ℝ (↑n) f → ContDiff ℝ ↑n fun x => Real.arsinh (f x)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.smul_hom : ∀ {k : Type u} {G : Type v} [inst : CommSemiring k] [inst_1 : Monoid G] {M N : Rep.{u_1, u, v} k G} (f : M ⟶ N) (r : k),
  Rep.Hom.hom (r • f) = r • Rep.Hom.hom f
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The free topological module over a topological space is functorial.  -/
TopModuleCat.freeMap : (R : Type u) →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] → {X Y : TopCat} → (X ⟶ Y) → (TopModuleCat.freeObj R X ⟶ TopModuleCat.freeObj R Y)
-- Init.Data.Iterators.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (it' : Std.IterM m β) (out : β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)),
  Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.yield it' out, h⟩ =
    Std.IterStep.yield { internalState := { inner := it', invariant := ⋯ } } ⟨out, ⋯⟩