mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.two_mul_carmichael_two_pow_of_three_le_eq_totient : ∀ {n : ℕ}, 3 ≤ n → 2 * ArithmeticFunction.carmichael (2 ^ n) = (2 ^ n).totient
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- the natural epimorphism  -/
CategoryTheory.Abelian.LeftResolution.π : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          (self : CategoryTheory.Abelian.LeftResolution ι) → self.F.comp ι ⟶ CategoryTheory.Functor.id A
-- Mathlib.Order.JordanHolder
/-- The equivalence relation on intervals implies any other notions of isomorphism.  -/
JordanHolderLattice.Iso.rel : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (e : X × X → X × X → Prop),
  (∀ {x : X × X}, e x x) →
    (∀ {x y : X × X}, e x y → e y x) →
      (∀ {x y z : X × X}, e x y → e y z → e x z) →
        (∀ {x y : X}, JordanHolderLattice.IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y)) →
          ∀ {x y : X × X}, JordanHolderLattice.Iso x y → e x y
-- Mathlib.Topology.Algebra.LinearTopology
/-- If the left and right actions of `R` on `M` coincide, then a topology is `Rᵐᵒᵖ`-linear
if and only if it is `R`-linear.  -/
IsCentralScalar.isLinearTopology_iff : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [inst_4 : Module Rᵐᵒᵖ M] [IsCentralScalar R M],
  IsLinearTopology Rᵐᵒᵖ M ↔ IsLinearTopology R M
