mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The bounded continuous map `x ↦ exp(⟪x, t⟫ * I)`.  -/
BoundedContinuousFunction.innerProbChar : {E : Type u_1} → [inst : SeminormedAddCommGroup E] → [InnerProductSpace ℝ E] → E → BoundedContinuousFunction E ℂ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Unfolded version of `sum_def` in terms of `Finset.sum`.  -/
SkewMonoidAlgebra.sum_def' : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} [inst_1 : AddCommMonoid N]
  (f : SkewMonoidAlgebra k G) (g : G → k → N), f.sum g = ∑ a ∈ f.support, g a (f.coeff a)
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.free_of_finite_type_torsion_free : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsPrincipalIdealRing R] [IsDomain R] [Finite ι] {s : ι → M},
  Submodule.span R (Set.range s) = ⊤ → ∀ [Module.IsTorsionFree R M], Module.Free R M
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.eq_1 : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] (hS : S ≤ nonZeroDivisors A),
  Localization.subalgebra K S hS =
    (Localization.mapToFractionRing K S (Localization S) hS).range.copy
      {x | ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩} ⋯
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.not_isIsolated : ∀ {V : Type u} [Nontrivial V] {G : SimpleGraph V}, G.Preconnected → ∀ (v : V), ¬G.IsIsolated v
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.Pattern.Model.ForwardSliceSearcher.toList_emptyBefore_eq : ∀ (s : String.Slice) (pos : s.Pos),
  { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos }.toList =
    if h : pos = s.endPos then [String.Slice.Pattern.SearchStep.matched pos pos]
    else
      String.Slice.Pattern.SearchStep.matched pos pos ::
        { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h }.toList
-- Init.Data.Array.Zip
Array.map_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : Option γ → Option δ → α} {cs : Array γ}
  {ds : Array δ}, Array.map f (Array.zipWithAll g cs ds) = Array.zipWithAll (fun x y => f (g x y)) cs ds
-- Init.Data.UInt.Lemmas
UInt16.ofNat_div : ∀ {a b : ℕ}, a < 2 ^ 16 → b < 2 ^ 16 → UInt16.ofNat (a / b) = UInt16.ofNat a / UInt16.ofNat b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_eq_get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m}, Std.DHashMap.Const.get m a h = (Std.DHashMap.Const.get? m a).get ⋯
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- **Alias** of the forward direction of `LinearMap.hasFiniteRange_iff_range`. -/
LinearMap.HasFiniteRange.fg_range : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasFiniteRange → f.range.FG
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.familyOfElementsOfSection.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) {U : Cᵒᵖ} (s s_1 : F.obj U) (e_s : s = s_1) ⦃Y : C⦄ (f f_1 : Y ⟶ Opposite.unop U)
  (e_f : f = f_1) (a : (G.sieveOfSection s).arrows f),
  G.familyOfElementsOfSection s f a = G.familyOfElementsOfSection s_1 f_1 ⋯
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- For every prime `p` dividing the order of a finite group `G` there exists an element of order
`p` in `G`. This is known as Cauchy's theorem.  -/
exists_prime_orderOf_dvd_card' : ∀ {G : Type u_3} [inst : Group G] [Finite G] (p : ℕ) [hp : Fact (Nat.Prime p)], p ∣ Nat.card G → ∃ x, orderOf x = p
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.checkDisambiguation.eq_def : ∀ (s : String) (p : s.Pos),
  Lean.checkDisambiguation✝ s p =
    if h : p ≠ s.endPos then
      have b := p.get h;
      if b = '_' then Lean.checkDisambiguation✝ s (p.next h)
      else
        if b = 'x' then Lean.checkLowerHex✝ 2 s (p.next h)
        else
          if b = 'u' then Lean.checkLowerHex✝ 4 s (p.next h)
          else
            if b = 'U' then Lean.checkLowerHex✝ 8 s (p.next h)
            else if (decide (b.val ≥ 48) && decide (b.val ≤ 57)) = true then true else false
    else true
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm.eq_1 : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : IsIntegrallyClosed A] [inst_4 : IsDomain A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B]
  [inst_7 : Algebra.IsIntegral A B] [inst_8 : Module.IsTorsionFree A B],
  Algebra.intNorm A B = Algebra.intNormAux A (FractionRing A) (FractionRing B) B
