mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Products.Associator
/-- The associator isomorphism is compatible with `prodFunctorToFunctorProd`.  -/
CategoryTheory.prod.prodFunctorToFunctorProdAssociator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (A : Type u₄) →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} A] →
                (CategoryTheory.prod.associativity (CategoryTheory.Functor A C) (CategoryTheory.Functor A D)
                          (CategoryTheory.Functor A E)).functor.comp
                    (((CategoryTheory.Functor.id (CategoryTheory.Functor A C)).prod
                          (CategoryTheory.prodFunctorToFunctorProd A D E)).comp
                      (CategoryTheory.prodFunctorToFunctorProd A C (D × E))) ≅
                  ((CategoryTheory.prodFunctorToFunctorProd A C D).prod
                        (CategoryTheory.Functor.id (CategoryTheory.Functor A E))).comp
                    ((CategoryTheory.prodFunctorToFunctorProd A (C × D) E).comp
                      (CategoryTheory.prod.associativity C D E).congrRight.functor)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The zeroth modified cyclotomic polynomial is `1`.  -/
Polynomial.cyclotomic'_zero : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.cyclotomic' 0 R = 1
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.map_apply_ιMulti : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) (m : Fin n → M),
  (exteriorPower.map n f) ((exteriorPower.ιMulti R n) m) = (exteriorPower.ιMulti R n) (⇑f ∘ m)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.not_in₁₁ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b b' : β},
  ¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₁ b')
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint and such that `A ⊔ B = S`, then `trace` and `algebraMap` commutes.
 -/
Subalgebra.LinearDisjoint.trace_algebraMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    A ⊔ B = ⊤ →
      ∀ [Module.Free R ↥B] [Module.Finite R ↥B] (x : ↥B),
        (Algebra.trace (↥A) S) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.trace R ↥B) x)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_zpow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] (a : α) (n : ℤ), {a} ^ n = {a ^ n}
