mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Perm
Vector.Perm.refl : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), xs.Perm xs
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- A `p`-adic number `u` with `‖u‖ = 1` is a unit of `ℤ_[p]`.  -/
PadicInt.mkUnits : {p : ℕ} → [hp : Fact (Nat.Prime p)] → {u : ℚ_[p]} → ‖u‖ = 1 → ℤ_[p]ˣ
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.neg : {α : Type u} → [inst : Lean.Grind.Semiring α] → Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.FieldTheory.Normal.Closure
Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [Algebra.IsAlgebraic F K],
  (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
    IntermediateField.normalClosure F K L = ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
-- Mathlib.Topology.Order.LeftRightLim
Monotone.le_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ {x y : α}, x < y → f x ≤ Function.leftLim f y
-- Lean.DocString.Parser
Lean.Doc.Parser.InList.mk : ℕ → Lean.Doc.Parser.OrderedListType ⊕ Lean.Doc.Parser.UnorderedListType → Lean.Doc.Parser.InList
-- Mathlib.Tactic.HaveI
_private.Mathlib.Tactic.HaveI.0.Mathlib.Tactic.HaveI.termHaveIDummy_ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natIsoSc'_hom_app_τ₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c),
  ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₃ = (X.XIsoOfEq hk).hom
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- An induction principle for reasoning about morphisms in SimplexCategoryGenRel, where we compose
with generators on the right.  -/
SimplexCategoryGenRel.hom_induction' : ∀ (P : CategoryTheory.MorphismProperty SimplexCategoryGenRel),
  (∀ {n : ℕ}, P (CategoryTheory.CategoryStruct.id (SimplexCategoryGenRel.mk n))) →
    (∀ {n m : ℕ} (u : SimplexCategoryGenRel.mk (m + 1) ⟶ SimplexCategoryGenRel.mk n) (i : Fin (m + 2)),
        P u → P (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i) u)) →
      (∀ {n m : ℕ} (u : SimplexCategoryGenRel.mk m ⟶ SimplexCategoryGenRel.mk n) (i : Fin (m + 1)),
          P u → P (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ i) u)) →
        ∀ {a b : SimplexCategoryGenRel} (f : a ⟶ b), P f
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If there is a fundamental domain `s`, then `HasFundamentalDomain` holds.  -/
MeasureTheory.IsFundamentalDomain.hasFundamentalDomain : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  (ν : MeasureTheory.Measure α) {s : Set α},
  MeasureTheory.IsFundamentalDomain G s ν → MeasureTheory.HasFundamentalDomain G α ν
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.prodEquiv_apply : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} {C : Type w₁} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : NonUnitalNonAssocSemiring C]
  [inst_5 : DistribMulAction R B] [inst_6 : DistribMulAction R C] (f : (A →ₙₐ[R] B) × (A →ₙₐ[R] C)),
  NonUnitalAlgHom.prodEquiv f = f.1.prod f.2
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The **left-translation shift** on configurations.

We call *configuration* an element of `G → A`.

Given a configuration `x : G → A` and an element `g : G` of the monoid, the shifted configuration
`mulShift g x` is defined by `(mulShift g x) h = x (g * h)`.

Intuitively, this moves the whole configuration "in the direction of `g`": the value
at position `h` in the shifted configuration is the value that was at position
`g * h` in the original one.

