mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Rat.Init
/-- Nonnegative rational numbers.  -/
«termℚ≥0» : Lean.ParserDescr
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
List.prod_map_lt_prod_map : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R]
  [NeZero 1] {ι : Type u_2} {s : List ι},
  s ≠ [] → ∀ (f g : ι → R), (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, f i < g i) → (List.map f s).prod < (List.map g s).prod
-- Mathlib.Topology.CompactOpen
/-- Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.
 -/
ContinuousMap.compRightContinuousMap : {X : Type u_2} →
  {Y : Type u_3} →
    (Z : Type u_4) →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : TopologicalSpace Z] → C(X, Y) → C(C(Y, Z), C(X, Z))
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.recordTriedSimpTheorem : Lean.Meta.Origin → Lean.Meta.SimpM Unit
-- Init.Data.List.Basic
/-- Pads `l : List α` on the left with repeated occurrences of `a : α` until it is of length `n`. If `l`
already has at least `n` elements, it is returned unmodified.

This is a tail-recursive version of `List.leftpad`, used at runtime.

Examples:
 * `[1, 2, 3].leftPadTR 5 0 = [0, 0, 1, 2, 3]`
 * `["red", "green", "blue"].leftPadTR 4 "blank" = ["blank", "red", "green", "blue"]`
 * `["red", "green", "blue"].leftPadTR 3 "blank" = ["red", "green", "blue"]`
 * `["red", "green", "blue"].leftPadTR 1 "blank" = ["red", "green", "blue"]`
 -/
List.leftpadTR : {α : Type u} → ℕ → α → List α → List α
-- Init.Data.String.Subslice
/-- Constructs a subslice of `s` given the bounds of the subslice. If the subslice would be
degenerate, this function panics.
 -/
String.Slice.subslice! : (s : String.Slice) → s.Pos → s.Pos → s.Subslice
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_le_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  BddBelow t → s.Nonempty → s ⊆ t → sInf t ≤ sInf s
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- The `δ`-thickened indicator of a set `E` is the function that equals `1` on `E`
and `0` outside a `δ`-thickening of `E` and interpolates (continuously) between
these values using `infEDist _ E`.

