mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_rid_symm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  ↑(TensorProduct.assoc R M N R) ∘ₗ ↑(TensorProduct.rid R (TensorProduct R M N)).symm =
    TensorProduct.map LinearMap.id ↑(TensorProduct.rid R N).symm
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. The number of elements in the heap.  -/
Batteries.BinomialHeap.Imp.Heap.size : {α : Type u_1} → Batteries.BinomialHeap.Imp.Heap α → ℕ
-- Mathlib.Topology.Algebra.Monoid
/-- Left-multiplication by a left-invertible element of a topological monoid is proper, i.e.,
inverse images of compact sets are compact.  -/
Filter.tendsto_cocompact_mul_left : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [SeparatelyContinuousMul M] {a b : M},
  b * a = 1 → Filter.Tendsto (fun x => a * x) (Filter.cocompact M) (Filter.cocompact M)
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_eq_of_associated_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {m n : α},
  Associated m n → ∀ (k : α), lcm m k = lcm n k
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM.loop.match_1.splitter : {α : Type u_2} →
  (n : ℕ) →
    (motive : { i // i ≤ n } → α → Sort u_1) →
      (x : { i // i ≤ n }) →
        (x_1 : α) →
          ((property : 0 ≤ n) → (x : α) → motive ⟨0, property⟩ x) →
            ((i : ℕ) → (h : i + 1 ≤ n) → (x : α) → motive ⟨i.succ, h⟩ x) → motive x x_1
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafBotEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} A],
  (CategoryTheory.sheafBotEquivalence A).functor = CategoryTheory.sheafToPresheaf ⊥ A
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_comp_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {υ : Type u_7} {T : Type u_8} [inst_3 : CommRing T]
  [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {b : τ → MvPowerSeries υ T},
  MvPowerSeries.HasSubst a →
    MvPowerSeries.HasSubst b →
      MvPowerSeries.subst b ∘ MvPowerSeries.subst a = MvPowerSeries.subst fun s => MvPowerSeries.subst b (a s)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- An element in SLₙ(F) induced by a diagonal matrix `1` on any other entries and `a`, `a⁻¹` on
positition `i` and `j` respectively where `i ≠ j`.  -/
Matrix.SpecialLinearGroup.diag2n : {F : Type u_1} →
  [inst : Field F] →
    {ι : Type u_2} →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] → {i j : ι} → i ≠ j → (a : F) → a ≠ 0 → Matrix.SpecialLinearGroup ι F
-- Mathlib.MeasureTheory.Group.Arithmetic
Submonoid.instMeasurableSMul : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : MeasurableSpace α] [inst_2 : Monoid M]
  [inst_3 : MulAction M α] [MeasurableSMul M α] (s : Submonoid M), MeasurableSMul (↥s) α
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.cosKernel_def : ∀ (a x : ℝ), ↑(HurwitzZeta.cosKernel (↑a) x) = jacobiTheta₂ (↑a) (Complex.I * ↑x)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.eq_zero_of_pair' : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x, y] → ∀ {s t : R}, s • x = t • y → s = 0 ∧ t = 0
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.isCompact_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] {n : ℕ}
  {i : Topology.RelCWComplex.cell C n}, IsCompact (Topology.RelCWComplex.cellFrontier n i)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.comm_symm : ∀ (R : Type uR) (A : Type uA) (B : Type uB) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  (Algebra.TensorProduct.comm R A B).symm = Algebra.TensorProduct.comm R B A
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.right_notMem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SSameSide x y → y ∉ s
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
/-- The Radon-Nikodym derivative `∂(μ.map g)/∂(ν.map g)` of the pushforward of measures by
a function `g : 𝓧 → 𝓨` evaluated at `g x` is a.e.-equal to the conditional expectation of `∂μ/∂ν`
with respect to the comap by `g` of the sigma-algebra on `𝓨`.

See `rnDeriv_map_ae_eq_trim` for the same statement, but with a.e. equality with respect to
the trimmed measure `ν.trim hg.comap_le`.  -/
MeasureTheory.rnDeriv_map : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ],
  μ.AbsolutelyContinuous ν →
    ∀ {g : 𝓧 → 𝓨},
      Measurable g →
        ∀ [hσ : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g ν)],
          (fun a => (MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g a)) =ᵐ[ν]
            ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]
-- Mathlib.Topology.WithTopology
WithTopology.image_ofTopology : ∀ {X : Type u_1} (t : TopologicalSpace X) (s : Set (WithTopology X t)),
  WithTopology.ofTopology '' s = WithTopology.toTopology t ⁻¹' s
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.mk : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  f.IsDistinguishedAt I → IsUnit h → g = ↑f * h → g.IsWeierstrassFactorizationAt f h I
-- Mathlib.Data.Set.Prod
Set.image_prodMk_subset_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {s : Set α},
  (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)
