mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Instances
Std.instLinearlyUpwardEnumerableOfTotalLeOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLE : ∀ {α : Type u_1} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α], Std.PRange.LinearlyUpwardEnumerable α
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.ext : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ₁ μ₂ : MeasureTheory.Measure α},
  (∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s) → μ₁ = μ₂
-- Mathlib.Data.Setoid.Partition
/-- The subtype of partitions of a type, endowed with the canonical order on partitions.  -/
Setoid.Partitions : Type u_2 → Type u_2
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.toStream_eq : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : RBTree.RBMap α β cmp}, Std.toStream t = (↑t).toStream
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication is commutative  -/
DirectSum.GCommSemiring.mul_comm : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddCommMonoid ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GCommSemiring A] (a b : GradedMonoid A), a * b = b * a
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
rothNumberNat_le : ∀ (N : ℕ), rothNumberNat N ≤ N
-- Std.Http.Data.Request
Std.Http.Request.Builder.mk.injEq : ∀ (line : Std.Http.Request.Head) (extensions : Std.Http.Extensions) (line_1 : Std.Http.Request.Head)
  (extensions_1 : Std.Http.Extensions),
  ({ line := line, extensions := extensions } = { line := line_1, extensions := extensions_1 }) =
    (line = line_1 ∧ extensions = extensions_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_monotone : ∀ {X Y : SSet} (f : X ⟶ Y), Monotone fun S => S.image f
-- Lean.Elab.DeclModifiers
Lean.Elab.ExpandDeclIdResult.mk : Lean.Name →
  Lean.Name → List Lean.Name → Option (Lean.TSyntax `Lean.Parser.Command.docComment) → Lean.Elab.ExpandDeclIdResult
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.curry_mulSingle : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : One M] [inst_2 : DecidableEq ι']
  (i : ι × ι') (b : M), Function.curry (Pi.mulSingle i b) = Pi.mulSingle i.1 (Pi.mulSingle i.2 b)
-- Mathlib.Data.ENat.Basic
/-- Version of `WithTop.eq_of_forall_natCast_le_iff` using `Nat.cast` rather than `WithTop.some`.  -/
ENat.eq_of_forall_natCast_le_iff : ∀ {m n : ℕ∞}, (∀ (a : ℕ), ↑a ≤ m ↔ ↑a ≤ n) → m = n
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x y : C) {z z' : D} (f : z ⟶ z') {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z' ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) f)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x y z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight y f))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x y z').inv h))
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.trans : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.SOppSide x y → s.SOppSide y z → s.SSameSide x z
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_map_add : ∀ {ι : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] {l : List ι} {f g : ι → M},
  (List.map (fun i => f i + g i) l).sum = (List.map f l).sum + (List.map g l).sum
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.IsModHom.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : D} [inst_5 : CategoryTheory.ModObj A M]
  [inst_6 : CategoryTheory.ModObj A N] {f : M ⟶ N},
  autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
          CategoryTheory.ModObj.smul)
      CategoryTheory.IsModHom.smul_hom._autoParam →
    CategoryTheory.IsModHom A f
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosure_map_eq : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  (K : IntermediateField F L) (σ : L →ₐ[F] L),
  IntermediateField.normalClosure F (↥(IntermediateField.map σ K)) L = IntermediateField.normalClosure F (↥K) L
-- Mathlib.Probability.Density
MeasureTheory.hasPDF_iff_of_aemeasurable : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E},
  AEMeasurable X ℙ →
    (MeasureTheory.HasPDF X ℙ μ ↔
      (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ ∧
        (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.commMon_forget₂_map : ∀ {X Y : CommRingCat} (f : X ⟶ Y), CategoryTheory.HasForget₂.forget₂.map f = CommMonCat.ofHom ↑(CommRingCat.Hom.hom f)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.mapOfCompatibleSMul_surjective : ∀ (R : Type u_3) (S : Type u_4) (T : Type u_5) (A : Type u_6) (B : Type u_7) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : Algebra S B] [inst_9 : Algebra T A]
  [inst_10 : SMulCommClass R T A] [inst_11 : SMulCommClass S T A] [inst_12 : SMulCommClass R S A]
  [inst_13 : TensorProduct.CompatibleSMul R S A B],
  Function.Surjective ⇑(Algebra.TensorProduct.mapOfCompatibleSMul R S T A B)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is equicontinuous, its closure for the product topology is also
equicontinuous. This would also be true for the coarser topology of pointwise convergence on `S`,
see `EquicontinuousOn.closure'`.  -/
Set.EquicontinuousOn.closure : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {A : Set (X → α)} {S : Set X},
  A.EquicontinuousOn S → (closure A).EquicontinuousOn S
-- Mathlib.Topology.Sets.Closeds
/-- The Galois insertion between sets and closeds.  -/
TopologicalSpace.Closeds.gi : {α : Type u_2} → [inst : TopologicalSpace α] → GaloisInsertion TopologicalSpace.Closeds.closure SetLike.coe
-- Lean.Parser.Types
Lean.Parser.Parser.info : Lean.Parser.Parser → Lean.Parser.ParserInfo
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.hom_eq_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f g : X ⟶ Y),
  f = g ↔ CategoryTheory.StructuredArrow.Hom.right f = CategoryTheory.StructuredArrow.Hom.right g
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.pretopology_toPrecoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (P : CategoryTheory.MorphismProperty C) [inst_2 : P.IsMultiplicative] [inst_3 : P.IsStableUnderBaseChange],
  P.pretopology.toPrecoverage = P.precoverage
-- Mathlib.Algebra.Lie.Ideal
instCoeLieIdealLieSubalgebra : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Coe (LieIdeal R L) (LieSubalgebra R L)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.IsRoot.eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R}, p.IsRoot x → Polynomial.eval x p = 0
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] (x : G), addOrderOf x • x = 0
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.self_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Limits.ColimitPresentation.self X).ι =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.const PUnit.{s + 1}).obj X)
-- Lean.Parser.Command
Lean.Parser.Command.opaque.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.NormNoninc.neg_iff : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f : NormedAddGroupHom V₁ V₂}, (-f).NormNoninc ↔ f.NormNoninc
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Constructs the list of keys of the map.  -/
RBTree.RBMap.Keys.toList : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → List α
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.lTensorOne'_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {N : Submodule R S}
  (y : R) (n : ↥N), N.lTensorOne' ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = y • n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSymbolTag : Lean.ToJson Lean.Lsp.SymbolTag
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
/-- The summands in the formula `Nat.Partition.hasProd_genFun` tends to infinity in their order.  -/
Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top : ∀ {R : Type u_1} [inst : CommSemiring R] (f : ℕ → ℕ → R) (i : ℕ),
  Filter.Tendsto (fun j => (f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))).order) Filter.atTop (nhds ⊤)
