mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DividedPowers.Basic
/-- A product of divided powers is a multinomial coefficient times the divided power

[Roby-1965], formula (III')  -/
DividedPowers.prod_dpow : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a : A} (hI : DividedPowers I) {ι : Type u_2} {s : Finset ι}
  {n : ι → ℕ}, a ∈ I → ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
-- Mathlib.Analysis.Normed.Order.Lattice
instHasSolidNormRat : HasSolidNorm ℚ
-- Mathlib.Order.Hom.WithTopBot
WithBot.coeOrderHom_apply : ∀ {α : Type u_4} [inst : Preorder α], ⇑WithBot.coeOrderHom = WithBot.some
-- Mathlib.Data.Fintype.EquivFin
/-- A non-infinite type is a fintype.  -/
fintypeOfNotInfinite : {α : Type u_4} → ¬Infinite α → Fintype α
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J)
  (x y : ↑(F.obj j)),
  CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j (x * y))
    ((CommRingCat.Colimits.Prequotient.of j x).mul (CommRingCat.Colimits.Prequotient.of j y))
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS'.eq_3 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ) (n : ℕ),
  complEDS' b c d k n.succ.succ =
    if hn : Even n then complEDS' b c d k (n / 2 + 1) * complEDS₂ b c d (↑(n / 2 + 1) * k)
    else
      have this := ⋯;
      complEDS' b c d k (n / 2 + 1) ^ 2 * normEDS b c d ((↑(n / 2 + 1) + 1) * k + 1) *
          normEDS b c d ((↑(n / 2 + 1) + 1) * k - 1) -
        complEDS' b c d k (n / 2 + 1 + 1) ^ 2 * normEDS b c d (↑(n / 2 + 1) * k + 1) *
          normEDS b c d (↑(n / 2 + 1) * k - 1)
-- Mathlib.RingTheory.Localization.Ideal
/-- **Alias** of `IsLocalization.disjoint_under_iff`. -/
IsLocalization.disjoint_comap_iff : ∀ {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] (J : Ideal S), Disjoint ↑M ↑(Ideal.under R J) ↔ J ≠ ⊤
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Enriched.Functor.whiskerLeft_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (K L M N : CategoryTheory.Functor C D)
  (g : CategoryTheory.MonoidalCategoryStruct.tensorObj (L.functorHom M) (M.functorHom N) ⟶ L.functorHom N) {X : C}
  (a :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.functorHom L)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (L.functorHom M) (M.functorHom N))).obj
      X),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          ((K.homObjFunctor L).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X)))) (g.app X)))
      a =
    (a.1, (CategoryTheory.ConcreteCategory.hom (g.app X)) a.2)
-- Mathlib.Algebra.Module.Equiv.Defs
/-- The two paths coercion can take to an `AddMonoidHom` are equivalent  -/
LinearEquiv.toAddMonoidHom_commutes : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  (↑e).toAddMonoidHom = e.toAddEquiv.toAddMonoidHom
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.coeffList_C_mul : ∀ {R : Type u_1} [inst : Semiring R] [NoZeroDivisors R] (P : Polynomial R) {x : R},
  x ≠ 0 → (Polynomial.C x * P).coeffList = List.map (fun x_1 => x * x_1) P.coeffList
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.right_distrib : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.instHasForget₂RingHomCarrierCommMonCatMonoidHomCarrier : CategoryTheory.HasForget₂ CommRingCat CommMonCat
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.binaryProductLimitCone_cone_π_app_left : ∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R),
  (M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } =
    ModuleCat.ofHom (LinearMap.fst R ↑M ↑N)
-- Lean.Data.Lsp.Diagnostics
/-- Additional Lean-specific metadata about the diagnostic.  -/
Lean.Lsp.DiagnosticWith.leanTags? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option (Array Lean.Lsp.LeanDiagnosticTag)
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkSizeOfMotives.loop : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → ℕ → Array Lean.Expr → Lean.MetaM α
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Presieve.pullbackArrows.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f f_1 : Y ⟶ X) (e_f : f = f_1)
  (R R_1 : CategoryTheory.Presieve X) (e_R : R = R_1) [inst_1 : R.HasPullbacks f] ⦃Y_1 : C⦄ (a a_1 : Y_1 ⟶ Y),
  a = a_1 → CategoryTheory.Presieve.pullbackArrows f R a = CategoryTheory.Presieve.pullbackArrows f_1 R_1 a_1