For example, if `G = ℤ` (with addition) and `A = {0, 1}`, then
`mulShift 1 x` is the sequence obtained from `x` by shifting every symbol one
step to the left.  -/
SymbolicDynamics.FullShift.mulShift : {A : Type u_1} → {G : Type u_2} → [Monoid G] → G → (G → A) → G → A
-- Lean.Meta.Match.Match
/-- Move variable `#i` to the beginning of the to-do list `p.vars`.  -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.moveToFront : Lean.Meta.Match.Problem → ℕ → Lean.Meta.Match.Problem
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.ext_iff : ∀ {α : Type u} {f g : Ultrafilter α}, f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {toPresheafedSpace : AlgebraicGeometry.PresheafedSpace C}
  {IsSheaf : toPresheafedSpace.presheaf.IsSheaf} {toPresheafedSpace_1 : AlgebraicGeometry.PresheafedSpace C}
  {IsSheaf_1 : toPresheafedSpace_1.presheaf.IsSheaf},
  { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf } =
      { toPresheafedSpace := toPresheafedSpace_1, IsSheaf := IsSheaf_1 } →
    toPresheafedSpace = toPresheafedSpace_1
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.epi_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : D} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∃ X' Y' f', ∃ (_ : CategoryTheory.Epi f'), Nonempty (CategoryTheory.Arrow.mk (L.map f') ≅ CategoryTheory.Arrow.mk f)
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- A coalgebra isomorphism preserves group-like elements.  -/
isGroupLikeElem_map_equiv : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Coalgebra R A] [inst_5 : Module R B]
  [inst_6 : Coalgebra R B] {a : A} [inst_7 : EquivLike F A B] [CoalgEquivClass F R A B] (f : F),
  IsGroupLikeElem R (f a) ↔ IsGroupLikeElem R a
-- Mathlib.Order.Monotone.Defs
instDecidableStrictMonoOfForallForallForallLt : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → {f : α → β} → [i : Decidable (∀ (a b : α), a < b → f a < f b)] → Decidable (StrictMono f)
-- Mathlib.CategoryTheory.Sites.SheafHom
/-- Given two sheaves `F` and `G` on a site `(C, J)` with values in a category `A`,
this `sheafHom F G` is the sheaf of types which sends an object `X : C`
to the type of morphisms between the "restrictions" of `F` and `G` to the category `Over X`.  -/
CategoryTheory.sheafHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          CategoryTheory.Sheaf J A → CategoryTheory.Sheaf J A → CategoryTheory.Sheaf J (Type (max (max u v') v))
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instAddOfContinuousAdd : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddZeroClass β] → [ContinuousAdd β] → Add (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.factorial_smul_hasseDeriv : ∀ {R : Type u_1} [inst : Semiring R] (k : ℕ), ⇑(k.factorial • Polynomial.hasseDeriv k) = (⇑Polynomial.derivative)^[k]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a `PullbackObjObj` of `f₁ : Arrow C₁` and `f₃ : Arrow C₃`, a `PullbackObjObj` of `f₁'` and
`f₃ : Arrow C₃`, and a morphism `f₁' ⟶ f₁`, this defines a morphism between the induced
pullback maps.  -/
CategoryTheory.Functor.PullbackObjObj.mapArrowLeft : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {f₁ f₁' : CategoryTheory.Arrow C₁} →
                {f₃ : CategoryTheory.Arrow C₃} →
                  (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) →
                    (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) →
                      (f₁' ⟶ f₁) → (CategoryTheory.Arrow.mk sq₁₃.π ⟶ CategoryTheory.Arrow.mk sq₁₃'.π)
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
/-- The cone over the tower
```
⋯ → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N
```
with cone point `∏ M`. This is a limit cone, see `CategoryTheory.Limits.SequentialProduct.isLimit`.
 -/
CategoryTheory.Limits.SequentialProduct.cone : {C : Type u_1} →
  {M N : ℕ → C} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      (f : (n : ℕ) → M n ⟶ N n) →
        [inst_1 : CategoryTheory.Limits.HasCountableProducts C] →
          CategoryTheory.Limits.Cone
            (CategoryTheory.Functor.ofOpSequence (CategoryTheory.Limits.SequentialProduct.functorMap f))
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_inv_div_log_sq_Ioi : ∀ {c : ℝ}, 1 < c → ∫ (t : ℝ) in Set.Ioi c, t⁻¹ / Real.log t ^ 2 = (Real.log c)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C} (α : X ⟶ Y),
  (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon C).map α =
    ((CategoryTheory.Functor.mapAddMonFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C).map α).app
      (CategoryTheory.AddMon.trivial (CategoryTheory.Discrete PUnit.{w + 1}))
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Postcomposing `f` with `Prod.fst` is `C^n`  -/
ContDiff.fst : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F × G},
  ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => (f x).1
-- Lean.Parser.Types
/-- If not `missing`, used for lazily calculating `unexpected` message and range in `mkErrorMessage`.
Otherwise, `ParserState.pos` is used as an empty range.  -/
Lean.Parser.Error.unexpectedTk : Lean.Parser.Error → Lean.Syntax
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.comp_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃),
  (φ₁₂.comp φ₂₃).τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.hasLimit_comp_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D)
  (E : CategoryTheory.Functor D C) [E.IsEquivalence] [CategoryTheory.Limits.HasLimit K],
  CategoryTheory.Limits.HasLimit (K.comp E)
-- Mathlib.Topology.EMetricSpace.Defs
Metric.mem_closedEBall_comm : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal},
  x ∈ Metric.closedEBall y ε ↔ y ∈ Metric.closedEBall x ε