-- Mathlib.Computability.Partrec
Primrec₂.to_comp : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, Primrec₂ f → Computable₂ f
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffOn_iff_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M H}
  {e' : OpenPartialHomeomorph M' H'} {f : M → M'} {s : Set M} {n : WithTop ℕ∞},
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I' n M' →
      s ⊆ e.source →
        Set.MapsTo f s e'.source →
          (ContMDiffOn I I' n f s ↔
            ContinuousOn f s ∧ ContDiffOn 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s))
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.instGroup.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : Group N],
  OneHom.instGroup =
    { toMonoid := OneHom.instMonoid, toInv := OneHom.instInv, toDiv := OneHom.instDiv, toZPow := ZPow.ofPow,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENatAux_le_nat : ∀ {x : Cardinal.{u_1}} {n : ℕ}, x.toENatAux ≤ ↑n ↔ x ≤ ↑n
-- Init.Data.BitVec.Basic
BitVec.cast_ofNat : ∀ {n m : ℕ} (h : n = m) (x : ℕ), BitVec.cast h (BitVec.ofNat n x) = BitVec.ofNat m x
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_smulBasis_right : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {G : Type u_7}
  [inst_8 : Group G] [inst_9 : DistribMulAction G M₂] [inst_10 : SMulCommClass G R M₂] (g : G) (f : M₁ →ₗ[R] M₂),
  (LinearMap.toMatrix v₁ (g • v₂)) f = (LinearMap.toMatrix v₁ v₂) (DistribSMul.toLinearMap R M₂ g⁻¹ ∘ₗ f)
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- A sphere centred at the origin in a valued ring is closed.  -/
Valued.isClosed_sphere : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  (r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀), IsClosed {x | Valued.v.restrict x = r}
-- Mathlib.Algebra.Group.Defs
nsmulRec'.eq_1 : ∀ {M : Type u_2} [inst : Zero M] [inst_1 : Add M] (x : M), nsmulRec' 0 x = 0
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.totallyBounded_subsets_of_totallyBounded : ∀ {α : Type u_1} [inst : UniformSpace α] {t : Set α}, TotallyBounded t → TotallyBounded {F | ↑F ⊆ t}
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.isClosed_topologicalClosure : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (s : Subalgebra R A), IsClosed ↑s.topologicalClosure
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.ι_p₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (self : HomotopicalAlgebra.PrepathObject A) {Z : C}
  (h : A ⟶ Z), CategoryTheory.CategoryStruct.comp self.ι (CategoryTheory.CategoryStruct.comp self.p₀ h) = h
-- Mathlib.Algebra.Order.Nonneg.Module
/-- A module over an ordered semiring is also a module over just the non-negative scalars.  -/
Nonneg.instModule : {R : Type u_1} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] → [inst_3 : AddCommMonoid M] → [Module R M] → Module { c // 0 ≤ c } M
-- Mathlib.Order.Filter.Map
Filter.map_comap_of_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Surjective f → ∀ (l : Filter β), Filter.map f (Filter.comap f l) = l
-- Mathlib.Algebra.Group.Subgroup.Actions
/-- The center of a group acts commutatively on that group.  -/
Subgroup.center.smulCommClass_right : ∀ {G : Type u_1} [inst : Group G], SMulCommClass G (↥(Subgroup.center G)) G
-- Lean.Meta.HaveTelescope
Lean.Meta.HaveInfo.mk.injEq : ∀ (typeBackDeps valueBackDeps : Std.HashSet ℕ) (decl : Lean.LocalDecl) (level : Lean.Level)
  (typeBackDeps_1 valueBackDeps_1 : Std.HashSet ℕ) (decl_1 : Lean.LocalDecl) (level_1 : Lean.Level),
  ({ typeBackDeps := typeBackDeps, valueBackDeps := valueBackDeps, decl := decl, level := level } =
      { typeBackDeps := typeBackDeps_1, valueBackDeps := valueBackDeps_1, decl := decl_1, level := level_1 }) =
    (typeBackDeps = typeBackDeps_1 ∧ valueBackDeps = valueBackDeps_1 ∧ decl = decl_1 ∧ level = level_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_toSubtype : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p]
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.Limits.biproduct.toSubtype f p) =
    if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkListLitAux : Lean.Expr → Lean.Expr → List Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ico_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a - b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c + b) (d + b)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_prod_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {ι : Type u_2} {s : Finset ι} {f : ι → M},
  UniqueFactorizationMonoid.radical (∏ i ∈ s, f i) ∣ ∏ i ∈ s, UniqueFactorizationMonoid.radical (f i)
