mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.DivMod.Lemmas
Int.fmod.eq_3 : ∀ (m n : ℕ), (Int.ofNat m.succ).fmod (Int.negSucc n) = Int.subNatNat (m % n.succ) n
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- A product of weighted homogeneous polynomials is weighted homogeneous, with weighted degree
equal to the sum of the weighted degrees.  -/
MvPolynomial.IsWeightedHomogeneous.prod : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {ι : Type u_4}
  (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ι → M) {w : σ → M},
  (∀ i ∈ s, MvPolynomial.IsWeightedHomogeneous w (φ i) (n i)) →
    MvPolynomial.IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Composing a continuous multilinear map with a continuous linear map gives again a
continuous multilinear map.  -/
ContinuousLinearMap.compContinuousMultilinearMap : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        {M₃ : Type w₃} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : (i : ι) → Module R (M₁ i)] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module R M₃] →
                        [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] →
                          [inst_8 : TopologicalSpace M₂] →
                            [inst_9 : TopologicalSpace M₃] →
                              (M₂ →L[R] M₃) → ContinuousMultilinearMap R M₁ M₂ → ContinuousMultilinearMap R M₁ M₃
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_mem_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α} {a : α}, a ∈ s → a⁻¹ ∈ s⁻¹
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a `DivInvOneMonoid` if `β` is a `DivInvOneMonoid`.  -/
FunLike.divInvOneMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : Inv F] →
                [inst_5 : Div F] →
                  [inst_6 : Pow F ℤ] →
                    [inst_7 : DivInvOneMonoid β] →
                      [IsOneApply F α β] →
                        [IsMulApply F α β] →
                          [IsInvApply F α β] →
                            [IsDivApply F α β] → [IsPowApply ℕ F α β] → [IsPowApply ℤ F α β] → DivInvOneMonoid F
-- Mathlib.Order.Category.PartOrdEmb
/-- The type of morphisms in `PartOrdEmb R`.  -/
PartOrdEmb.Hom : PartOrdEmb → PartOrdEmb → Type u
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The partial derivative `W_Y(X, Y)` with respect to `Y` of the polynomial `W(X, Y)` associated to
a Weierstrass curve `W` in affine coordinates.  -/
WeierstrassCurve.Affine.polynomialY : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Affine R → Polynomial (Polynomial R)
-- Mathlib.Topology.UniformSpace.Basic
bot_uniformity : ∀ {α : Type ua}, uniformity α = Filter.principal SetRel.id
-- Batteries.Data.Char.Basic
Char.ofNatAux.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) (h : n.isValidChar), Char.ofNatAux n h = Char.ofNatAux n_1 ⋯
-- Mathlib.Computability.Language
Language.map_kstar : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : Language α),
  (Language.map f) (KStar.kstar l) = KStar.kstar ((Language.map f) l)
-- Mathlib.Condensed.Discrete.Module
/-- Auxiliary definition for `functorIsoDiscrete`.  -/
LightCondMod.LocallyConstant.functorIsoDiscreteAux₂ : (R : Type u) →
  [inst : Ring R] →
    (M : ModuleCat R) →
      (LightCondensed.discrete (ModuleCat R)).obj M ≅
        (LightCondensed.discrete (ModuleCat R)).obj
          (ModuleCat.of R (LocallyConstant ↑(LightProfinite.of PUnit.{u + 1}).toTop ↑M))
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
/-- `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
`takeWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually
prove termination (`Finite` or `Productive` instances, for example) of a `takeWhile` iterator.
 -/
Std.Iterators.Types.TakeWhile.PlausibleStep : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [Std.Iterator α m β] →
        {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
          Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.horizontal_apply : ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Combinatorics.Line α ι) (v : ι' → α) (x : α),
  ↑(l.horizontal v) x = Sum.elim (↑l x) v
-- Mathlib.Order.Sublocale
Sublocale.himp_mem : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} {a b : X}, b ∈ S → a ⇨ b ∈ S
-- Mathlib.Tactic.DefEqTransformations
/-- `eta_expand at loc` eta expands all sub-expressions at the given location.
It also beta reduces any applications of eta expanded terms, so it puts it
into an eta-expanded "normal form."
This also exists as a `conv`-mode tactic.