-- Aesop.Rule.Name
Aesop.RuleName : Type
-- Mathlib.Data.Nat.Factorial.Basic
/-- Avoid in favor of `Nat.factorial_mul_ascFactorial'` if you can. ℕ-division isn't worth it.  -/
Nat.ascFactorial_eq_div' : ∀ (n k : ℕ), 0 < n → n.ascFactorial k = (n + k - 1).factorial / (n - 1).factorial
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.instFinite : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  {P : β → Prop}, Std.Iterators.Finite (Std.Iterators.Types.Attach α m P) m
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumCongr_symm_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13} [inst_8 : TopologicalSpace M']
  [inst_9 : ChartedSpace H M'] {N : Type u_15} [inst_10 : TopologicalSpace N] [inst_11 : ChartedSpace H N]
  {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [inst_12 : TopologicalSpace N'] [inst_13 : ChartedSpace H N']
  (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n), φ.symm.sumCongr ψ.symm = (φ.sumCongr ψ).symm
-- Init.Data.Dyadic.Basic
/-- The number of trailing zeros in the binary representation of `i`.  -/
Int.trailingZeros : ℤ → ℕ
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.State.mk : Lean.NameMap (Array Lean.Name) → Lean.NameSet → Lean.CollectAxioms.State✝
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.VAddInvariantMeasure.vadd : ∀ {M : Type v} {α : Type w} [inst : VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure M α μ] (c : ENNReal), MeasureTheory.VAddInvariantMeasure M α (c • μ)
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotientInfEquivSupQuotient_symm_apply_right : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M)
  {x : ↥(p ⊔ p')}, ↑x ∈ p' → (LinearMap.quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.tail?.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (h : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.Heap.tail? le h =
    Option.map (fun x => x.2) (Batteries.BinomialHeap.Imp.Heap.deleteMin le h)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabMutualDef.elabAsync : Array Lean.Expr →
  Lean.Elab.Command.Scope →
    Array Lean.Elab.DefView →
      Lean.Elab.DefViewElabHeader → Lean.Elab.DefView → Lean.Elab.ExpandDeclIdResult → Lean.Elab.TermElabM Unit
-- Mathlib.LinearAlgebra.Basis.VectorSpace
quotient_prod_linearEquiv : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (p : Submodule K V), Nonempty (((V ⧸ p) × ↥p) ≃ₗ[K] V)
-- Mathlib.Algebra.Order.IsBotOne
bot_eq_one : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α] [inst_3 : OrderBot α], ⊥ = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensor_id : ∀ (x y : AugmentedSimplexCategory),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id x)
      (CategoryTheory.CategoryStruct.id y) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z}, CategoryTheory.IsPullback fst snd f g → CategoryTheory.IsPushout g.op f.op snd.op fst.op
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeConnectedSpaceCarrierCarrierCommRingCat : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms fun x => ConnectedSpace ↥x
-- Mathlib.RingTheory.Valuation.RamificationGroup
/-- The valuation subring `A` (considered as a subset of `L`)
is stable under the action of the decomposition group.  -/
ValuationSubring.subMulAction : (K : Type u_1) →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (A : ValuationSubring L) → SubMulAction (↥(ValuationSubring.decompositionSubgroup K A)) L
-- Mathlib.Data.Rat.Star
NNRat.instStarOrderedRing : StarOrderedRing ℚ≥0
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.map_extend_nhds_of_boundaryless : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {x : M},
  x ∈ f.source → Filter.map (↑(f.extend I)) (nhds x) = nhds (↑(f.extend I) x)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.limitsOfShape_congr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J']
  (e : J ≌ J'), P.limitsOfShape J = P.limitsOfShape J'
-- Mathlib.CategoryTheory.Bicategory.Product
/-- The cartesian product of two bicategories.  -/
CategoryTheory.Bicategory.prod : (B : Type u₁) →
  [CategoryTheory.Bicategory B] → (C : Type u₂) → [CategoryTheory.Bicategory C] → CategoryTheory.Bicategory (B × C)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.iff_of_iSup_eq_top : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y]
  {ι : Type u_1} (U : ι → ↑X.affineOpens),
  ⨆ i, ↑(U i) = ⊤ → (P f ↔ ∀ (i : ι), Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ ↑(U i) ⋯)))
-- Init.System.IO
/-- Checks whether the indicated path can be read and is a directory. This function will traverse
symlinks.
 -/
System.FilePath.isDir : System.FilePath → BaseIO Bool
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : Subsingleton S]
  (c : MvPolynomial PUnit.{u_2 + 1} R) (x : S), SMul.smul c x = (MvPolynomial.aeval fun x => 1).toRingHom c * x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxKeyD fallback = t₂.maxKeyD fallback
