mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.l_naturality : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft CategoryTheory.FreeMonoidalCategory.unit f).comp
      (CategoryTheory.FreeMonoidalCategory.Hom.l_hom Y))
    ((CategoryTheory.FreeMonoidalCategory.Hom.l_hom X).comp f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v : V} (x : V) (x_1 : x ∈ SimpleGraph.Walk.nil.support),
  SimpleGraph.Walk.nil.takeUntil x x_1 = ⋯.mpr SimpleGraph.Walk.nil
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_eq_zero_iff : ∀ {α : Type u_1} {G : SimpleGraph α}, G.radius = 0 ↔ Nonempty α ∧ Subsingleton α
-- Lean.Syntax
Lean.SyntaxNode.modifyArgs : Lean.SyntaxNode → (Array Lean.Syntax → Array Lean.Syntax) → Lean.Syntax
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_neg : ∀ {G : Type u_4} [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : MeasurableNeg G],
  (MeasurableEquiv.neg G).symm = MeasurableEquiv.neg G
-- Mathlib.Data.Fintype.Basic
Unique.fintype : {α : Type u_4} → [Unique α] → Fintype α
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Given a co-Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and another morphism
`φ' : a ⟶ b'` which also lifts `f`. Then any morphism `ψ : b ⟶ b'` lifting `𝟙 S` such that
`g ≫ ψ = φ'` must equal the map induced by the universal property of `φ`.  -/
CategoryTheory.Functor.IsCocartesian.map_uniq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCocartesian f φ] {b' : 𝒳}
  (φ' : a ⟶ b') [inst_3 : p.IsHomLift f φ'] (ψ : b ⟶ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) ψ],
  CategoryTheory.CategoryStruct.comp φ ψ = φ' → ψ = CategoryTheory.Functor.IsCocartesian.map p f φ φ'
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- This `ForIn'`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
 -/
Std.IteratorLoop.finiteForIn' : {m : Type w → Type w'} →
  {n : Type x → Type x'} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] →
          [Monad n] →
            ((γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) →
              ForIn' n (Std.IterM m β) β { mem := fun it out => it.IsPlausibleIndirectOutput out }
-- Mathlib.Testing.Plausible.Functions
Plausible.TotalFunction.DFinsupp.sampleableExt : {α : Type u} →
  {β : Type v} →
    [DecidableEq α] →
      [inst : Zero β] →
        [DecidableEq β] →
          [Plausible.SampleableExt α] → [Plausible.SampleableExt β] → [Repr α] → Plausible.SampleableExt (Π₀ (x : α), β)
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- If a functor inverts homotopy equivalences, it sends homotopic maps to the same map.  -/
Homotopy.map_eq_of_inverts_homotopyEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} {φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁),
  (∀ (j : ι), ∃ i, c.Rel i j) →
    ∀ [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)]
      [HomologicalComplex.HasHomotopyCofiber
          (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F)
            (-CategoryTheory.CategoryStruct.id F))]
      {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
      (H : CategoryTheory.Functor (HomologicalComplex C c) D),
      (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy H → H.map φ₀ = H.map φ₁
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The residue of `completedHurwitzZetaEven a s` at `s = 1` is equal to `1`.  -/
HurwitzZeta.completedHurwitzZetaEven_residue_one : ∀ (a : UnitAddCircle),
  Filter.Tendsto (fun s => (s - 1) * HurwitzZeta.completedHurwitzZetaEven a s) (nhdsWithin 1 {1}ᶜ) (nhds 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) (j : J),
  (c.ici j).isoBot = CategoryTheory.Iso.refl ((⋯.functor.comp c.F).obj ⊥)
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsLEObjSingleFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : C) (n : ℤ), ((DerivedCategory.Plus.singleFunctor C n).obj X).IsLE n
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- `p.Fiber S` is isomorphic to the quotient `Sₚ ⧸ pSₚ`.  -/
Ideal.Fiber.algEquivAux₁ : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            [inst_3 : p.IsPrime] →
              p.Fiber S ≃ₐ[S]
                Localization (Algebra.algebraMapSubmonoid S p.primeCompl) ⧸
                  Ideal.map (algebraMap S (Localization (Algebra.algebraMapSubmonoid S p.primeCompl)))
                    (Ideal.map (algebraMap R S) p)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.ofNat : ℕ → Turing.PartrecToTM2.K'
-- Mathlib.Data.Set.Sups
Set.iUnion_image_sup_left : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t : Set α), ⋃ a ∈ s, (fun x1 x2 => x1 ⊔ x2) a '' t = s ⊻ t
-- Mathlib.Order.Hom.Basic
/-- Constant function bundled as an `OrderHom`.  -/
OrderHom.const : (α : Type u_6) → [inst : Preorder α] → {β : Type u_7} → [inst_1 : Preorder β] → β →o α →o β
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f : α → β} [inst_1 : Zero β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ),
  MeasureTheory.FinStronglyMeasurable (MeasureTheory.AEFinStronglyMeasurable.mk f hf) μ
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The canonical projection map `D ≀ᵣ Q →* Q`, as a group hom.  -/
RegularWreathProduct.rightHom : {D : Type u_1} → {Q : Type u_2} → [inst : Group D] → [inst_1 : Group Q] → D ≀ᵣ Q →* Q
-- Mathlib.Order.Filter.Extr
Filter.EventuallyLE.isMaxFilter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  g ≤ᶠ[l] f → f a = g a → IsMaxFilter f l a → IsMaxFilter g l a
-- Mathlib.Tactic.Linter.Style
/-- The "longFile" linter emits a warning on files which are longer than a certain number of lines
(`linter.style.longFileDefValue` by default on mathlib, no limit for downstream projects).
If this option is set to `N` lines, the linter warns once a file has more than `N` lines.
A value of `0` silences the linter entirely.
 -/
