mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.π_tensor_id_actRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))
        T.X)
      (Bimod.TensorBimod.actRight P Q) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X Q.X T.X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actRight)
        (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.instDecidableEqWalkingParallelPair : DecidableEq CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.withBotCoe : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.IsSuccLimit x → Order.IsSuccLimit ↑x
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Typecheck an object of `C` as an object of `ForgetEnrichment W C`.  -/
CategoryTheory.ForgetEnrichment.of : {C : Type u₁} →
  (W : Type v) →
    [inst : CategoryTheory.Category.{w, v} W] →
      [inst_1 : CategoryTheory.MonoidalCategory W] →
        [inst_2 : CategoryTheory.EnrichedCategory W C] → C → CategoryTheory.ForgetEnrichment W C
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.limitCompYonedaIsoCocone_hom : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (X : C),
  (CategoryTheory.Limits.limitCompYonedaIsoCocone F X).hom =
    TypeCat.ofHom fun a =>
      {
        app := fun j =>
          (CategoryTheory.ConcreteCategory.hom
              (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj X)) (Opposite.op j)))
            a,
        naturality := ⋯ }
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.LeapSecond.mk : ℤ → ℤ → Std.Time.TimeZone.TZif.LeapSecond
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.instCompleteSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} [CompleteSpace β],
  CompleteSpace (UniformOnFun α β 𝔖)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.PreSubmersivePresentation.cotangentComplexAux_apply : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.PreSubmersivePresentation R S ι σ) (x : ↥P.ker) (i : σ),
  P.cotangentComplexAux (Algebra.Extension.Cotangent.mk x) i =
    (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) ↑x)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.hp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (self : W₁.FunctorialFactorizationData W₂) (f : CategoryTheory.Arrow C), W₂ (self.p.app f)
-- Mathlib.RingTheory.Bialgebra.Quotient
Bialgebra.Quotient.counit_mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Bialgebra R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : (Submodule.restrictScalars R I).IsCoideal] (a : A),
  CoalgebraStruct.counit ((Ideal.Quotient.mk I) a) = CoalgebraStruct.counit a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_comp_isoCocycles₁_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ 1) (groupCohomology.isoCocycles₁ B).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).hom (groupCohomology.mapCocycles₁ f φ)
-- Mathlib.Algebra.Group.Defs
/-- Zero is a right neutral element for addition  -/
AddZeroClass.add_zero : ∀ {M : Type u} [self : AddZeroClass M] (a : M), a + 0 = a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The quotient map from the 2-cycles of `A`, as a submodule of `G × G →₀ A`, to `H₂(G, A)`.  -/
groupHomology.H2π : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ModuleCat.of k ↥(groupHomology.cycles₂ A) ⟶ groupHomology.H2 A
-- Mathlib.Algebra.Ring.Semireal.Defs
/-- Linearly ordered semirings with the property `a ≤ b → ∃ c, a + c = b` (e.g. `ℕ`)
are semireal.
 -/
instIsSemirealOfIsStrictOrderedRingOfExistsAddOfLE : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R], IsSemireal R
-- Mathlib.Order.Heyting.Hom
HeytingHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
  [inst_2 : HeytingAlgebra γ] {f : HeytingHom α β} {g₁ g₂ : HeytingHom β γ},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.natCast_add : ∀ {R : Type u_1} [inst : CommSemiring R] {b₁ b₂ : R} {a₁ a₂ : ℕ}, ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂
-- Mathlib.Algebra.Algebra.Defs
Algebra.toSMul : {R : Type u} → {A : Type v} → {inst : CommSemiring R} → {inst_1 : Semiring A} → [self : Algebra R A] → SMul R A
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The trifunctor `F (- ⊗ (- ⊗ -))`  -/
CategoryTheory.MonoidalCategory.curriedTensorPostPost' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C D))
-- Mathlib.Analysis.Analytic.Constructions
/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic.  -/
AnalyticOnNhd.mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f g : E → A}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 g s → AnalyticOnNhd 𝕜 (fun x => f x * g x) s
-- Mathlib.Algebra.GroupWithZero.Defs
IsCancelMulZero.toIsLeftCancelMulZero : ∀ {M₀ : Type u} {inst : Mul M₀} {inst_1 : Zero M₀} [self : IsCancelMulZero M₀], IsLeftCancelMulZero M₀
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_indep_iff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {I : Set α} {N : Matroid β},
  Set.InjOn f (f ⁻¹' N.E) → ((N.comap f).Indep I ↔ N.Indep (f '' I))
-- Mathlib.Computability.Primrec.List
Primrec.list_append : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ fun x1 x2 => x1 ++ x2
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) {i : Fin n},
  snf.bM.coord (snf.f i) ∘ₗ N.subtype = snf.a i • snf.bN.coord i