-- Lean.Level
Lean.Level.instToFormat : Std.ToFormat Lean.Level
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul_k : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsEquipartition.card_biUnion_offDiag_le : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {ε : 𝕜},
  0 < ε → P.IsEquipartition → 4 / ε ≤ ↑P.parts.card → ↑(P.parts.biUnion Finset.offDiag).card ≤ ε / 2 * ↑A.card ^ 2
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
AhlswedeZhang.supSum_of_univ_notMem : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {𝒜 : Finset (Finset α)} [Nonempty α],
  𝒜.Nonempty →
    Finset.univ ∉ 𝒜 → AhlswedeZhang.supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.mk : Lean.Environment →
  Lean.Environment →
    Lean.Name →
      Lean.ConstantKind →
        Option Lean.ConstantKind →
          IO.Promise Lean.ConstantVal →
            IO.Promise Lean.Environment.ConstPromiseVal✝ →
              IO.Promise Lean.Kernel.Environment →
                IO.Promise (Lean.NameMap Lean.AsyncConst✝) → Lean.Environment.AddConstAsyncResult
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry.congr_simp : ∀ {α : Type u} {β : Type v} (t t_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t : t = t_1) (h : t.isEmpty = false),
  Std.DTreeMap.Internal.Impl.Const.minEntry t h = Std.DTreeMap.Internal.Impl.Const.minEntry t_1 ⋯
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.isIso_of_bijective : ∀ {x y : SimplexCategory} {f : x ⟶ y},
  Function.Bijective (SimplexCategory.Hom.toOrderHom f).toFun → CategoryTheory.IsIso f
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `Bundle.Trivialization.eq_sum_localFrameCoeff_smul`. -/
Bundle.Trivialization.eq_sum_localFrame_coeff_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [inst_14 : MemTrivializationAtlas e] {b : Module.Basis ι 𝕜 F}
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x' : M} {s : (x : M) → V x} [inst_16 : Fintype ι],
  x' ∈ e.baseSet → s x' = ∑ i, (Bundle.Trivialization.localFrameCoeff I e b i x') (s x') • e.localFrame b i x'
