mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `i` is an isomorphism such that `i.hom ≫ l = f`, then the cokernel of `f` is a cokernel of
`l`.  -/
CategoryTheory.Limits.cokernel.ofIsoComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            {Z : C} →
              (l : Z ⟶ Y) →
                (i : X ≅ Z) →
                  (h : CategoryTheory.CategoryStruct.comp i.hom l = f) →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.cokernel.π f) ⋯)
-- Batteries.Recycling.RBTree.WF
/-- A balanced tree has the red-red invariant.  -/
RBTree.RBNode.RedRed.balanced : ∀ {p : Prop} {x : Type u_1} {t : RBTree.RBNode x} {c : RBTree.RBColor} {n : ℕ},
  t.Balanced c n → RBTree.RBNode.RedRed p t n
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- Constructor for morphisms to `X.cycles`.  -/
CategoryTheory.Abelian.SpectralObject.liftCycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (n₀ n₁ : ℤ) →
                    (hn₁ : n₀ + 1 = n₁) →
                      {A : C} →
                        (x : A ⟶ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)) →
                          CategoryTheory.CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0 → (A ⟶ X.cycles f g n₀)
-- Std.Data.String.ToNat
String.toNat?_eq_some_ofDigitChars : ∀ {s : String}, s.isNat = true → s.toNat? = some (Nat.ofDigitChars 10 (List.filter (fun x => x != '_') s.toList) 0)
-- Mathlib.Topology.Sheaves.Functors
/-- The pullback of a sheaf by an open embedding `f` is isomorphic to its naive pullback
`IsOpenEmbedding.sheafPullback`, i.e. to the composition by the functor `IsOpenMap.functor f`.
Also, this is an isomorphism of functors.
 -/
Topology.IsOpenEmbedding.sheafPullbackIso : {X Y : TopCat} →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{w, u_1} A] →
      {f : X ⟶ Y} →
        (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) →
          {FA : A → A → Type u_2} →
            {CA : A → Type w} →
              [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
                [inst_2 : CategoryTheory.ConcreteCategory A FA] →
                  [inst_3 : CategoryTheory.Limits.HasColimits A] →
                    [inst_4 : CategoryTheory.Limits.HasLimits A] →
                      [inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] →
                        [inst_6 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] →
                          [inst_7 : (CategoryTheory.forget A).ReflectsIsomorphisms] →
                            TopCat.Sheaf.pullback A f ≅ Topology.IsOpenEmbedding.sheafPullback A hf
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_iff_tendsto : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x ↔
    Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) (nhdsWithin x s) (nhds 0)
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.ofFn.eq_1 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α), Array.ofFn f = Array.ofFn.go✝ f (Array.emptyWithCapacity n) n ⋯
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_apply' : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : Multiplicative M →* A) (f : AddMonoidAlgebra R M),
  ((AddMonoidAlgebra.lift R A M) F) f = f.coeff.sum fun a b => (algebraMap R A) b * F (Multiplicative.ofAdd a)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.Hom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (x_2 y : C), (CategoryTheory.Join.left x_2).Hom (CategoryTheory.Join.left y) = ULift.{v₂, v₁} (x_2 ⟶ y)