-- Mathlib.Data.Finset.Card
Finset.card_map : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} (f : α ↪ β), (Finset.map f s).card = s.card
-- Mathlib.Algebra.Ring.Parity
even_iff_two_dvd : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a ↔ 2 ∣ a
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mem_genEigenspace_one : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M}, x ∈ (f.genEigenspace μ) 1 ↔ f x = μ • x
-- Mathlib.CategoryTheory.Limits.Indization.Products
CategoryTheory.Limits.isIndObject_limit_of_discrete_of_hasLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type v}
  [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) (CategoryTheory.Functor Cᵒᵖ (Type v))),
  (∀ (a : CategoryTheory.Discrete α), CategoryTheory.Limits.IsIndObject (F.obj a)) →
    CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit F)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_typein_limit : ∀ {o : Ordinal.{u}}, (∀ a < o, Order.succ a < o) → iSup ⇑(Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding = o
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.smul_τ₂ : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (a : R) (φ : S₁ ⟶ S₂), (a • φ).τ₂ = a • φ.τ₂
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.instInhabited : {R : Type u} → [inst : CommRing R] → Inhabited (CommBialgCat R)
-- Mathlib.SetTheory.Lists
Lists'.cons'.injEq : ∀ {α : Type u} {b : Bool} (a : Lists' α b) (a_1 : Lists' α true) (b_1 : Bool) (a_2 : Lists' α b_1)
  (a_3 : Lists' α true), (a.cons' a_1 = a_2.cons' a_3) = (b = b_1 ∧ a ≍ a_2 ∧ a_1 = a_3)
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- Multiplicity of the ideal norm, for coprime ideals.
This is essentially just a repackaging of the Chinese Remainder Theorem.
 -/
cardQuot_mul_of_coprime : ∀ {S : Type u_1} [inst : CommRing S] {I J : Ideal S},
  IsCoprime I J → Submodule.cardQuot (I * J) = Submodule.cardQuot I * Submodule.cardQuot J
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for casting `BitVec`s along an equality of the size.  -/
BitVec.reduceCast : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function has a power series on a ball, then so does its derivative.  -/
HasFPowerSeriesOnBall.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F],
  HasFPowerSeriesOnBall f p x r → HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivCLM_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  {c : ℝ} {v : E}, TestFunction.lineDerivCLM 𝕜 (c • v) = c • TestFunction.lineDerivCLM 𝕜 v
-- Aesop.Check
Aesop.Check.mk.sizeOf_spec : ∀ (toOption : Lean.Option Bool), sizeOf { toOption := toOption } = 1 + sizeOf toOption
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.hasNoetherianRange_iff_hasFiniteRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {u : V →ₗ[K] V₂},
  u.HasNoetherianRange ↔ u.HasFiniteRange
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instOrderTop : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → OrderTop (OpenAddSubgroup G)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.tsum_le_of_sum_range_le : ∀ {f : ℕ → NNReal} {c : NNReal}, (∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) → ∑' (n : ℕ), f n ≤ c
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instInhabitedPower.default : Lean.Grind.CommRing.Power
-- Mathlib.CategoryTheory.Extensive
/-- A category has pullback of inclusions if it has all pullbacks along coproduct injections.  -/
CategoryTheory.HasPullbacksOfInclusions : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasBinaryCoproducts C] → Prop
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- Being the additive normal closure of a finite set is invariant under
surjective homomorphism.  -/
AddSubgroup.IsFinitelyNormallyGenerated.map : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {N : AddSubgroup G},
  N.IsFinitelyNormallyGenerated →
    ∀ {f : G →+ H}, Function.Surjective ⇑f → (AddSubgroup.map f N).IsFinitelyNormallyGenerated
-- Mathlib.Data.Seq.Basic
Stream'.Seq.tail.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α), s.tail = ⟨(↑s).tail, ⋯⟩
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.message.sizeOf_spec : ∀ (msg : Std.Format), sizeOf (Lean.IR.LogEntry.message msg) = 1 + sizeOf msg
-- Mathlib.Order.Category.LinOrd
/-- `OrderDual` as a functor.  -/
LinOrd.dual : CategoryTheory.Functor LinOrd LinOrd
-- Init.Control.Lawful.Instances
ExceptT.run_map : ∀ {m : Type u_1 → Type u_2} {α β ε : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α),
  (f <$> x).run = Except.map f <$> x.run
-- Init.Notation
/-- A product type in which the types may be propositions, usually written `α ×' β`.

This type is primarily used internally and as an implementation detail of proof automation. It is
rarely useful in hand-written code.


Conventions for notations in identifiers:

 * The recommended spelling of `×'` in identifiers is `PProd`. -/
«term_×'_» : Lean.TrailingParserDescr
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.mulFn? : Lean.Meta.Sym.Arith.Ring → Option Lean.Expr
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_mod_two_eq_one : ∀ {a b : ℕ}, (a &&& b) % 2 = 1 ↔ a % 2 = 1 ∧ b % 2 = 1
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.helper₆ : ∀ {c : Char} {o : Option Char} {b : BitVec 32},
  c.val.toBitVec = b → (∀ (d : Char), o = some d → d.val.toBitVec = b) → o.isSome = true → o = some c
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.NullMeasurableSet.smul : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [MeasurableConstSMul G α] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (c : G), MeasureTheory.NullMeasurableSet (c • s) μ
-- Lean.Meta.Instances
Lean.Meta.checkImpossibleInstance : Lean.ConstantInfo → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Finsupp
Finsupp.erase_eq_sub_single : ∀ {ι : Type u_1} {G : Type u_6} [inst : AddGroup G] (f : ι →₀ G) (a : ι), Finsupp.erase a f = f - fun₀ | a => f a
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α},
  FiniteMultiplicity a b → ∀ {n : ℕ}, ↑n < emultiplicity a b → n < multiplicity a b
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- If `P` is stable under composition and `f : X ⟶ Y` satisfies `P`,
this is the functor `P.Over Q X ⥤ P.Over Q Y` given by composing with `f`.  -/
CategoryTheory.MorphismProperty.Over.map : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          {X Y : T} →
            [P.IsStableUnderComposition] → {f : X ⟶ Y} → P f → CategoryTheory.Functor (P.Over Q X) (P.Over Q Y)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- A path object `P` is good if the morphism
`P.p : P.P ⟶ A ⨯ A` is a fibration.  -/
HomotopicalAlgebra.PathObject.IsGood : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.PathObject A →
          [CategoryTheory.Limits.HasBinaryProduct A A] → [HomotopicalAlgebra.CategoryWithFibrations C] → Prop