-- Lean.Meta.Tactic.Grind.Types
/-- We use this auxiliary constant to mark delayed symmetric congruence proofs.
**Example:** `a = b` is symmetrically congruent to `c = d` if `a = d` and `b = c`.

**Note:** We previously used `congrPlaceholderProof` for this case, but it
caused non-termination during proof term construction when `a = b = c = d`.
The issue was that we did not have enough information to determine how
`a = b` and `c = d` became congruent. The new marker resolves this issue.

If `congrPlaceholderProof` is used, then `a = b` became congruent to `c = d`
because `a = c` and `b = d`.
If `eqCongrSymmPlaceholderProof` is used, then it was because `a = d` and `b = c`.

**Example:** suppose we have the following equivalence class:
```
{p, q, p = q, q = p, True}
```
Recall that `True` is always the root of its equivalence class.
Assume we also have the following two paths in the class:
```
1. p -> p = q -> q = p -> True
2. q -> True
```
Now suppose we try to build a proof for `p = True`.
We must construct a proof for `(p = q) = (q = p)`.
These equalities are congruent, but if we try to prove `p = q` and `q = p`
using the facts `p = True` and `q = True`, we end up trying to prove `p = True` again.
In other words, we are missing the information that `p = q` became congruent to `q = p`
because of the symmetric case. By using `eqCongrSymmPlaceholderProof`, we retain this information.
 -/
Lean.Meta.Grind.eqCongrSymmPlaceholderProof : Lean.Expr
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.star_comp : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst_1 : Quiver V] (φ : U ⥤q V) {W : Type u_2} [inst_2 : Quiver W]
  (ψ : V ⥤q W) (u : U), (φ ⋙q ψ).star u = ψ.star (φ.obj u) ∘ φ.star u
-- Mathlib.Data.ENNReal.Inv
/-- If `a ≠ 0` and `a ≠ ∞`, then right multiplication by `a` maps infimum to infimum.