-- Mathlib.Order.Filter.IndicatorFunction
mulIndicator_eventuallyLE_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : One β] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {l : Filter α},
  f ≤ᶠ[l ⊓ Filter.principal s] g → s.mulIndicator f ≤ᶠ[l] s.mulIndicator g
-- Mathlib.Algebra.Group.Basic
neg_injective : ∀ {G : Type u_3} [inst : InvolutiveNeg G], Function.Injective Neg.neg
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonReferenceContext.fromJson : Lean.Json → Except String Lean.Lsp.ReferenceContext
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.zoom.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode.Path α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α)
  (y : α) (b : RBTree.RBNode α) (path : RBTree.RBNode.Path α)
  (h_1 : (path : RBTree.RBNode.Path α) → motive RBTree.RBNode.nil path)
  (h_2 :
    (n : RBTree.RBNode α) →
      (c : RBTree.RBColor) →
        (a : RBTree.RBNode α) →
          (y : α) →
            (b : RBTree.RBNode α) →
              n = RBTree.RBNode.node c a y b →
                (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a y b) path),
  (match RBTree.RBNode.node c a y b, path with
    | RBTree.RBNode.nil, path => h_1 path
    | n@h:(RBTree.RBNode.node c a y b), path => h_2 n c a y b h path) =
    h_2 (RBTree.RBNode.node c a y b) c a y b ⋯ path
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Stats.mk.inj : ∀ {usedTheorems : Lean.Meta.Simp.UsedSimps} {diag : Lean.Meta.Simp.Diagnostics}
  {usedTheorems_1 : Lean.Meta.Simp.UsedSimps} {diag_1 : Lean.Meta.Simp.Diagnostics},
  { usedTheorems := usedTheorems, diag := diag } = { usedTheorems := usedTheorems_1, diag := diag_1 } →
    usedTheorems = usedTheorems_1 ∧ diag = diag_1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftIso R i).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- Structure recording good behaviour of a property of functions `M → N` w.r.t. compatible
choices of both a chart on `M` and `N`. Currently, we ask for the property to be stable under
restriction of the domain chart, and local in the target.

Motivating examples are immersions and submersions of smooth manifolds.  -/
Manifold.IsLocalSourceTargetProperty : {H : Type u_6} →
  {G : Type u_8} →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace G] →
        {M : Type u_10} →
          {N : Type u_12} →
            [inst_2 : TopologicalSpace M] →
              [inst_3 : TopologicalSpace N] →
                ((M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop) → Prop
-- Std.Do.WP.SimpLemmas
EStateM.tryCatch.eq_1 : ∀ {ε σ δ : Type u} [inst : EStateM.Backtrackable δ σ] {α : Type u} (x : EStateM ε σ α) (handle : ε → EStateM ε σ α)
  (s : σ),
  x.tryCatch handle s =
    match x s with
    | EStateM.Result.error e s_1 => handle e (EStateM.Backtrackable.restore s_1 (EStateM.Backtrackable.save s))
    | ok => ok
-- Mathlib.RingTheory.Finiteness.Basic
/-- **Alias** of `Submodule.FG.restrictScalars_of_surjective`. -/
Submodule.fg_restrictScalars : ∀ {R : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A] [inst_1 : AddCommMonoid M] [inst_2 : Module A M]
  {S : Submodule A M} [inst_3 : CommSemiring R] [inst_4 : Algebra R A] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M], S.FG → Function.Surjective ⇑(algebraMap R A) → (Submodule.restrictScalars R S).FG
-- Std.Http.Test.Helpers
/-- Read the full request body and echo it back as text/plain.
 -/
Std.Http.Internal.Test.echoHandler : Std.Http.Internal.Test.TestHandler
-- Mathlib.Data.List.Sort
List.decidableSortedLT : {α : Type u_1} → [inst : Preorder α] → [DecidableLT α] → DecidablePred List.SortedLT
-- Mathlib.Order.WellFounded
WellFounded.irrefl : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → Std.Irrefl r
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- **Alias** of `IsEllipticDvdSequence`.

---