-- Mathlib.Data.List.Sym
_private.Mathlib.Data.List.Sym.0.List.sym2.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_1 ()
-- Aesop.Forward.State
Aesop.ForwardState.mk.injEq : ∀ (ruleStates : Lean.PHashMap Aesop.RuleName Aesop.RuleState)
  (hyps : Lean.PHashMap Lean.FVarId (Lean.PArray (Aesop.RuleName × Aesop.PremiseIndex)))
  (patSubsts : Lean.PHashMap Aesop.PatSubstSource (Lean.PArray (Aesop.RuleName × Aesop.Substitution)))
  (ruleStates_1 : Lean.PHashMap Aesop.RuleName Aesop.RuleState)
  (hyps_1 : Lean.PHashMap Lean.FVarId (Lean.PArray (Aesop.RuleName × Aesop.PremiseIndex)))
  (patSubsts_1 : Lean.PHashMap Aesop.PatSubstSource (Lean.PArray (Aesop.RuleName × Aesop.Substitution))),
  ({ ruleStates := ruleStates, hyps := hyps, patSubsts := patSubsts } =
      { ruleStates := ruleStates_1, hyps := hyps_1, patSubsts := patSubsts_1 }) =
    (ruleStates = ruleStates_1 ∧ hyps = hyps_1 ∧ patSubsts = patSubsts_1)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_zero' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε], MeasureTheory.eLpNorm (fun x => 0) p μ = 0
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.HasArgminEstimator.exists_isArgminEstimator : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [inst : StandardBorelSpace Θ]
  [inst_1 : Nonempty Θ] {𝓨 : Type u_4} [inst_2 : MeasurableSpace 𝓨] {ℓ : Θ → 𝓨 → ENNReal}
  {P : ProbabilityTheory.Kernel Θ 𝓧} [inst_3 : ProbabilityTheory.IsFiniteKernel P] {π : MeasureTheory.Measure Θ}
  [inst_4 : MeasureTheory.IsFiniteMeasure π],
  ProbabilityTheory.HasArgminEstimator ℓ P π → ∃ f, ProbabilityTheory.IsArgminEstimator ℓ P π f
-- Init.Grind.Ring.Basic
/-- Addition is associative.  -/
Lean.Grind.Semiring.add_assoc : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a b c : α), a + b + c = a + (b + c)
-- Mathlib.Control.Traversable.Basic
/-- An `ApplicativeTransformation` preserves `pure`.  -/
ApplicativeTransformation.preserves_pure' : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (self : ApplicativeTransformation F G) {α : Type u} (x : α), self.app α (pure x) = pure x
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- `WithLp.equiv` as a uniform isomorphism.  -/
PiLp.uniformEquiv : (p : ENNReal) →
  {ι : Type u_2} → (β : ι → Type u_4) → [inst : (i : ι) → UniformSpace (β i)] → PiLp p β ≃ᵤ ((i : ι) → β i)
-- Mathlib.Order.Preorder.Chain
IsMaxChain.image : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {c : Set α},
  IsMaxChain r c → IsMaxChain s (⇑e '' c)