-- Mathlib.Topology.MetricSpace.MetricSeparated
/-- A set `s` is `ε`-separated if the extended distance between any two distinct
elements is strictly greater than `ε`.  -/
Metric.IsSeparated : {X : Type u_1} → [PseudoEMetricSpace X] → ENNReal → Set X → Prop
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ioo_of_strictMonoOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → ContinuousOn f (Set.Icc a b) → StrictMonoOn f (Set.Icc a b) → f '' Set.Ioo a b = Set.Ioo (f a) (f b)
-- Mathlib.Algebra.Star.Subsemiring
/-- Copy of a non-unital star subalgebra with a new `carrier` equal to the old one. Useful to fix
definitional equalities.  -/
StarSubsemiring.copy : {R : Type v} →
  [inst : NonAssocSemiring R] →
    [inst_1 : StarRing R] → (S : StarSubsemiring R) → (s : Set R) → s = ↑S → StarSubsemiring R
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.id : Lean.Meta.Grind.Arith.Linear.NatStruct → ℕ
-- Mathlib.Analysis.Normed.Group.Basic
mem_eball_zero_iff : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E} {r : ENNReal}, a ∈ Metric.eball 0 r ↔ ‖a‖ₑ < r
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- Contracting a set is the same as contracting a basis for the set, and deleting the rest.  -/
Matroid.IsBasis.contract_eq_contract_delete : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → M.contract X = (M.contract I).delete (X \ I)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.negFn? : Lean.Meta.Grind.Arith.CommRing.Ring → Option Lean.Expr
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_normalizer_iff' : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {g : G},
  g ∈ AddSubgroup.normalizer ↑H ↔ ∀ (n : G), n + g ∈ H ↔ g + n ∈ H
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- We say that a collection of functions form a smooth partition of unity on a set `s` if

* all functions are infinitely smooth and nonnegative;
* the family `fun i ↦ support (f i)` is locally finite;
* for all `x ∈ s` the sum `∑ᶠ i, f i x` equals one;
* for all `x`, the sum `∑ᶠ i, f i x` is less than or equal to one.  -/
SmoothPartitionOfUnity : Type uι →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            ModelWithCorners ℝ E H →
              (M : Type uM) →
                [inst : TopologicalSpace M] → [ChartedSpace H M] → optParam (Set M) Set.univ → Type (max uM uι)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.i₁_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (self : HomotopicalAlgebra.Precylinder A) {Z : C}
  (h : A ⟶ Z), CategoryTheory.CategoryStruct.comp self.i₁ (CategoryTheory.CategoryStruct.comp self.π h) = h
-- Mathlib.Data.Fin.Tuple.Basic
/-- Updating an element and taking the beginning commute.  -/
Fin.init_update_castSucc : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α i.castSucc),
  Fin.init (Function.update q i.castSucc y) = Function.update (Fin.init q) i y
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_ofInt : ∀ (n : ℤ), Int16.ofBitVec (BitVec.ofInt 16 n) = Int16.ofInt n
-- Mathlib.Order.UpperLower.Prod
LowerSet.bot_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (t : LowerSet β), ⊥ ×ˢ t = ⊥
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.iSup_eapprox_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal},
  Measurable f → ∀ (a : α), ⨆ n, (MeasureTheory.SimpleFunc.eapprox f n) a = f a
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_map_nhds_eq : ∀ {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁),
  Filter.map (⇑e.symm) (nhds (e x)) = nhds x
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.coe_bot : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R], ↑⊥ = {0}
-- Mathlib.Order.Interval.Lex
NonemptyInterval.instDecidableLELexOfDecidableEqOfDecidableLT : {α : Type u_1} →
  [inst : LT α] →
    [inst_1 : LE α] → [DecidableEq α] → [DecidableLT α] → [DecidableLE α] → DecidableLE (Lex (NonemptyInterval α))
