mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₂₃ (CategoryTheory.CategoryStruct.comp h₂₃.p₂ h_1) =
    CategoryTheory.CategoryStruct.comp h.p₃ h_1
-- Lean.Server.Requests
Lean.Server.RequestError.ofIoError : IO.Error → Lean.Server.RequestError
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The map from the restriction of a presheafed space.
 -/
AlgebraicGeometry.PresheafedSpace.ofRestrict : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {U : TopCat} →
      (X : AlgebraicGeometry.PresheafedSpace C) →
        {f : U ⟶ ↑X} → (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) → X.restrict h ⟶ X
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.bot_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⊥.addSubgroupOf H = ⊥
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.finsetSum_singleton`. -/
Set.finset_sum_singleton : ∀ {M : Type u_5} {ι : Type u_6} [inst : AddCommMonoid M] (s : Finset ι) (I : ι → M), ∑ i ∈ s, {I i} = {∑ i ∈ s, I i}
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.adjoin_rootSet : ∀ {K : Type v} [inst : Field K] (f : Polynomial K), Algebra.adjoin K (f.rootSet f.SplittingField) = ⊤
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcReleaseParams.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (sessionId : UInt64) (refs : Array Lean.Json) (uri_1 : Lean.Lsp.DocumentUri)
  (sessionId_1 : UInt64) (refs_1 : Array Lean.Json),
  ({ uri := uri, sessionId := sessionId, refs := refs } = { uri := uri_1, sessionId := sessionId_1, refs := refs_1 }) =
    (uri = uri_1 ∧ sessionId = sessionId_1 ∧ refs = refs_1)
-- Init.Omega.IntList
Lean.Omega.IntList.get.eq_1 : ∀ (xs : Lean.Omega.IntList) (i : ℕ), xs.get i = xs[i]?.getD 0
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.to_isSeparable : ∀ {F : Type u_1} {inst : Field F} {E : Type u_2} {inst_1 : Field E} {inst_2 : Algebra F E} [self : IsGalois F E],
  Algebra.IsSeparable F E
-- Mathlib.NumberTheory.Padics.Complex
PadicAlgCl.instCoePadic : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Coe ℚ_[p] (PadicAlgCl p)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.instReprExpr_lean.repr : Nat.Internal.Linear.Expr → ℕ → Std.Format
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Multiplying by an a.e. strongly measurable scalar *function* with values in a group preserves
a.e. strong measurability. This is the varying-scalar analogue of
`aestronglyMeasurable_const_smul_iff`.  -/
aestronglyMeasurable_smul_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {G : Type u_6} [inst_1 : Group G] [inst_2 : MulAction G β] [inst_3 : TopologicalSpace G] [ContinuousInv G]
  [ContinuousSMul G β] {c : α → G},
  MeasureTheory.AEStronglyMeasurable c μ →
    (MeasureTheory.AEStronglyMeasurable (fun x => c x • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ)
-- Mathlib.Topology.NhdsWithin
eventually_nhds_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop},
  (∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchClone.tmpMVarId : Lean.MVarId
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.one_div_add_one_div : ∀ (p q r : ENNReal) [p.HolderTriple q r], 1 / p + 1 / q = 1 / r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α} {hc : t.maxKeyD fallback ∈ t}, t.getKey (t.maxKeyD fallback) hc = t.maxKeyD fallback
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- When `I ⊓ J` is a sub-dp-ideal of `I`, this is the divided power structure on the ideal
`I(A⧸J)` of the quotient.  -/
DividedPowers.Quotient.dividedPowers : {A : Type u_1} →
  [inst : CommRing A] →
    {I : Ideal A} →
      (hI : DividedPowers I) →
        {J : Ideal A} → hI.IsSubDPIdeal (J ⊓ I) → DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Differentiable.comp_mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {g : F → F'}
  {f : M → F} {x : M}, Differentiable 𝕜 g → MDiffAt f x → MDiffAt (g ∘ f) x
-- Mathlib.Topology.Order.OrderClosed
Ioc_mem_nhdsLE_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioc a c → Set.Ioc a c ∈ nhdsWithin b (Set.Iic b)
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in a commutative Banach algebra `𝔸` over a normed field `𝕂` of
characteristic zero has strict Fréchet derivative `NormedSpace.exp x • 1 : 𝔸 →L[𝕂] 𝔸`
at any point `x` in the disk of convergence.  -/
hasStrictFDerivAt_exp_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸},
  x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius → HasStrictFDerivAt NormedSpace.exp (NormedSpace.exp x • 1) x
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.nil : {α : Type u} → Ordnode α
-- Mathlib.Analysis.Convex.Join
convexJoin_segments : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (a b c d : E),
  convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜) {a, b, c, d}
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
/-- Define a left action of `Cᵒᵖ` on `Dᵒᵖ` from a left action of `C` on `D` via
the formula `(op c) ⊙ₗ (op d) = op (c ⊙ₗ d)`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction : (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] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH0_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.shortComplexH0 A).f = groupHomology.d₁₀ A
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.add_liftCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {A : C} (k k' : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) (hk' : CategoryTheory.CategoryStruct.comp k' S.g = 0),
  S.liftCycles k hk + S.liftCycles k' hk' = S.liftCycles (k + k') ⋯
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.sc j ≅ K.sc' i j k` when `c.prev j = i` and `c.next j = k`.  -/
HomologicalComplex.isoSc' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) → (i j k : ι) → c.prev j = i → c.next j = k → (K.sc j ≅ K.sc' i j k)
-- Lean.DocString.Parser
Lean.Doc.Parser.UnorderedListType.noConfusionType : Sort v✝ → Lean.Doc.Parser.UnorderedListType → Lean.Doc.Parser.UnorderedListType → Sort v✝
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.natTransQ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q : ℕ)
  (x : CategoryTheory.SimplicialObject C), (AlgebraicTopology.DoldKan.natTransQ q).app x = AlgebraicTopology.DoldKan.Q q
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- A homeomorphism induces an open partial homeomorphism on the whole space  -/
Homeomorph.toOpenPartialHomeomorph : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → OpenPartialHomeomorph X Y
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.rightHom_comp_splitting : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (s : S.Splitting), S.rightHom.comp ↑s = AddMonoidHom.id G
-- Batteries.Recycling.RBTree.Basic
/-- `alter cut f t` simultaneously handles inserting, erasing and replacing an element
using a function `f : Option α → Option α`. It is passed the result of `t.find? cut`
and can either return `none` to remove the element or `some a` to replace/insert
the element with `a` (which must have the same ordering properties as the original element).

