mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.sMulCommClass_mk : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : CommRing S] (f : R →+* S) (M : Type v) [I : AddCommGroup M]
  [inst_2 : Module S M], SMulCommClass R S M
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.centralMoment_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {p : ℕ} {μ : MeasureTheory.Measure Ω},
  p ≠ 0 → ProbabilityTheory.centralMoment 0 p μ = 0
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.existsUnique : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M}, ∃! k, IsPrimitiveRoot ζ k
-- Mathlib.NumberTheory.Height.MvPolynomial
AbsoluteValue.iSup_abv_linearMap_apply_le : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_2} {ι' : Type u_3} [inst_1 : Fintype ι] [Finite ι']
  (v : AbsoluteValue K ℝ) (A : ι' × ι → K) (x : ι → K),
  ⨆ j, v (∑ i, A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_addUnits : ∀ {G : Type u_1} [inst : AddMonoid G] {y : AddUnits G}, addOrderOf ↑y = addOrderOf y
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.enrichedNatTransYoneda_map : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  [inst_4 : CategoryTheory.BraidedCategory V] (F G : CategoryTheory.EnrichedFunctor V C D) {X Y : Vᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.enrichedNatTransYoneda F G).map f =
    TypeCat.ofHom fun σ => { app := fun X_1 => CategoryTheory.CategoryStruct.comp f.unop (σ.app X_1), naturality := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prodIso_inv : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex),
  (A.prodIso B).inv = SSet.Subcomplex.lift (CategoryTheory.MonoidalCategoryStruct.tensorHom A.ι B.ι) ⋯
-- Init.Data.UInt.Lemmas
UInt64.zero_mod : ∀ {a : UInt64}, 0 % a = 0
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_eq_zero_of_subsingleton : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_5} [Subsingleton ι] (x : ι → K),
  Height.logHeight x = 0
-- Init.Data.List.Lemmas
List.getElem?_append : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, (l₁ ++ l₂)[i]? = if i < l₁.length then l₁[i]? else l₂[i - l₁.length]?
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- We have a bijection of homsets which will be used to construct the right adjoint to the comparison
functor.
 -/
CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              (A : adj.toComonad.Coalgebra) →
                (B : C) →
                  [inst_2 : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] →
                    ((CategoryTheory.Comonad.comparison adj).obj B ⟶ A) ≃
                      (B ⟶ CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj A)
-- Mathlib.Data.Vector.Basic
List.Vector.get.eq_1 : ∀ {α : Type u_1} {n : ℕ} (l : List.Vector α n) (i : Fin n), l.get i = (↑l).get (Fin.cast ⋯ i)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instIsStableUnderBaseChangeSchemeLocallyQuasiFinite : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.LocallyQuasiFinite
-- Mathlib.Order.Lattice.Nat
/-- This instance is necessary, otherwise the lattice operations would be derived via
`ConditionallyCompleteLinearOrderBot` and marked as noncomputable.  -/
Nat.instLattice : Lattice ℕ
-- Init.Data.UInt.Bitwise
UInt8.toUInt64_not : ∀ (a : UInt8), (~~~a).toUInt64 = ~~~a.toUInt64 % 256
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] (f : X ⟶ Y),
  (CategoryTheory.tensorLeftHomEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y Yᘁ Xᘁ).symm
      (CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Xᘁ)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Yᘁ).hom (fᘁ)
-- Init.Data.List.MapIdx
List.mapFinIdx_nil : ∀ {α : Type u_1} {β : Type u_2} {f : (i : ℕ) → α → i < 0 → β}, [].mapFinIdx f = []
-- Mathlib.Data.List.Basic
List.instLawfulIdentityAppendNil_mathlib : ∀ {α : Type u}, Std.LawfulIdentity Append.append []
-- Mathlib.Tactic.Translate.GuessName
/-- A set of strings of names that end in a capital letter.
* If the string contains a lowercase letter, the string should be split between the first occurrence
  of a lower-case letter followed by an upper-case letter.
* If multiple strings have the same prefix, they should be grouped by prefix
* In this case, the second list should be prefix-free
  (no element can be a prefix of a later element)