`thickenedIndicatorAux` is the unbundled `ℝ≥0∞`-valued function. See `thickenedIndicator`
for the (bundled) bounded continuous function with `ℝ≥0`-values.  -/
thickenedIndicatorAux : {α : Type u_1} → [PseudoEMetricSpace α] → ℝ → Set α → α → ENNReal
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- When two right extensions `α₁ : RightExtension L F₁` and `α₂ : RightExtension L F₂`
are essentially the same via an isomorphism of functors `F₁ ≅ F₂`,
then `α₁` is universal iff `α₂` is.  -/
CategoryTheory.Functor.RightExtension.isUniversalEquivOfIso₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            {L : CategoryTheory.Functor C D} →
              {F₁ F₂ : CategoryTheory.Functor C H} →
                (α₁ : L.RightExtension F₁) →
                  (α₂ : L.RightExtension F₂) →
                    (e : F₁ ≅ F₂) →
                      (e' : CategoryTheory.CostructuredArrow.left α₁ ≅ CategoryTheory.CostructuredArrow.left α₂) →
                        CategoryTheory.CategoryStruct.comp (L.whiskerLeft e'.hom)
                              (CategoryTheory.CostructuredArrow.hom α₂) =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.CostructuredArrow.hom α₁) e.hom →
                          CategoryTheory.CostructuredArrow.IsUniversal α₁ ≃
                            CategoryTheory.CostructuredArrow.IsUniversal α₂
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexFinsetRange_repr : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [inst_3 : Fintype ι] [inst_4 : DecidableEq M] (x : M) (i : ι)
  (h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯), (b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_torsionBySet_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Submodule.torsionBySet R (↥(Submodule.torsionBySet R M s)) s = ⊤
-- Mathlib.Algebra.Group.Subsemigroup.Membership
/-- An induction principle for elements of `⨆ i, S i`. If `C` holds all
elements of `S i` for all `i`, and is preserved under addition, then it holds for all elements of
the supremum of `S`.  -/
AddSubsemigroup.iSup_induction : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup M) {C : M → Prop} {x₁ : M},
  x₁ ∈ ⨆ i, S i → (∀ (i : ι), ∀ x₂ ∈ S i, C x₂) → (∀ (x y : M), C x → C y → C (x + y)) → C x₁
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- An image map is a morphism `image f → image g` fitting into a commutative square and satisfying
the obvious commutativity conditions.  -/
CategoryTheory.Limits.ImageMap.map_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  (self : CategoryTheory.Limits.ImageMap sq),
  CategoryTheory.CategoryStruct.comp self.map (CategoryTheory.Limits.image.ι g.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq)
-- Mathlib.Order.Interval.Set.Union
/-- Union of consecutive intervals contains the interval defined by the initial and final points.  -/
Ioc_subset_biUnion_Ioc : ∀ {X : Type u_1} [inst : LinearOrder X] (N : ℕ) (a : ℕ → X),
  Set.Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Set.Ioc (a i) (a (i + 1))
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.ofBool_eq_if : ∀ (b : Bool), BitVec.ofBool b = bif b then 1#1 else 0#1
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.QuasiCompact f] (x : ↥Y),
  AlgebraicGeometry.IsFinite (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f x)
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_of_lt : ∀ {n k : ℕ} (h : k < n), (finRotate (n + 1)) ⟨k, ⋯⟩ = ⟨k + 1, ⋯⟩
-- Mathlib.Order.Ideal
Order.Cofinal.instInhabited : {P : Type u_1} → [inst : Preorder P] → Inhabited (Order.Cofinal P)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instMulQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → (c : RingCon R) → Mul c.Quotient
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_log_b_mul_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < Real.log (b i * ↑n)
-- Mathlib.Algebra.Category.MonCat.Shrink
MonCat.shrinkFunctor_obj_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C MonCat)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] (X : C),
  ↑((MonCat.shrinkFunctor.{w, w', v, u} F).obj X) = Shrink.{w, w'} ↑(F.obj X)
-- Mathlib.Algebra.Group.Units.Defs
/-- An element `a : M` of a `Monoid` is a unit if it has a two-sided inverse.
The actual definition says that `a` is equal to some `u : Mˣ`, where
`Mˣ` is a bundled version of `IsUnit`.  -/
IsUnit : {M : Type u_1} → [Monoid M] → M → Prop
-- Mathlib.Tactic.FunProp.Types
/-- Get predicate on names indicating whether they should be unfolded.  -/
Mathlib.Meta.FunProp.unfoldNamePred : Mathlib.Meta.FunProp.FunPropM (Lean.Name → Bool)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instLEInftyOfNatWithTopENat_1 : ENat.LEInfty 1
-- Mathlib.Util.Notation3
/-- Matcher for an expression satisfying a given predicate.  -/
Mathlib.Notation3.matchExpr : (Lean.Expr → Bool) → Mathlib.Notation3.Matcher
-- Init.Data.Array.Find
Array.find?_replicate_of_pos : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α},
  p a = true → Array.find? p (Array.replicate n a) = if n = 0 then none else some a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The chosen kernels and cokernels of the limits API give a `LeftHomologyData`  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : CategoryTheory.Limits.HasKernel S.g] →
          [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)] → S.LeftHomologyData
-- Lean.Elab.Tactic.Induction
/-- The code path shared between `induction` and `fun_induct`; when we already have an `elimInfo`
and the `targets` contains the implicit targets
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.evalInductionCore : Lean.Syntax →
  Lean.Meta.ElimInfo → Array Lean.Expr → optParam (Array (Lean.Ident × Lean.FVarId)) #[] → Lean.Elab.Tactic.TacticM Unit