-- Mathlib.Condensed.Module
/-- The forgetful functor from condensed `R`-modules to condensed sets.  -/
Condensed.forget : (R : Type (u + 1)) → [inst : Ring R] → CategoryTheory.Functor (CondensedMod R) CondensedSet
-- Lean.MetavarContext
/-- A user-friendly name for the metavariable. If anonymous then there is no such name.  -/
Lean.MetavarDecl.userName : Lean.MetavarDecl → Lean.Name
-- Mathlib.Order.Filter.AtTopBot.Archimedean
tendsto_intCast_atBot_iff : ∀ {α : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R]
  {f : α → ℤ} {l : Filter α}, Filter.Tendsto (fun n => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.specialLinearGroup_is_two_pretransitive : ∀ (K : Type u_1) (V : Type u_2) [inst : AddCommGroup V] [inst_1 : Field K] [inst_2 : Module K V],
  MulAction.IsMultiplyPretransitive (SpecialLinearGroup K V) (Projectivization K V) 2
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.ext : ∀ {R : Type u_2} {A : Type u_3} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  {inst_3 : Coalgebra R A} {x y : GroupLike R A}, ↑x = ↑y → x = y
-- Mathlib.Algebra.Homology.Opposite
/-- Sends a complex `X` with objects in `Vᵒᵖ` to the corresponding complex with objects in `V`.  -/
HomologicalComplex.unopSymm : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → HomologicalComplex Vᵒᵖ c.symm → HomologicalComplex V c
-- Mathlib.Data.Complex.Basic
Complex.mul_I_im : ∀ (z : ℂ), (z * Complex.I).im = z.re
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.instSmoothSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.Smooth f],
  AlgebraicGeometry.Smooth (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.RingTheory.Ideal.Prod
Ideal.idealProdEquiv_symm_apply : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal R) (J : Ideal S),
  Ideal.idealProdEquiv.symm (I, J) = I.prod J
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.comp_neg_X_leadingCoeff_eq : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R),
  (p.comp (-Polynomial.X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take_getVert : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ), (p.take n).getVert m = p.getVert (min n m)
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
`dropWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually
prove termination (`Finite` or `Productive` instances, for example) of a `dropWhile` iterator.
 -/
Std.Iterators.Types.DropWhile.PlausibleStep : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [Std.Iterator α m β] →
        {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
          Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Mathlib.Topology.Algebra.Group.Matrix
/-- The topology on `SL n R` is functorial in `R`.  -/
Continuous.specialLinearGroup_map : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] {f : R →+* S},
  Continuous ⇑f → Continuous ⇑(Matrix.SpecialLinearGroup.map f)
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : αᵒᵈ) (b : β), OrderDual.ofDual (a ^ b) = OrderDual.ofDual a ^ b
-- Mathlib.Data.Finsupp.Antidiagonal
Finsupp.sum_antidiagonal_swap : ∀ {α : Type u} [inst : DecidableEq α] {M : Type u_1} [inst_1 : AddCommMonoid M] (n : α →₀ ℕ)
  (f : (α →₀ ℕ) → (α →₀ ℕ) → M),
  ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p.1 p.2 = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p.2 p.1
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.coe_eq_zero : ∀ {𝕜 : Type u_1} [inst : Zero 𝕜] [inst_1 : PseudoMetricSpace 𝕜] {a : ↑(Metric.closedBall 0 1)}, ↑a = 0 ↔ a = 0
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ici_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n),
  ∑ i ≥ Fin.cast h a, f i = ∑ i ≥ a, f (Fin.cast h i)
-- Mathlib.Order.Monotone.Defs
monotone_snd : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β], Monotone Prod.snd
-- Init.Data.Order.ClassesExtra
Std.LawfulOrderCmp : {α : Type u_1} → (α → α → Ordering) → [LE α] → Prop
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.support_ofFinset : ∀ {α : Type u_1} {f : α → ENNReal} {s : Finset α} (h : ∑ a ∈ s, f a = 1) (h' : ∀ a ∉ s, f a = 0),
  (PMF.ofFinset f s h h').support = ↑s ∩ Function.support f
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.ret : Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Λ'
-- Mathlib.Algebra.Module.Submodule.Defs
/-- A submodule of a `Module` is a `Module`.  -/
SMulMemClass.toModule : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_1} →
            [inst_3 : SetLike A M] → [inst_4 : AddSubmonoidClass A M] → [SMulMemClass A R M] → (S' : A) → Module R ↥S'
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.eq_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) {x : X} {y : Y},
  x = h.symm y ↔ h x = y
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- `ContinuousSemilinearMapClass F σ M M₂` asserts `F` is a type of bundled continuous
`σ`-semilinear maps `M → M₂`.  See also `ContinuousLinearMapClass F R M M₂` for the case where
`σ` is the identity map on `R`.  A map `f` between an `R`-module and an `S`-module over a ring
homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y`
and `f (c • x) = (σ c) • f x`.  -/
ContinuousSemilinearMapClass : (F : Type u_1) →
  {R : outParam (Type u_2)} →
    {S : outParam (Type u_3)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type u_4)) →
              [TopologicalSpace M] →
                [inst_3 : AddCommMonoid M] →
                  (M₂ : outParam (Type u_5)) →
                    [TopologicalSpace M₂] →
                      [inst_5 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → [FunLike F M M₂] → Prop
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Auxiliary definition for `Adjunction.comp`.  -/
CategoryTheory.Bicategory.Adjunction.compCounit : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f₁ : a ⟶ b} →
        {g₁ : b ⟶ a} →
          {f₂ : b ⟶ c} →
            {g₂ : c ⟶ b} →
              CategoryTheory.Bicategory.Adjunction f₁ g₁ →
                CategoryTheory.Bicategory.Adjunction f₂ g₂ →
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g₂ g₁)
                      (CategoryTheory.CategoryStruct.comp f₁ f₂) ⟶
                    CategoryTheory.CategoryStruct.id c)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.iInf_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {ι : Sort u_3} (f : ι → I.Filtration M), (iInf f).N = ⨅ i, (f i).N
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.Script.TacticBuilder.isGlobalSimpTheorem : Lean.Meta.SimpTheorems → Lean.Meta.Simprocs → Lean.Meta.Origin → Bool
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} {ι : Type w} {π : ι → α} {cofan₁ : CategoryTheory.Limits.Cofan fun i => A (π i)}
  {cofan₂ : CategoryTheory.Limits.Cofan fun i => B (π i)} {isColimit₁ : CategoryTheory.Limits.IsColimit cofan₁}
  {isColimit₂ : CategoryTheory.Limits.IsColimit cofan₂} {m : cofan₁.pt ⟶ cofan₂.pt}
  {hm :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (cofan₁.inj i) m =
          CategoryTheory.CategoryStruct.comp (g (π i)) (cofan₂.inj i))
      HomotopicalAlgebra.AttachCells.hm._autoParam}
  {g₁ : cofan₁.pt ⟶ X₁} {g₂ : cofan₂.pt ⟶ X₂} {isPushout : CategoryTheory.IsPushout g₁ m f g₂} {ι_1 : Type w}
  {π_1 : ι_1 → α} {cofan₁_1 : CategoryTheory.Limits.Cofan fun i => A (π_1 i)}
  {cofan₂_1 : CategoryTheory.Limits.Cofan fun i => B (π_1 i)} {isColimit₁_1 : CategoryTheory.Limits.IsColimit cofan₁_1}
  {isColimit₂_1 : CategoryTheory.Limits.IsColimit cofan₂_1} {m_1 : cofan₁_1.pt ⟶ cofan₂_1.pt}
  {hm_1 :
    autoParam
      (∀ (i : ι_1),
        CategoryTheory.CategoryStruct.comp (cofan₁_1.inj i) m_1 =
          CategoryTheory.CategoryStruct.comp (g (π_1 i)) (cofan₂_1.inj i))
      HomotopicalAlgebra.AttachCells.hm._autoParam}
  {g₁_1 : cofan₁_1.pt ⟶ X₁} {g₂_1 : cofan₂_1.pt ⟶ X₂} {isPushout_1 : CategoryTheory.IsPushout g₁_1 m_1 f g₂_1},
  { ι := ι, π := π, cofan₁ := cofan₁, cofan₂ := cofan₂, isColimit₁ := isColimit₁, isColimit₂ := isColimit₂, m := m,
        hm := hm, g₁ := g₁, g₂ := g₂, isPushout := isPushout } =
      { ι := ι_1, π := π_1, cofan₁ := cofan₁_1, cofan₂ := cofan₂_1, isColimit₁ := isColimit₁_1,
        isColimit₂ := isColimit₂_1, m := m_1, hm := hm_1, g₁ := g₁_1, g₂ := g₂_1, isPushout := isPushout_1 } →
    ι = ι_1 ∧
      π ≍ π_1 ∧
        cofan₁ ≍ cofan₁_1 ∧
          cofan₂ ≍ cofan₂_1 ∧ isColimit₁ ≍ isColimit₁_1 ∧ isColimit₂ ≍ isColimit₂_1 ∧ m ≍ m_1 ∧ g₁ ≍ g₁_1 ∧ g₂ ≍ g₂_1
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcOptions.mk.injEq : ∀ (highlightMatchesProvider? : Option Lean.Lsp.HighlightMatchesOptions) (rpcWireFormat? : Option Lean.Lsp.RpcWireFormat)
  (highlightMatchesProvider?_1 : Option Lean.Lsp.HighlightMatchesOptions)
  (rpcWireFormat?_1 : Option Lean.Lsp.RpcWireFormat),
  ({ highlightMatchesProvider? := highlightMatchesProvider?, rpcWireFormat? := rpcWireFormat? } =
      { highlightMatchesProvider? := highlightMatchesProvider?_1, rpcWireFormat? := rpcWireFormat?_1 }) =
    (highlightMatchesProvider? = highlightMatchesProvider?_1 ∧ rpcWireFormat? = rpcWireFormat?_1)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