-- Std.Http.Internal.Char
/-- BWS = OWS (character class alias)
 -/
Std.Http.Internal.Char.bws : Char → Bool
-- Mathlib.Topology.ExtremallyDisconnected
/-- Theorem 2.5 in [Gleason, *Projective topological spaces*][gleason1958]:
in the category of compact spaces and continuous maps,
the projective spaces are precisely the extremally disconnected spaces.  -/
CompactT2.ExtremallyDisconnected.projective : ∀ {A : Type u} [inst : TopologicalSpace A] [ExtremallyDisconnected A] [CompactSpace A] [T2Space A],
  CompactT2.Projective A
-- Mathlib.Algebra.Field.Rat
NNRat.coe_inv : ∀ (q : ℚ≥0), ↑q⁻¹ = (↑q)⁻¹
-- Batteries.Data.Fin.Coding
/-- Encode `Char` into `Fin Char.count`.  -/
Fin.encodeChar : Char → Fin Char.count
-- Mathlib.Algebra.Category.CommBialgCat
commBialgCatEquivComonCommAlgCat_unitIso_hom_app : ∀ (R : Type u) [inst : CommRing R] (X : CommBialgCat R),
  (commBialgCatEquivComonCommAlgCat R).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.CharP.MixedCharZero
/-- A ring of characteristic zero has equal characteristic iff it does not
have mixed characteristic for any `p`.
 -/
EqualCharZero.iff_not_mixedCharZero : ∀ (R : Type u_1) [inst : CommRing R] [CharZero R],
  (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) ↔ ∀ p > 0, ¬MixedCharZero R p