The proposition that a sequence indexed by `ℤ` is an EDS.  -/
IsEllDivSequence : {R : Type u_1} → [CommRing R] → (ℤ → R) → Prop
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_zero : Cardinal.aleph 0 = Cardinal.aleph0
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The functor which associates to a functor `F` the bifunctor `F - ⊗ F -`.  -/
CategoryTheory.MonoidalCategory.curriedTensorPreFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor C (CategoryTheory.Functor C D))
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongr_trans : ∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2}
  {ι₃ : Type u_3} (σ₁ : ι₁ ≃ ι₂) (σ₂ : ι₂ ≃ ι₃) (m : MultilinearMap R (fun x => M₂) M₃),
  MultilinearMap.domDomCongr (σ₁.trans σ₂) m = MultilinearMap.domDomCongr σ₂ (MultilinearMap.domDomCongr σ₁ m)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommSemigroupOfAddHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → AddCommSemigroup (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)],
  DirectLimit.instAddCommSemigroupOfAddHomClass =
    { toAddSemigroup := DirectLimit.instAddSemigroupOfAddHomClass, add_comm := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_ε_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.Monoidal],
  (F.obj n).map ((CategoryTheory.Functor.LaxMonoidal.ε F).app X) =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor n).inv).app X)
      ((CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) n).app X)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- A computable instance of `CartesianMonoidalCategory` for `Over X` when `C` has
chosen pullbacks. Contrast this with the noncomputable instance provided by
`CategoryTheory.Over.cartesianMonoidalCategory`.
 -/
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.ChosenPullbacks C] → (X : C) → CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Over X)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrLeft_refl : ∀ {M : Type u_4} {N : Type u_8} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N],
  (AddEquiv.refl M).addMonoidHomCongrLeft = AddEquiv.refl (M →+ N)
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.epi_iff_surjective : ∀ {X Y : LightProfinite} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_inv_nat_nhds_zero : Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A basis that is orthonormal is an orthonormal basis.  -/
Module.Basis.toOrthonormalBasis : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] → (v : Module.Basis ι 𝕜 E) → Orthonormal 𝕜 ⇑v → OrthonormalBasis ι 𝕜 E
-- Lean.Meta.Tactic.Grind.Main
/-- Returns a new goal for the given metavariable.  -/
Lean.Meta.Grind.mkGoalCore : Lean.MVarId → Lean.Meta.Grind.GrindM Lean.Meta.Grind.Goal
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.hasExponent_of_finiteDimensional : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [IsPurelyInseparable K L]
  [FiniteDimensional K L], IsPurelyInseparable.HasExponent K L
-- Mathlib.NumberTheory.MahlerMeasure
/-- **Alias** of `Polynomial.ncard_boxPoly`. -/
Polynomial.card_eq_of_natDegree_le_of_coeff_le : ∀ (n : ℕ) (B₁ B₂ : Fin (n + 1) → ℝ), (Polynomial.boxPoly n B₁ B₂).ncard = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitArg.mk.sizeOf_spec : ∀ (arg type app : Lean.Expr),
  sizeOf { arg := arg, type := type, app := app } = 1 + sizeOf arg + sizeOf type + sizeOf app
-- Mathlib.Geometry.Polygon.Basic
/-- A polygon with `n` vertices in a type `P`.  -/
Polygon : Type u_1 → ℕ → Type u_1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_eq_get! : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m.WF → ∀ {a : α} {h' : a ∈ m}, m.get a h' = m.get! a
-- Mathlib.Util.Superscript
Mathlib.Tactic.Superscript.Mapping.mk.injEq : ∀ (toNormal toSpecial toNormal_1 toSpecial_1 : Std.HashMap Char Char),
  ({ toNormal := toNormal, toSpecial := toSpecial } = { toNormal := toNormal_1, toSpecial := toSpecial_1 }) =
    (toNormal = toNormal_1 ∧ toSpecial = toSpecial_1)
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.LawfulMapOperator : (α : Type) →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α) →
        [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] → Prop
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_eq_iSup_biInf_of_nat : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : ℕ → Prop} {u : ℕ → α},
  Filter.bliminf u Filter.atTop p = ⨆ i, ⨅ j, ⨅ (_ : p j ∧ i ≤ j), u j
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_injective : ∀ (n : ℕ), Function.Injective Fin.castSucc
-- Mathlib.Analysis.Calculus.Deriv.Pi
deriv_update : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : NontriviallyNormedField 𝕜] [Finite ι] (x : ι → 𝕜)
  (i : ι) (y : 𝕜), deriv (Function.update x i) y = Pi.single i 1
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW_isoClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.isoClosure.trW = P.trW
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.mk : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] →
              [inst_4 : Semiring B] →
                [inst_5 : Algebra R B] →
                  [inst_6 : Star B] →
                    (toAlgHom : A →ₐ[R] B) →
                      (∀ (x : A), (↑↑toAlgHom.toRingHom).toFun (star x) = star ((↑↑toAlgHom.toRingHom).toFun x)) →
                        A →⋆ₐ[R] B