TopRep.homogeneousCochains.d_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (i : ℕ)
  (σ : ↑(X.homogeneousCochains.X i).toModuleCat),
  ↑((TopModuleCat.Hom.hom (X.homogeneousCochains.d i (i + 1))) σ) = (TopRep.Hom.hom (X.d (i + 1))) ↑σ
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instIsScalarTower_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M N] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [IsScalarTower M N α], IsScalarTower M Nᵒᵈ α
-- Mathlib.Topology.MetricSpace.Polish
/-- Any nonempty Polish space is the continuous image of the fundamental space `ℕ → ℕ`.  -/
PolishSpace.exists_nat_nat_continuous_surjective : ∀ (α : Type u_3) [inst : TopologicalSpace α] [PolishSpace α] [Nonempty α], ∃ f, Continuous f ∧ Function.Surjective f
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
OrderedFinpartition.atomic.eq_1 : ∀ (n : ℕ),
  OrderedFinpartition.atomic n =
    { length := n, partSize := fun x => 1, partSize_pos := ⋯, emb := fun m x => m, emb_strictMono := ⋯,
      parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  {D₁ D₂ : F.DescentData' sq sq₃} →
                    (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i) →
                      autoParam
                          (∀ (i₁ i₂ : ι),
                            CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom i₁))
                                (D₂.hom i₁ i₂) =
                              CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
                                ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom i₂)))
                          CategoryTheory.Pseudofunctor.DescentData'.Hom.comm._autoParam →
                        D₁.Hom D₂