-- Batteries.Data.List.Basic
/-- `List.dropSlice n m xs` removes a slice of length `m` at index `n` in list `xs`.  -/
List.dropSlice : {α : Type u_1} → ℕ → ℕ → List α → List α
-- Mathlib.Algebra.Order.Kleene
Prod.instKleeneAlgebra : {α : Type u_1} → {β : Type u_2} → [KleeneAlgebra α] → [KleeneAlgebra β] → KleeneAlgebra (α × β)
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Multiplicative (ι → G)` is equivalent to `ι → Multiplicative G`.  -/
MulEquiv.funMultiplicative : (ι : Type u_1) → (G : Type u_2) → [inst : Add G] → Multiplicative (ι → G) ≃* (ι → Multiplicative G)
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt.mk : ∀ {C : Type u₁} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₃, u₃} H]
  {F : CategoryTheory.Functor C H} {W : CategoryTheory.MorphismProperty C} {X : C},
  W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X) → F.HasPointwiseLeftDerivedFunctorAt W X
-- Init.Data.Range.Polymorphic.Basic
Std.Rxc.HasSize.mk : {α : Type u} → (α → α → ℕ) → Std.Rxc.HasSize α
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.eqOn_Ico_of_ae_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X]
  {m : MeasurableSpace X} [inst_3 : TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  [DenselyOrdered X] {a b : X} {f g : X → Y},
  f =ᵐ[μ.restrict (Set.Ico a b)] g →
    ContinuousOn f (Set.Ico a b) → ContinuousOn g (Set.Ico a b) → Set.EqOn f g (Set.Ico a b)
-- Mathlib.Order.Filter.NAry
Filter.NeBot.of_map₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
  (Filter.map₂ m f g).NeBot → g.NeBot
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The category of types has `Σ j, f j` as the coproduct of a type family `f : J → Type`.
 -/
CategoryTheory.Limits.Types.coproductColimitCocone : {J : Type v} → (F : J → Type (max v u)) → CategoryTheory.Limits.ColimitCocone (CategoryTheory.Discrete.functor F)
-- Mathlib.Algebra.Lie.IdealOperations
LieIdeal.map_comap_incl : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I₁ I₂ : LieIdeal R L},
  LieIdeal.map I₁.incl (LieIdeal.comap I₁.incl I₂) = I₁ ⊓ I₂
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Icc_add_one_left_eq_Icc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a b : α},
  a ≤ b → insert a (Set.Icc (a + 1) b) = Set.Icc a b
-- Init.Data.Vector.Find
Vector.findSome?_replicate : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  Vector.findSome? f (Vector.replicate n a) = if n = 0 then none else f a
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A purely inseparable extension has separable degree one.  -/
IsPurelyInseparable.sepDegree_eq_one : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E],
  Field.sepDegree F E = 1
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
_private.Mathlib.RingTheory.DedekindDomain.SelmerGroup.0.IsDedekindDomain.«term_⟮_,_⟯» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.map_one : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S), f 1 = 1
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instLinear : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      (V : Type u) →
        [inst_1 : CategoryTheory.Category.{v, u} V] →
          [inst_2 : CategoryTheory.Preadditive V] →
            (c : ComplexShape ι) → [CategoryTheory.Linear R V] → CategoryTheory.Linear R (HomotopyCategory V c)
-- Init.GetElem
Fin.getElem!_fin : ∀ {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → ℕ → Prop} {n : ℕ} [inst : GetElem? Cont ℕ Elem Dom] (a : Cont)
  (i : Fin n) [inst_1 : Inhabited Elem], a[i]! = a[↑i]!
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.map_inl_inv_coprodComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] {Z : D} (h : F.obj A ⨿ F.obj B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given `F : C ⥤ D`, this is `F.partialRightAdjoint` on morphisms.  -/
CategoryTheory.Functor.partialRightAdjointMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {X Y : F.PartialRightAdjointSource} → (X ⟶ Y) → (F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Y)
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.sUnion : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X} {S : Set (Set X)},
  (∀ s ∈ S, Convexity.IsStarConvexSet R x s) → Convexity.IsStarConvexSet R x (⋃₀ S)
-- Init.Dynamic
TypeNameData : Type u → NonemptyType
-- Mathlib.Data.Nat.Dist
Nat.dist_eq_intro : ∀ {n m k l : ℕ}, n + m = k + l → n.dist k = l.dist m
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.ofHom_id : ∀ {M : Type u} [inst : CommMonoid M],
  CommMonCat.ofHom (MonoidHom.id M) = CategoryTheory.CategoryStruct.id (CommMonCat.of M)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- This is a slightly more convenient method to verify that a kernel fork is a limit cone. It
only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.isLimitAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (t : CategoryTheory.Limits.KernelFork f) →
            (lift : (s : CategoryTheory.Limits.KernelFork f) → s.pt ⟶ t.pt) →
              (∀ (s : CategoryTheory.Limits.KernelFork f),
                  CategoryTheory.CategoryStruct.comp (lift s) (CategoryTheory.Limits.Fork.ι t) =
                    CategoryTheory.Limits.Fork.ι s) →
                (∀ (s : CategoryTheory.Limits.KernelFork f) (m : s.pt ⟶ t.pt),
                    CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Fork.ι t) =
                        CategoryTheory.Limits.Fork.ι s →
                      m = lift s) →
                  CategoryTheory.Limits.IsLimit t
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertMany_list_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} {l : List (α × β)},
  m.WF → (Std.DHashMap.Raw.Const.insertMany m l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) m l)
-- Mathlib.Algebra.Category.Ring.FinitePresentation
/-- If `S` is a finitely presented `R`-algebra, `S : Under R` is finitely presentable.  -/
CommRingCat.isFinitelyPresentable_under : ∀ (R : CommRingCat) (S : CategoryTheory.Under R),
  (CommRingCat.Hom.hom S.hom).FinitePresentation → CategoryTheory.IsFinitelyPresentable S
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- The lineality space of a cone is the largest submodule contained in the cone.  -/
PointedCone.gc_ofSubmodule_lineal : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E], GaloisConnection PointedCone.ofSubmodule PointedCone.lineal
-- Mathlib.Data.Rat.Lemmas
Rat.inv_natCast_num : ∀ (a : ℕ), (↑a)⁻¹.num = (↑a).sign
-- Mathlib.Algebra.Algebra.Unitization
Unitization.mk_bijective : ∀ {R : Type u_1} {A : Type u_2}, Function.Bijective Unitization.mk
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_zero : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  (g' : α → F') (l : Filter α), (fun _x => 0) =o[l] g'
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.hasBasis_nhds_zero_of_basis : ∀ {α : Type u_1} {G : Type u_2} {ι : Type u_3} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G]
  {p : ι → Prop} {b : ι → Set G},
  (nhds 0).HasBasis p b → (nhds 0).HasBasis p fun i => {f | ∀ (x : α), UniformFun.toFun f x ∈ b i}
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.factor_surjective : ∀ {R : Type u} [inst : Ring R] {S T : Ideal R} [inst_1 : S.IsTwoSided] [inst_2 : T.IsTwoSided] (H : S ≤ T),
  Function.Surjective ⇑(Ideal.Quotient.factor H)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedCaseTrace.default : Lean.Meta.Grind.CaseTrace
-- Mathlib.Data.Int.SuccPred
Int.instSuccAddOrder : SuccAddOrder ℤ
-- Mathlib.Data.Finsupp.Defs
_private.Mathlib.Data.Finsupp.Defs.0.Finsupp.onFinsetSupport.eq_1 : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (s : Finset α) (f : α → M),
  Finsupp.onFinsetSupport s f = {a ∈ s | f a ≠ 0}
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `MonoidHom.domRestrictHom_apply`. -/
MonoidHom.restrictHom_apply : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Type u_5} [inst_1 : SetLike S M] [inst_2 : SubmonoidClass S M] (M' : S)
  (A : Type u_6) [inst_3 : CommMonoid A] (f : M →* A), (MonoidHom.domRestrictHom M' A) f = f.domRestrict M'
-- Mathlib.Order.Circular
/-- The circular partial order obtained from "looping around" a partial order.
See note [reducible non-instances].  -/
PartialOrder.toCircularPartialOrder : (α : Type u_1) → [PartialOrder α] → CircularPartialOrder α
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.modify.eq_1 : ∀ {α : Type u} (xs : Array α) (i : ℕ) (f : α → α), xs.modify i f = (xs.modifyM i fun x => pure (f x)).run
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.toNormPoly.eq_1 : ∀ (c : Nat.Internal.Linear.ExprCnstr),
  c.toNormPoly =
    match c.lhs.toNormPoly.cancel c.rhs.toNormPoly with
    | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }
-- Mathlib.Topology.EMetricSpace.BoundedVariation
MonotoneOn.locallyBoundedVariationOn : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α}, MonotoneOn f s → LocallyBoundedVariationOn f s
-- Mathlib.Order.InitialSeg
/-- Principal segment from an empty type into a type with a minimal element.  -/
PrincipalSeg.ofIsEmpty : {α : Type u_1} →
  {β : Type u_2} →
    {s : β → β → Prop} → (r : α → α → Prop) → [IsEmpty α] → {b : β} → (∀ (b' : β), ¬s b' b) → PrincipalSeg r s
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.supSet.eq_1 : ∀ {α : Type u_1} [inst : SupSet α], ULift.supSet = { sSup := fun s => { down := sSup (ULift.up ⁻¹' s) } }
-- Mathlib.Data.TypeVec
TypeVec.repeat_eq_append1 : ∀ {β : Type u_1} {n : ℕ} (α : TypeVec.{u_1} n), (α ::: β).repeatEq = TypeVec.splitFun α.repeatEq (Function.uncurry Eq)
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.Types.coend.condition_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} {j j' : J} (f : j ⟶ j')
  {Z : Type (max w u)} (h : CategoryTheory.Limits.Types.coend F ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.coend.ι F j) h) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j')).map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.coend.ι F j') h)
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `Rat.den a`.  -/
Mathlib.Meta.Positivity.evalNNRatDen : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso : ∀ (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 x_1 : C) (x_2 : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x x_1 x_2 =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (Opposite.op x) (Opposite.op x_1)
          (Opposite.op x_2)).symm.unop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A B : C),
  CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Functor.id C) A B =
    CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B))