The element is used linearly if `t` is unshared.
 -/
RBTree.RBNode.alter : {α : Type u_1} → (α → Ordering) → (Option α → Option α) → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (z : ℤ), ⌈↑z⌉ = z
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_and : ∀ (a b : ISize) (h : System.Platform.numBits = 32), (a &&& b).toBitVec32 h = a.toBitVec32 h &&& b.toBitVec32 h
-- Init.Data.SInt.Bitwise
ISize.toInt64_xor : ∀ (a b : ISize), (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.mk.injEq : ∀ (goal : Aesop.GoalRef) (priority : Aesop.Percent) (lastExpandedInIteration addedInIteration : Aesop.Iteration)
  (goal_1 : Aesop.GoalRef) (priority_1 : Aesop.Percent)
  (lastExpandedInIteration_1 addedInIteration_1 : Aesop.Iteration),
  ({ goal := goal, priority := priority, lastExpandedInIteration := lastExpandedInIteration,
        addedInIteration := addedInIteration } =
      { goal := goal_1, priority := priority_1, lastExpandedInIteration := lastExpandedInIteration_1,
        addedInIteration := addedInIteration_1 }) =
    (goal = goal_1 ∧
      priority = priority_1 ∧
        lastExpandedInIteration = lastExpandedInIteration_1 ∧ addedInIteration = addedInIteration_1)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.mem_saturation_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid} {x : S}, x ∈ s.saturation M H ↔ ∃ m ∈ M, m • x ∈ s