Mathlib.Linter.linter.style.longFile : Lean.Option ℕ
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.PlausibleStep.start : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β} {it' : Std.IterM m β} {out : β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    it.internalState.dropping = true →
      (P out).Property { down := false } →
        Std.Iterators.Types.DropWhile.PlausibleStep it
          (Std.IterStep.yield (Std.IterM.Intermediate.dropWhileWithPostcondition P false it') out)
-- Mathlib.Topology.MetricSpace.Cauchy
/-- Yet another metric characterization of Cauchy sequences on integers. This one is often the
most efficient.  -/
cauchySeq_iff_le_tendsto_0 : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : ℕ → α},
  CauchySeq s ↔
    ∃ b,
      (∀ (n : ℕ), 0 ≤ b n) ∧
        (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (nhds 0)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.lift_K_comp_cyclesIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (h.liftK k hk) h.cyclesIso.inv = S.liftCycles k hk
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- Special case of the **Plünnecke-Ruzsa inequality**. Multiplication version.  -/
Finset.pluennecke_ruzsa_inequality_pow_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] {A : Finset G},
  A.Nonempty → ∀ (B : Finset G) (n : ℕ), ↑(B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- The implicit function defined by a $C^n$ implicit equation is $C^n$. This applies to the general
form of the implicit function theorem.  -/
ImplicitFunctionData.contDiffAt_implicitFunction : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {φ : ImplicitFunctionData 𝕜 E₁ E₂ F} {n : WithTop ℕ∞},
  ContDiffAt 𝕜 n φ.leftFun φ.pt →
    ContDiffAt 𝕜 n φ.rightFun φ.pt → n ≠ 0 → ContDiffAt 𝕜 n (Function.uncurry φ.implicitFunction) (φ.prodFun φ.pt)
-- Mathlib.Data.Set.Restrict
Set.restrictPreimage_injective : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
  Function.Injective f → Function.Injective (t.restrictPreimage f)
-- Mathlib.Data.Finmap
Finmap.entries_insert_of_notMem : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s : Finmap β},
  a ∉ s → (Finmap.insert a b s).entries = ⟨a, b⟩ ::ₘ s.entries
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.StructuredArrow.isClosedUnderLimitsOfShape : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} J] {P : CategoryTheory.MorphismProperty T} [P.RespectsIso]
  [CategoryTheory.Limits.PreservesLimitsOfShape J L] [CategoryTheory.Limits.HasLimitsOfShape J A]
  (c : (D : CategoryTheory.Functor J T) → [CategoryTheory.Limits.HasLimit D] → CategoryTheory.Limits.Cone D)
  (hc :
    (D : CategoryTheory.Functor J T) →
      [inst_6 : CategoryTheory.Limits.HasLimit D] → CategoryTheory.Limits.IsLimit (c D)),
  (∀ (D : CategoryTheory.Functor J T) [inst_6 : CategoryTheory.Limits.HasLimit D] {X : T}
      (s : (CategoryTheory.Functor.const J).obj X ⟶ D),
      (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })) →
    ∀ (X : T), (CategoryTheory.MorphismProperty.structuredArrowObj L P).IsClosedUnderLimitsOfShape J
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map'_comp_map' : ∀ {β : Type w} {α : Type w₂} {γ : Type w₃} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C}
  {g : β → C} {h : γ → C} [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g]
  [inst_3 : CategoryTheory.Limits.HasProduct h] (p : β → α) (p' : γ → β) (q : (b : β) → f (p b) ⟶ g b)
  (q' : (c : γ) → g (p' c) ⟶ h c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map' p' q') =
    CategoryTheory.Limits.Pi.map' (p ∘ p') fun c => CategoryTheory.CategoryStruct.comp (q (p' c)) (q' c)
-- Mathlib.Topology.Bornology.Absorbs
absorbs_inter : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
  {s t u : Set α}, Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.equivProjectivization_apply_infinity : ∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : DecidableEq K],
  (OnePoint.equivProjectivization K) OnePoint.infty = Projectivization.mk K ![1, 0] ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The complex cosine function is everywhere differentiable, with the derivative `-sin x`.  -/