For example, if `f` takes two arguments, then `f` becomes `fun x y => f x y`
and `f x` becomes `fun y => f x y`.

This can be useful to turn, for example, a raw `HAdd.hAdd` into `fun x y => x + y`.
 -/
Mathlib.Tactic.convEta_expand : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_eq_get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {a : α} {h' : a ∈ t}, Std.DTreeMap.Raw.Const.get t a h' = (Std.DTreeMap.Raw.Const.get? t a).get ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.coe_associatedHom : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring S] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : Algebra S R] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2],
  ⇑(QuadraticMap.associatedHom S) = ⇑QuadraticMap.associated
-- Std.Do.PostCond
Std.Do.ExceptConds.entails.eq_def : ∀ {ps : Std.Do.PostShape} (x y : Std.Do.ExceptConds ps),
  x.entails y =
    match ps, x, y with
    | Std.Do.PostShape.pure, x, y => True
    | Std.Do.PostShape.arg σ ps, x, y => x.entails y
    | Std.Do.PostShape.except ε ps, x, y => (∀ (e : ε), x.1 e ⊢ₛ y.1 e) ∧ x.2.entails y.2
-- Mathlib.RingTheory.Coalgebra.Hom
/-- Copy of a `CoalgHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
CoalgHom.copy : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] →
            [inst_3 : AddCommMonoid B] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] → (f : A →ₗc[R] B) → (f' : A → B) → f' = ⇑f → A →ₗc[R] B
-- Mathlib.RingTheory.Perfection
PreTilt.valAux_zero : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K]
  {p : ℕ} [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p], PreTilt.valAux K v O p 0 = 0
-- Mathlib.Algebra.CharP.Algebra
/-- A nontrivial `ℚ`-algebra has characteristic zero.

This cannot be a (local) instance because it would immediately form a loop with the
instance `DivisionRing.toRatAlgebra`. It's probably easier to go the other way: prove `CharZero R`
and automatically receive an `Algebra ℚ R` instance.
 -/
algebraRat.charZero : ∀ (R : Type u_3) [Nontrivial R] [inst : Ring R] [Algebra ℚ R], CharZero R
-- Mathlib.Order.Interval.Multiset
Multiset.mem_Iio : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {b x : α}, x ∈ Multiset.Iio b ↔ x < b
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative
`1` at zero, as long as it converges on a neighborhood of zero.  -/
hasStrictDerivAt_exp_zero_of_radius_pos : ∀ {𝕂 : Type u_1} [inst : NontriviallyNormedField 𝕂] [CompleteSpace 𝕂] [CharZero 𝕂],
  0 < (NormedSpace.expSeries 𝕂 𝕂).radius → HasStrictDerivAt NormedSpace.exp 1 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toList_ric_eq : ∀ {n i : ℕ}, ((*...=n).toList[i]?.isNone = true) = (n < i)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The map that sends `a : idealSet` to an element of `integerSet`. This map exists because
`J` is an integral ideal.  -/
NumberField.mixedEmbedding.fundamentalCone.idealSetMap : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) →
        ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) →
          ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)
-- Mathlib.RingTheory.FreeRing
/-- The canonical ring homomorphism `FreeRing α →+* FreeRing β` generated by a map `α → β`.  -/
FreeRing.map : {α : Type u} → {β : Type v} → (α → β) → FreeRing α →+* FreeRing β
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- Thanks to `tensorUnit` being initial in `AugmentedSimplexCategory`, we get
a morphism `Δ' ⟶ Δ ⊗ Δ'` for every pair of objects `Δ, Δ'`.  -/
AugmentedSimplexCategory.inr : (x y : AugmentedSimplexCategory) → y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj x y
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.toNeg : {R : Type u} → [self : AddGroupWithOne R] → Neg R
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?.eq_go : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (x : Option ((a : α) × β a))
  (t : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.getEntryGT? k t).or x = Std.DTreeMap.Internal.Impl.getEntryGT?.go k x t
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Algebra.Order.SuccPred.WithBot
WithBot.succ_ofNat : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : AddMonoidWithOne α] [inst_3 : SuccAddOrder α]
  (n : ℕ) [inst_4 : n.AtLeastTwo], (OfNat.ofNat n).succ = OfNat.ofNat n + 1
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivWithinAt.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {f' g' : StrongDual ℝ E} {x : E}
  {s : Set E},
  HasFDerivWithinAt f f' s x →
    HasFDerivWithinAt g g' s x →
      0 < f x →
        HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.toFn_comp_ofFn_eq_id : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] (n : ℕ) (v : Fin n → R),
  (Polynomial.toFn n) ((Polynomial.ofFn n) v) = v
