mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.IsReflexivePair.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B},
  (∃ s,
      CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧
        CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B) →
    CategoryTheory.IsReflexivePair f g
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.PredTrans.pushOption.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- A measure `μ` is separable if there exists a countable and measure-dense family of sets.

The term "separable" is justified by the fact that the definition translates to the usual notion
of separability in the metric space made by constant indicators equipped with the `Lᵖ` norm.  -/
MeasureTheory.IsSeparable : {X : Type u_1} → [m : MeasurableSpace X] → MeasureTheory.Measure X → Prop
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- Given a weight `w`, the decomposition of `MvPolynomial σ R` into weighted homogeneous
submodules  -/
MvPolynomial.weightedDecomposition : (R : Type u_1) →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      {σ : Type u_3} →
        (w : σ → M) →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : DecidableEq M] → DirectSum.Decomposition (MvPolynomial.weightedHomogeneousSubmodule R w)
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertZoneId : Std.Time.ZoneId → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The coordinates of a representative of `P + Q` for two distinct projective point representatives
`P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `![0, 0, 0]`.  -/
WeierstrassCurve.Projective.addXYZ : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → (Fin 3 → R) → Fin 3 → R
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.continuousMapClass : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂],
  ContinuousMapClass (ContinuousMultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.Order.Fin.Tuple
Fin.liftFun_cons : ∀ {α : Type u_1} {n : ℕ} (r : α → α → Prop) [IsTrans α r] {f : Fin n → α} {a : α},
  Relator.LiftFun (fun x1 x2 => x1 < x2) r (Fin.cons a f) (Fin.cons a f) ↔
    (∀ (i : Fin n), r a (f i)) ∧ Relator.LiftFun (fun x1 x2 => x1 < x2) r f f
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isValidEq : Int.Internal.Linear.Poly → Bool
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_notMem_affineSpan_faceOpposite : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.incenter ∉ affineSpan ℝ (Set.range (s.faceOpposite i).points)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'}
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {X'' Y'' : C} {h : X'' ⟶ Y''}
  (ψ : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk h) {Z : C} (h_1 : (data.factorizationData h).Z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (data.mapZ (CategoryTheory.CategoryStruct.comp φ ψ)) h_1 =
    CategoryTheory.CategoryStruct.comp (data.mapZ φ) (CategoryTheory.CategoryStruct.comp (data.mapZ ψ) h_1)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.coe_one : ∀ (M : Type u_4) [inst : AddZero M], ⇑1 = id
-- Init.Data.String.Basic
String.Slice.Pos.startInclusive_le_str : ∀ {s : String.Slice} {pos : s.Pos}, s.startInclusive ≤ pos.str
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- A morphism `f : I ⟶ J` is exponentiable if the pullback functor `Over J ⥤ Over I`
has a right adjoint.  -/
CategoryTheory.IsExponentiable : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.ChosenPullbacks C] → CategoryTheory.MorphismProperty C
-- Init.Data.Vector.Lemmas
Vector.getElem?_extract : ∀ {α : Type u_1} {n i : ℕ} {as : Vector α n} {start stop : ℕ},
  (as.extract start stop)[i]? = if i < min stop n - start then as[start + i]? else none
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformlyOn.exists : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α], SummableUniformlyOn f s → ∃ g, HasSumUniformlyOn f g s
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.eq_4 : Lean.Grind.instBEqIntInterval.beq Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii = true
-- Mathlib.Order.LiminfLimsup
/-- The `limsSup` of a filter `f` is the infimum of the `a` such that the inequality
`x ≤ a` eventually holds for `f`.  -/
Filter.limsSup : {α : Type u_1} → [ConditionallyCompleteLattice α] → Filter α → α
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] (b : J.L) {Z : C} (h : ∐ I.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b)
      (CategoryTheory.CategoryStruct.comp I.fstSigmaMap h) =
    CategoryTheory.CategoryStruct.comp (I.fst b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right (J.fst b)) h)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_rightUnitor_aux₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
        (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.Analysis.RCLike.Basic
RCLike.continuous_ofReal : ∀ {K : Type u_1} [inst : RCLike K], Continuous RCLike.ofReal
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rco.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rco α},
  r.toList = (Std.Rco.Internal.iter r).toList
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  CategoryTheory.CategoryStruct.comp S.L₀X₂ToP (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) = S.L₀.g
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
coe_toIdeal : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (I : HomogeneousIdeal 𝒜), ↑I.toIdeal = ↑I
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive monoid is isomorphic to the opposite of its opposite.  -/
AddEquiv.opOp : (M : Type u_3) → [inst : Add M] → M ≃+ Mᵃᵒᵖᵃᵒᵖ
-- Aesop.Script.TacticState
Aesop.Script.TacticState.getVisibleGoalIndex? : Aesop.Script.TacticState → Lean.MVarId → Option ℕ
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Array.idxOf.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α), Array.idxOf a = Array.findIdx fun x => x == a
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- The linear equivalence between `n × n` matrices and bilinear forms on `n → R`  -/
Matrix.toBilin' : {R₁ : Type u_1} →
  [inst : CommSemiring R₁] →
    {n : Type u_5} → [Fintype n] → [DecidableEq n] → Matrix n n R₁ ≃ₗ[R₁] LinearMap.BilinForm R₁ (n → R₁)
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.coeff_expand_mul : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) (m : ℕ),
  (PowerSeries.coeff (p * m)) ((PowerSeries.expand p hp) φ) = (PowerSeries.coeff m) φ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.Topology.Algebra.UniformConvergence
instAddCommGroupUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : AddCommGroup β],
  instAddCommGroupUniformOnFun = { toAddGroup := instAddGroupUniformOnFun, add_comm := ⋯ }
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_succ_right_eq_insert : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a < b → Set.Ioo a (Order.succ b) = insert b (Set.Ioo a b)
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instSemilatticeSup : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] →
      [inst_1 : Bot α] → [inst_2 : SemilatticeSup β] → [inst_3 : OrderBot β] → SemilatticeSup (SupBotHom α β)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instZero : {α : Type u_1} → [Zero α] → Zero (Lex α)
-- Mathlib.Order.LiminfLimsup
OrderIso.limsup_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_6} [inst : ConditionallyCompleteLattice β]
  [inst_1 : ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ),
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) OrderIso.limsup_apply._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) OrderIso.limsup_apply._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) OrderIso.limsup_apply._auto_5 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) OrderIso.limsup_apply._auto_7 →
          g (Filter.limsup u f) = Filter.limsup (fun x => g (u x)) f
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
HasCompactSupport.enorm_le_lintegral_Ici_deriv : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F},
  ContDiff ℝ 1 f → HasCompactSupport f → ∀ (x : ℝ), ‖f x‖ₑ ≤ ∫⁻ (y : ℝ) in Set.Iic x, ‖deriv f y‖ₑ
-- Mathlib.Data.Int.NatAbs
Int.natAbs_natCast_sub_natCast_of_ge : ∀ {a b : ℕ}, b ≤ a → (↑a - ↑b).natAbs = a - b
-- Mathlib.GroupTheory.Coset.Basic
/-- Equality of two right cosets `s + a` and `s + b`.  -/
RightAddCosetEquivalence : {α : Type u_1} → [Add α] → Set α → α → α → Prop
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lcompₛₗ.eq_1 : ∀ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} (R₅ : Type u_18) {M : Type u_19} {N : Type u_20} (P : Type u_21)
  [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : Semiring R₅] {σ₁₂ : R →+* R₂}
  (σ₂₃ : R₂ →+* R₃) {σ₁₃ : R →+* R₃} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : Module R M] [inst_8 : Module R₂ N] [inst_9 : Module R₃ P] [inst_10 : Module R₅ P]
  [inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_12 : SMulCommClass R₃ R₅ P] (f : M →ₛₗ[σ₁₂] N),
  LinearMap.lcompₛₗ R₅ P σ₂₃ f = (LinearMap.id.flip ∘ₛₗ f).flip
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- For an adjoint quadruple `L ⊣ F ⊣ G ⊣ R` where `F` (and hence also `R`) is fully faithful and
its domain / codomain has all pushouts resp. pullbacks, the natural transformation `G ⟶ L` is an
epimorphism iff the natural transformation `F ⟶ R` is a monomorphism.  -/
CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R) [inst_2 : F.Full]
  [inst_3 : F.Faithful] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPushouts D],
  CategoryTheory.Epi q.leftTriple.rightToLeft ↔ CategoryTheory.Mono q.rightTriple.leftToRight
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natTransHomologyπ_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c), (HomologicalComplex.natTransHomologyπ C c i).app K = K.homologyπ i
-- Mathlib.Data.PSigma.Order
/-- The lexicographical `≤` on a sigma type.  -/
PSigma.Lex.le : {ι : Type u_1} → {α : ι → Type u_2} → [LT ι] → [(i : ι) → LE (α i)] → LE (Σₗ' (i : ι), α i)
-- Mathlib.Tactic.Linter.Style
/-- `findLambdaSyntax stx` extracts from `stx` all syntax nodes of `kind` `Term.fun`.  -/
Mathlib.Linter.Style.lambdaSyntax.findLambdaSyntax : Lean.Syntax → Array Lean.Syntax
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_associator_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F G H : CategoryTheory.Functor C C) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.associator F G H).hom.app X =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) H).obj X)
-- Mathlib.Algebra.GroupWithZero.Basic
zero_zpow : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (n : ℤ), n ≠ 0 → 0 ^ n = 0
-- Mathlib.Topology.Algebra.Group.Torsor
ContinuousWithinAt.vsub : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : AddGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : TopologicalSpace α]
  {f g : α → P} {x : α} {s : Set α},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun x => f x -ᵥ g x) s x
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_self : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : R} (hx : x ∈ M), IsLocalization.mk' S x ⟨x, hx⟩ = 1
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.f_hasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i j k : self.J),
  CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_length_eq_nilpotencyClass`.