Complex.hasDerivAt_cos : ∀ (x : ℂ), HasDerivAt Complex.cos (-Complex.sin x) x
-- Mathlib.Order.Notation
Max.ext_iff : ∀ {α : Type u} {x y : Max α}, x = y ↔ max = max
-- Mathlib.Data.Finset.Card
Finset.le_card_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), t.card - s.card ≤ (t \ s).card
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.pi : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {ι : Type u_3} [Finite α] {f : ι → α → M},
  (∀ (a : α), Function.HasFiniteSupport fun x => f x a) → Function.HasFiniteSupport f
-- Mathlib.Algebra.Group.Even
even_ofMul_iff : ∀ {α : Type u_2} [inst : Mul α] {a : α}, Even (Additive.ofMul a) ↔ IsSquare a
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.vecMulBilin_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : SMulCommClass S R A]
  [inst_6 : SMulCommClass S A A] [inst_7 : IsScalarTower R A A] [inst_8 : Fintype m] (v : m → A) (M : Matrix m n A),
  ((Matrix.vecMulBilin R S) v) M = Matrix.vecMul v M
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_memPartition_le : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (t n)) → ∀ (n : ℕ), MeasurableSpace.generateFrom (memPartition t n) ≤ m
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.of_subtype : ∀ {α : Type u} [t : TopologicalSpace α] (s : Set α) [TopologicalSpace.SeparableSpace ↑s], TopologicalSpace.IsSeparable s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Order.Category.BddLat
BddLat.coe_of : ∀ (α : Type u_1) [inst : Lattice α] [inst_1 : BoundedOrder α], ↑(BddLat.of α).toLat = α
-- Mathlib.Combinatorics.SetFamily.LYM
Finset.sized_falling : ∀ {α : Type u_2} [inst : DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)), Set.Sized k ↑(Finset.falling k 𝒜)
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_zero : String.Pos.Raw.byteIdx 0 = 0
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.add_zsmul : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a b : ℤ) (c : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.zsmul (a + b) c =
    Lean.Grind.IntModule.OfNatModule.add (Lean.Grind.IntModule.OfNatModule.zsmul a c)
      (Lean.Grind.IntModule.OfNatModule.zsmul b c)
-- Lean.DocString.Parser
/-- Parses as `ifVerso` if the option `doc.verso` is `true`, or as `ifNotVerso` otherwise.
 -/
Lean.Doc.Parser.ifVerso : Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.RingTheory.DedekindDomain.Different
map_equiv_traceDual : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [IsFractionRing A K]
  [inst_12 : IsDomain A] [inst_13 : IsFractionRing B L] [inst_14 : IsDomain B] [inst_15 : FaithfulSMul A B]
  (I : Submodule B (FractionRing B)),
  Submodule.map (FractionRing.algEquiv B L).toLinearMap (Submodule.traceDual A (FractionRing A) I) =
    Submodule.traceDual A K (Submodule.map (FractionRing.algEquiv B L).toLinearMap I)
-- Init.Data.UInt.Bitwise
UInt64.ofBitVec_not : ∀ (a : BitVec 64), { toBitVec := ~~~a } = ~~~{ toBitVec := a }
-- Lean.Meta.Tactic.Grind.MarkAccessible
/-- Return `some originalName` if `name` is a name generated by `markAccessible`.
`originalName` is the original name before `markAccessible` was invoked.
 -/
Lean.Meta.Grind.getOriginalName? : Lean.Name → Option Lean.Name
-- Mathlib.Data.Sign.Defs
SignType.nonneg_iff : ∀ {a : SignType}, 0 ≤ a ↔ a = 0 ∨ a = 1
-- Mathlib.RingTheory.Ideal.Maps
Algebra.idealMap_apply_coe : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : Semiring S] [inst_2 : Algebra R S] (I : Ideal R)
  (c : ↥I), ↑((Algebra.idealMap S I) c) = (algebraMap R S) ↑c
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instCreatesColimitsOfShapeOverSchemeTopMorphismPropertyOverDiscreteForgetOfSmall : (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) →
  [AlgebraicGeometry.IsZariskiLocalAtSource P] →
    {S : AlgebraicGeometry.Scheme} →
      (J : Type u_2) →
        [Small.{u, u_2} J] →
          CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J)
            (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Dep.of_contract : ∀ {α : Type u_1} {M : Matroid α} {X C : Set α},
  (M.contract C).Dep X → autoParam (C ⊆ M.E) Matroid.Dep.of_contract._auto_1 → M.Dep (C ∪ X)
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
/-- A change of basis formula for barycentric coordinates.

See also `AffineBasis.toMatrix_vecMul_coords`.  -/
AffineBasis.toMatrix_inv_vecMul_toMatrix : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : CommRing k] [inst_3 : Module k V] [inst_4 : DecidableEq ι] [inst_5 : Fintype ι] (b b₂ : AffineBasis ι k P)
  (x : P), Matrix.vecMul (b.coords x) (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
-- Mathlib.RingTheory.Localization.Integer
/-- Given `a : S`, `S` a localization of `R`, `IsInteger R a` iff `a` is in the image of
the localization map from `R` to `S`.  -/
IsLocalization.IsInteger : (R : Type u_1) → [inst : CommSemiring R] → {S : Type u_2} → [inst_1 : CommSemiring S] → [Algebra R S] → S → Prop
-- Mathlib.NumberTheory.LSeries.Nonvanishing
DirichletCharacter.zetaMul.eq_1 : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N), χ.zetaMul = ↑ArithmeticFunction.zeta * toArithmeticFunction fun x => χ ↑x
-- Mathlib.Order.Preorder.Finite
Set.Finite.exists_maximal : ∀ {α : Type u_2} [inst : LE α] [IsTrans α LE.le] {s : Set α}, s.Finite → s.Nonempty → ∃ i, Maximal (fun x => x ∈ s) i
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.hom_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C}
  (g1 g2 : CategoryTheory.Limits.widePushout B objs arrows ⟶ X),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j) g1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j) g2) →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows) g1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows) g2 →
      g1 = g2