-- Init.Data.List.Control
List.forIn_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m (ForInStep β)} {b : β},
  forIn [] b f = pure b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {l : List α} {k : α}, k ∈ t → (t.insertManyIfNewUnit l).getKey! k = t.getKey! k
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `lt_div_iff₀` for a version with multiplication on the other side.  -/
lt_div_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (a < b / c ↔ c * a < b)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- The canonical map induced by `truncTotal` from multivariate power series to
the quotient ring of multivariate polynomials by the `n`-th power of
the ideal spanned by all variables.  -/
MvPowerSeries.truncTotalAlgHom : (σ : Type u_3) →
  (R : Type u_4) →
    [Finite σ] →
      [inst : CommRing R] →
        (n : ℕ) → MvPowerSeries σ R →ₐ[MvPolynomial σ R] MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.diagonal_apply : ∀ {α : Type u_5} {ι : Type u_6} [inst : Nonempty ι] (x : α), ↑(Combinatorics.Line.diagonal α ι) x = fun x_1 => x
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F] (i : I)
  {Z : CategoryTheory.Functor C (Type u₂)} (h : CategoryTheory.coyoneda.obj (F.rightOp.obj i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op) h
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- the rank function  -/
SSet.Subcomplex.Pairing.RankFunction.rank : {X : SSet} →
  {A : X.Subcomplex} → {P : A.Pairing} → {α : Type v} → [inst : PartialOrder α] → P.RankFunction α → ↑P.II → α
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instSFiniteProdVolume : ∀ {α : Type u_4} {β : Type u_5} [inst : MeasureTheory.MeasureSpace α] [MeasureTheory.SFinite MeasureTheory.volume]
  [inst_2 : MeasureTheory.MeasureSpace β] [MeasureTheory.SFinite MeasureTheory.volume],
  MeasureTheory.SFinite MeasureTheory.volume
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.anyM_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.anyM p it = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' x => do
        let __do_lift ← p x
        if __do_lift.down = true then pure { down := true } else Std.IterM.anyM p it'
      | Std.IterStep.skip it' => Std.IterM.anyM p it'
      | Std.IterStep.done => pure { down := false }
-- Init.Data.List.MinMaxIdx
List.minIdxOn_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[i] ≤ f xs[j]) → List.minIdxOn f xs h ≤ i
-- Mathlib.Control.ULift
/-- Applicative sequencing.  -/
PLift.seq : {α : Sort u} → {β : Sort v} → PLift (α → β) → (Unit → PLift α) → PLift β
-- Mathlib.Topology.MetricSpace.Algebra
NNReal.isBoundedSMul : IsBoundedSMul NNReal NNReal
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_symm_coe_above : ∀ {n : ℕ} {i : Fin (n + 1)} {m : Fin n}, i ≤ m.castSucc → (finSuccEquiv' i).symm (some m) = m.succ
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.isCompl_range_lmapDomain_span : ∀ {R : Type u_1} {ι : Type u_3} [inst : Semiring R] {α : Type u_4} {β : Type u_5} {u : α → ι} {v : β → ι},
  IsCompl (Set.range u) (Set.range v) →
    IsCompl (Finsupp.lmapDomain R R u).range (Submodule.span R (Set.range fun x => fun₀ | v x => 1))
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Reindexing a simplex along an `Equiv` of index types does not change the circumradius.  -/
Affine.Simplex.circumradius_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P m) (e : Fin (m + 1) ≃ Fin (n + 1)),
  (s.reindex e).circumradius = s.circumradius
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.forget_map : ∀ {X Y : PartOrdEmb} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget PartOrdEmb).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Combinatorics.SimpleGraph.Girth
/-- The girth of a simple graph is the length of its smallest cycle, or junk value `0` if the graph is
acyclic.
 -/
SimpleGraph.girth : {α : Type u_1} → SimpleGraph α → ℕ
-- Mathlib.Data.Stream.Init
Stream'.take_succ : ∀ {α : Type u} (n : ℕ) (s : Stream' α), Stream'.take n.succ s = s.head :: Stream'.take n s.tail
-- Mathlib.Order.Max
IsTop.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsTop x → IsTop x.1
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.pow_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g s → ∀ (n : ℕ), MonovaryOn (f ^ n) g s
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Flattening nested `iConvexComb`s.

See `iConvexComb_assoc''` for a more dependent version, and `iConvexComb_assoc`
for a less dependent one.  -/
Convexity.iConvexComb_assoc' : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {J : Type u_9} (s : Convexity.StdSimplex R I)
  (f : I → Convexity.StdSimplex R J) (g : I → J → M),
  (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) (g i)) =
    Convexity.iConvexComb (Convexity.iConvexComb s fun i => Convexity.StdSimplex.map (fun x => (i, x)) (f i))
      (Function.uncurry g)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  v 0 = 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def
/-- The predicate `HasGaussianLaw X P` means that under the measure `P`,
`X` has a Gaussian distribution.  -/
ProbabilityTheory.HasGaussianLaw : {Ω : Type u_1} →
  {E : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      [TopologicalSpace E] →
        [inst : AddCommMonoid E] → [Module ℝ E] → [mE : MeasurableSpace E] → (Ω → E) → MeasureTheory.Measure Ω → Prop
-- Mathlib.Order.Basic
Prod.mk_lt_mk_of_le_of_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b₁ b₂ : β},
  a₁ ≤ a₂ → b₁ < b₂ → (a₁, b₁) < (a₂, b₂)