---

The nilpotency class of a nilpotent `G` is equal to the length of the lower central series.  -/
lowerCentralSeries_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
-- Mathlib.Logic.Equiv.Bool
Bool.not_bijective : Function.Bijective not
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.spanFinrank_maximalIdeal : ∀ {R : Type u_1} {inst : CommRing R} [self : IsRegularLocalRing R],
  ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) = ringKrullDim R
-- Mathlib.Order.Defs.PartialOrder
not_lt_of_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_id_f_map_mono : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) [CategoryTheory.Mono φ]
  (i : ℕ), CategoryTheory.Mono ((groupCohomology.cochainsMap (MonoidHom.id G) φ).f i)
-- Init.Data.Slice.Notation
/-- Slices `carrier` up to `range.upper` \(inclusive\).
   -/
Std.Ric.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Ric.Sliceable α β γ] → α → Std.Ric β → γ
-- Init.Data.Order.Classes
/-- This typeclass states that `max a b = if b ≤ a then a else b` (for any `DecidableLE α` instance).
 -/
Std.LawfulOrderLeftLeaningMax : (α : Type u) → [Max α] → [LE α] → Prop
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_zero_one' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left), CategoryTheory.ComposableArrows.Precomp.map F f 0 ⟨0 + 1, ⋯⟩ ⋯ = f
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
map_prod : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] {G : Type u_7}
  [inst_2 : FunLike G M N] [MonoidHomClass G M N] (g : G) (f : ι → M) (s : Finset ι),
  g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalSeminormedCommRing.mk : {α : Type u_5} →
  [toNonUnitalSeminormedRing : NonUnitalSeminormedRing α] → (∀ (a b : α), a * b = b * a) → NonUnitalSeminormedCommRing α