-- Mathlib.Data.Rel
SetRel.comp_empty : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β), R.comp ∅ = ∅
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcompFunctor_map_hom : ∀ (C : Type u_1) {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E] (A : Type u_5)
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] {F₁ F₂ : CategoryTheory.SingleFunctors C D A} (φ : F₁ ⟶ F₂)
  (a : A),
  ((CategoryTheory.SingleFunctors.postcompFunctor C A G).map φ).hom a = CategoryTheory.Functor.whiskerRight (φ.hom a) G
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict_hasLift : ∀ {ι : 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.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e), e.HasLift (e.homRestrict ψ)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Clause.mem_cons : ∀ {α : Type u_1} {l : Std.Sat.Literal α} {c : List (Std.Sat.Literal α)} {v : α},
  Std.Sat.CNF.Clause.Mem v (l :: c) ↔ v = l.1 ∨ Std.Sat.CNF.Clause.Mem v c
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular monomorphism in `Cᵒᵖ` induces a regular epimorphism in `C`.  -/
CategoryTheory.RegularMono.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} → {f : X ⟶ Y} → CategoryTheory.RegularMono f → CategoryTheory.RegularEpi f.unop
-- Mathlib.Data.Set.Basic
Set.decidableUniv : {α : Type u} → (a : α) → Decidable (a ∈ Set.univ)
-- Mathlib.Algebra.Algebra.Basic
ULift.down_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  ((algebraMap R (ULift.{u_4, u_2} A)) r).down = (algebraMap R A) r
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.eisSummand.eq_1 : ∀ (k : ℤ) (v : Fin 2 → ℤ) (z : UpperHalfPlane), EisensteinSeries.eisSummand k v z = (↑(v 0) * ↑z + ↑(v 1)) ^ (-k)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams : Lean.FromJson Lean.Lsp.CallHierarchyIncomingCallsParams
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.coe_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M → N) (hmul : ∀ (x y : M), f (x * y) = f x * f y),
  ⇑{ toFun := f, map_mul' := hmul } = f
-- Init.Data.String.Basic
String.get : String → String.Pos.Raw → Char
-- Std.Http.Data.URI.Encoding
Std.Http.URI.isValidUTF8_of_isAsciiByte : ∀ (ba : ByteArray), ba.data.all Std.Http.Internal.Char.isAsciiByte = true → ba.IsValidUTF8
-- Mathlib.Analysis.Normed.Module.Bases
/-- The coefficient functional value for the basis construction.  -/
SchauderBasis.RankOneDecomposition.basisCoeff : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] → [inst_2 : NormedSpace 𝕜 X] → SchauderBasis.RankOneDecomposition 𝕜 X → ℕ → X → 𝕜
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_add_two_add_one : ∀ (b n : ℕ), (b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
-- Mathlib.Algebra.Order.Sub.Defs
tsub_add_eq_tsub_tsub : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] (a b c : α),
  a - (b + c) = a - b - c
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.zero_isRoot_iff_coeff_zero_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.IsRoot 0 ↔ p.coeff 0 = 0
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- If a monoid `M` continuously acts on an R₁ topological space `X`,
`g` is an element of `M` such that its integer powers are dense in `M`,
and `μ` is a finite inner regular measure on `X` which is ergodic with respect to the action of `M`,
then the scalar multiplication by `g` is an ergodic map.  -/
ergodic_smul_of_denseRange_zpow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [ContinuousInv G] {X : Type u_2}
  [inst_3 : TopologicalSpace X] [R1Space X] [inst_5 : MeasurableSpace X] [BorelSpace X] [inst_7 : MulAction G X]
  [ContinuousSMul G X] {g : G},
  (DenseRange fun x => g ^ x) →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul G X μ],
      Ergodic (fun x => g • x) μ
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.integrableOn_toReal_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  μ s ≠ ⊤ → MeasureTheory.IntegrableOn (fun x => (μ.rnDeriv ν x).toReal) s ν
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.HasReflexiveCoequalizers.has_coeq : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasReflexiveCoequalizers C]
  ⦃A B : C⦄ (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g], CategoryTheory.Limits.HasCoequalizer f g