-- Mathlib.GroupTheory.Finiteness
Monoid.fg_range : ∀ {M : Type u_1} [inst : Monoid M] {M' : Type u_3} [inst_1 : Monoid M'] [Monoid.FG M] (f : M →* M'),
  Monoid.FG ↥(MonoidHom.mrange f)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_addNatEmb_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Finset.map (Fin.addNatEmb m) (Finset.Ioc i j) = Finset.Ioc (i.addNat m) (j.addNat m)
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instBEqFunIndParamKind : BEq Lean.Meta.FunIndParamKind
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_eq_prod : ∀ {α : Type u_3} {β : Type u_6} [inst : CommMonoid β] (s : Finset α) (f : α → β), s.noncommProd f ⋯ = s.prod f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {km : α}, t.maxKey? = some km → t.getKey! km = km
-- Mathlib.Algebra.Group.Conj
ConjClasses.instOne.eq_1 : ∀ {α : Type u} [inst : Monoid α], ConjClasses.instOne = { one := ⟦1⟧ }
-- Lean.Elab.DefView
Lean.Elab.DefKind.opaque.sizeOf_spec : sizeOf Lean.Elab.DefKind.opaque = 1
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.counit_comul_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.ComonObj X] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.counit X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv h
-- Mathlib.RingTheory.Ideal.Operations
Ideal.disjoint_powers_iff_notMem : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} (y : R), I.IsRadical → (Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_mono : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} [L.NeBot],
  Multipliable f L → Multipliable g L → f ≤ g → ∏'[L] (n : ι), f n ≤ ∏'[L] (n : ι), g n
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.pow_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℕ)
  (a : DoubleCentralizer 𝕜 A), (a ^ n).toProd.1 = a.toProd.1 ^ n
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- a family of sections which generate the sheaf of modules  -/
SheafOfModules.GeneratingSections.s : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → (self : M.GeneratingSections) → self.I → M.sections
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The right unitor in the localized monoidal category `LocalizedMonoidal L W ε`.  -/
CategoryTheory.Localization.Monoidal.rightUnitor : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).flip.obj unit ≅
                        CategoryTheory.Functor.id (CategoryTheory.LocalizedMonoidal L W ε)
-- Mathlib.Data.Finset.Grade
Finset.erase_covBy : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∈ s → s.erase a ⋖ s
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeToSubmodule_ne_bot : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : FractionalIdeal S P}, ↑I ≠ ⊥ ↔ I ≠ 0
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.sigma : ∀ {ι : Type u_3} (X : ι → Type u_4) [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), PrespectralSpace (X i)],
  PrespectralSpace ((i : ι) × X i)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- An acyclic graph (forest) is 2-colorable.  -/
SimpleGraph.IsAcyclic.colorable_two : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → G.Colorable 2
-- Aesop.Index.Forward
Aesop.ForwardIndex.mk.injEq : ∀ (tree : Lean.Meta.DiscrTree (Aesop.ForwardRule × Aesop.PremiseIndex))
  (nameToRule : Lean.PHashMap Aesop.RuleName Aesop.ForwardRule) (constRules : Lean.PHashSet Aesop.ForwardRule)
  (tree_1 : Lean.Meta.DiscrTree (Aesop.ForwardRule × Aesop.PremiseIndex))
  (nameToRule_1 : Lean.PHashMap Aesop.RuleName Aesop.ForwardRule) (constRules_1 : Lean.PHashSet Aesop.ForwardRule),
  ({ tree := tree, nameToRule := nameToRule, constRules := constRules } =
      { tree := tree_1, nameToRule := nameToRule_1, constRules := constRules_1 }) =
    (tree = tree_1 ∧ nameToRule = nameToRule_1 ∧ constRules = constRules_1)
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- To UV-compress a set family, we compress each of its elements, except that we don't want to
reduce the cardinality, so we keep all elements whose compression is already present.  -/
FinsetFamily.term𝓒 : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_empty : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], NonUnitalAlgebra.adjoin R ∅ = ⊥
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom₂.mk.sizeOf_spec : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} [inst_1 : SizeOf B] [inst_2 : SizeOf C]
  (hom : f.hom ⟶ g.hom), sizeOf { hom := hom } = 1 + sizeOf hom
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_mem_nonZeroDivisors : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {a b : M₀},
  a * b ∈ nonZeroDivisors M₀ ↔ a ∈ nonZeroDivisors M₀ ∧ b ∈ nonZeroDivisors M₀
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ Y₁ Y₂ : B} {t : X₁ ⟶ Y₁}
  {l : X₁ ⟶ X₂} {r : Y₁ ⟶ Y₂} {b : X₂ ⟶ Y₂} (sq : CategoryTheory.CommSq t l r b) (φ : X₁ ⟶ Y₂)
  (hφ : CategoryTheory.CategoryStruct.comp t r = φ),
  F.isoMapOfCommSq sq = (F.mapComp' t r φ ⋯).symm ≪≫ F.mapComp' l b φ ⋯
-- Mathlib.MeasureTheory.Measure.MeasureSpace
_private.Mathlib.MeasureTheory.Measure.MeasureSpace.0.MeasureTheory.Measure.measure_le_sInf : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m : Set (MeasureTheory.Measure α)},
  (∀ μ' ∈ m, μ ≤ μ') → μ ≤ sInf m