Todo: automate the translation from `String` to an element in this `TreeMap`
  (but this would require having something similar to the `rb_lmap` from Lean 3).  -/
Mathlib.Tactic.GuessName.endCapitalNames : Std.TreeMap String (List String) compare
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.mk : ∀ {α : Type u_2} [inst : LE α] {s : Set α},
  (∀ t ⊆ s, t.Nonempty → t.Countable → ∀ (x : α), IsLUB t x → x ∈ s) → CountableSupClosed s
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformLeft.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  Finset.mulETransformLeft e x = (x.1 ∩ MulOpposite.op e • x.1, x.2 ∪ e⁻¹ • x.2)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- the components map to `S`  -/
AlgebraicGeometry.Scheme.AffineCover.f : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    (self : AlgebraicGeometry.Scheme.AffineCover P S) → (j : self.I₀) → AlgebraicGeometry.Spec (self.X j) ⟶ S
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `N` is flat, then any two commutative
elements of `↥(M ⊓ N)` are not `R`-linearly independent (namely, their span is not `R ^ 2`).  -/
Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ [Nontrivial R] [Module.Flat R ↥N] (a b : ↥(M ⊓ N)), Commute ↑a ↑b → ¬LinearIndependent R ![a, b]
-- Mathlib.Algebra.Order.Round
/-- Formula for `round` in terms of `Int.floor`, a version that works over any ring.

TODO: decide if we want to use this as a definition. It may be slightly faster over `ℚ`.  -/
round_eq_div : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α),
  round x = (⌊2 * x⌋ + 1) / 2
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mrevertPat∀_» : Lean.ParserDescr
-- Init.Core
/-- Strict superset relation: `a ⊃ b`  

Conventions for notations in identifiers:

 * The recommended spelling of `⊃` in identifiers is `ssuperset` (prefer `⊂` over `⊃`). -/
«term_⊃_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Trace.Basic
Algebra.trace_eq_of_ringEquiv : ∀ {A : Type u_7} {B : Type u_8} {C : Type u_9} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A C] [inst_4 : Algebra B C] (e : A ≃+* B),
  (algebraMap B C).comp ↑e = algebraMap A C → ∀ (x : C), e ((Algebra.trace A C) x) = (Algebra.trace B C) x
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Does any element of the map satisfy property `P`?

```
Any (fun x ↦ x < 2) {1, 2, 3} = True
Any (fun x ↦ x < 2) {2, 3, 5} = False
```
 -/
Ordnode.Any : {α : Type u_1} → (α → Prop) → Ordnode α → Prop
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
/-- The norm associated with a Hilbert C⋆-module. It is not registered as a norm, since a type
might already have a norm defined on it.  -/
CStarModule.norm : (A : Type u_3) → {E : Type u_4} → [Norm A] → [Inner A E] → Norm E
-- Lean.Elab.Open
/-- A local copy of name resolution state that allows us to immediately use new open decls
in further name resolution as in `open Lean Elab`.
 -/
Lean.Elab.OpenDecl.State : Type
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instIsCentralScalar : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M] [inst_5 : IsScalarTower R M M]
  [inst_6 : IsScalarTower R M X] [inst_7 : SMul Rᵐᵒᵖ M] [inst_8 : SMul Rᵐᵒᵖ X] [inst_9 : IsScalarTower Rᵐᵒᵖ M M]
  [inst_10 : IsScalarTower Rᵐᵒᵖ M X] [IsCentralScalar R M], IsCentralScalar R (OreLocalization S X)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddMonoidHom.eqLocusM.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f g : M →+ N),
  f.eqLocusM g = { carrier := {x | f x = g x}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Std.Time.Format
/-- The LongDateFormat, which follows the pattern `EEEE, MMMM d, uuuu HH:mm:ss` for
representing a full date and time with the day of the week and month name.
 -/
Std.Time.Formats.longDateFormat : Std.Time.GenericFormat (Std.Time.Awareness.only Std.Time.TimeZone.GMT)
-- Mathlib.Data.List.ReduceOption
List.reduceOption_map : ∀ {α : Type u_1} {β : Type u_2} {l : List (Option α)} {f : α → β},
  (List.map (Option.map f) l).reduceOption = List.map f l.reduceOption
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.skipped : Aesop.SafeRulesResult
-- Mathlib.Lean.Expr.Basic
/-- `nm.splitAt n` splits a name `nm` in two parts, such that the *second* part has depth `n`,
i.e. `(nm.splitAt n).2.getNumParts = n` (assuming `nm.getNumParts ≥ n`).
Example: ``splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat)``.  -/
Lean.Name.splitAt : Lean.Name → ℕ → Lean.Name × Lean.Name
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extend.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} (c : CategoryTheory.Limits.Cocone F) {X : C} (f : c.pt ⟶ X),
  c.extend f = { pt := X, ι := CategoryTheory.CategoryStruct.comp c.ι ((CategoryTheory.Functor.const J).map f) }