-- Mathlib.Analysis.Convex.Strict
DirectedOn.strictConvex_sUnion : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : SMul 𝕜 E] {S : Set (Set E)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) S → (∀ s ∈ S, StrictConvex 𝕜 s) → StrictConvex 𝕜 (⋃₀ S)
-- Mathlib.Algebra.Order.Round
Int.map_round : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Field β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] [inst_6 : FloorRing α] [inst_7 : FloorRing β]
  [inst_8 : FunLike F α β] [RingHomClass F α β] (f : F), StrictMono ⇑f → ∀ (a : α), round (f a) = round a
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterM.match_1.eq_1 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (ULift.{u_1, 0} Bool)} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) { down := false })
  (h_1 : (hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩)
  (h_2 : (hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩),
  (match ⟨{ down := false }, hf⟩ with
    | ⟨{ down := false }, hf⟩ => h_1 hf
    | ⟨{ down := true }, hf⟩ => h_2 hf) =
    h_1 hf
-- Init.Data.SInt.Lemmas
ISize.sub_eq_iff_eq_add : ∀ {a b c : ISize}, a - b = c ↔ a = c + b
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The difference of two vector measure is a vector measure.  -/
MeasureTheory.VectorMeasure.sub : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommGroup M] →
        [inst_1 : TopologicalSpace M] →
          [IsTopologicalAddGroup M] →
            MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α M
-- Init.Data.Array.Monadic
/-- We can express a for loop over an array as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
 -/
Array.forIn'_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  (f : (a : α) → a ∈ xs → β → m (ForInStep β)) (init : β),
  forIn' xs init f =
    ForInStep.value <$>
      Array.foldlM
        (fun b x =>
          match x with
          | ⟨a, m_1⟩ =>
            match b with
            | ForInStep.yield b => f a m_1 b
            | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) xs.attach
-- Mathlib.Tactic.GCongr.Core
/-- (Internal for `gcongr`)
Elaborates to an expression satisfying `hasHoleAnnotation`.  -/
Mathlib.Tactic.GCongr.elabCHoleExpand : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- **Alias** of `SkewMonoidAlgebra.coeff_equivMapDomain`. -/
SkewMonoidAlgebra.toFinsupp_equivMapDomain : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : AddCommMonoid k] (f : G ≃ H) (l : SkewMonoidAlgebra k G),
  (SkewMonoidAlgebra.equivMapDomain f l).coeff = Finsupp.equivMapDomain f l.coeff
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Context.mk.sizeOf_spec : ∀ (m returnType : Lean.Syntax) (uvars : Array Lean.Elab.Term.Do.Var) (kind : Lean.Elab.Term.Do.ToTerm.Kind),
  sizeOf { m := m, returnType := returnType, uvars := uvars, kind := kind } =
    1 + sizeOf m + sizeOf returnType + sizeOf uvars + sizeOf kind
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.triangleOfDegreewiseSplit_obj₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting),
  (CochainComplex.triangleOfDegreewiseSplit S σ).obj₁ = S.X₁
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Affine map from a smaller to a larger subspace of the same space.

This is the affine version of `Submodule.inclusion`.  -/
AffineSubspace.inclusion : {k : Type u_1} →
  {V₁ : Type u_2} →
    {P₁ : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] →
            [inst_3 : AddTorsor V₁ P₁] →
              {S₁ S₂ : AffineSubspace k P₁} → [inst_4 : Nonempty ↥S₁] → (h : S₁ ≤ S₂) → ↥S₁ →ᵃ[k] ↥S₂
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The canonical isomorphism `(triangle φ)⟦n⟧ ≅ triangle (φ⟦n⟧')`.  -/
CochainComplex.mappingCone.shiftTriangleIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            (n : ℤ) →
              (CategoryTheory.Pretriangulated.Triangle.shiftFunctor (CochainComplex C ℤ) n).obj
                  (CochainComplex.mappingCone.triangle φ) ≅
                CochainComplex.mappingCone.triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.stepBound.eq_1 : ∀ (n : ℕ), SzemerediRegularity.stepBound n = n * 4 ^ n
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.InjectivePresentation.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X J : C}
  {injective : autoParam (CategoryTheory.Injective J) CategoryTheory.InjectivePresentation.injective._autoParam}
  {f : X ⟶ J} {mono : autoParam (CategoryTheory.Mono f) CategoryTheory.InjectivePresentation.mono._autoParam} {J_1 : C}
  {injective_1 : autoParam (CategoryTheory.Injective J_1) CategoryTheory.InjectivePresentation.injective._autoParam}
  {f_1 : X ⟶ J_1} {mono_1 : autoParam (CategoryTheory.Mono f_1) CategoryTheory.InjectivePresentation.mono._autoParam},
  { J := J, injective := injective, f := f, mono := mono } =
      { J := J_1, injective := injective_1, f := f_1, mono := mono_1 } →
    J = J_1 ∧ f ≍ f_1
