mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If `F` is an equivalence, it's a left adjoint.  -/
CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.IsEquivalence], F.IsLeftAdjoint
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.coeff_pderiv : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ),
  (MvPowerSeries.coeff n) ((MvPowerSeries.pderiv R i) f) = (MvPowerSeries.coeff (n + fun₀ | i => 1)) f * (↑(n i) + 1)
-- Mathlib.Analysis.Normed.Field.Basic
Real.toNNReal_mul_nnnorm : ∀ {x : ℝ} (y : ℝ), 0 ≤ x → x.toNNReal * ‖y‖₊ = ‖x * y‖₊
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] (μ : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure μ] [OpensMeasurableSpace X] (f : BoundedContinuousFunction X ℝ),
  ∫ (x : X), f x ∂μ = ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.LinearAlgebra.Prod
/-- Taking the product of two maps with the same codomain is equivalent to taking the product of
their domains.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.  -/
LinearMap.coprodEquiv : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        (S : Type u_3) →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : AddCommMonoid M₃] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] →
                          [inst_8 : Module S M₃] →
                            [inst_9 : SMulCommClass R S M₃] → ((M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ≃ₗ[S] M × M₂ →ₗ[R] M₃
-- Mathlib.Topology.Algebra.Monoid
Filter.HasBasis.mul_self : ∀ {ι : Type u_1} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulOneClass M] [ContinuousMul M] {p : ι → Prop}
  {s : ι → Set M}, (nhds 1).HasBasis p s → (nhds 1).HasBasis p fun i => s i * s i
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) (a a_1 a_2 : List α),
  List.MergeSort.Internal.mergeTR.go✝ le a a_1 a_2 =
    match a, a_1, a_2 with
    | [], l₂, acc => acc.reverseAux l₂
    | l₁, [], acc => acc.reverseAux l₁
    | x :: xs, y :: ys, acc =>
      if le x y = true then List.MergeSort.Internal.mergeTR.go✝ le xs (y :: ys) (x :: acc)
      else List.MergeSort.Internal.mergeTR.go✝ le (x :: xs) ys (y :: acc)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.instCartesianMonoidalCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.CartesianMonoidalCategory (CategoryTheory.AddMon C)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.map_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  {a : σ → MvPowerSeries τ R},
  MvPowerSeries.HasSubst a →
    ∀ {h : R →+* S} (f : MvPowerSeries σ R),
      (MvPowerSeries.map h) (MvPowerSeries.subst a f) =
        MvPowerSeries.subst (fun i => (MvPowerSeries.map h) (a i)) ((MvPowerSeries.map h) f)
-- Mathlib.RingTheory.Localization.BaseChange
/-- `S ⊗[R] A[M⁻¹]` is the localization of `S ⊗[R] A` at `M`.  -/
IsLocalization.tensorProduct_tensorProduct_right : ∀ (R : Type u_7) (S : Type u_8) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {A : Type u_9}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (M : Submonoid A) (B : Type u_10) [inst_5 : CommSemiring B]
  [inst_6 : Algebra R B] [inst_7 : Algebra A B] [IsScalarTower R A B] [IsLocalization M B]
  [inst_10 : Algebra (TensorProduct R S A) (TensorProduct R S B)]
  [IsScalarTower S (TensorProduct R S A) (TensorProduct R S B)],
  (algebraMap (TensorProduct R S A) (TensorProduct R S B)).comp Algebra.TensorProduct.includeRight.toRingHom =
      Algebra.TensorProduct.includeRight.comp (algebraMap A B) →
    IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) (TensorProduct R S B)
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.splitByLoop_append : ∀ {α : Type u_1} {m : List α} {r : α → α → Bool} {l g : List α} {a : α},
  List.IsChain (fun x y => r x y = true) (g.reverse ++ a :: l) →
    (∀ x ∈ m.head?, r ((a :: l).getLast ⋯) x = false) →
      List.splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: List.splitBy r m
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.PointsWithCircumcenterIndex.pointIndex.sizeOf_spec : ∀ {n : ℕ} (a : Fin (n + 1)), sizeOf (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a) = 1 + sizeOf a
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R), PowerSeries.subst a f = MvPowerSeries.subst (fun x => a) f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_algebraMap_nnreal : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (r : NNReal),
  ((algebraMap NNReal A) r)⁺ = (algebraMap NNReal A) r