-- Mathlib.RingTheory.NormalClosure
Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S],
  FaithfulSMul S
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Init.Data.Range.Polymorphic.UInt
UInt32.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize UInt32
-- Mathlib.GroupTheory.Subgroup.Saturated
Submonoid.PowSaturated.eq_1 : ∀ {G : Type u_1} [inst : Monoid G] (H : Submonoid G), H.PowSaturated = ∀ ⦃n : ℕ⦄ ⦃g : G⦄, g ^ n ∈ H → n = 0 ∨ g ∈ H
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_X₁ : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ) (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃'
        hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).X₁ =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.le_inf_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {β : Type u_5} [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] {s t : Finset α} {f : α → β} {a : β}, a ≤ (s * t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link2.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3) →
      (r : Std.DTreeMap.Internal.Impl α β) →
        (hr : r.Balanced) →
          ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
              r = Std.DTreeMap.Internal.Impl.leaf → motive Std.DTreeMap.Internal.Impl.leaf hr) →
            ((szr : ℕ) →
                (k'' : α) →
                  (v'' : β k'') →
                    (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
                      (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) →
                        r = Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' →
                          motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') hr) →
              motive r hr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negDblY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 = Q 0 * P 2 →
            P 1 * Q 2 ≠ W.negY Q * P 2 →
              W.negDblY P / W.dblZ P =
                W.toAffine.negAddY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                  (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Make a `ContMDiffVectorBundle` from a `ContMDiffVectorPrebundle`.  -/
VectorPrebundle.contMDiffVectorBundle : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle 𝕜 F E) [ha : VectorPrebundle.IsContMDiff IB a n], ContMDiffVectorBundle n F E IB
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_sSup : ∀ {M : Type u_2} [inst : MulOneClass M] (S : Set (Submonoid M)), (sSup S).op = sSup (Submonoid.unop ⁻¹' S)
-- Lean.Parser.Extra
Lean.Parser.patternIgnore.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Sat.CNF.Basic
Std.Sat.CNF.emptyWithCapacity.eq_1 : ∀ {α : Type u_1} (n : ℕ), Std.Sat.CNF.emptyWithCapacity n = { clauses := Array.emptyWithCapacity n }
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- Scalar multiplication of `R ⧸ (I • ⊤)` on `M ⧸ (I • ⊤)`. This is used in order to have
good definitional behaviour for the module instance on adic completions  -/
AdicCompletion.instSMulQuotientIdealHSMulTopSubmodule : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → {M : Type u_3} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → SMul (R ⧸ I • ⊤) (M ⧸ I • ⊤)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (x x_1 : ℕ) (x_2 : x ≤ x_1),
  FirstOrder.Language.BoundedFormula.castLE x_2 FirstOrder.Language.BoundedFormula.falsum =
    FirstOrder.Language.BoundedFormula.falsum
-- Mathlib.Logic.Equiv.Sum
Equiv.sigmaSumDistrib_symm_apply : ∀ {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (a : (i : ι) × α i ⊕ (i : ι) × β i),
  (Equiv.sigmaSumDistrib α β).symm a = Sum.elim (Sigma.map id fun x => Sum.inl) (Sigma.map id fun x => Sum.inr) a
-- Mathlib.Data.Multiset.Bind
Multiset.singleton_join : ∀ {α : Type u_1} (a : Multiset α), {a}.join = a
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- `mapAddGrp` is functorial in the left-exact functor.  -/
CategoryTheory.Functor.mapAddGrpFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            CategoryTheory.Functor (C ⥤ₗ D) (CategoryTheory.Functor (CategoryTheory.AddGrp C) (CategoryTheory.AddGrp D))
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- The box product distributes over the disjoint sum of graphs.  -/
SimpleGraph.Iso.boxProdSumDistrib : {V : Type u_4} →
  {W₁ : Type u_8} →
    {W₂ : Type u_9} →
      (G : SimpleGraph V) → (H₁ : SimpleGraph W₁) → (H₂ : SimpleGraph W₂) → G □ (H₁ ⊕g H₂) ≃g G □ H₁ ⊕g G □ H₂
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Extension of scalars turns an `R`-module into an `S`-module by M ↦ S ⨂ M
 -/
ModuleCat.ExtendScalars.obj' : {R : Type u₁} → {S : Type u₂} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → ModuleCat R → ModuleCat S
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.instIsConvexDist : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P], Convexity.IsConvexDist P
-- Mathlib.Computability.EpsilonNFA
εNFA.isPath_singleton : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {s t : σ} {a : Option α}, M.IsPath s t [a] ↔ t ∈ M.step s a
-- Mathlib.ModelTheory.Syntax
/-- A function to help relabel the variables in bounded formulas.  -/
FirstOrder.Language.BoundedFormula.relabelAux : {α : Type u'} → {β : Type v'} → {n : ℕ} → (α → β ⊕ Fin n) → (k : ℕ) → α ⊕ Fin k → β ⊕ Fin (n + k)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- `bipartiteDoubleCover G` has two vertices `inl v` and `inr v` for each vertex `v` in `G`
such that `inl v` (`inr v`) is adjacent to `inr w` (`inl w`) iff `v` is adjacent to `w` in `G`.  -/
SimpleGraph.bipartiteDoubleCover : {V : Type u_1} → SimpleGraph V → SimpleGraph (V ⊕ V)
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_a_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.AC.Expr) (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_a_cert lhs rhs lhs' rhs' = (lhs.toSeq.beq' lhs').and' (rhs.toSeq.beq' rhs')
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
/-- A simplicial set `X` is nonsingular if for any
nondegenerate simplex `x` (of dimension `n`), the corresponding
morphism `Δ[n] ⟶ X` is a monomorphism.  -/
SSet.Nonsingular : SSet → Prop
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (Topology.WithUpper α)
-- Init.Prelude
instInhabitedList : {α : Type u_1} → Inhabited (List α)
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `TopologicalSpace.generatedBy_le`. -/
deltaGenerated_le : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y},
  TopologicalSpace.generatedBy X ≤ tY
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Given an image factorisation `X ⟶ I ⟶ Y` of an arrow `f`, an isomorphism `I ≅ I'` induces a new
image factorisation `X ⟶ I' ⟶ Y` of `f`.
 -/
CategoryTheory.Limits.ImageFactorisation.ofIsoI : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (F : CategoryTheory.Limits.ImageFactorisation f) →
          {I' : C} → (F.F.I ≅ I') → CategoryTheory.Limits.ImageFactorisation f
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.IsColimit.fac : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F}
  (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β),
  CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) = f i
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_eq_one_iff : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.relrank B = 1 ↔ B ≤ A
-- Init.Prelude
/-- Extracts a wrapped proof or value from a universe-lifted proposition or type.  -/
PLift.down : {α : Sort u} → PLift α → α
-- Mathlib.Computability.DFA
DFA.instInhabited : {α : Type u} → {σ : Type v} → [Inhabited σ] → Inhabited (DFA α σ)
-- Mathlib.Data.Finsupp.MonomialOrder
/-- The lexicographic order on `σ →₀ ℕ`, as a `MonomialOrder`  -/
MonomialOrder.lex : {σ : Type u_1} → [inst : LinearOrder σ] → [WellFoundedGT σ] → MonomialOrder σ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₁₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (self : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp self.v₁₂ self.v₂₃ = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM),
  PresheafOfModules.ModuleColimit.map hcR hcM hcM (CategoryTheory.CategoryStruct.id M) = LinearMap.id
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f g : A ⟶ B),
  f = g ↔ f.left = g.left