-- Mathlib.Analysis.Normed.Group.Pointwise
sphere_zero_add_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), Metric.sphere 0 δ + {x} = Metric.sphere x δ
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.mulOccursInAt.eq_1 : ∀ {A : Type u_1} {G : Type u_2} [inst : Inhabited A] [inst_1 : Monoid G] (p : SymbolicDynamics.FullShift.Pattern A G)
  (x : G → A) (g : G), p.mulOccursInAt x g = ∀ h ∈ p.support, x (g * h) = p.config h
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk.injEq : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (toSublattice : Sublattice α)
  (compl_mem' : ∀ {a : α}, a ∈ toSublattice.carrier → aᶜ ∈ toSublattice.carrier) (bot_mem' : ⊥ ∈ toSublattice.carrier)
  (toSublattice_1 : Sublattice α) (compl_mem'_1 : ∀ {a : α}, a ∈ toSublattice_1.carrier → aᶜ ∈ toSublattice_1.carrier)
  (bot_mem'_1 : ⊥ ∈ toSublattice_1.carrier),
  ({ toSublattice := toSublattice, compl_mem' := compl_mem', bot_mem' := bot_mem' } =
      { toSublattice := toSublattice_1, compl_mem' := compl_mem'_1, bot_mem' := bot_mem'_1 }) =
    (toSublattice = toSublattice_1)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.zsmul_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f : C(α, β)) (z : ℤ) (x : α), (z • f) x = z • f x
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.toIsAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsFinite f], AlgebraicGeometry.IsAffineHom f
-- Init.Conv
/-- `{ convs }` runs the list of `convs` on the current target, and any subgoals that
remain are trivially closed by `skip`.  -/
Lean.Parser.Tactic.Conv.nestedConv : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk'_mk_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y''),
  (CategoryTheory.StructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.comp g g') =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk f).homMk' g)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f (T.map g))).homMk' g')
        (CategoryTheory.eqToHom ⋯))
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go_eq.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : ℕ),
  x.entryAtIdx? x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, x => none
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n =>
      match compare n l.size with
      | Ordering.lt => l.entryAtIdx? n
      | Ordering.eq => some ⟨k, v⟩
      | Ordering.gt => r.entryAtIdx? (n - l.size - 1)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.mul.inj : ∀ {R : Type u} {a b a_1 b_1 : Rack.PreEnvelGroup R}, a.mul b = a_1.mul b_1 → a = a_1 ∧ b = b_1
-- Init.Data.Vector.Algebra
Vector.add_hmul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} [inst : Add α] [Add β] [inst_2 : Add γ] [inst_3 : HMul α β γ],
  (∀ (c d : α) (x : β), (c + d) * x = c * x + d * x) → ∀ (c d : α) (xs : Vector β n), (c + d) * xs = c * xs + d * xs
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.mkFinite_map : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X)
  (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (isClosedBase : IsClosed D) (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ) (i : cell n),
  Topology.RelCWComplex.map n i = map n i
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanILeanHeaderSetupInfoParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanILeanHeaderSetupInfoParams
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isInt_sub : ∀ {α : Type u_1} [inst : Ring α] {f : α → α → α} {a b : α} {a' b' c : ℤ},
  f = HSub.hSub →
    Mathlib.Meta.NormNum.IsInt a a' →
      Mathlib.Meta.NormNum.IsInt b b' → a'.sub b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c
-- Lean.Data.SMap
Lean.SMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] [inst_3 : SizeOf β] (stage₁ : Bool)
  (map₁ : Std.HashMap α β) (map₂ : Lean.PHashMap α β),
  sizeOf { stage₁ := stage₁, map₁ := map₁, map₂ := map₂ } = 1 + sizeOf stage₁ + sizeOf map₁ + sizeOf map₂
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.whiskerRight_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} {M₁ M₂ : Bimod X Y} (f : M₁ ⟶ M₂) (N : Bimod Y Z),
  (Bimod.whiskerRight f N).hom =
    CategoryTheory.Limits.colimMap
      (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M₁.actRight N.X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₁.X Y.X N.X).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁.X N.actLeft))
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight M₂.actRight N.X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₂.X Y.X N.X).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₂.X N.actLeft))
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X) N.X)
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom N.X) ⋯ ⋯)
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.tsupport_mem_nhds : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E], tsupport ↑f ∈ nhds c
-- Mathlib.Algebra.Order.Group.Equiv
coe_toLexAddEquiv : ∀ (α : Type u_1) [inst : Add α], ⇑(toLexAddEquiv α) = ⇑toLex
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instDistribMulAction : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          {R : Type u_4} →
            [inst_2 : Semiring R] →
              [inst_3 : DistribMulAction R M] →
                [ContinuousConstSMul R M] →
                  [inst_5 : ContinuousAdd M] → DistribMulAction R (MeasureTheory.VectorMeasure α M)