-- Mathlib.Logic.Function.Basic
Function.instIrreflOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [Std.Irrefl r], Std.Irrefl (Function.onFun r f)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearEquiv_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
  [inst_7 : Module R₂ E₂], Function.Injective LinearIsometryEquiv.toContinuousLinearEquiv
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.asIsoHomologyι_inv_comp_homologyι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp (S.asIsoHomologyι hg).inv S.homologyι = CategoryTheory.CategoryStruct.id S.opcycles
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₁₃ = CategoryTheory.Arrow.Hom.left f.hom
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] {M' : Type u_10}
  [inst_11 : TopologicalSpace M'] [inst_12 : ChartedSpace H' M'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) {f : M' → M},
  ContMDiff I' (I.transContinuousLinearEquiv e) n f ↔ ContMDiff I' I n f
-- Mathlib.Data.Vector.Basic
List.Vector.set.eq_1 : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : Fin n) (a : α), v.set i a = ⟨(↑v).set (↑i) a, ⋯⟩
-- Init.Prelude
/-- The homogeneous version of `HXor`: `a ^^^ b : α` where `a b : α`.  -/
XorOp : Type u → Type u
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor on `AddGrpCat.{u}` creates `u`-small limits.  -/
AddGrpCat.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} AddGrpCat.uliftFunctor
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.monotone_map : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Monotone (FirstOrder.Language.Substructure.map f)
-- ProofWidgets.Component.RefreshComponent
/-- A task that resolves when this state has become out-of-date.
It resolves with `some ()` if a new state is available,
and with `none` if the display will never be updated again.

It is implemented using `RefreshToken.promise.result?`,
but we don't store the `Promise` here
in order to make sure it can reach a refcount of 0.  -/
ProofWidgets.RefreshComponent.RefreshState.next : ProofWidgets.RefreshComponent.RefreshState → Task (Option Unit)
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.charZero : ∀ {R : Type u} [inst : Semiring R] [CharZero R], CharZero (Polynomial R)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.coe_quotientKerEquivRangeS_mk : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] (f : M →+* P) (x : M),
  ↑((RingCon.quotientKerEquivRangeS f) ↑x) = f x
-- Lean.DocString.Extension
/-- A snippet of a Verso module text.

A snippet consists of text followed by subsections. Because the sequence of snippets that occur in a
source file are conceptually a single document, they have a consistent header nesting structure.
This means that initial textual content of a snippet is a continuation of the text at the end of the
prior snippet.

The actual hierarchical structure of the document is reconstructed from the sequence of snippets.

The _terminal nesting_ of a sequence of snippets is 0 if there are no sections in the sequence.
Otherwise, it is one greater than the nesting of the last snippet's last section. The module
docstring elaborator maintains the invariant that each snippet's first section's level is at most
the terminal nesting of the preceding snippets, and that the level of each section within a snippet
is at most one greater than the preceding section's level.
 -/
Lean.VersoModuleDocs.Snippet : Type
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_add : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
  Polynomial.eval₂ f x (p + q) = Polynomial.eval₂ f x p + Polynomial.eval₂ f x q
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- When `ι` contains a unique element and `f : X ⟶ S` is a morphism,
the composition of `F.toDescentDataAsCoalgebra (fun (_ : ι) ↦ f)`
and the functor of the equivalence
`DescentDataAsCoalgebra.coalgebraEquivalence F ι f` identifies to
`Comonad.comparison` applied to the adjunction corresponding to
`F.map f.op.toLoc`.  -/
CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      (ι : Type u_2) →
        [inst_1 : Unique ι] →
          {X S : C} →
            (f : X ⟶ S) →
              (F.toDescentDataAsCoalgebra fun x => f).comp
                  (CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor ≅
                CategoryTheory.Comonad.comparison (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
/-- The tensor-hom adjunction `(· ⊗ G) ⊣ Hom(G, ·)`.  -/
CategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] →
        (G : C) → CategoryTheory.IsGrothendieckAbelian.tensorObj G ⊣ CategoryTheory.preadditiveCoyonedaObj G
-- Mathlib.Algebra.Category.CoalgCat.Basic
CategoryTheory.Iso.toCoalgEquiv_toCoalgHom : ∀ {R : Type u} [inst : CommRing R] {X Y : CoalgCat R} (i : X ≅ Y), ↑i.toCoalgEquiv = CoalgCat.Hom.toCoalgHom i.hom
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
AlgebraicGeometry.Scheme.zariskiTopology_eq : AlgebraicGeometry.Scheme.zariskiTopology = AlgebraicGeometry.Scheme.zariskiPretopology.toGrothendieck
-- Mathlib.LinearAlgebra.Pi
/-- The linear equivalence between linear functions on a finite product of modules and
families of functions on these modules. See note [bundled maps over different rings].  -/
LinearMap.lsum : (R : Type u) →
  {M : Type v} →
    {ι : Type x} →
      [inst : Semiring R] →
        (φ : ι → Type i) →
          [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_2 : (i : ι) → Module R (φ i)] →
              [DecidableEq ι] →
                (S : Type u_1) →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] →
                      [Fintype ι] →
                        [inst_7 : Semiring S] →
                          [inst_8 : Module S M] →
                            [inst_9 : SMulCommClass R S M] → ((i : ι) → φ i →ₗ[R] M) ≃ₗ[S] ((i : ι) → φ i) →ₗ[R] M
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_C_mul : ∀ {σ : Type u_1} {A : Type u_3} [inst : CommRing A] [NoZeroDivisors A] (a : A),
  a ≠ 0 → ∀ (φ : MvPolynomial σ A), (MvPolynomial.C a * φ).vars = φ.vars