-- Lean.Meta.CongrTheorems
/-- If `f` is a class constructor, return a bitmask `m` s.t. `m[i]` is true if the `i`-th parameter
corresponds to a subobject field.

We use this function to implement the special support for class constructors at `getCongrSimpKinds`.
See issue #1808
 -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.getClassSubobjectMask? : Lean.Expr → Lean.MetaM (Option (Array Bool))
-- Mathlib.Topology.ContinuousOn
nhdsWithin_le_comap : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → nhdsWithin x s ≤ Filter.comap f (nhdsWithin (f x) (f '' s))
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Produce an `AlternatingMap` out of a `MultilinearMap`, by summing over all argument
permutations.  -/
MultilinearMap.alternatization : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N' : Type u_6} →
            [inst_3 : AddCommGroup N'] →
              [inst_4 : Module R N'] →
                {ι : Type u_7} → [Fintype ι] → [DecidableEq ι] → MultilinearMap R (fun x => M) N' →+ M [⋀^ι]→ₗ[R] N'
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.find?_prop_eq_find?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.find? p = s.find? fun x => decide (p x)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.col_eq_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.col = Matrix.of.symm A.transpose
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀ : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] (M' : Submodule R M), IsLocalizedModule p (Submodule.toLocalized₀ p f M')
-- Mathlib.Order.SymmDiff
sdiff_symmDiff_left : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), a \ symmDiff a b = a ⊓ b
-- Mathlib.Data.Set.Finite.Monad
Set.fintypeSeq : {α : Type u} →
  {β : Type v} → [DecidableEq β] → (f : Set (α → β)) → (s : Set α) → [Fintype ↑f] → [Fintype ↑s] → Fintype ↑(f.seq s)
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.continuousAt_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y},
  IsOpenQuotientMap f → ∀ {g : Y → Z} {x : X}, ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the reverse direction of `spectrum.inv₀_mem_inv_iff`. -/