-- Mathlib.Algebra.Order.Sub.Basic
Even.tsub : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] [AddLeftReflectLE α] {m n : α}, Even m → Even n → Even (m - n)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_coconeMorphism : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F)
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.Limits.colimit.coconeMorphism c).hom =
    c.ι.app j
-- Init.Data.Array.MinMax
Array.max?_le_iff : ∀ {α : Type u_1} {a : α} [inst : Max α] [inst_1 : LE α] [Std.LawfulOrderSup α] {xs : Array α},
  xs.max? = some a → ∀ {x : α}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
-- Mathlib.Order.CompleteLattice.Basic
Antitone.iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : Preorder α] [inst_1 : CompleteLattice β] {f : ι → α → β},
  (∀ (i : ι), Antitone (f i)) → Antitone (⨅ i, f i)
-- Mathlib.Logic.Nonempty
nonempty_prod : ∀ {α : Type u_1} {β : Type u_2}, Nonempty (α × β) ↔ Nonempty α ∧ Nonempty β
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitUnopIsoUnopColimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.limitUnopIsoUnopColimit F =
    CategoryTheory.Limits.limit.isoLimitCone
      { cone := CategoryTheory.Limits.coneUnopOfCocone (CategoryTheory.Limits.colimit.cocone F),
        isLimit := CategoryTheory.Limits.isLimitConeUnopOfCocone F (CategoryTheory.Limits.colimit.isColimit F) }
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.symm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.Equiv m₂ → m₂.Equiv m₁
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso.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} {s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t),
  P.conePointUniqueUpToIso Q = (CategoryTheory.Limits.Cone.forget F).mapIso (P.uniqueUpToIso Q)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} {fallback b : β a}, (t.insert a b).getD a fallback = b
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.borelUpper.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H),
  b.borelUpper = { toSubmodule := (LieSubalgebra.lieSpan R L (Set.range b.e)).toSubmodule, lie_mem := ⋯ }
-- Mathlib.Order.SuccPred.Basic
SuccOrder.mk : {α : Type u_3} →
  [inst : Preorder α] →
    (succ : α → α) →
      (∀ (a : α), a ≤ succ a) → (∀ {a : α}, succ a ≤ a → IsMax a) → (∀ {a b : α}, a < b → succ a ≤ b) → SuccOrder α
-- Lean.Environment
Lean.Environment.header : Lean.Environment → Lean.EnvironmentHeader
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instAddMonoid : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → [ContinuousAdd M₂] → AddMonoid (ContinuousMultilinearMap R M₁ M₂)
-- Mathlib.CategoryTheory.Preadditive.Schur
CategoryTheory.endomorphism_simple_eq_smul_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] {X : C}
  [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] (f : X ⟶ X), ∃ c, c • CategoryTheory.CategoryStruct.id X = f
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.π_precompose : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g f' g' : X ⟶ Y}
  {α : CategoryTheory.Limits.parallelPair f g ⟶ CategoryTheory.Limits.parallelPair f' g'}
  {c : CategoryTheory.Limits.Cofork f' g'},
  CategoryTheory.Limits.Cofork.π ((CategoryTheory.Limits.Cocone.precompose α).obj c) =
    CategoryTheory.CategoryStruct.comp (α.app CategoryTheory.Limits.WalkingParallelPair.one) c.π