-- Std.Async.Basic
/-- Converts `IO (Task α)` into `Async`.
 -/
Std.Async.Async.ofIOTask : {α : Type} → IO (Task α) → Std.Async.Async α
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.tail : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} {q : G.Walk u' v'},
  p.IsSubwalk q → p.tail.IsSubwalk q
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.lt_normThreshold_zero : ∀ {a : ℝ}, 0 < a → a / (1 - √2) < ProbabilityTheory.Fernique.normThreshold a 0
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.toAlgHom_ofAlgHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_2} {S' : Type u_1} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f : P.Ring →ₐ[R] P'.Ring)
  (H :
    (IsScalarTower.toAlgHom R P'.Ring S').comp f =
      (IsScalarTower.toAlgHom R S S').comp (IsScalarTower.toAlgHom R P.Ring S)),
  (Algebra.Extension.Hom.ofAlgHom f H).toAlgHom = f
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- If `0 < n`, then `a i` has order `(2 * n) / gcd (2 * n) i`.
 -/
QuaternionGroup.orderOf_a : ∀ {n : ℕ} [NeZero n] (i : ZMod (2 * n)), orderOf (QuaternionGroup.a i) = 2 * n / (2 * n).gcd i.val
-- Lean.Declaration
Lean.instReprDefinitionSafety.repr : Lean.DefinitionSafety → ℕ → Std.Format
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.Normal.conjAct : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ (g : ConjAct G), g • H = H
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_diagonal : ∀ {m : Type u_2} {o : Type u_4} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o] [inst_2 : DecidableEq m]
  (d : m × o → α) (k : o), (Matrix.diagonal d).blockDiag k = Matrix.diagonal fun i => d (i, k)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc : ∀ {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} (self : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁)
  (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
  (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q)
  {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₃.op.toLoc).toFunctor.obj (self.obj i₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.hom q f₁ f₂ hf₁ hf₂)
      (CategoryTheory.CategoryStruct.comp (self.hom q f₂ f₃ hf₂ hf₃) h) =
    CategoryTheory.CategoryStruct.comp (self.hom q f₁ f₃ hf₁ hf₃) h
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instIsLeftCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsLeftCancelAdd α], IsLeftCancelAdd (Lex α)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.δ_naturality : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G]
  {X1 X2 : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hX1 : X1.ShortExact) (hX2 : X2.ShortExact) (F : X1 ⟶ X2)
  (i : ℤ),
  CategoryTheory.CategoryStruct.comp (TateCohomology.δ hX1 i) ((tateCohomologyFunctor (i + 1)).map F.τ₁) =
    CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map F.τ₃) (TateCohomology.δ hX2 i)
-- Init.Data.List.Nat.Basic
List.mem_eraseIdx_iff_getElem : ∀ {α : Type u_1} {x : α} {l : List α} {k : ℕ}, x ∈ l.eraseIdx k ↔ ∃ i, ∃ (h : i < l.length), i ≠ k ∧ l[i] = x
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.zero : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ], ProbabilityTheory.HasCondSubgaussianMGF m hm 0 0 μ
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.coe_mk : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (toFun : M → N)
  (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x)
  (exists_companion' : ∃ B, ∀ (x y : M), toFun (x + y) = toFun x + toFun y + (B x) y),
  ⇑{ toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' } = toFun
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C) {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) h
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.growsPolynomially_one_sub_smoothingFn : AkraBazziRecurrence.GrowsPolynomially fun x => 1 - AkraBazziRecurrence.smoothingFn x