-- Std.Http.Data.Headers.Basic
/-- The content length in bytes.
 -/
Std.Http.Header.ContentLength.length : Std.Http.Header.ContentLength → ℕ
-- Mathlib.Control.Fix
_private.Mathlib.Control.Fix.0.Part.Fix.approx.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (i : ℕ) (h_1 : Unit → motive 0) (h_2 : (i : ℕ) → motive i.succ),
  (match i.succ with
    | 0 => h_1 ()
    | i.succ => h_2 i) =
    h_2 i
-- Mathlib.Data.Fintype.BigOperators
card_vector : ∀ {α : Type u_1} [inst : Fintype α] (n : ℕ), Fintype.card (List.Vector α n) = Fintype.card α ^ n
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.shiftFunctorObjXIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n i m : ℤ) (hm : m = i + n), K.shiftFunctorObjXIso n i m hm = K.shiftFunctorObjXIso n i m hm
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_eq_max_inv : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {a : α}, |a|ₘ = max a a⁻¹
-- Init.Data.String.Lemmas.Intercalate
String.intercalate_cons_of_ne_nil : ∀ {s t : String} {l : List String}, l ≠ [] → s.intercalate (t :: l) = t ++ s ++ s.intercalate l
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, local version for any measure.
Let filters `l` and `l'` be related by `TendstoIxxClass Ioc`.
If `f` has a finite limit `c` at `l ⊓ ae μ`, where `μ` is a measure
finite at `l`, then `∫ x in u..v, f x ∂μ = -μ (Ioc v u) • c + o(μ(Ioc v u))` as both
`u` and `v` tend to `l` so that `v ≤ u`.