-- Lean.Setup
Lean.ModuleArtifacts.irSig? : Lean.ModuleArtifacts → Option System.FilePath
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.minEntry?.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.minEntry? x =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => some (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      Std.DTreeMap.Internal.Impl.Const.minEntry? l
-- Mathlib.Combinatorics.Quiver.Path
/-- `Path a b` is the type of paths from `a` to `b` through the arrows of `G`.  -/
Quiver.Path : {V : Type u} → [Quiver V] → V → V → Type (max u v)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.instNoPrefixPatternModel : ∀ {pat : String.Slice}, String.Slice.Pattern.Model.NoPrefixPatternModel pat
-- Lean.Meta.SynthInstance
/-- Create a `key` for the goal associated with the given metavariable.
That is, we create a key for the type of the metavariable.

We must instantiate assigned metavariables before we invoke `mkTableKey`.  -/
Lean.Meta.SynthInstance.mkTableKeyFor : Lean.MetavarContext → Lean.Expr → Lean.Meta.SynthInstance.SynthM Lean.Expr
-- Mathlib.Logic.Equiv.Basic
/-- If for each `x` we have `p x ↔ q (f x)`, then `Σ y : {y // q y}, f ⁻¹' {y}` is equivalent
to `{x // p x}`.  -/
Equiv.sigmaSubtypeFiberEquivSubtype : {α : Type u_9} →
  {β : Type u_10} →
    (f : α → β) →
      {p : α → Prop} → {q : β → Prop} → (∀ (x : α), p x ↔ q (f x)) → (y : Subtype q) × { x // f x = ↑y } ≃ Subtype p
-- Mathlib.CategoryTheory.Monoidal.Tor
CategoryTheory.Tor'_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (k : C) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Tor' C n).obj k).map f =
    (CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringRight C).map f) n).app k
-- Lean.Parser.Do
Lean.Parser.Term.doFor.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.isChain : ∀ {α : Type u_1} {r : α → α → Prop} {c : Set α}, ChainClosure r c → IsChain r c
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.expand_zmod : ∀ {σ : Type u_1} {p : ℕ} [inst : Fact (Nat.Prime p)] (f : MvPolynomial σ (ZMod p)), (MvPolynomial.expand p) f = f ^ p
-- Init.Data.String.Defs
String.Pos.Raw.byteIdx_add_slide : ∀ {p : String.Pos.Raw} {s : String.Slice}, (p + s).byteIdx = p.byteIdx + s.utf8ByteSize
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.mem_coe_toEdge : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} (h : M.IsMatching) {v : V} (hv : v ∈ M.verts),
  v ∈ ↑(h.toEdge ⟨v, hv⟩)
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_uInt8ToBitVec : ∀ (n : UInt8), { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedInstance.default : Lean.Meta.SynthInstance.Instance
-- Mathlib.RingTheory.WittVector.Complete
/-- If `k` is a perfect ring of characteristic `p`, there is an isomorphism between the quotient
`𝕎 k / p` and `k`.
 -/
WittVector.quotientPEquiv : {p : ℕ} →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} → [inst : CommRing k] → [CharP k p] → [PerfectRing k p] → WittVector p k ⧸ Ideal.span {↑p} ≃+* k
-- Init.Prelude
/-- Non-strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
 -/
UInt8.le : UInt8 → UInt8 → Prop
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.smul_Lp_const : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] [inst_5 : MeasureTheory.IsFiniteMeasure μ] (c : Mᵈᵐᵃ) (a : E),
  c • (MeasureTheory.Lp.const p μ) a = (MeasureTheory.Lp.const p μ) a
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_neg : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : Neg R] (A : Matrix m n R), (-A).vec = -A.vec
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.cons_sub_cons : ∀ {α : Type u_1} {n : ℕ} [inst : Sub α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α),
  Matrix.vecCons x v - Matrix.vecCons y w = Matrix.vecCons (x - y) (v - w)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : Multiplicative M →* A) (a : M) (b : R),
  ((AddMonoidAlgebra.lift R A M) F) (AddMonoidAlgebra.single a b) = b • F (Multiplicative.ofAdd a)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.algebraMap_ne_zero : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {x : Polynomial K},
  x ≠ 0 → (algebraMap (Polynomial K) (RatFunc K)) x ≠ 0
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- An element a divides the sum a + b if and only if a divides b.  -/
dvd_add_self_left : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, a ∣ a + b ↔ a ∣ b