mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_inv_app_hom_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F X : CategoryTheory.Functor C V)
  (a :
    (CategoryTheory.coyoneda.obj
          (Opposite.op
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V), F).2)).obj
      X)
  (X_1 : CategoryTheory.Discrete PUnit.{1} × C),
  ((CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso F).inv.app X))
          a).app
      X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X_1.2)).hom
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.prod.leftUnitorEquivalence C).unit.app X_1).2)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X_1.2)).inv
          (CategoryTheory.CategoryStruct.comp
            (((CategoryTheory.CategoryStruct.id
                      ((CategoryTheory.prod.leftInverseUnitor C).comp
                          (CategoryTheory.MonoidalCategory.externalProduct
                            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)) F) ⟶
                        (CategoryTheory.prod.leftInverseUnitor C).comp
                          (((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).prod
                                (CategoryTheory.Functor.id C)).comp
                            ((CategoryTheory.MonoidalCategory.tensor C).comp X)))).hom'
                  ((TypeCat.ofHom fun g =>
                        CategoryTheory.CategoryStruct.comp g
                          (((CategoryTheory.Functor.whiskeringLeft C C V).map
                                (CategoryTheory.NatIso.ofComponents
                                    (fun x => CategoryTheory.MonoidalCategoryStruct.leftUnitor x) ⋯).inv).app
                            X)).hom'
                    ((TypeCat.ofHom fun g =>
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.NatIso.ofComponents
                                (fun x => (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj x)).symm) ⋯).inv
                            g).hom'
                      a))).app
              X_1.2)
            (CategoryTheory.CategoryStruct.comp (X.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X_1.2).hom)
              (CategoryTheory.CategoryStruct.comp
                (X.map ((CategoryTheory.prod.leftUnitorEquivalence C).unitInv.app X_1).2)
                (X.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X_1.2).inv))))))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → (↑m).toArray.size = (↑m).size
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.forgetToPresheafModuleCat_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ)
  (hX : CategoryTheory.Limits.IsInitial X) {X_1 Y : PresheafOfModules R} (f : X_1 ⟶ Y),
  (PresheafOfModules.forgetToPresheafModuleCat X hX).map f = PresheafOfModules.forgetToPresheafModuleCatMap X hX f
-- ProofWidgets.Component.MakeEditLink
/-- Replace `range` with `newText`.
If `newSelection?` is absent, place the cursor at the end of the new text.
If `newSelection?` is present, select the range it specifies within `newText`.
See also `MakeEditLinkProps.ofReplaceRange'`.  -/
ProofWidgets.MakeEditLinkProps.ofReplaceRange : Lean.Server.DocumentMeta →
  Lean.Lsp.Range → String → optParam (Option (String.Pos.Raw × String.Pos.Raw)) none → ProofWidgets.MakeEditLinkProps
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.operating.sizeOf_spec : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToForwardSearcher pat σ] [inst_1 : (a : String.Slice) → SizeOf (σ a)] [inst_2 : SizeOf ρ]
  (currPos : s.Pos) (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)),
  sizeOf (String.Slice.SplitInclusiveIterator.operating currPos searcher) = 1 + sizeOf currPos + sizeOf searcher
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
BoundedContinuousFunction.instCommCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : CommCStarAlgebra A] → CommCStarAlgebra (BoundedContinuousFunction α A)
-- Mathlib.Data.Nat.Find
_private.Mathlib.Data.Nat.Find.0.Nat.lbp : {p : ℕ → Prop} → ℕ → ℕ → Prop
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasCondSubgaussianMGF m hm X c μ →
    ∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] F),
  ContinuousLinearMap.rTensor G (-f) = -ContinuousLinearMap.rTensor G f
-- Mathlib.RingTheory.Jacobson.Radical
Module.le_comap_jacobson : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), Module.jacobson R M ≤ Submodule.comap f (Module.jacobson R₂ M₂)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} (x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat)
  (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
  HomogeneousLocalization.mk z ∈
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base) x).asIdeal ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β},
  (Std.ExtHashMap.filter f m).getD k fallback = (m[k]?.pfilter fun x_2 h' => f (m.getKey k ⋯) x_2).getD fallback
-- Init.Data.SInt.Lemmas
Int32.add_zero : ∀ (a : Int32), a + 0 = a
-- Mathlib.Control.LawfulFix
/-- `toUnit` as a monotone function  -/
Part.toUnitMono : {α : Type u_1} → (Part α →o Part α) → (Unit → Part α) →o Unit → Part α
-- Mathlib.Analysis.InnerProductSpace.Basic
isNonneg_inner : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E], (innerₗ E).IsNonneg
-- Mathlib.Analysis.Polynomial.Basic
/-- **Alias** of `Polynomial.div_tendsto_atTop_zero_iff_degree_lt`. -/
Polynomial.div_tendsto_zero_iff_degree_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q ≠ 0 →
    (Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (nhds 0) ↔ P.degree < Q.degree)