-- Mathlib.RingTheory.WittVector.Truncated
/-- `x.coeff i` is the `i`th entry of `x`.  -/
TruncatedWittVector.coeff : {p n : ℕ} → {R : Type u_1} → Fin n → TruncatedWittVector p n R → R
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.cyclesOpIso_inv_naturality : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i).op (K.cyclesOpIso i).inv =
    CategoryTheory.CategoryStruct.comp (L.cyclesOpIso i).inv
      (HomologicalComplex.cyclesMap ((HomologicalComplex.opFunctor V c).map φ.op) i)
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
CategoryTheory.Monoidal.Reflective.instIsIsoMapTensorHomAppUnit : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  [inst_3 : CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Functor D C} [L.Monoidal]
  {R : CategoryTheory.Functor C D} [R.Faithful] [R.Full] (adj : L ⊣ R) (d d' : D),
  CategoryTheory.IsIso (L.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app d) (adj.unit.app d')))
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_filter_key_eq_length_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {f : α → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst) l).length = l.length ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true), f (Std.Internal.List.getKey a l h) = true)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.mk.injEq : ∀ {J : Type u_1} [inst : LinearOrder J] (as as_1 : J), ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- The Beta integral is convergent for all `u, v` of positive real part.  -/
Complex.betaIntegral_convergent : ∀ {u v : ℂ},
  0 < u.re → 0 < v.re → IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) MeasureTheory.volume 0 1
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_iSup : ∀ {ι : Sort u_1} (f : ι → ENNReal), (⨆ i, f i)⁻¹ = ⨅ i, (f i)⁻¹
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] (s : Set β) (b : β), s -ᵥ {b} = (fun x => x -ᵥ b) '' s
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (unit unit_1 : CategoryTheory.Functor.id C ⟶ F.comp G) (e_unit : unit = unit_1)
  (counit counit_1 : G.comp F ⟶ CategoryTheory.Functor.id D) (e_counit : counit = counit_1)
  (left_triangle_components :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (F.map (unit.app X)) (counit.app (F.obj X)) =
        CategoryTheory.CategoryStruct.id (F.obj X))
  (right_triangle_components :
    ∀ (Y : D),
      CategoryTheory.CategoryStruct.comp (unit.app (G.obj Y)) (G.map (counit.app Y)) =
        CategoryTheory.CategoryStruct.id (G.obj Y)),
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
      right_triangle_components := right_triangle_components } =
    { unit := unit_1, counit := counit_1, left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] {i j : E.toPreOneHypercover.I₀} (k : E.toPreOneHypercover.I₁ i j),
  (E.toSaturateOfHasPullbacks.s₁ k).fst = CategoryTheory.Limits.pullback.fst (E.f i) (E.f j)
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.shuffleIt : {α : Type u} → Array α → StdGen → Array α × StdGen
-- Mathlib.GroupTheory.Solvable
Equiv.Perm.not_isSolvable : ∀ (X : Type u_3), 5 ≤ Cardinal.mk X → ¬Group.IsSolvable (Equiv.Perm X)
-- Batteries.Data.List.Lemmas
List.idxOf_mem_idxsOf : ∀ {α : Type u_1} {xs : List α} {x : α} [inst : BEq α], List.idxOf x xs < xs.length → List.idxOf x xs ∈ List.idxsOf x xs
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The left fraction from `X` to `Y` given by a morphism `f : X ⟶ Y`.  -/
CategoryTheory.MorphismProperty.LeftFraction.ofHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) → {X Y : C} → (X ⟶ Y) → [W.ContainsIdentities] → W.LeftFraction X Y
-- Mathlib.Algebra.Order.Interval.Basic
instAddInterval.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α],
  instAddInterval = { add := WithBot.map₂ fun x1 x2 => x1 + x2 }
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- The forgetful functor from the pro-étale site of `S` to schemes over `S` is fully faithful.  -/
AlgebraicGeometry.Scheme.ProEt.forgetFullyFaithful : (S : AlgebraicGeometry.Scheme) → (AlgebraicGeometry.Scheme.ProEt.forget S).FullyFaithful
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPair_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E')
  (d : D), (CategoryTheory.Join.mapPair Fₗ Fᵣ).obj (CategoryTheory.Join.right d) = CategoryTheory.Join.right (Fᵣ.obj d)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.apply_symm_apply : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) (a_1 : H),
  e (e.symm a_1) = a_1