spectrum.inv₀_mem_inv : ∀ {R : Type u} {A : Type v} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : Aˣ},
  r ∈ spectrum R ↑a → r⁻¹ ∈ spectrum R ↑a⁻¹
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- The determinant, but only the terms of a given sign.
`A.detp 1` is written `|A|⁺` in the literature and `A.detp (-1)` is written `|A|⁻`.  -/
Matrix.detp : {n : Type u_1} → {R : Type u_3} → [Fintype n] → [DecidableEq n] → [CommSemiring R] → ℤˣ → Matrix n n R → R
-- Mathlib.Algebra.Homology.Augment
CochainComplex.augmentTruncate_inv_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ), C.augmentTruncate.inv.f 0 = CategoryTheory.CategoryStruct.id (C.X 0)
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
/-- This is [serre1965](Ch. V, §9, Lemma 3).  -/
RootPairing.baseOf_pairwise_pairing_le_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : CommRing R] [inst_3 : Module R M] [inst_4 : Module R N] (P : RootPairing ι R M N)
  {S : Type u_5} [inst_5 : LinearOrder S] [inst_6 : AddCommGroup S] [IsOrderedAddMonoid S] (f : M →+ S) [CharZero R]
  [IsDomain R] [inst_10 : P.IsCrystallographic],
  (∀ (i : ι), f (P.root i) ≠ 0) → (IsAddIndecomposable.baseOf (⇑P.root) f).Pairwise fun i j => P.pairingIn ℤ i j ≤ 0
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderComposition], P.precoverage.IsStableUnderComposition
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.isOpenMap_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenMap ⇑(CompactCoherentification.mk X)