-- Mathlib.Combinatorics.Colex
/-- The equivalence `Nat.equivBitIndices` enumerates `Finset ℕ` in colexicographic order.  -/
Finset.orderIsoColex : ℕ ≃o Colex (Finset ℕ)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [inst_3 : NormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'}, ContDiffAt 𝕜 n f x → f x ≠ 0 → ContDiffAt 𝕜 n f⁻¹ x
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_imp : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l] (p₁ p₂ : Prop),
  (p₁ → p₂) → Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp p₁) (Lean.Order.CompleteLattice.ofProp p₂)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.comap_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f → MeasurableSpace.comap f inst_1 = inst
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.Node.sizeOf_spec : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : SizeOf α] [inst_1 : SizeOf β] (a : Option β)
  (a_1 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp),
  sizeOf (Lean.PrefixTreeNode.Node a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.indep' : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ]
  {p1 p2 : Set (Set Ω)},
  (∀ s ∈ p1, MeasurableSet s) →
    (∀ s ∈ p2, MeasurableSet s) →
      IsPiSystem p1 →
        IsPiSystem p2 →
          ProbabilityTheory.IndepSets p1 p2 μ →
            ProbabilityTheory.Indep (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) μ
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.ext_elem_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) {x y : S}, x = y ↔ ∀ i < f.natDegree, h.coeff x i = h.coeff y i
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.IsDynCoverOf.monotone_subset : ∀ {X : Type u_1} {T : X → X} {F G s : Set X} {U : SetRel X X} {n : ℕ},
  F ⊆ G → Dynamics.IsDynCoverOf T G U n s → Dynamics.IsDynCoverOf T F U n s
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.exists_le_iSup_basicOpen_and_smul_eq_smul_and_eq_const : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  IsCompact ↑U →
    ∀ (s : (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)),
      ∃ ι x a b,
        ∃ (ibU : ∀ (i : ι), PrimeSpectrum.basicOpen (b i) ≤ U),
          U ≤ ⨆ i, PrimeSpectrum.basicOpen (b i) ∧
            (∀ (i j : ι), b j • a i = b i • a j) ∧
              ∀ (i : ι),
                (CategoryTheory.ConcreteCategory.hom
                      ((AlgebraicGeometry.structureSheafInType R M).presheaf.map ⋯.hom.op))
                    s =
                  AlgebraicGeometry.StructureSheaf.const (a i) (b i) (PrimeSpectrum.basicOpen (b i)) ⋯
