mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.of_and : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop}
  [inst_1 : OrderBot ι] [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E],
  ProbabilityTheory.Locally (fun Y => p Y ∧ q Y) 𝓕 X P →
    ProbabilityTheory.Locally p 𝓕 X P ∧ ProbabilityTheory.Locally q 𝓕 X P
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.pow : ∀ {𝕜 : 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] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'}, MDiffAt[s] p z → ∀ (n : ℕ), MDiffAt[s] (p ^ n) z
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.sdiff : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsLowerSet s → (∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) → IsLowerSet (s \ t)
-- Mathlib.Data.Sigma.Basic
PSigma.mk.inj_iff : ∀ {α : Sort u_1} {β : α → Sort u_2} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}, ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ b₁ ≍ b₂
-- Mathlib.Topology.Sheaves.Flasque
TopCat.Sheaf.IsFlasque.pushforward_isFlasque : ∀ {X : TopCat} {C : Type v} [inst : CategoryTheory.Category.{w, v} C] {Y : TopCat} (F : TopCat.Sheaf C X) [F.IsFlasque]
  (f : X ⟶ Y), ((TopCat.Sheaf.pushforward C f).obj F).IsFlasque
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftByIsoClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a : A) [P.IsStableUnderShiftBy a],
  P.isoClosure.IsStableUnderShiftBy a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_iff_toList_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp},
  t₁.Equiv t₂ ↔ (Std.DTreeMap.Const.toList t₁).Perm (Std.DTreeMap.Const.toList t₂)
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.property : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsImmersionAtOfComplement F I J n f x →
    Manifold.LiftSourceTargetPropertyAt I J n f x (Manifold.ImmersionAtProp F I J M N)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
WfDvdMonoid.not_isUnit_iff_exists_factors_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] (a : α),
  a ≠ 0 → (¬IsUnit a ↔ ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.instSetLike : {V : Type u} → {G : SimpleGraph V} → SetLike G.ConnectedComponent V
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  {x x' : ↑(X.presheaf.obj (Opposite.op ⊤))} {t t' : A} {d d' : ℕ} {H : f t = x} {h0d : 0 < d} {hd : t ∈ 𝒜 d}
  {H' : f t' = x'} {h0d' : 0 < d'} {hd' : t' ∈ 𝒜 d'} {s : A} (hts : t * s = t') {n : ℕ} (hn : d + n = d'),
  s ∈ 𝒜 n →
    ∀ {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj 𝒜 ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯)
          (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f H h0d hd)
            (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen 𝒜 t).ι h)) =
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f H' h0d' hd')
          (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen 𝒜 t').ι h)
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_diagonal : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroClass α] (M : Matrix n n α) (w : n → α),
  M.hadamard (Matrix.diagonal w) = Matrix.diagonal (M.diag * w)
-- Mathlib.Topology.MetricSpace.Gluing
/-- The left injection of a space in a disjoint union is an isometry  -/
Metric.isometry_inl : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y], Isometry Sum.inl
-- Mathlib.Algebra.GroupWithZero.Action.Prod
Prod.mulActionWithZero : {M : Type u_1} →
  {N : Type u_2} →
    {R : Type u_5} →
      [inst : MonoidWithZero R] →
        [inst_1 : Zero M] →
          [inst_2 : Zero N] → [MulActionWithZero R M] → [MulActionWithZero R N] → MulActionWithZero R (M × N)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero F.leftDerivedZeroIsoSelf.inv =
    CategoryTheory.CategoryStruct.id (F.leftDerived 0)
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function between
finite sets `s` and `t` and a number `b` such that `#t • b ≤ #s`, there exists `y ∈ t` such
that its preimage in `s` has at least `b` elements.
See also `Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to` for a stronger statement.  -/
Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
  [inst_1 : CommSemiring M] [inst_2 : LinearOrder M] [IsStrictOrderedRing M],
  (∀ a ∈ s, f a ∈ t) → t.Nonempty → t.card • b ≤ ↑s.card → ∃ y ∈ t, b ≤ ↑{x ∈ s | f x = y}.card