See also `measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge` for a version assuming
`[intervalIntegral.FTCFilter a l l']` and `[MeasureTheory.IsLocallyFiniteMeasure μ]`. If `l` is one
of `𝓝[≥] a`, `𝓝[≤] a`, `𝓝 a`, then it's easier to apply the non-primed version. The primed version
also works, e.g., for `l = l' = Filter.atTop`.  -/
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {c : E}
  {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [CompleteSpace E]
  [l'.IsMeasurablyGenerated] [Filter.TendstoIxxClass Set.Ioc l l'],
  StronglyMeasurableAtFilter f l' μ →
    Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c) →
      μ.FiniteAtFilter l' →
        Filter.Tendsto u lt l →
          Filter.Tendsto v lt l →
            v ≤ᶠ[lt] u →
              (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ + μ.real (Set.Ioc (v t) (u t)) • c) =o[lt] fun t =>
                μ.real (Set.Ioc (v t) (u t))
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
PowerBasis.ofAdjoinEqTop'.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x x_1 : S} (e_x : x = x_1)
  (hx : IsIntegral R x) (hx' : R[x] = ⊤), PowerBasis.ofAdjoinEqTop' hx hx' = PowerBasis.ofAdjoinEqTop' ⋯ ⋯
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.one_le_sum_inv_index_of_leftCoset_cover : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ → 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The comultiplication on the tensor product of two comonoids is
the tensor product of the comultiplications followed by the tensor strength
(to shuffle the factors back into order).
 -/
CategoryTheory.Comon.tensorObj_comul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A B : C) [inst_3 : CategoryTheory.ComonObj A]
  [inst_4 : CategoryTheory.ComonObj B],
  CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.MonoidalCategory.tensorμ A A B B)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.degree = p.support.max
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.insert.sizeOf_spec : ∀ {basis : Tactic.ComputeAsymptotics.Basis} (f : ℝ → ℝ) (ex : Tactic.ComputeAsymptotics.BasisExtension basis),
  sizeOf (Tactic.ComputeAsymptotics.BasisExtension.insert f ex) = 1 + sizeOf basis + sizeOf ex
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.indefiniteDiagonal_transform : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) [inst : DecidableEq p] [inst_1 : DecidableEq q] [inst_2 : CommRing R]
  [inst_3 : Fintype p] [inst_4 : Fintype q] {i : R},
  i * i = -1 →
    (LieAlgebra.Orthogonal.Pso p q R i).transpose * LieAlgebra.Orthogonal.indefiniteDiagonal p q R *
        LieAlgebra.Orthogonal.Pso p q R i =
      1
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.proj.inj : ∀ {a : Lean.Name} {a_1 a_2 : ℕ} {a_3 : Lean.Name} {a_4 a_5 : ℕ},
  Lean.Meta.DiscrTree.Key.proj a a_1 a_2 = Lean.Meta.DiscrTree.Key.proj a_3 a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.injective : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  Function.Injective ⇑e
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The left lift along the identity.  -/
CategoryTheory.Bicategory.LeftLift.alongId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a c : B} → (g : c ⟶ a) → CategoryTheory.Bicategory.LeftLift (CategoryTheory.CategoryStruct.id a) g
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- An equivalent expression of `IsSemilinearSet` in terms of `Finset` instead of `Set.Finite`.  -/
isSemilinearSet_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsSemilinearSet s ↔ ∃ S, (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ ↑S