-- Std.Data.ExtTreeMap.Basic
/-- Updates the values of the map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.ExtTreeMap.filterMap : {α : Type u} →
  {β : Type v} →
    {γ : Type w} → {cmp : α → α → Ordering} → (α → β → Option γ) → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α γ cmp
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ≅ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.hom)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.inv) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Algebra.GradedMonoid
SetLike.GradeZero.coe_pow : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  {A : ι → S} [inst_3 : SetLike.GradedMonoid A] (a : ↥(A 0)) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- The functorial map taking `ψ : A →⋆ₐ[ℂ] B` to a continuous function
`characterSpace ℂ B → characterSpace ℂ A` obtained by pre-composition with `ψ`.  -/
WeakDual.CharacterSpace.compContinuousMap : {A : Type u_1} →
  {B : Type u_2} →
    {𝕜 : Type u_4} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedRing A] →
          [inst_2 : NormedAlgebra 𝕜 A] →
            [CompleteSpace A] →
              [inst_4 : StarRing A] →
                [inst_5 : NormedRing B] →
                  [inst_6 : NormedAlgebra 𝕜 B] →
                    [CompleteSpace B] →
                      [inst_8 : StarRing B] →
                        (A →⋆ₐ[𝕜] B) → C(↑(WeakDual.characterSpace 𝕜 B), ↑(WeakDual.characterSpace 𝕜 A))
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson.eq_2 : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R), Polynomial.dickson k a 1 = Polynomial.X
-- Mathlib.Data.Rel
/-- A relation `R` is transitive if `a ~[R] b` and `b ~[R] c` together imply `a ~[R] c`.  -/
SetRel.IsTrans : {α : Type u_1} → SetRel α α → Prop
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Hom_def : ∀ (J : Type u_1) [inst : LinearOrder J] (i j : CategoryTheory.SimplicialThickening J),
  (i ⟶[SSet] j) = CategoryTheory.nerve (i ⟶ j)
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.isLocalization_of_algEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : Algebra R P] [IsLocalization M S]
  (h : S ≃ₐ[R] P), IsLocalization M P
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonParameterInformation.toJson : Lean.Lsp.ParameterInformation → Lean.Json
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order_eq_order : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, φ.order = MvPowerSeries.order φ
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R) {Z : CommRingCat}
  (h : (S.mkUnder (TensorProduct ↑R ↑S ↑A.right)).right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom (CommRingCat.ofHom (algebraMap ↑R ↑S)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Under.Hom.right (CommRingCat.tensorProdObjIsoPushoutObj S A).inv) h) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom) h
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_mul_right_one : ∀ {α : Type u_2} [inst : Group α] {b : α}, (fun x => x * b) ⁻¹' 1 = {b⁻¹}
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instTop : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → Top (TwoSidedIdeal R)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_maxKey!_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → (cmp k t.maxKey!).isLE = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback : β a},
      (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {x : A}, x ∈ Subalgebra.toSubmodule S ↔ x ∈ S
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.PatternArgKind.relevant.sizeOf_spec : sizeOf Lean.Meta.Grind.NormalizePattern.PatternArgKind.relevant = 1
-- Mathlib.Data.Ordmap.Invariants
Ordnode.equiv_iff : ∀ {α : Type u_1} {t₁ t₂ : Ordnode α}, t₁.Sized → t₂.Sized → (t₁.Equiv t₂ ↔ t₁.toList = t₂.toList)
-- Mathlib.Order.Hom.Bounded
TopHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β] (f : TopHom α β), f.comp (TopHom.id α) = f
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_Iic : ∀ (a : ℝ), Real.exp '' Set.Iic a = Set.Ioc 0 (Real.exp a)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.subgroup_eq_bot : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  FiniteMulArchimedeanClass.subgroup ⊤ = ⊥
-- Mathlib.Order.SetIsMax
Set.not_isMin_coe : ∀ {J : Type u} [inst : Preorder J] {S : Set J} (m : ↑S), ¬IsMin m → ¬IsMin ↑m
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffOn_one : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {s : Set M} {n : WithTop ℕ∞}
  [inst_11 : One M'], ContMDiffOn I I' n 1 s
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instBEqFunIndParamKind.beq : Lean.Meta.FunIndParamKind → Lean.Meta.FunIndParamKind → Bool
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
EisensteinSeries.G2_T_transform : SlashAction.map 2 ModularGroup.T EisensteinSeries.G2 = EisensteinSeries.G2
-- Init.Data.SInt.Bitwise
ISize.toInt8_xor : ∀ (a b : ISize), (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
-- Init.GetElem
get_getElem? : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [inst_1 : LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [inst_2 : Decidable (dom c i)]
  (h : c[i]?.isSome = true), c[i]?.get h = c[i]
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instAlgebraSubtypeMemOfNat : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} →
                  [inst_5 : GradedRing 𝒜] → {x : Submonoid A} → Algebra (↥(𝒜 0)) (HomogeneousLocalization 𝒜 x)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C) {X Y : C} (f : Y ⟶ X)
  {S : CategoryTheory.Sieve X}, K.Saturate X S → K.Saturate Y (CategoryTheory.Sieve.pullback f S)
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeAddMonoid.symbols_of : ∀ {α : Type u_1} [inst : DecidableEq α] {m : α}, (FreeAddMonoid.of m).symbols = {m}
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The first homotopy group at `x` is isomorphic to the fundamental group.  -/
HomotopyGroup.pi1MulEquivFundamentalGroup : {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → HomotopyGroup.Pi 1 X x ≃* FundamentalGroup X x
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsZeroOrMarkovKernel κ]
  (η : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsZeroOrMarkovKernel η],
  ProbabilityTheory.IsZeroOrMarkovKernel (η.comp κ)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.mk.inj : ∀ {K : Type u_1} {V : Type u_2} {inst : DivisionRing K} {inst_1 : AddCommGroup V} {inst_2 : Module K V}
  {carrier : Set (Projectivization K V)}
  {mem_add' :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier →
        Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier}
  {carrier_1 : Set (Projectivization K V)}
  {mem_add'_1 :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier_1 →
        Projectivization.mk K w hw ∈ carrier_1 → Projectivization.mk K (v + w) hvw ∈ carrier_1},
  { carrier := carrier, mem_add' := mem_add' } = { carrier := carrier_1, mem_add' := mem_add'_1 } → carrier = carrier_1
-- Init.Data.Array.MapIdx
Array.toList_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β},
  (xs.mapFinIdx f).toList = xs.toList.mapFinIdx fun i a h => f i a h