-- Mathlib.Util.WithWeakNamespace
/-- Changes the current namespace without causing scoped things to go out of scope  -/
Lean.Elab.Command.withWeakNamespace : {α : Type} → Lean.Name → Lean.Elab.Command.CommandElabM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Reachable.coe_toSubgraph : ∀ {V : Type u} {G H : SimpleGraph V} {u v : V} (h : H ≤ G),
  H.Reachable u v → (SimpleGraph.toSubgraph H h).coe.Reachable ⟨u, trivial⟩ ⟨v, trivial⟩
-- Mathlib.Analysis.Normed.Module.Basic
NontriviallyNormedField.cobounded_neBot : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜], (Bornology.cobounded 𝕜).NeBot
-- Std.Sync.CancellationToken
/-- Custom cancellation reason
 -/
Std.CancellationReason.custom : String → Std.CancellationReason
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg.injEq : ∀ (e : Lean.Expr) (p : Int.Internal.Linear.Poly) (e_1 : Lean.Expr) (p_1 : Int.Internal.Linear.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg e p = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg e_1 p_1) =
    (e = e_1 ∧ p = p_1)
-- Mathlib.Data.Fintype.Card
List.Nodup.length_le_card : ∀ {α : Type u_4} [inst : Fintype α] {l : List α}, l.Nodup → l.length ≤ Fintype.card α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go input distance curr hcurr s).get idx ⋯ = s.get idx hidx
-- Init.Data.UInt.Basic
/-- Decides whether one 16-bit unsigned integer is less than or equal to another. Usually accessed via the
`DecidableLE UInt16` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (15 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : UInt16) ≤ 5 then "yes" else "no") = "no"`
 * `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
 * `show (7 : UInt16) ≤ 7 by decide`
 -/
UInt16.decLe : (a b : UInt16) → Decidable (a ≤ b)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.fst.eq_1 : ∀ (M : Type u_1) (α : Type u_2) (β : Type u_3) [inst : VAdd M α] [inst_1 : VAdd M β],
  AddActionHom.fst M α β = { toFun := Prod.fst, map_vadd' := ⋯ }
-- Init.Data.FloatArray.Basic
FloatArray.instGetElemNatFloatLtSize : GetElem FloatArray ℕ Float fun xs i => i < xs.size
-- Mathlib.Algebra.Order.Hom.Ring
/-- The proposition that the function preserves the order bijectively.  -/
OrderRingIso.map_le_map_iff' : ∀ {α : Type u_6} {β : Type u_7} [inst : Mul α] [inst_1 : Add α] [inst_2 : Mul β] [inst_3 : Add β] [inst_4 : LE α]
  [inst_5 : LE β] (self : α ≃+*o β) {a b : α}, self.toFun a ≤ self.toFun b ↔ a ≤ b
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.get!_eq_getValueCast! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} [inst_3 : Inhabited (β a)],
      m.get! a = Std.Internal.List.getValueCast! a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Lean.Meta.Sym.Arith.Types
/-- `CommSemiring` instance for `type`  -/
Lean.Meta.Sym.Arith.CommSemiring.commSemiringInst : Lean.Meta.Sym.Arith.CommSemiring → Lean.Expr
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.eq_zero_iff_of_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a b : α},
      a ∈ s →
        b ∈ s →
          b ≤ a →
            (variationOnFromTo f s a b = 0 ↔
              ∀ ⦃x : α⦄, x ∈ s ∩ Set.Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Set.Icc b a → edist (f x) (f y) = 0)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.hasSum_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} (e : γ ≃ β), HasSum (f ∘ ⇑e) a ↔ HasSum f a
-- Lean.Meta.Tactic.Assert
Lean.Meta.AssertAfterResult.fvarId : Lean.Meta.AssertAfterResult → Lean.FVarId
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.mk.inj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {X₁ : C₁}
  {w : X₂ ⟶ Φ.functor.obj X₁} {hw : W₂ w} {X₁_1 : C₁} {w_1 : X₂ ⟶ Φ.functor.obj X₁_1} {hw_1 : W₂ w_1},
  { X₁ := X₁, w := w, hw := hw } = { X₁ := X₁_1, w := w_1, hw := hw_1 } → X₁ = X₁_1 ∧ w ≍ w_1
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_pi : ∀ {ι : Type u} (α : ι → Type v), Cardinal.mk ((i : ι) → α i) = Cardinal.prod fun i => Cardinal.mk (α i)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_indep_sdiff_iff : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis I X → ((M.contract X).Indep (J \ X) ↔ M.Indep (J \ X ∪ I))