-- Mathlib.Topology.Constructions.SumProd
/-- `(X ⊕ Y) ⊕ Z` is homeomorphic to `X ⊕ (Y ⊕ Z)`.  -/
Homeomorph.sumAssoc : (X : Type u) →
  (Y : Type v) →
    (Z : Type u_2) →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : TopologicalSpace Z] → (X ⊕ Y) ⊕ Z ≃ₜ X ⊕ Y ⊕ Z
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_sInf : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Set (Subring R)), (sInf S).op = sInf (Subring.unop ⁻¹' S)
-- Mathlib.Analysis.Normed.Group.Real
norm_norm' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (x : E), ‖‖x‖‖ = ‖x‖
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ Y₁ : C}
  (φ : X₁ ⟶ Y₁) (X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' C).map φ).app X₂).app X₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₂)
          X₃)
        (CategoryTheory.MonoidalCategoryStruct.associator Y₁ X₂ X₃).hom)
-- Std.Time.Date.Basic
/-- Convert `Day.Offset` into `Second.Offset`.
 -/
Std.Time.Second.Offset.ofDays : Std.Time.Day.Offset → Std.Time.Second.Offset
-- Mathlib.Topology.Compactness.Lindelof
Subsingleton.lindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [Subsingleton X], LindelofSpace X
-- Mathlib.FieldTheory.KummerExtension
autEquivRootsOfUnity_apply_rootOfSplit : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] [inst_4 : NeZero n] (σ : Gal(L/K)),
  σ (rootOfSplitsXPowSubC ⋯ a L) = (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.index_le_of_leftCoset_cover_const : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ι → G},
  ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ → H.index ≤ s.card
-- Mathlib.Order.Filter.Basic
Filter.generate_univ : ∀ {α : Type u}, Filter.generate Set.univ = ⊥
-- Mathlib.Data.Set.Semiring
SetSemiring.down_mul : ∀ {α : Type u_1} [inst : Mul α] (s t : SetSemiring α),
  SetSemiring.down (s * t) = SetSemiring.down s * SetSemiring.down t
-- Mathlib.Data.List.Basic
List.flatMap_congr : ∀ {α : Type u} {β : Type v} {l : List α} {f g : α → List β}, (∀ x ∈ l, f x = g x) → List.flatMap f l = List.flatMap g l
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.Balanced.depth_le : ∀ {α : Type u_1} {t : RBTree.RBNode α} {c : RBTree.RBColor} {n : ℕ},
  t.Balanced c n → t.depth ≤ RBTree.RBNode.depthUB c n
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey!_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β},
      (Std.Internal.List.Const.modifyKey k f l).isEmpty = false →
        Std.Internal.List.maxKey! (Std.Internal.List.Const.modifyKey k f l) =
          if (Std.Internal.List.maxKey! l == k) = true then k else Std.Internal.List.maxKey! l
-- Mathlib.CategoryTheory.Galois.Topology
/-- If `H` is an open subset of `Aut F` such that `1 ∈ H`, there exists a finite
set `I` of connected objects of `C` such that every `σ : Aut F` that induces the identity
on `F.obj X` for all `X ∈ I` is contained in `H`. In other words: The kernel
of the evaluation map `Aut F →* ∏ X : I ↦ Aut (F.obj X)` is contained in `H`.
 -/
CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  {H : Set (CategoryTheory.Aut F)},
  1 ∈ H →
    IsOpen H →
      ∃ I x,
        (∀ X ∈ I, CategoryTheory.PreGaloisCategory.IsConnected X) ∧
          ∀ (σ : CategoryTheory.Aut F), (∀ (X : ↑I), σ.hom.app ↑X = CategoryTheory.CategoryStruct.id (F.obj ↑X)) → σ ∈ H
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instCofibrationI₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_4 : CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood],
  HomotopicalAlgebra.Cofibration P.i₀
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Strand.mk.injEq : ∀ (hPos : ℕ) (startPoint endPoint : Mathlib.Tactic.Widget.StringDiagram.Node)
  (atom₁ : Mathlib.Tactic.BicategoryLike.Atom₁) (hPos_1 : ℕ)
  (startPoint_1 endPoint_1 : Mathlib.Tactic.Widget.StringDiagram.Node) (atom₁_1 : Mathlib.Tactic.BicategoryLike.Atom₁),
  ({ hPos := hPos, startPoint := startPoint, endPoint := endPoint, atom₁ := atom₁ } =
      { hPos := hPos_1, startPoint := startPoint_1, endPoint := endPoint_1, atom₁ := atom₁_1 }) =
    (hPos = hPos_1 ∧ startPoint = startPoint_1 ∧ endPoint = endPoint_1 ∧ atom₁ = atom₁_1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndProj_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (b : B) {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b}
  (f : X ⟶ Y),
  (CategoryTheory.Comma.costructuredArrowSndProj L R b).map f = CategoryTheory.CostructuredArrow.homMk f.left.left ⋯
-- Mathlib.Analysis.Seminorm
Seminorm.comp_id : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E), p.comp LinearMap.id = p
-- Lean.Meta.Tactic.Refl
/-- Try to apply `heq_of_eq`. If successful, then return new goal, otherwise return `mvarId`.
 -/