-- Mathlib.LinearAlgebra.Orientation
/-- `adjust_to_orientation` gives a basis with the required orientation.  -/
Module.Basis.orientation_adjustToOrientation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  [inst_7 : Nonempty ι] (e : Module.Basis ι R M) (x : Orientation R M ι), (e.adjustToOrientation x).orientation = x
-- Mathlib.Analysis.Convex.Cone.Basic
/-- The closure of image of a proper cone under an `R`-linear map is a proper cone. We
use continuous maps here so that the comap of f is also a map between proper cones.  -/
ProperCone.comap : {R : Type u_2} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : IsOrderedRing R] →
            [inst_3 : AddCommMonoid E] →
              [inst_4 : TopologicalSpace E] →
                [inst_5 : Module R E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : TopologicalSpace F] →
                      [inst_8 : Module R F] → (E →L[R] F) → ProperCone R F → ProperCone R E
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.CategoryStruct.mk : {obj : Type u} →
  [toQuiver : Quiver obj] →
    ((X : obj) → X ⟶ X) → ({X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)) → CategoryTheory.CategoryStruct.{v, u} obj
-- Mathlib.Order.CompleteLattice.Basic
Set.BijOn.iSup_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {s : Set β} {t : Set γ} {f : β → γ}
  (g : γ → α), Set.BijOn f s t → ⨆ x ∈ s, g (f x) = ⨆ y ∈ t, g y
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.sheafComposeIso_inv_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.HasWeakSheafify J A]
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.HasSheafCompose F] [inst_6 : J.PreservesSheafification F]
  (P : CategoryTheory.Functor Cᵒᵖ A) {Z : CategoryTheory.Functor Cᵒᵖ B} (h : CategoryTheory.sheafify J (P.comp F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J F P).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) h
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
/-- Conditional (Lebesgue) expectation of a function, with notation `P⁻[X|mΩ]`.

It is defined as `0` if either `¬ mΩ ≤ mΩ₀` or `hm : mΩ ≤ mΩ₀` but `¬ SigmaFinite (P.trim hm)`.

One should typically not use the definition directly.
 -/
MeasureTheory.condLExp : {Ω : Type u_2} → {mΩ₀ : MeasurableSpace Ω} → MeasurableSpace Ω → MeasureTheory.Measure Ω → (Ω → ENNReal) → Ω → ENNReal
-- Mathlib.LinearAlgebra.TensorProduct.Prod
/-- Tensor products distribute over a product on the right.  -/
TensorProduct.prodRight : (R : Type u_1) →
  (S : Type u_2) →
    (M₁ : Type u_3) →
      (M₂ : Type u_4) →
        (M₃ : Type u_5) →
          [inst : CommSemiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M₁] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : AddCommMonoid M₃] →
                    [inst_5 : Algebra R S] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module S M₁] →
                          [inst_8 : IsScalarTower R S M₁] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module R M₃] →
                                TensorProduct R M₁ (M₂ × M₃) ≃ₗ[S] TensorProduct R M₁ M₂ × TensorProduct R M₁ M₃
-- Mathlib.Algebra.Ring.NonZeroDivisors
dvd_cancel_left_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] {x y r : R}, r ∈ nonZeroDivisors R → (r * x ∣ r * y ↔ x ∣ y)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_comp_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N], Monoid.Coprod.snd.comp Monoid.Coprod.inl = 1
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalStarSubalgebra.unitization.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : SetLike S A]
  [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] [inst_7 : StarMemClass S A] (s : S),
  NonUnitalStarSubalgebra.unitization s = Unitization.starLift (NonUnitalStarSubalgebraClass.subtype s)