-- Mathlib.Combinatorics.Quiver.Schreier
/-- A Schreier graph for a monoid `M` acting on `V` with generators `ι : S → M`.
Vertices are elements of `V`, and there is an edge from `x` to `y` for each `s : S`
such that `ι s • x = y`.  -/
Quiver.SchreierGraph : (V : Type u_1) → {M : Type u_2} → [SMul M V] → {S : Type u_3} → (S → M) → Type u_1
-- Mathlib.Algebra.Group.TypeTags.Basic
toAdd_eq_zero : ∀ {α : Type u_1} [inst : Zero α] {x : Multiplicative α}, Multiplicative.toAdd x = 0 ↔ x = 1
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsQuasiInverse.equiv_of_right : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃},
  u.IsQuasiInverse v → u'.IsQuasiInverse v' → v ≈ v' → u ≈ u'
-- Std.Http.Protocol.H1
/-- Dispatches body parsing according to current reader body-framing sub-state.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.parseBody : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    Std.Http.Protocol.H1.Reader.BodyState →
      Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Mathlib.Data.NNRat.Defs
NNRat.coe_add : ∀ (p q : ℚ≥0), ↑(p + q) = ↑p + ↑q
-- Init.Data.SInt.Lemmas
Int32.ofNat_div : ∀ {a b : ℕ}, a < 2 ^ 31 → b < 2 ^ 31 → Int32.ofNat (a / b) = Int32.ofNat a / Int32.ofNat b
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.hom_eq_iff_not_disjoint : ∀ {V : Type u} {G : SimpleGraph V} {K L : Set V} (C : G.ComponentCompl L) (h : K ⊆ L) (D : G.ComponentCompl K),
  SimpleGraph.ComponentCompl.hom h C = D ↔ ¬Disjoint ↑C ↑D
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- the component maps satisfy `P`  -/
AlgebraicGeometry.Scheme.AffineCover.map_prop : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (self : AlgebraicGeometry.Scheme.AffineCover P S) (j : self.I₀), P (self.f j)
-- Mathlib.Tactic.Linarith.Verification
/-- If `prf` is a proof of `t R s`, `typeOfIneqProof prf` returns the type of `t`.  -/
Mathlib.Tactic.Linarith.typeOfIneqProof : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioo_of_Ioc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α},
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ioc (a i) (b i)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- An extensionality for measures. It is `ext_of_generateFrom_of_iUnion` formulated in terms of
`FiniteSpanningSetsIn`.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.ext : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {C : Set (Set α)},
  m0 = MeasurableSpace.generateFrom C → IsPiSystem C → ∀ (h : μ.FiniteSpanningSetsIn C), (∀ s ∈ C, μ s = ν s) → μ = ν
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.traj_map_frestrictLe_apply : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a b : ℕ) (x : (i : ↥(Finset.Iic a)) → X ↑i),
  MeasureTheory.Measure.map (Preorder.frestrictLe b) ((ProbabilityTheory.Kernel.traj κ a) x) =
    (ProbabilityTheory.Kernel.partialTraj κ a b) x
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.ofMeasurable_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} {m0 : m ∅ ⋯ = 0}
  {mU :
    ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
      Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯}
  (s : Set α) (hs : MeasurableSet s), (MeasureTheory.Measure.ofMeasurable m m0 mU) s = m s hs
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.emptyOn_dual_eq : ∀ {α : Type u_1}, (Matroid.emptyOn α)✶ = Matroid.emptyOn α
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.of.sizeOf_spec : ∀ (η : Mathlib.Tactic.BicategoryLike.AtomIso), sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η) = 1 + sizeOf η
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instFunLikeSubtypeMemSubsemiringCenter : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → FunLike (↥(Subsemiring.center (CentroidHom α))) α α
-- Mathlib.Order.WithBot
WithTop.untopA_lt_iff : ∀ {α : Type u_1} {a : α} [inst : LT α] {x : WithTop α} [inst_1 : Nonempty α], x ≠ ⊤ → (x.untopA < a ↔ x < ↑a)
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.equivalenceJ_functor : ∀ {C₁ : Type u₁} {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₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), (w.equivalenceJ g).functor = CategoryTheory.TwoSquare.EquivalenceJ.functor w g
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.splitter : {β β' : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → Std.Iterators.PostconditionT n (Option β')} →
      (out : β) →
        (motive : Subtype (f out).Property → Sort u_3) →
          (__do_lift : Subtype (f out).Property) →
            ((h' : (f out).Property none) → motive ⟨none, h'⟩) →
              ((out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩) → motive __do_lift
-- Mathlib.RingTheory.Finiteness.Projective
Module.Finite.exists_comp_eq_id_of_projective : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Finite R M]
  [Module.Projective R M], ∃ n f g, Function.Surjective ⇑f ∧ Function.Injective ⇑g ∧ f ∘ₗ g = LinearMap.id
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.zero_div_nonneg : ∀ {α : Type u_2} [inst : GroupWithZero α] {g : Filter α}, g.NeBot → 0 ≤ 0 / g
-- Mathlib.Data.Rat.Denumerable
/-- **Denumerability of the Rational Numbers**  -/
Rat.instDenumerable : Denumerable ℚ
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopCat.Sheaf.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X}
  (F : TopCat.Presheaf C X) (F' : TopCat.Sheaf C X),
  TopologicalSpace.Opens.IsBasis (Set.range B) →
    ∀ {α β : F ⟶ F'.obj}, (∀ (i : ι), α.app (Opposite.op (B i)) = β.app (Opposite.op (B i))) → α = β
-- Init.Data.Array.Lemmas
Array.toListRev_eq : ∀ {α : Type u_1} {xs : Array α}, xs.toListRev = xs.toList.reverse
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_inf_eq_map_inf_comap : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {p' : Submodule R₂ M₂},
  Submodule.map f p ⊓ p' = Submodule.map f (p ⊓ Submodule.comap f p')
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the year to the given `year` value. The month and day
remain unchanged, with any out-of-range days clipped to the nearest valid date.
 -/
Std.Time.PlainDateTime.withYearClip : Std.Time.PlainDateTime → Std.Time.Year.Offset → Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ D₃ : F.DescentDataAsCoalgebra f} (φ : D₁ ⟶ D₂)
  (φ' : D₂ ⟶ D₃) (i : ι),
  (CategoryTheory.CategoryStruct.comp φ φ').hom i = CategoryTheory.CategoryStruct.comp (φ.hom i) (φ'.hom i)
-- Mathlib.Data.List.Sort
List.sortedGE_iff_antitone_get : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGE ↔ Antitone l.get
-- Mathlib.Order.SetDissipate
/-- `dissipate s` is the intersection of `s y` for `y ≤ x`.  -/
Set.dissipate : {α : Type u_1} → {β : Type u_2} → [LE α] → (α → Set β) → α → Set β
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.fst_map₂ : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  {f g : a ⟶ b} (a_1 : f ⟶ g), (CategoryTheory.Bicategory.Prod.fst B C).map₂ a_1 = a_1.1
-- Mathlib.Topology.Separation.Basic
Finite.instDiscreteTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] [Finite X], DiscreteTopology X
-- Mathlib.Data.List.Rotate
List.IsRotated.eq_1 : ∀ {α : Type u} (l l' : List α), (l ~r l') = ∃ n, l.rotate n = l'
-- Mathlib.Computability.Primrec.List
/-- `List.modify` by a primitive recursive function is primitive recursive.  -/
Primrec.list_modify : ∀ {α : Type u_1} [inst : Primcodable α] {f : α → α}, Primrec f → Primrec₂ fun l n => l.modify n f
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- Make a term of `Meq P S`.  -/
CategoryTheory.Meq.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                  {X : C} →
                    {P : CategoryTheory.Functor Cᵒᵖ D} →
                      (S : J.Cover X) → CategoryTheory.ToType (P.obj (Opposite.op X)) → CategoryTheory.Meq P S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_le_size_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.size ≤ (t.erase k).size + 1
-- Init.Control.Lawful.Basic
seqRight_pure_unit : ∀ {f : Type → Type u_1} [inst : Applicative f] [LawfulApplicative f] (x : f Unit), x *> pure () = x
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_empty : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (f : α → β) (h : (↑∅).Pairwise (Function.onFun Commute f)),
  ∅.noncommProd f h = 1
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- The convolution of a Gaussian measure `μ` and its map by `x ↦ -x` is centered.  -/
ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [SecondCountableTopology E] (L : StrongDual ℝ E),
  ∫ (x : E), L x ∂μ.conv (MeasureTheory.Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) = 0
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkFunIndStx : Lean.NameSet → Lean.Expr → Lean.TSyntax `tactic → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- Define the nontrivial quadratic character on `ZMod 4`, `χ₄`.
It corresponds to the extension `ℚ(√-1)/ℚ`.  -/
ZMod.χ₄ : MulChar (ZMod 4) ℤ
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.toPercent? : Aesop.Frontend.Priority → Option Aesop.Percent
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = false → Std.Internal.List.insertEntry k v l = ⟨k, v⟩ :: l
-- Lean.Elab.Do.Basic
/-- Restores the local context to `oldCtx` and adds the new reaching definitions of the mut vars and
result. Then resume the continuation `k` with the `mutVars` restored to the given `oldMutVars`.

This function is useful to de-nest
```
let mut x := 0
let y := 3
let z ← do
  let mut y ← e
  x := y + 1
  pure y
let y := y + 3
pure (x + y + z)
```
into
```
let mut x := 0
let y := 3
let mut y† ← e
x := y† + 1
let z ← pure y†
let y := y + 3
pure (x + y + z)
```
Note that the continuation of the `let z ← ...` bind, roughly
``k := .cont `z _ `(let y := y + 3; pure (x + y + z))``,
needs to be elaborated in a local context that contains the reassignment of `x`, but not the shadowing
mut var definition of `y`.
 -/
Lean.Elab.Do.withLCtxKeepingMutVarDefs : {α : Type} → Lean.LocalContext → Lean.Elab.Do.Context → Lean.Name → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Compose a `MulActionWithZero` with a `MonoidWithZeroHom`, with action `f r' • m`  -/
MulActionWithZero.compHom : {M₀ : Type u_2} →
  {M₀' : Type u_3} →
    (A : Type u_7) →
      [inst : MonoidWithZero M₀] →
        [inst_1 : MonoidWithZero M₀'] →
          [inst_2 : Zero A] → [MulActionWithZero M₀ A] → (M₀' →*₀ M₀) → MulActionWithZero M₀' A
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.instHasCoproduct : ∀ {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X],
  CategoryTheory.Limits.HasCoproduct X
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sum_sum : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [inst : Fintype ι] {ι' : Type u_3} [inst_1 : Fintype ι'] {Y : ι' → Ω → ℝ},
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    (∀ (i : ι'), MeasureTheory.MemLp (Y i) 2 μ) →
      ProbabilityTheory.covariance (∑ i, X i) (∑ j, Y j) μ = ∑ i, ∑ j, ProbabilityTheory.covariance (X i) (Y j) μ
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOpEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.coconeOpEquiv =
    CategoryTheory.Equivalence.mk''
      { obj := fun c => (Opposite.unop c).op, map := fun {Y X} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun c => Opposite.op c.unop, map := fun {Y X} f => Opposite.op { hom := f.hom.unop, w := ⋯ },
        map_id := ⋯, map_comp := ⋯ }
      (CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ))
      (CategoryTheory.Iso.refl
        ({ obj := fun c => Opposite.op c.unop, map := fun {Y X} f => Opposite.op { hom := f.hom.unop, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }.comp
          { obj := fun c => (Opposite.unop c).op, map := fun {Y X} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ }))
      ⋯
-- Mathlib.Algebra.Group.TypeTags.Basic
isLeftRegular_toMul : ∀ {α : Type u} [inst : Monoid α] {a : Additive α}, IsLeftRegular (Additive.toMul a) ↔ IsAddLeftRegular a
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_cot_ofReal_re : ∀ (x : ℝ), ↑(↑x).cot.re = (↑x).cot
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a k : α}
  {v : β k}, (m.insert k v).get? a = if h : (k == a) = true then some (cast ⋯ v) else m.get? a
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.prod.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (w : Monoid.PushoutI.NormalWord d),
  w.prod = (Monoid.PushoutI.base φ) w.head * Monoid.PushoutI.ofCoprodI w.prod
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_surjective : ∀ {R : Type u} {M : Type v} [Nonempty M], Function.Surjective TrivSqZeroExt.fst