-- Mathlib.GroupTheory.OrderOfElement
charP_of_prime_pow_injective : ∀ (R : Type u_6) [inst : Ring R] [inst_1 : Fintype R] (p n : ℕ) [hp : Fact (Nat.Prime p)],
  Fintype.card R = p ^ n → (∀ i ≤ n, ↑p ^ i = 0 → i = n) → CharP R (p ^ n)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- (Implementation). Given an iso between the pullbacks of two sheaves, we can whisker it with
`coyoneda` to obtain an iso between the pullbacks of the sheaves of maps from `X`.
 -/
CategoryTheory.Functor.IsCoverDense.isoOver : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {A : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
              {G : CategoryTheory.Functor C D} →
                {ℱ ℱ' : CategoryTheory.Sheaf K A} →
                  (G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) →
                    (X : A) →
                      G.op.comp (CategoryTheory.sheafOver ℱ X).obj ≅ G.op.comp (CategoryTheory.sheafOver ℱ' X).obj
-- Mathlib.Order.Basic
Pi.himp_apply : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → HImp (π i)] (x y : (i : ι) → π i) (i : ι), (y ⇨ x) i = y i ⇨ x i
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given a functor `A : C ⥤ ℰ` (with `Category.{v₂} ℰ`) and an auxiliary universe `w`,
this is the functor `ℰ ⥤ Cᵒᵖ ⥤ Type max w v₂` which sends `(E : ℰ) (c : Cᵒᵖ)`
to the homset `A.obj C ⟶ E` (considered in the higher universe `max w v₂`).
Under the existence of a suitable pointwise left Kan extension, it is shown in
`uliftYonedaAdjunction` that this functor has a left adjoint.

Defined as in [MM92], Chapter I, Section 5, Theorem 2.
 -/
CategoryTheory.Presheaf.restrictedULiftYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ℰ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ] →
        CategoryTheory.Functor C ℰ → CategoryTheory.Functor ℰ (CategoryTheory.Functor Cᵒᵖ (Type (max w v₂)))
-- Mathlib.Algebra.Group.Prod
AddEquiv.coe_prodAssoc : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P], ⇑AddEquiv.prodAssoc = ⇑(Equiv.prodAssoc M N P)
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.IsStronglyConnected.isSStronglyConnected_of_hom : ∀ {V : Type u_2} [inst : Quiver V],
  Quiver.IsStronglyConnected V → ∀ {i₀ j₀ : V} (e₀ : i₀ ⟶ j₀), Quiver.IsSStronglyConnected V