-- Mathlib.Data.Finset.Insert
Finset.ssubset_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t
-- Mathlib.GroupTheory.Coxeter.Length
_private.Mathlib.GroupTheory.Coxeter.Length.0.CoxeterSystem.termS_ : Lean.ParserDescr
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Max α} {inst_1 : Max β} {inst_2 : Bot α} {inst_3 : Bot β}
  {toSupHom : SupHom α β} {map_bot' : toSupHom.toFun ⊥ = ⊥} {toSupHom_1 : SupHom α β}
  {map_bot'_1 : toSupHom_1.toFun ⊥ = ⊥},
  { toSupHom := toSupHom, map_bot' := map_bot' } = { toSupHom := toSupHom_1, map_bot' := map_bot'_1 } →
    toSupHom = toSupHom_1
-- Mathlib.Order.Filter.Pi
/-- The indexed product of a (possibly, infinite) family of pure filters `pure (f i)`
is generated by the sets of functions that are equal to `f` on a finite set.

If the index type is finite, then the indexed product of pure filters is a pure filter,
see `pi_pure`.  -/
Filter.mem_pi_pure : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i} {s : Set ((i : ι) → α i)},
  (s ∈ Filter.pi fun i => pure (f i)) ↔ ∃ I, I.Finite ∧ ∀ (g : (i : ι) → α i), (∀ i ∈ I, g i = f i) → g ∈ s
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.dist_iConvexComb_left_le : ∀ {I : Type u_1} {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X]
  (f : Convexity.StdSimplex ℝ I) (g : I → X) (x : X),
  dist (Convexity.iConvexComb f g) x ≤ Convexity.iConvexComb f fun i => dist (g i) x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDeriv_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {c : F} {x : 𝕜}, iteratedDeriv n (fun x => c) x = if n = 0 then c else 0
-- Mathlib.CategoryTheory.Action.Concrete
TypeCat.endEquiv_apply : ∀ (X : Type u) (f : Function.End X), (TypeCat.endEquiv X) f = TypeCat.ofHom f
-- Mathlib.Data.Finset.Update
Function.updateFinset_univ_apply : ∀ {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  {y : (i : ↥Finset.univ) → π ↑i} {i : ι}, Function.updateFinset x Finset.univ y i = y ⟨i, ⋯⟩
-- Mathlib.Data.Finset.Insert
Finset.mem_insert_coe : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {x y : α}, x ∈ insert y s ↔ x ∈ insert y ↑s
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The `R`-algebra equivalence relating `FreeProduct` and `FreeProduct.asPowers`.  -/
LinearAlgebra.FreeProduct.asPowersEquiv : {I : Type u} →
  [inst : DecidableEq I] →
    (R : Type v) →
      [inst_1 : CommSemiring R] →
        (A : I → Type w) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] →
              LinearAlgebra.FreeProduct.asPowers R A ≃ₐ[R] LinearAlgebra.FreeProduct R A
-- Mathlib.Analysis.SpecificLimits.Basic
NNReal.exists_pos_sum_of_countable : ∀ {ε : NNReal}, ε ≠ 0 → ∀ (ι : Type u_4) [Countable ι], ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
-- Mathlib.RingTheory.Ideal.Basic
Ideal.prod_mem : ∀ {α : Type u_2} [inst : CommSemiring α] {ι : Type u_5} {f : ι → α} {s : Finset ι} (I : Ideal α) {i : ι},
  i ∈ s → f i ∈ I → ∏ i ∈ s, f i ∈ I
-- Init.Data.Int.DivMod.Pow
_private.Init.Data.Int.DivMod.Pow.0.Int.ediv_pow : ∀ {a b : ℤ} {n : ℕ}, b ∣ a → (a / b) ^ n = a ^ n / b ^ n
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.leadingCoeff_basis : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  Set.InjOn v ↑s → i ∈ s → (Lagrange.basis s v i).leadingCoeff = (∏ j ∈ s.erase i, (v i - v j))⁻¹
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.traj_map_frestrictLe_of_le : ∀ {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 : ℕ} (hab : a ≤ b),
  (ProbabilityTheory.Kernel.traj κ b).map (Preorder.frestrictLe a) =
    ProbabilityTheory.Kernel.deterministic (Preorder.frestrictLe₂ hab) ⋯