-- Mathlib.Order.Filter.Basic
Filter.mem_inf_of_left : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ f → s ∈ f ⊓ g
-- Lean.PrettyPrinter.Parenthesizer
/-- Execute `x` at the right-most child of the current node, if any, then advance to the left.  -/
Lean.PrettyPrinter.Parenthesizer.visitArgs : Lean.PrettyPrinter.ParenthesizerM Unit → Lean.PrettyPrinter.ParenthesizerM Unit
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
tprod_eq_of_multipliable_unconditional : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  [T2Space α] [L.NeBot] [L.LeAtTop], Multipliable f → ∏'[L] (b : β), f b = ∏' (b : β), f b
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.eq_iff_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [IsLocalization M S] [inst_5 : Algebra R P]
  [IsLocalization M P] {x y : R}, (algebraMap R S) x = (algebraMap R S) y ↔ (algebraMap R P) x = (algebraMap R P) y
-- Mathlib.CategoryTheory.Opposites
/-- Given a natural transformation `α : F.unop ⟶ G.unop`, we can take the opposite of each
component obtaining a natural transformation `G ⟶ F`.  -/
CategoryTheory.NatTrans.removeUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} → (F.unop ⟶ G.unop) → (G ⟶ F)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_le_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k t = true → ∀ {fallback : α}, (compare (t.minKeyD fallback) k).isLE = true
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Run a `TreeM` computation using `d : RefinedDiscrTree`, without losing the reference to `d`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.runTreeM : {α β : Type} →
  Lean.Meta.RefinedDiscrTree α → Lean.Meta.RefinedDiscrTree.TreeM✝ α β → Lean.MetaM (β × Lean.Meta.RefinedDiscrTree α)
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of the reverse direction of `Cardinal.le_aleph0_iff_set_countable`. -/
Set.Countable.le_aleph0 : ∀ {α : Type u} {s : Set α}, s.Countable → Cardinal.mk ↑s ≤ Cardinal.aleph0
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
deriv_sqrt_mul_log : ∀ (x : ℝ), deriv (fun x => √x * Real.log x) x = (2 + Real.log x) / (2 * √x)
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.eq_of_eqOn_of_field_closure_eq_top : ∀ {K : Type u} [inst : DivisionRing K] {L : Type v} [inst_1 : Semiring L] {s : Set K},
  Subfield.closure s = ⊤ → ∀ {f g : K →+* L}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.julian0.injEq : ∀ (day day_1 : Std.Time.Internal.Bounded.LE 0 365),
  (Std.Time.TimeZone.TransitionSpec.julian0 day = Std.Time.TimeZone.TransitionSpec.julian0 day_1) = (day = day_1)
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.idealHeight_eq_coheight : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)), x.asIdeal.height = Order.coheight x
-- Mathlib.Data.Setoid.Basic
Setoid.kerLift_mk : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α), Setoid.kerLift f ⟦x⟧ = f x
-- Init.Conv
/-- `repeat convs` runs the sequence `convs` repeatedly until it fails to apply.  -/
Lean.Parser.Tactic.Conv.convRepeat_ : Lean.ParserDescr
-- Mathlib.Data.Num.Lemmas
Num.cast_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α], ↑0 = 0
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_int32ToInt : ∀ (x : Int32) {h₁ : Int16.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int16.maxValue.toInt},
  Int16.ofIntLE x.toInt h₁ h₂ = x.toInt16
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.differentiableAt_Gamma : ∀ (s : ℂ), (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℂ Complex.Gamma s
-- Mathlib.RingTheory.Valuation.Integers
/-- The ideal of elements of the valuation subring whose valuation is less than a certain unit.  -/
Valuation.ltIdeal : {R : Type u} →
  {Γ₀ : Type v} →
    [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → (v : Valuation R Γ₀) → Γ₀ˣ → Ideal ↥v.integer
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
/-- Define a left action of `Cᴹᵒᵖ` on `D` from a right action of `C` on `D` via
the formula `mop c ⊙ₗ d = d ⊙ᵣ c`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
            CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᴹᵒᵖ D
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.join_red_of_step : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red.Step L₁ L₂ → Relation.Join FreeAddGroup.Red L₁ L₂
-- Mathlib.Data.Fintype.Card
Fintype.card_unique : ∀ {α : Type u_1} [Unique α] [h : Fintype α], Fintype.card α = 1
-- Mathlib.Algebra.Squarefree.Basic
Int.squarefree_natAbs : ∀ {n : ℤ}, Squarefree n.natAbs ↔ Squarefree n