mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Star
differentiableOn_star_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {s : Set E} [TrivialStar 𝕜],
  DifferentiableOn 𝕜 (fun y => star (f y)) s ↔ DifferentiableOn 𝕜 f s
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Monoid` across an `Equiv`  -/
Equiv.monoid : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Monoid β] → Monoid α
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.diagSub.match_1.splitter : (motive : (n : ℕ) → (α : TypeVec.{u_1} n) → (x : Fin2 n) → α x → Sort u_2) →
  (n : ℕ) →
    (α : TypeVec.{u_1} n) →
      (x : Fin2 n) →
        (x_1 : α x) →
          ((n : ℕ) → (α : TypeVec.{u_1} (n + 1)) → (a : Fin2 n) → (x : α a.fs) → motive (n + 1) α a.fs x) →
            ((n : ℕ) → (α : TypeVec.{u_1} (n + 1)) → (x : α Fin2.fz) → motive (n + 1) α Fin2.fz x) → motive n α x x_1
-- Init.Data.Nat.Coprime
Nat.Coprime.dvd_of_dvd_mul_right : ∀ {k n m : ℕ}, k.Coprime n → k ∣ m * n → k ∣ m
-- Std.Http.Internal.LowerCase
/-- Predicate asserting that a string is in lowercase form.
 -/
Std.Http.Internal.IsLowerCase : String → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves biproducts of `f` if `F` maps every bilimit bicone over `f` to a
bilimit bicone over `F.obj ∘ f`.  -/
CategoryTheory.Limits.PreservesBiproduct.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {J : Type w₁}
  {f : J → C} {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms}
  [self : CategoryTheory.Limits.PreservesBiproduct f F] {b : CategoryTheory.Limits.Bicone f} (a : b.IsBilimit),
  Nonempty (F.mapBicone b).IsBilimit
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If a point `x : U` is a closed point, then its corresponding prime ideal is maximal.  -/
AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U),
  IsClosed {↑x} → (hU.primeIdealOf x).asIdeal.IsMaximal
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_ofNat : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).imI = 0
-- Mathlib.Data.List.SplitBy
List.splitBy_flatten : ∀ {α : Type u_1} {r : α → α → Bool} {l : List (List α)},
  [] ∉ l →
    (∀ m ∈ l, List.IsChain (fun x y => r x y = true) m) →
      List.IsChain (fun a b => ∃ (ha : a ≠ []) (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l →
        List.splitBy r l.flatten = l
-- Std.Sat.CNF.Relabel
/-- Change the literal type in a `CNF` formula from `α` to `β` by using `r`.
 -/
Std.Sat.CNF.relabel : {α : Type u_1} → {β : Type u_2} → (α → β) → Std.Sat.CNF α → Std.Sat.CNF β
-- Mathlib.RingTheory.Flat.TorsionFree
Module.Flat.isTorsionFree : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Flat R M], Module.IsTorsionFree R M
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.constAlter₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} {h : 0 < m.buckets.size} {a : α}
  {f : Option β → Option β} (a_1 : m.WF), Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.reindex_appTop_coord : ∀ {n m : Type u} (i : m → n) (S : AlgebraicGeometry.Scheme) (j : m),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.reindex i S)))
      (AlgebraicGeometry.AffineSpace.coord S j) =
    AlgebraicGeometry.AffineSpace.coord S (i j)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.comp_refl : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G'), f.comp SimpleGraph.Iso.refl = f
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.toByteArray_left_eq : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → t₁.toByteArray = s.toByteArray.extract 0 p.offset.byteIdx
-- Mathlib.Data.Seq.Defs
/-- Take the first `n` elements of the sequence (producing a list)  -/
Stream'.Seq.take : {α : Type u} → ℕ → Stream'.Seq α → List α
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedHull.balanced : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (s : Set E),
  Balanced 𝕜 (balancedHull 𝕜 s)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.laplacian_eq_sum : ∀ {ι : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℂ F] [inst_5 : Fintype ι]
  (b : OrthonormalBasis ι ℝ E) (f : TemperedDistribution E F),
  Laplacian.laplacian f = ∑ i, LineDeriv.lineDerivOp (b i) (LineDeriv.lineDerivOp (b i) f)
-- Mathlib.CategoryTheory.Skeletal
/-- `fromThinSkeleton C` exhibits the thin skeleton as a skeleton.  -/
CategoryTheory.ThinSkeleton.thinSkeleton_isSkeleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : Quiver.IsThin C],
  CategoryTheory.IsSkeletonOf C (CategoryTheory.ThinSkeleton C) (CategoryTheory.ThinSkeleton.fromThinSkeleton C)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instToFormat : {α : Type} → [Std.ToFormat α] → Std.ToFormat (Lean.Meta.RefinedDiscrTree α)
-- Mathlib.LinearAlgebra.Ray
/-- Negating a nonzero vector.  -/
RayVector.instNeg : {M : Type u_2} → [inst : AddCommGroup M] → {R : Type u_4} → Neg (RayVector R M)
-- Mathlib.Data.Finset.Card
Finset.lt_wf : ∀ {α : Type u_4}, WellFounded LT.lt
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_eq_top : ∀ {M : Type u_2} [inst : MulOneClass M] {S : Submonoid M}, S.op = ⊤ ↔ S = ⊤
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjointOfUnion_subset_of_mem : ∀ {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C),
  j ∈ J → ⋃₀ ↑(hC.disjointOfUnion hJ j) ⊆ j
-- Lean.Environment
Lean.OLeanLevel.exported.sizeOf_spec : sizeOf Lean.OLeanLevel.exported = 1
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCompl_apply_inl : ∀ {α : Type u_9} {p : α → Prop} [inst : DecidablePred p] (x : { a // p a }), (Equiv.sumCompl p) (Sum.inl x) = ↑x
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_div : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 ≤ ArchimedeanClass.mk x →
    0 ≤ -ArchimedeanClass.mk y →
      ArchimedeanClass.stdPart (x / y) = ArchimedeanClass.stdPart x / ArchimedeanClass.stdPart y
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A continuous linear equivalence induces a homeomorphism.  -/
ContinuousLinearEquiv.toHomeomorph : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] → [inst_9 : Module R₂ M₂] → (M₁ ≃SL[σ₁₂] M₂) → M₁ ≃ₜ M₂
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `zipWithLeft`.  -/
List.zipWithLeftTR : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → Option β → γ) → List α → List β → List γ
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileChangeType.Deleted : Lean.Lsp.FileChangeType
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- If a `G`-representation on `A` is trivial, this is the group isomorphism between
`H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A` defined by `⟦single g a⟧ ↦ ⟦g⟧ ⊗ a`.  -/
groupHomology.H1AddEquivOfIsTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        [A.IsTrivial] → ↑(groupHomology.H1 A) ≃+ TensorProduct ℤ (Additive (Abelianization G)) ↑A
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measure_add_closure_zero : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] [inst_3 : AddGroup G]
  [IsTopologicalAddGroup G] (s : Set G) (μ : MeasureTheory.Measure G), μ (s + closure {0}) = μ s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β},
  m.getKey? k = some k' →
    (Std.ExtHashMap.filter f m).getD k fallback = (Option.filter (fun x => f k' x) m[k]?).getD fallback
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_sum_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] (s : Finset ι) (q : ℕ) (a : ι → R) (x : ι → M),
  DividedPowerAlgebra.dp R q (∑ i ∈ s, a i • x i) =
    ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, DividedPowerAlgebra.dp R (Multiset.count i ↑k) (x i)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.ι_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {a b : B} (f : a ⟶ b),
  P.ι.naturality f =
    CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp (P.fullsubcategory.map f) { toFunctor := (P.prop b).ι })
-- Std.Internal.Do.ExceptPost
Std.Internal.Do.EPost.Cons.mk.inj : ∀ {eh : Type u} {et : Type v} {head : eh} {tail : et} {head_1 : eh} {tail_1 : et},
  EPost.Cons.mk✝ head tail = EPost.Cons.mk✝ head_1 tail_1 → head = head_1 ∧ tail = tail_1
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.restrictionLE_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) (k : J) (hk : k ≤ i),
  (CategoryTheory.SmallObject.restrictionLE F hi).obj ⟨k, hk⟩ = F.obj ⟨k, ⋯⟩
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_iff_target_of_mem_source : ∀ {𝕜 : 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'] {f : M → M'} {s : Set M}
  [IsManifold I' 1 M'] {x : M} {y : M'},
  f x ∈ (chartAt H' y).source → (MDiffAt[s] f x ↔ ContinuousWithinAt f s x ∧ MDiffAt[s] (↑(extChartAt I' y) ∘ f) x)
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_mul_eq_top_of_contentIdeal_eq_top : ∀ {R : Type u_3} [inst : CommRing R] {p q : Polynomial R},
  p.contentIdeal = ⊤ → q.contentIdeal = ⊤ → (p * q).contentIdeal = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- `coprod F G` is a colimit cocone.  -/
CategoryTheory.FunctorToTypes.binaryCoproductColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.FunctorToTypes.binaryCoproductCocone F G)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.definition : Lean.Lsp.SemanticTokenModifier
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_singleton : ∀ {α : Type u_1} (a : α) (f : α → ℕ), Nat.multinomial {a} f = 1
-- Init.Data.ByteArray.Lemmas
ByteArray.toList_empty : ByteArray.empty.toList = []
-- Mathlib.RingTheory.Finiteness.Ideal
/-- Let `f : R →+* S` be a surjective ring homomorphism, and let `I` be an ideal of `R`. If `f(I)`
and `I ∩ ker(f)` are finitely generated ideals, then `I` is also finitely generated.  -/
Ideal.fg_of_fg_map_of_fg_inf_ker_of_surjective : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} {I : Ideal R},
  (Ideal.map f I).FG → (I ⊓ RingHom.ker f).FG → Function.Surjective ⇑f → I.FG
-- Init.Data.UInt.Lemmas
UInt16.toFin_sub : ∀ (a b : UInt16), (a - b).toFin = a.toFin - b.toFin
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Z : C) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Z)
      (CategoryTheory.CategoryStruct.comp f h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_insert_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k : α} {v : β k} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_iUnion_iff : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] (s : ι → Set α)
  (p : α → Prop), (∀ᵐ (x : α) ∂μ.restrict (⋃ i, s i), p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), p x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyData_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology], S.leftHomologyData.H = S.leftHomology
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fstFunctor_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fstFunctor F G X).obj S = S.fst
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C)}
  {f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData.f i j)}
  {toGlueData_1 : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C)}
  {f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData_1.f i j)},
  { toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 } →
    toGlueData = toGlueData_1
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- The image of a `LocalSubring` as a `LocalSubring`.  -/
LocalSubring.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] → [inst_1 : CommRing S] → [Nontrivial S] → (R →+* S) → LocalSubring R → LocalSubring S
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.ext_iff : ∀ {𝕜 : 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} {F : Type u_5} {inst_6 : NormedAddCommGroup F}
  {inst_7 : NormedSpace 𝕜 F} {V : M → Type u_6} {inst_8 : TopologicalSpace (Bundle.TotalSpace F V)}
  {inst_9 : (x : M) → AddCommGroup (V x)} {inst_10 : (x : M) → Module 𝕜 (V x)}
  {inst_11 : (x : M) → TopologicalSpace (V x)} {inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)}
  {inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)} {inst_14 : FiberBundle F V} {x y : CovariantDerivative I F V},
  x = y ↔ ↑x = ↑y
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.piPremeasure.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] (m : (i : ι) → MeasureTheory.OuterMeasure (α i))
  (s : Set ((i : ι) → α i)), MeasureTheory.piPremeasure m s = ∏ i, (m i) (Function.eval i '' s)
-- Mathlib.Algebra.Lie.OfAssociative
LieSubalgebra.coe_ad_pow : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (H : LieSubalgebra R L)
  (x y : ↥H) (n : ℕ), ↑(((LieAlgebra.ad R ↥H) x ^ n) y) = ((LieAlgebra.ad R L) ↑x ^ n) ↑y
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
/-- Auxiliary definition for the `MonoidalClosed` instance on `Module R`.
(This is only a separate definition in order to speed up typechecking.)
 -/
ModuleCat.monoidalClosedHomEquiv : {R : Type u} →
  [inst : CommRing R] →
    (M N P : ModuleCat R) →
      ((CategoryTheory.MonoidalCategory.tensorLeft M).obj N ⟶ P) ≃
        (N ⟶ ((CategoryTheory.linearCoyoneda R (ModuleCat R)).obj (Opposite.op M)).obj P)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.instIsPrincipalSpanSingletonSet : ∀ {R : Type u_1} [inst : Semiring R] (x : R), (R ∙ x).IsPrincipal
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.toFun_eq_coe : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {f : TestFunction Ω F n}, f.toFun = ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod_isoCoprod_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  (CategoryTheory.Limits.biprod.isoCoprod X Y).hom =
    CategoryTheory.Limits.biprod.desc CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.transport_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G),
  CategoryTheory.Functor.OplaxMonoidal.η G =
    CategoryTheory.CategoryStruct.comp (i.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.Functor.OplaxMonoidal.η F)
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.sum_smul : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • Polynomial.X
-- Batteries.Data.List.Perm
List.Perm.inter : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ t₁ t₂ : List α}, l₁.Perm l₂ → t₁.Perm t₂ → (l₁ ∩ t₁).Perm (l₂ ∩ t₂)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.maxKey?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.maxKey? = t₂.maxKey?
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramBuilderM.run : {α : Type} → ProofWidgets.Penrose.DiagramBuilderM α → Lean.MetaM α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertManyIfNewUnit_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp],
  Std.ExtDTreeMap.Const.insertManyIfNewUnit t [] = t
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {s : Finset ι} {ι' : Type u_9}
  [inst_2 : DecidableEq ι'] [AddLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ y ∉ t, ∑ x ∈ s with g x = y, f x ≤ 0) → ∑ x ∈ s, f x ≤ ∑ y ∈ t, ∑ x ∈ s with g x = y, f x
-- Mathlib.Analysis.Asymptotics.TVS
/-- `f =o[𝕜; l] g` (`IsLittleOTVS 𝕜 l f g`) is a generalization of `f =o[l] g` (`IsLittleO l f g`)
that works in topological `𝕜`-vector spaces.

Given two functions `f` and `g` taking values in topological vector spaces
over a normed field `K`,
we say that $f = o(g)$ if for any neighborhood of zero `U` in the codomain of `f`
there exists a neighborhood of zero `V` in the codomain of `g`
such that $\operatorname{gauge}_{K, U} (f(x)) = o(\operatorname{gauge}_{K, V} (g(x)))$,
where $\operatorname{gauge}_{K, U}(y) = \inf \{‖c‖ \mid y ∈ c • U\}$.

We use an `ENNReal`-valued function `egauge` for the gauge,
so we unfold the definition of little o instead of reusing it.  -/
Asymptotics.«term_=o[_;_]_» : Lean.TrailingParserDescr
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.Result.step.sizeOf_spec : ∀ (e h : Lean.Expr), sizeOf (Lean.Meta.MonadSimp.Result.step e h) = 1 + sizeOf e + sizeOf h
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.linearEquiv_fun : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite R M] [Nontrivial M],
  IsIsotypic R M → ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- The tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N`  -/
TensorProduct.finsuppLeft : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    (N : Type u_4) →
                      [inst_7 : AddCommMonoid N] →
                        [inst_8 : Module R N] →
                          (ι : Type u_5) → [DecidableEq ι] → TensorProduct R (ι →₀ M) N ≃ₗ[S] ι →₀ TensorProduct R M N
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.ι_colimMap : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (α : G ⟶ F) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G j) (CategoryTheory.Limits.colimMap α) =
    CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.Limits.colimit.ι F j)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.AddMonObj A} {M N : CategoryTheory.AddMod D A} {x y : M.Hom N}, x = y ↔ x.hom = y.hom