-- Mathlib.Order.CompleteBooleanAlgebra
biInf_sup_biInf : ∀ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : Set ι}
  {t : Set ι'}, (⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j = ⨅ p ∈ s ×ˢ t, f p.1 ⊔ g p.2
-- Std.Time.DateTime.Timestamp
/-- Subtracts an `Hour.Offset` from the given `Timestamp`.
 -/
Std.Time.Timestamp.subHours : Std.Time.Timestamp → Std.Time.Hour.Offset → Std.Time.Timestamp
-- Mathlib.Probability.Density
MeasureTheory.pdf_of_not_haveLebesgueDecomposition : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {X : Ω → E},
  ¬(MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ → MeasureTheory.pdf X ℙ μ = 0
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- In any abelian category with enough injectives,
`InjectiveResolution.of Z` constructs an injective resolution of the object `Z`.
 -/
CategoryTheory.InjectiveResolution.of : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.EnoughInjectives C] → (Z : C) → CategoryTheory.InjectiveResolution Z
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has cofiltered limits is said to have `AB5Star` (in literature `AB5*`)
provided that cofiltered limits are exact.
 -/
CategoryTheory.AB5Star : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasCofilteredLimits C] → Prop
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
IsSMulRegular.notMem_of_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : R},
  IsSMulRegular M x → ∀ {p : Ideal R}, p ∈ (Module.annihilator R M).minimalPrimes → x ∉ p
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.List.ProveNilOrConsResult.nil.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(List «$α»)} (pf : Q(«$s» = [])),
  sizeOf (Mathlib.Meta.List.ProveNilOrConsResult.nil pf) = 1 + sizeOf pf
-- Mathlib.GroupTheory.Nilpotent
Group.isNilpotent_congr : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (e : G ≃* H),
  Group.IsNilpotent G ↔ Group.IsNilpotent H
-- Init.Data.Vector.Lemmas
Vector.toList_singleton : ∀ {α : Type u_1} {x : α}, (Vector.singleton x).toList = [x]
-- Lean.Meta.Sym.Simp.SimpM
/-- Runs a `SimpM` computation with the given methods, configuration, and state.
The `transientCache` is always reset (context-dependent results don't survive across
invocations). The `persistentCache` and `funext` cache are preserved from `s`.  -/
Lean.Meta.Sym.Simp.SimpM.run : {α : Type} →
  Lean.Meta.Sym.Simp.SimpM α →
    optParam Lean.Meta.Sym.Simp.Methods { } →
      optParam Lean.Meta.Sym.Simp.Config { } →
        optParam Lean.Meta.Sym.Simp.State { } → Lean.Meta.Sym.SymM (α × Lean.Meta.Sym.Simp.State)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.inf_of_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α},
  μ.FiniteAtFilter f → μ.FiniteAtFilter (f ⊓ g)