-- Mathlib.CategoryTheory.GradedObject.Braiding
/-- The braiding `tensorObj X Y ≅ tensorObj Y X` when `X` and `Y` are graded objects
indexed by a commutative additive monoid.  -/
CategoryTheory.GradedObject.Monoidal.braiding : {I : Type u_1} →
  [inst : AddCommMonoid I] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (X Y : CategoryTheory.GradedObject I C) →
            [CategoryTheory.BraidedCategory C] →
              [inst_4 : X.HasTensor Y] →
                [inst_5 : Y.HasTensor X] →
                  CategoryTheory.GradedObject.Monoidal.tensorObj X Y ≅
                    CategoryTheory.GradedObject.Monoidal.tensorObj Y X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.ofList.eq_1 : ∀ {α : Type u} {β : α → Type v} (l : List ((a : α) × β a)) (cmp : α → α → Ordering),
  Std.DTreeMap.ofList l cmp = { inner := Std.DTreeMap.Internal.Impl.ofList l, wf := ⋯ }
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- If `C` is a preadditive category and `X` is an augmented simplicial object
in `C` that has an extra degeneracy, then the augmentation on the alternating
face map complex of `X` is a homotopy equivalence.  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X : CategoryTheory.SimplicialObject.Augmented C} →
          X.ExtraDegeneracy →
            HomotopyEquiv
              (AlgebraicTopology.AlternatingFaceMapComplex.obj (CategoryTheory.SimplicialObject.Augmented.drop.obj X))
              ((ChainComplex.single₀ C).obj (CategoryTheory.SimplicialObject.Augmented.point.obj X))
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_orbit_iff : ∀ {γ : Type u_2} {α : Type u_3} [inst : SMul γ α] {a₁ a₂ : α}, a₂ ∈ MulAction.orbit γ a₁ ↔ ∃ x, x • a₁ = a₂
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.nerveEquiv_symm_apply_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : C) {X Y : Fin 1} (x : X ⟶ Y),
  (SSet.OneTruncation₂.nerveEquiv.symm f).map x = CategoryTheory.CategoryStruct.id f
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- For `A : Matrix V V α`, `A.compl` is supposed to be the adjacency matrix of
the complement graph of the graph induced by `A.adjMatrix`.  -/
Matrix.compl : {α : Type u_1} → {V : Type u_2} → [Zero α] → [One α] → [DecidableEq α] → [DecidableEq V] → Matrix V V α → Matrix V V α
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.smul_cons : ∀ {α : Type u_1} {M : Type u_2} {n : ℕ} [inst : SMul M α] (x : M) (y : α) (v : Fin n → α),
  x • Matrix.vecCons y v = Matrix.vecCons (x • y) (x • v)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.eq_right : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ t₃ t₄ : String}, p.Splits t₁ t₂ → p.Splits t₃ t₄ → t₂ = t₄
-- Init.Meta.Defs
Lean.TSyntax.Compat.instCoeTailArraySyntaxTSepArray : {k : Lean.SyntaxNodeKinds} → {sep : String} → CoeTail (Array Lean.Syntax) (Lean.Syntax.TSepArray k sep)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_tensorObj_comon_comul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Comon C),
  CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.mul.unop
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The product of two affine subspaces as an affine subspace.  -/
AffineSubspace.prod : {k : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module k V] →
                [inst_3 : AddTorsor V P] →
                  [inst_4 : AddCommGroup W] →
                    [inst_5 : Module k W] →
                      [inst_6 : AddTorsor W Q] → AffineSubspace k P → AffineSubspace k Q → AffineSubspace k (P × Q)