See `ENNReal.iInf_mul'` for the general case, and `ENNReal.iInf_mul` for another special case that
assumes `Nonempty ι` but does not require `a ≠ 0`.  -/
ENNReal.iInf_mul_of_ne : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → (⨅ i, f i) * a = ⨅ i, f i * a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Pattern to get `Walk.nil` with the vertex as an explicit argument.  -/
SimpleGraph.Walk.nil' : {V : Type u} → {G : SimpleGraph V} → (u : V) → G.Walk u u
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_apply_left`. -/
Equiv.Perm.SameCycle.apply_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle (f x) y
-- Mathlib.LinearAlgebra.Reflection
/-- Given an element `x` in a module `M` and a linear form `f` on `M` for which `f x = 2`, we define
the endomorphism of `M` for which `y ↦ y - (f y) • x`.

It is an involutive endomorphism of `M` fixing the kernel of `f` for which `x ↦ -x`.  -/
Module.reflection : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {x : M} → {f : Module.Dual R M} → f x = 2 → M ≃ₗ[R] M
-- Std.Async.Timer
/-- Create a `Selector` that resolves once `s` has finished. `s` only starts when it runs inside of a Selectable.
 -/
Std.Async.Sleep.selector : Std.Async.Sleep → Std.Async.Selector Unit
-- Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
/-- When the base object is terminal, a limit wide pullback cone can be obtained
from a limit fan.  -/
CategoryTheory.Limits.WidePullbackCone.isLimitOfFan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      {B : C} →
        {objs : ι → C} →
          (arrows : (j : ι) → objs j ⟶ B) →
            {c : CategoryTheory.Limits.Fan objs} →
              CategoryTheory.Limits.IsLimit c →
                (hB : CategoryTheory.Limits.IsTerminal B) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.WidePullbackCone.ofFan arrows c hB)
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2Computable.mk : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} →
      {f : α → β} →
        (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ) →
          ((a : α) →
              Turing.TM2Outputs toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
                (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a))))) →
            Turing.TM2Computable ea eb f
-- Lean.Meta.Tactic.Grind.Types
/-- If `heqProofs := true`, then some proofs in the equivalence class are based
on heterogeneous equality.
 -/
Lean.Meta.Grind.ENode.heqProofs : Lean.Meta.Grind.ENode → Bool
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.instLaxMonoidalRestrictScalars : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (f : R →+* S) → (ModuleCat.restrictScalars f).LaxMonoidal
-- Mathlib.Topology.Path
Path.extend_trans_of_half_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X} (γ₁ : Path x y) (γ₂ : Path y z) {t : ℝ},
  1 / 2 ≤ t → (γ₁.trans γ₂).extend t = γ₂.extend (2 * t - 1)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The generic case of the first simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i j : Fin (n + 2)},
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (X.δ j.succ) (X.δ i) =
      CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.δ j)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_mulMon : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  k ≥ 0 →
    p.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.mulMon k m p) =
        ↑k.toNat * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denoteS ctx p
-- Lean.ErrorExplanation
Lean.ErrorExplanation.Metadata.mk.injEq : ∀ (summary sinceVersion : String) (severity : Lean.MessageSeverity) (removedVersion? : Option String)
  (summary_1 sinceVersion_1 : String) (severity_1 : Lean.MessageSeverity) (removedVersion?_1 : Option String),
  ({ summary := summary, sinceVersion := sinceVersion, severity := severity, removedVersion? := removedVersion? } =
      { summary := summary_1, sinceVersion := sinceVersion_1, severity := severity_1,
        removedVersion? := removedVersion?_1 }) =
    (summary = summary_1 ∧ sinceVersion = sinceVersion_1 ∧ severity = severity_1 ∧ removedVersion? = removedVersion?_1)
-- Init.Data.BitVec.Lemmas
BitVec.not_inj : ∀ {w : ℕ} {x y : BitVec w}, ~~~x = ~~~y ↔ x = y
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedLambdaTheorem.default : Mathlib.Meta.FunProp.LambdaTheorem
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X}
  {X_1 Y_1 :
    CategoryTheory.ObjectProperty.FullSubcategory fun f =>
      (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom}
  (g : X_1 ⟶ Y_1),
  (TopCat.Presheaf.generateEquivalenceOpensLe_functor' U).map g =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.Hom.left g.hom)
-- Init.Try
Lean.Try.instInhabitedConfig.default : Lean.Try.Config
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If each `Rⁿ` is a Noetherian `R`-module, then `R` satisfies the strong rank condition.
Not an instance for performance reasons.

If `R` is a ring, the assumption is equivalent to `R` being a left-Noetherian ring, but this
is not necessarily the case for semirings: `ℕ` is a Noetherian semiring but `ℕ²` is not a
Noetherian `ℕ`-module. (`ℕ` does satisfy the strong rank condition.)  -/
StrongRankCondition.of_isNoetherian : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] [∀ (n : ℕ), IsNoetherian R (Fin n → R)], StrongRankCondition R
-- Mathlib.Algebra.Group.Basic
sub_add_eq_sub_sub_swap : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b c : α), a - (b + c) = a - c - b
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_sup : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S₁ S₂ : Subsemiring R), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.dist.eq_1 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (x_2 y : X),
  Metric.Sum.dist (Sum.inl x_2) (Sum.inl y) = dist x_2 y
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)]
  {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j)
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)) =
    CategoryTheory.Limits.limit.π G (j, k)
-- Mathlib.Algebra.Homology.Embedding.Extend
ComplexShape.Embedding.instAdditiveHomologicalComplexExtendFunctor : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C], (e.extendFunctor C).Additive
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.contains t.maxKey! = true
-- Mathlib.Algebra.BigOperators.Expect
Finset.exists_ne_zero_of_expect_ne_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} {f : ι → M},
  (s.expect fun i => f i) ≠ 0 → ∃ i ∈ s, f i ≠ 0
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.toAddSubmonoid_strictMono : ∀ {G : Type u_1} [inst : AddGroup G], StrictMono AddSubgroup.toAddSubmonoid
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- The zero morphism maps every pseudoelement to 0.  -/
CategoryTheory.Abelian.Pseudoelement.zero_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C} (Q : C)
  (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply 0 a = 0