Lean.MVarId.heqOfEq : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α},
  (Std.DTreeMap.Const.insertManyIfNewUnit t l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.RingTheory.Etale.QuasiFinite
IsLocalization.Away.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (S : Type u_4) [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsLocalization.Away x S = IsLocalization (Submonoid.powers x) S
-- Mathlib.CategoryTheory.Functor.Flat
/-- A functor `F : C ⥤ D` is representably flat if the comma category `(X/F)` is cofiltered for
each `X : D`.
 -/
CategoryTheory.RepresentablyFlat : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Init.Data.String.Lemmas.Splits
String.Pos.sliceTo_cast : ∀ {s t : String} {hst : s = t} (p q : s.Pos) {h : q.cast hst ≤ p.cast hst},
  (p.cast hst).sliceTo (q.cast hst) h = (p.sliceTo q ⋯).cast ⋯
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_iso_inv_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : (CategoryTheory.CatCenter C)ˣ) {X Y : C} (f : X ≅ Y),
  (z • f).inv = CategoryTheory.CategoryStruct.comp f.inv ((↑z⁻¹).app X)
-- Lean.Parser.Basic
Lean.Parser.ParserCategory.mk.inj : ∀ {declName : Lean.Name} {kinds : Lean.Parser.SyntaxNodeKindSet} {tables : Lean.Parser.PrattParsingTables}
  {behavior : Lean.Parser.LeadingIdentBehavior} {declName_1 : Lean.Name} {kinds_1 : Lean.Parser.SyntaxNodeKindSet}
  {tables_1 : Lean.Parser.PrattParsingTables} {behavior_1 : Lean.Parser.LeadingIdentBehavior},
  { declName := declName, kinds := kinds, tables := tables, behavior := behavior } =
      { declName := declName_1, kinds := kinds_1, tables := tables_1, behavior := behavior_1 } →
    declName = declName_1 ∧ kinds = kinds_1 ∧ tables = tables_1 ∧ behavior = behavior_1
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.aux.congr_simp : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (g g_1 : L ≃+* L),
  g = g_1 →
    ∀ (n n_1 : ℕ) (e_n : n = n_1) [inst_2 : NeZero n],
      modularCyclotomicCharacter.aux g n = modularCyclotomicCharacter.aux g_1 n_1
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.stoppedProcess_localSeq : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop}
  [inst_1 : OrderBot ι] [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E]
  (hX : ProbabilityTheory.Locally p 𝓕 X P) (n : ℕ),
  p (MeasureTheory.stoppedProcess (fun i => {ω | ⊥ < hX.localSeq n ω}.indicator (X i)) (hX.localSeq n))
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.nonUnitalSubsemiringClass : ∀ (S : Type u_1) (R : Type u) [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [SubsemiringClass S R],
  NonUnitalSubsemiringClass S R
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierTensorLeft : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (F : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))),
  CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u_1, max u u_1, max (max (u + 1) u_1) v_1,
      max (max (u + 1) u_1) v_1}
    (CategoryTheory.MonoidalCategory.tensorLeft F)
-- Std.Data.ExtHashMap.Basic
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.ExtHashMap.ofList : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → List (α × β) → Std.ExtHashMap α β
-- Mathlib.Data.List.MinMax
List.minimum_ne_top_of_ne_nil : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α}, l ≠ [] → l.minimum ≠ ⊤
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monadMonEquiv_inverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.Monad.monadMonEquiv C).inverse = CategoryTheory.Monad.monToMonad C
-- Mathlib.Topology.Order.OrderClosed
disjoint_nhds_atBot : ∀ {α : Type u} [inst : Preorder α] [NoBotOrder α] [inst_2 : TopologicalSpace α] [ClosedIicTopology α] (a : α),
  Disjoint (nhds a) Filter.atBot
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.mk : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    (toSlashInvariantForm : SlashInvariantForm Γ k) →
      MDiff ⇑toSlashInvariantForm →
        (∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm.toFun k) → CuspForm Γ k
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.ofWithBot_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {boxes : Finset (WithBot (BoxIntegral.Box ι))}
  {le_of_mem : ∀ J ∈ boxes, J ≤ ↑I} {pairwise_disjoint : (↑boxes).Pairwise Disjoint},
  (∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J') → BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_isSome_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = (Std.Internal.List.getEntry? a l).isSome
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β},
  s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSymbolInformation.fromJson : Lean.Json → Except String Lean.Lsp.SymbolInformation