-- Mathlib.Combinatorics.Graph.Maps
Graph.vertexSet_map : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} (f : α → α') (G : Graph α β),
  (Graph.map f G).vertexSet = f '' G.vertexSet
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.gcdB_zero_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {s : R}, EuclideanDomain.gcdB 0 s = 1
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.biUnion_op_smul_finset : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidableEq α] (s t : Finset α),
  (t.biUnion fun a => MulOpposite.op a • s) = s * t
-- Mathlib.Topology.Instances.Irrational
/-- **Alias** of `IsGδ.setOfPred_irrational`. -/
IsGδ.setOf_irrational : IsGδ {x | Irrational x}
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- If `b ≤ a`, given the trajectory up to time `a`, the trajectory up to time `b` is
deterministic and is equal to the restriction of the trajectory up to time `a`.  -/
ProbabilityTheory.Kernel.partialTraj_le : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} (hba : b ≤ a),
  ProbabilityTheory.Kernel.partialTraj κ a b = ProbabilityTheory.Kernel.deterministic (Preorder.frestrictLe₂ hba) ⋯
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- This is the natural linear isometry induced by `f : E ≃ₗᵢ F`.  -/
LinearIsometry.rTensor : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      (G : Type u_4) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : InnerProductSpace 𝕜 F] →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : InnerProductSpace 𝕜 G] → (E →ₗᵢ[𝕜] F) → TensorProduct 𝕜 E G →ₗᵢ[𝕜] TensorProduct 𝕜 F G
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_eq : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R)
  [inst_1 : Decidable (f = 0)], m.withBotDegree f = if f = 0 then ⊥ else ↑(m.degree f)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.ne_intCast : ∀ (z : UpperHalfPlane) (n : ℤ), ↑z ≠ ↑n
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.pullback_monoidHom_def : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : R1Space α] [inst_2 : Group α]
  [inst_3 : TopologicalSpace β] [inst_4 : R1Space β] [inst_5 : Group β] [inst_6 : ContinuousMul β]
  [inst_7 : NormedAddCommGroup γ] {φ : α →* β} (hφ : Topology.IsClosedEmbedding ⇑φ)
  (f : CompactlySupportedContinuousMap β γ) (b : β) (a : α),
  (CompactlySupportedContinuousMap.pullback_monoidHom hφ f b) a = f (b * φ a)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X)
      ((F.map h).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app X)
        ((F.mapComp g h).hom.toNatTrans.app ((F.map f).toFunctor.obj X)))
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_map : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {A : DiscreteQuotient X} {B B' : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (h : B ≤ B')
  (a : Quotient A.toSetoid), DiscreteQuotient.ofLE h (DiscreteQuotient.map f cond a) = DiscreteQuotient.map f ⋯ a