-- Init.Data.SInt.Lemmas
Int64.ofIntClamp_toInt : ∀ (x : Int64), Int64.ofIntClamp x.toInt = x
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedExtensionState : Inhabited Lean.Meta.Grind.ExtensionState
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_div : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (m : F) {s t : Set α}, ⇑m '' (s / t) = ⇑m '' s / ⇑m '' t
-- Mathlib.Order.Filter.Extr
/-- `is_maxFilter f l a` means that `f x ≤ f a` for all `x` in some `l`-neighborhood of `a`  -/
IsMaxFilter : {α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Filter α → α → Prop
-- Init.Core
/-- Auxiliary definition for generating compact `noConfusion` for enumeration types  -/
noConfusionEnum : {α : Sort u} →
  {β : Sort v} → [inst : DecidableEq β] → (f : α → β) → {P : Sort w} → {x y : α} → x = y → noConfusionTypeEnum f P x y
-- Mathlib.GroupTheory.HNNExtension
/-- **Britton's Lemma**. Any reduced word whose product is an element of `G`, has no
occurrences of `t`.  -/
HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (w : HNNExtension.NormalWord.ReducedWord G A B),
  HNNExtension.NormalWord.ReducedWord.prod φ w ∈ HNNExtension.of.range → w.toList = []
-- Lean.LibrarySuggestions.SineQuaNon
/-- Constants which should not be used as triggers.

Use `run_cmd modifyEnv fun env => triggerDenyListExt.addEntry env trigger` to add a trigger to the deny list.
 -/
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.triggerDenyListExt : Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet
-- Mathlib.Order.Heyting.Basic
hnot_le_comm : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢b ≤ a ↔ ￢a ≤ b
-- Mathlib.Logic.Function.Defs
Pi.map_apply : ∀ {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} (f : (i : ι) → α i → β i) (a : (i : ι) → α i) (i : ι),
  Pi.map f a i = f i (a i)
-- Mathlib.MeasureTheory.Category.MeasCat
/-- An example of an algebra on `Measure`: the nonnegative Lebesgue integral is a hom, behaving
nicely under the monad operations.  -/
MeasCat.Integral : MeasCat.Giry.Algebra
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.finrank_eq_finrank_subalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L),
  Module.finrank K ↥F.toSubalgebra = Module.finrank K ↥F
-- Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
IntermediateField.rank_sup_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E),
  Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_neg : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N), ↑(-m) = -↑m
-- Mathlib.Data.Num.Lemmas
Num.bit1.eq_2 : ∀ (p : PosNum), (Num.pos p).bit1 = Num.pos p.bit1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w n : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec n → ℕ → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Topology.MetricSpace.Bounded
Metric.closedBall_compl_subset_of_mem_cocompact : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  s ∈ Filter.cocompact α → ∀ (c : α), ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.essentiallySmall_op_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P.op ↔
    CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_subset_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ⊆ Set.Iio b ↔ a < b
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.Num.gcdAux.match_1.eq_1 : ∀ (motive : ℕ → Num → Num → Sort u_1) (x b : Num) (h_1 : (x b : Num) → motive 0 x b)
  (h_2 : (n : ℕ) → (b : Num) → motive n.succ Num.zero b) (h_3 : (n : ℕ) → (a b : Num) → motive n.succ a b),
  (match 0, x, b with
    | 0, x, b => h_1 x b
    | n.succ, Num.zero, b => h_2 n b
    | n.succ, a, b => h_3 n a b) =
    h_1 x b
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabImage.mk.injEq : ∀ (alt : String) (name : Lean.StrLit) (alt_1 : String) (name_1 : Lean.StrLit),
  ({ alt := alt, name := name } = { alt := alt_1, name := name_1 }) = (alt = alt_1 ∧ name = name_1)