-- Lean.Data.Json.Parser
Lean.Json.Parser.natNonZero : Std.Internal.Parsec.String.Parser ℕ
-- Init.PropLemmas
exists_prop_eq : ∀ {α : Sort u_1} {a' : α} {p : (a : α) → a = a' → Prop}, (∃ a, ∃ (h : a = a'), p a h) ↔ p a' ⋯
-- Mathlib.Order.Filter.AtTopBot.Archimedean
tendsto_ratCast_atBot_iff : ∀ {α : Type u_1} {R : Type u_2} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R]
  {f : α → ℚ} {l : Filter α}, Filter.Tendsto (fun n => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.indexEquiv_mul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (x y : P.Hom P),
  ⇑(x * y).indexEquiv = ⇑x.indexEquiv ∘ ⇑y.indexEquiv
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side, version subtracting vectors.  -/
Orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).sin * ‖x - y‖ = ‖y‖
-- Std.Http.Data.Response
/-- The HTTP status for the response.
 -/
Std.Http.Response.Head.status : Std.Http.Response.Head → Std.Http.Status
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_eraseIdx_of_le : ∀ {α : Type u} {a : α} {i j : ℕ} {as : List α},
  i < as.length → j ≤ i → (as.eraseIdx i).insertIdx j a = (as.insertIdx j a).eraseIdx (i + 1)
-- Mathlib.Data.Nat.Factorization.Basic
/-- **Alias** of `Nat.setOfPred_pow_dvd_eq_Icc_factorization`. -/
Nat.setOf_pow_dvd_eq_Icc_factorization : ∀ {n p : ℕ}, Nat.Prime p → n ≠ 0 → {i | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p)
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.toRat.match_1.splitter : (motive : Dyadic → Sort u_1) →
  (x : Dyadic) →
    (Unit → motive Dyadic.zero) →
      ((n : ℤ) → (k : ℕ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n (Int.ofNat k) hn)) →
        ((n : ℤ) → (k : ℕ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n (Int.negSucc k) hn)) → motive x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ext_mem_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {t₁ t₂ : Std.ExtTreeSet α cmp},
  t₁ = t₂ ↔ ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromyFunctor_obj : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) (x : FundamentalGroupoid X), cov.monodromyFunctor.obj x = ↑(p ⁻¹' {x.as})
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.inf_sup_assoc_of_le_of_neg_le : ∀ {R : Type u_8} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Submodule R M}
  (t : Submodule R M) {p : Submodule R M}, p ≤ s → -p ≤ s → s ⊓ t ⊔ p = s ⊓ (t ⊔ p)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.zero_ndinter : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), Multiset.ndinter 0 s = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtensionId : ∀ {C : Type u_1} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] (F₀ : CategoryTheory.Functor C H),
  F₀.IsRightKanExtension F₀.leftUnitor.hom
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The congruence relation defined by the kernel of a group homomorphism is equal to its kernel
as a congruence relation.
 -/
QuotientGroup.con_ker_eq_conKer : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (f : G →* M), QuotientGroup.con f.ker = Con.ker f
-- Mathlib.Order.SuccPred.Basic
Order.Icc_succ_left_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax a → Set.Icc (Order.succ a) b = Set.Ioc a b
-- Mathlib.LinearAlgebra.Orientation
/-- A type class fixing an orientation of a module.  -/
Module.Oriented : (R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [IsStrictOrderedRing R] →
        (M : Type u_2) → [inst_3 : AddCommMonoid M] → [Module R M] → Type u_4 → Type (max (max u_1 u_2) u_4)
-- Mathlib.Data.List.Chain
/-- If `r` is well-founded, the lexicographic order on `r`-decreasing chains is also.  -/
WellFounded.list_chain' : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → WellFounded (List.lex_chains r)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat.toSlice pos₁ pos₂
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.le_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [inst_2 : SeparatelyContinuousMul M]
  (s : Subsemigroup M), s ≤ s.topologicalClosure
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_lt_succ_iff : ∀ {n : ℕ} {a b : Fin n}, a.castSucc < b.succ ↔ a ≤ b