-- Std.Data.DTreeMap.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.DTreeMap.erase : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Std.DTreeMap α β cmp
-- Init.Data.UInt.Bitwise
UInt64.shiftRight_eq_shiftRight_mod : ∀ (a b : UInt64), a >>> b = a >>> (b % 64)
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.instNeg.eq_1 : ∀ {R : Type u_2} {M : Type u_3} [inst : Neg R],
  Mathlib.Tactic.Module.NF.instNeg =
    {
      neg := fun l =>
        List.map
          (fun x =>
            match x with
            | (a, x) => (-a, x))
          l }
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
ValuativeRel.nonarchimedeanRing : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : ValuativeRel R], NonarchimedeanRing R
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.join_le_of_equivalence_of_le`. -/
Relation.join_of_equivalence : ∀ {α : Type u_1} {r r' : α → α → Prop}, Equivalence r → r' ≤ r → Relation.Join r' ≤ r
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedZeroHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N], instInhabitedZeroHom = { default := 0 }
-- Mathlib.Data.Finsupp.Basic
/-- `Finsupp.comapDomain` is an `AddMonoidHom`.  -/
Finsupp.comapDomain.addMonoidHom : {α : Type u_1} →
  {β : Type u_2} → {M : Type u_5} → [inst : AddZeroClass M] → {f : α → β} → Function.Injective f → (β →₀ M) →+ α →₀ M
-- Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
GenContFract.of_convergence : ∀ {K : Type u_1} (v : K) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorRing K]
  [Archimedean K] [inst_5 : TopologicalSpace K] [OrderTopology K],
  Filter.Tendsto (GenContFract.of v).convs Filter.atTop (nhds v)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.condIndepFun : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_3}
  {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iCondIndepFun m' hm' f μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.CondIndepFun m' hm' (f i) (f j) μ
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousAt.comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {γ : Type u_4}
  [inst_1 : TopologicalSpace γ] {x : γ} {g : γ → α},
  SemicontinuousAt r (g x) → ContinuousAt g x → SemicontinuousAt (r ∘ g) x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} {f g : M₁ ⟶ M₂}, (∀ (X : Cᵒᵖ), f.app X = g.app X) → f = g
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.subConst_empty_left : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (B : Finset G), ∅.subConst B = 0
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso : ∀ (R : Type u) [inst : CommRing R] (x x_1 : HopfAlgCat R),
  (HopfAlgCat.MonoidalCategory.inducingFunctorData R).μIso x x_1 =
    CategoryTheory.Iso.refl
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x)
        ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_1))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.semigroup.eq_1 : ∀ {α : Type u_2} [inst : Semigroup α], Set.semigroup = { toMul := Set.mul, mul_assoc := ⋯ }
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.hasFiniteIntegral_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} ⦃f : γ → E⦄,
  MeasureTheory.StronglyMeasurable f →
    (MeasureTheory.HasFiniteIntegral f ((η.comp κ) a) ↔
      (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral f (η x)) ∧
        MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : γ), ‖f y‖ ∂η x) (κ a))