-- Init.Data.Iterators.Consumers.Loop
/-- Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldlM`.

This function is deprecated. Instead of `it.allowNontermination.foldM`, use `it.foldM`.
 -/
Std.Iter.Partial.foldM : {m : Type x → Type x'} →
  [Monad m] →
    {α β : Type w} →
      {γ : Type x} →
        [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → (γ → β → m γ) → γ → Std.Iter.Partial β → m γ
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality_assoc : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : CochainComplex C₁ ℤ} (f : X ⟶ Y)
  {Z : DerivedCategory C₂} (h : DerivedCategory.Q.obj ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map (DerivedCategory.Q.map f))
      (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app Y) h) =
    CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X)
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map f))
        h)
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_range : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  (M.mulMap N).range = M * N
-- Mathlib.Algebra.Category.MonCat.Basic
CategoryTheory.Iso.commMonCatIsoToMulEquiv.eq_1 : ∀ {X Y : CommMonCat} (i : X ≅ Y),
  i.commMonCatIsoToMulEquiv = (CommMonCat.Hom.hom i.hom).toMulEquiv (CommMonCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.toLp_inj : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  {𝕜 : Type u_3} [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E]
  {f g : C(α, E)} [μ.IsOpenPosMeasure], (ContinuousMap.toLp p μ 𝕜) f = (ContinuousMap.toLp p μ 𝕜) g ↔ f = g
-- Mathlib.Analysis.Complex.Exponential
/-- scoped notation for the real exponential function  -/
Real.termRexp : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_nonempty : ∀ {G : Type u_1} [inst : Group G] (s : Subgroup G), (↑s).Nonempty
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
/-- If a stochastic process `Y` is such that for each `s`, `Y s` can be written as a linear
combination of finitely many values of a Gaussian process, then `Y` is a Gaussian process.  -/
ProbabilityTheory.IsGaussianProcess.of_isGaussianProcess : ∀ {S : Type u_1} {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  {X : T → Ω → E} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E] {F : Type u_6} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  [inst_7 : MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] {Y : S → Ω → F},
  ProbabilityTheory.IsGaussianProcess X P →
    (∀ (s : S), ∃ I L, ∀ (ω : Ω), Y s ω = L (I.restrict fun x => X x ω)) → ProbabilityTheory.IsGaussianProcess Y P
-- Init.Data.UInt.Lemmas
Fin.mk_uInt32ToNat : ∀ (n : UInt32), ⟨n.toNat, ⋯⟩ = n.toFin
-- Mathlib.NumberTheory.NumberField.DedekindZeta
/-- The Dedekind zeta function of a number field. It is defined as the `L`-series with coefficients
the number of integral ideals of norm `n`.
 -/
NumberField.dedekindZeta : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℂ → ℂ
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_nsmul : ∀ (x : ℂ) (n : ℕ), Complex.exp (n • x) = Complex.exp x ^ n
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isMatch_iff_slice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat pos ↔ String.Slice.Pattern.Model.IsMatch pat.toSlice pos
-- Mathlib.Topology.Category.CompHausLike.Cartesian
/-- Explicit binary fan in `CompHausLike P`, given that the predicate `P` is preserved under taking
type-theoretic products.
 -/
CompHausLike.productCone : {P : TopCat → Prop} →
  (X Y : CompHausLike P) → [CompHausLike.HasProp P (↑X.toTop × ↑Y.toTop)] → CategoryTheory.Limits.BinaryFan X Y
-- Mathlib.GroupTheory.Index
Subgroup.card_dvd_of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G'),
  Function.Surjective ⇑f → Nat.card G' ∣ Nat.card G
-- Mathlib.Order.SemiconjSup
/-- Consider two actions `f₁ f₂ : G → α → α` of a group on a complete lattice by order
isomorphisms. Then the map `x ↦ ⨆ g : G, (f₁ g)⁻¹ (f₂ g x)` semiconjugates each `f₁ g'` to `f₂ g'`.

This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homéomorphismes du cercle et
cohomologie bornée][ghys87:groupes].  -/
Function.sSup_div_semiconj : ∀ {α : Type u_1} {G : Type u_4} [inst : CompleteLattice α] [inst_1 : Group G] (f₁ f₂ : G →* α ≃o α) (g : G),
  Function.Semiconj (fun x => ⨆ g', (f₁ g')⁻¹ ((f₂ g') x)) ⇑(f₂ g) ⇑(f₁ g)
-- Mathlib.RingTheory.Trace.Quotient
_private.Mathlib.RingTheory.Trace.Quotient.0.termPS_1 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
CategoryTheory.Enriched.HasConicalLimit.mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {V : outParam (Type u')}
  [inst_1 : CategoryTheory.Category.{v', u'} V] [inst_2 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_3 : CategoryTheory.Category.{v, u} C] [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C]
  {F : CategoryTheory.Functor J C} [toHasLimit : CategoryTheory.Limits.HasLimit F],
  autoParam (∀ (X : C), CategoryTheory.Limits.PreservesLimit F (CategoryTheory.eCoyoneda V X))
      CategoryTheory.Enriched.HasConicalLimit.preservesLimit_eCoyoneda._autoParam →
    CategoryTheory.Enriched.HasConicalLimit V F