-- Lean.Elab.MutualInductive
/-- Compute a bit-mask that for `indType`. The size of the resulting array `result` is the arity of `indType`.
The first `numParams` elements are `false` since they are parameters.
For `i ∈ [numParams, arity)`, we have that `result[i]` if this index of the inductive family is fixed.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.computeFixedIndexBitMask : ℕ → Lean.InductiveType → Array Lean.Expr → Lean.MetaM (Array Bool)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMulZeroOneClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → MulZeroOneClass (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] →
                      MulZeroOneClass (DirectLimit G f)
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- Restricting a chart to its source `s ⊆ M` yields a chart in the maximal atlas of `s`.  -/
StructureGroupoid.restriction_mem_maximalAtlas_subtype : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H},
  e ∈ atlas H M →
    Nonempty ↑e.source →
      ∀ [HasGroupoid M G] [ClosedUnderRestriction G],
        let s := { carrier := e.source, is_open' := ⋯ };
        let t := { carrier := e.target, is_open' := ⋯ };
        ∀ c' ∈ atlas H ↥t,
          e.toHomeomorphSourceTarget.toOpenPartialHomeomorph.trans c' ∈ StructureGroupoid.maximalAtlas (↥s) G
-- Init.Data.Nat.Basic
Nat.lt_succ_iff_lt_or_eq : ∀ {m n : ℕ}, m < n.succ ↔ m < n ∨ m = n
-- Mathlib.Analysis.Convex.Uniform
UniformConvexSpace.toStrictConvexSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [UniformConvexSpace E], StrictConvexSpace ℝ E
-- Mathlib.Data.Finset.Interval
Finset.Icc_eq_filter_powerset : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), Finset.Icc s t = {u ∈ t.powerset | s ⊆ u}
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.smul_nonneg : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m0} {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : PartialOrder F]
  [IsOrderedAddMonoid F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] [IsOrderedModule ℝ F] {f : ι → Ω → F} {c : ℝ},
  0 ≤ c → MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Submartingale (c • f) ℱ μ
-- Mathlib.Order.Filter.Basic
Filter.not_le : ∀ {α : Type u} {f g : Filter α}, ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.mul_assoc : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {na nb nc : ℕ}
  (a : TensorPower R na M) (b : TensorPower R nb M) (c : TensorPower R nc M),
  (TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
-- Mathlib.Algebra.Homology.Bifunctor
/-- The morphism `mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c` induced by
morphisms of complexes `K₁ ⟶ L₁` and `K₂ ⟶ L₂`.  -/
HomologicalComplex.mapBifunctorMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            {K₁ L₁ : HomologicalComplex C₁ c₁} →
                              {K₂ L₂ : HomologicalComplex C₂ c₂} →
                                (K₁ ⟶ L₁) →
                                  (K₂ ⟶ L₂) →
                                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                      [inst_6 : F.PreservesZeroMorphisms] →
                                        [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                          (c : ComplexShape J) →
                                            [inst_8 : TotalComplexShape c₁ c₂ c] →
                                              [inst_9 : K₁.HasMapBifunctor K₂ F c] →
                                                [inst_10 : L₁.HasMapBifunctor L₂ F c] →
                                                  [inst_11 : DecidableEq J] →
                                                    K₁.mapBifunctor K₂ F c ⟶ L₁.mapBifunctor L₂ F c
-- Mathlib.Condensed.Light.Explicit
/-- A `LightCondSet` version of `LightCondensed.ofSheafLightProfinite`.  -/
LightCondSet.ofSheafLightProfinite : (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] → CategoryTheory.regularTopology.EqualizerCondition F → LightCondSet
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_le_of_apply_getElem_le_apply_getElem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} (h : xs ≠ []) {i : ℕ} (hi : i < xs.length),
  (∀ (j : ℕ) (x : j < xs.length), f xs[j] ≤ f xs[i]) → List.maxIdxOn f xs h ≤ i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (Std.HashMap.Raw.unitOfList l)[k]? = if l.contains k = true then some () else none
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- The lemma `fromCols_mul_fromRows_eq_one_comm` specialized to the case where the index sets
`n₁` and `n₂`, are the result of subtyping by a predicate and its complement.  -/
Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm : ∀ {R : Type u_1} {n : Type u_5} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (p : n → Prop)
  [inst_3 : DecidablePred p] (A₁ : Matrix n { i // p i } R) (A₂ : Matrix n { i // ¬p i } R)
  (B₁ : Matrix { i // p i } n R) (B₂ : Matrix { i // ¬p i } n R),
  A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Pairwise intersection of two `0`-hypercovers.  -/
CategoryTheory.Precoverage.ZeroHypercover.inter : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {T : C} →
        [J.IsStableUnderBaseChange] →
          [J.IsStableUnderComposition] →
            (E : J.ZeroHypercover T) →
              (F : J.ZeroHypercover T) →
                [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] → J.ZeroHypercover T