-- Mathlib.Order.BoundedOrder.Basic
/-- Pullback an `OrderBot`.  -/
OrderBot.lift : {α : Type u} →
  {β : Type v} →
    [inst : LE α] →
      [inst_1 : Bot α] →
        [inst_2 : LE β] → [inst_3 : OrderBot β] → (f : α → β) → (∀ (b a : α), f b ≤ f a → b ≤ a) → f ⊥ = ⊥ → OrderBot α
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.match_3.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Zipper α β → Sort u_3)
  (es : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (z' : Lean.PersistentHashMap.Zipper α β) (h_1 : Unit → motive Lean.PersistentHashMap.Zipper.done)
  (h_2 :
    (es : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      (z' : Lean.PersistentHashMap.Zipper α β) → motive (Lean.PersistentHashMap.Zipper.consEntries es z'))
  (h_3 :
    (keys : Subarray α) →
      (vals : Subarray β) →
        (hsz : Std.Slice.size keys = Std.Slice.size vals) →
          (z' : Lean.PersistentHashMap.Zipper α β) →
            motive (Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z')),
  (match Lean.PersistentHashMap.Zipper.consEntries es z' with
    | Lean.PersistentHashMap.Zipper.done => h_1 ()
    | Lean.PersistentHashMap.Zipper.consEntries es z' => h_2 es z'
    | Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z' => h_3 keys vals hsz z') =
    h_2 es z'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {V W X Y : C} (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) {Z : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f g)
        (CategoryTheory.CategoryStruct.comp f h))
      h_1
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_le_degrees_card : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R), p.totalDegree ≤ p.degrees.card
-- Mathlib.Algebra.GroupWithZero.Center
/-- In a group with zero, the center of the units is the preimage of the center.  -/
Set.center_units_eq : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀], Set.center G₀ˣ = Units.val ⁻¹' Set.center G₀
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
instAddActionSubtypeMemAddSubgroupStabilizerSetElem.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] (s : Set α),
  instAddActionSubtypeMemAddSubgroupStabilizerSetElem G α s =
    { toVAdd := VAdd.ofStabilizer G α s, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.RingTheory.KrullDimension.PID
IsPrincipalIdealRing.ringKrullDim_eq_one : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R], ¬IsField R → ringKrullDim R = 1
-- Init.Data.UInt.Lemmas
UInt64.ofFin_div : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a / b) = UInt64.ofFin a / UInt64.ofFin b
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallMax : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P]
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)