-- Batteries.Data.Fin.Lemmas
Fin.coe_modNat : ∀ {m n : ℕ} (i : Fin (m * n)), ↑i.modNat = ↑i % n
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_ofIntClamp_of_lt : ∀ {n : ℤ}, n < 2 ^ 31 → (Int32.ofIntClamp n).toNatClampNeg = n.toNat
-- Std.Data.DHashMap.Raw
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.DHashMap.Raw.Const.insertMany : {α : Type u} →
  {β : Type v} →
    [BEq α] →
      [Hashable α] →
        {ρ : Type w} → [ForIn Id ρ (α × β)] → (Std.DHashMap.Raw α fun x => β) → ρ → Std.DHashMap.Raw α fun x => β
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_ringEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ⇑e.toRingEquiv = ⇑e
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂_comp_d₂₁_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k (G →₀ ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.d₃₂ A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.d₂₁ A) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Lean.Parser.Command
/-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names  -/
Lean.Parser.Command.declId : Lean.Parser.Parser
-- Mathlib.Data.Fin.Embedding
Fin.castAddEmb_apply : ∀ {n : ℕ} (m : ℕ) (i : Fin n), (Fin.castAddEmb m) i = Fin.castAdd m i
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.stateT : Lean.Elab.Do.MonadInfo → Array Lean.Elab.Do.MutVar → Lean.Expr → Lean.Elab.Do.ControlStack → Lean.Elab.Do.ControlStack
-- Lean.Structure
/-- Returns the full set of field names for the given structure,
"flattening" all the parent structures that are subobject fields.
If `includeSubobjectFields` is true, then subobject `toParent` projections are included,
and otherwise they are omitted.

For example, given `Bar` such that
```lean
structure Foo where a : Nat
structure Bar extends Foo where b : Nat
```
this returns ``#[`toFoo, `a, `b]``, or ``#[`a, `b]`` when `includeSubobjectFields := false`.
 -/
Lean.getStructureFieldsFlattened : Lean.Environment → Lean.Name → optParam Bool true → Array Lean.Name
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_filter_eq_bot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {a : α}, a +ᵥ f = ⊥ ↔ f = ⊥
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.insertNew : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {v : α} {path : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.Balanced c n path RBTree.RBColor.black 0 → ∃ n, (path.insertNew v).Balanced RBTree.RBColor.black n
-- Mathlib.Data.Set.Countable
Set.range_enumerateCountable_of_mem : ∀ {α : Type u} {s : Set α} (h : s.Countable) {default : α},
  default ∈ s → Set.range (Set.enumerateCountable h default) = s
-- Mathlib.Data.Fin.SuccPred
finCongr_refl : ∀ {n : ℕ} (h : optParam (n = n) ⋯), finCongr h = Equiv.refl (Fin n)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instVAdd : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} → [inst_2 : AddAction R X] → VAdd (AddOreLocalization S R) (AddOreLocalization S X)
-- Mathlib.Order.Filter.Tendsto
Filter.eventuallyEq_of_left_inv_of_right_inv : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g₁ g₂ : β → α} {fa : Filter α} {fb : Filter β},
  (∀ᶠ (x : α) in fa, g₁ (f x) = x) → (∀ᶠ (y : β) in fb, f (g₂ y) = y) → Filter.Tendsto g₂ fb fa → g₁ =ᶠ[fb] g₂
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isLocal_iff_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {X Y : C}
  (f : X ⟶ Y), P X → P Y → (P.isLocal f ↔ CategoryTheory.IsIso f)