mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Defs
isAddUnit_iff_exists_neg' : ∀ {M : Type u_1} [inst : AddMonoid M] [IsDedekindFiniteAddMonoid M] {a : M}, IsAddUnit a ↔ ∃ b, b + a = 0
-- Mathlib.Geometry.Manifold.Notation
/-- Captures information when a model with corners is the trivial model on a normed space
(or on an inner product space, which is also a normed space):
contains the expressions describing the normed space and its base field.

Searching for a model with corners will return an `Option NormedSpaceInfo`,
which is `some` if and only if the trivial model on a normed space was found.
 -/
Manifold.Elab.NormedSpaceInfo : Type
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget_createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat),
  AddCommGrpCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfNatIso
      (CategoryTheory.Iso.refl
        ((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).comp (CategoryTheory.forget AddGrpCat)))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.jp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.associator_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H I : CategoryTheory.AddGrp C),
  (CategoryTheory.MonoidalCategoryStruct.associator G H I).hom.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).hom
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- For any `a` and `b`, `a ≤ a * b`  -/
CanonicallyOrderedMul.le_mul_self : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : LE α} [self : CanonicallyOrderedMul α] (a b : α), a ≤ b * a
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.expandSimpleMatch : Lean.Syntax → Lean.Term → Lean.Ident → Lean.Term → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Star.TensorProduct
TensorProduct.instInvolutiveStar : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : StarAddMonoid A] →
              [inst_4 : Module R A] →
                [StarModule R A] →
                  [inst_6 : AddCommMonoid B] →
                    [inst_7 : StarAddMonoid B] →
                      [inst_8 : Module R B] → [StarModule R B] → InvolutiveStar (TensorProduct R A B)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.inv_mul_cancel.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] (a : Rack.PreEnvelGroup R),
  sizeOf (Rack.PreEnvelGroupRel'.inv_mul_cancel a) = 1 + sizeOf a
-- Mathlib.Order.Grade
/-- The grade of an element in a graded order. Morally, this is the number of elements you need to
go down by to get to `⊥`.  -/
grade : (𝕆 : Type u_1) → {α : Type u_3} → [inst : Preorder 𝕆] → [inst_1 : Preorder α] → [GradeOrder 𝕆 α] → α → 𝕆
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.consCollision.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (keys : Subarray α) (vals : Subarray β)
  (a : Std.Slice.size keys = Std.Slice.size vals) (a_1 : Lean.PersistentHashMap.Zipper α β),
  sizeOf (Lean.PersistentHashMap.Zipper.consCollision keys vals a a_1) =
    1 + sizeOf keys + sizeOf vals + sizeOf a + sizeOf a_1
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
LinearEquiv.isAssociatedPrime_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (l : M ≃ₗ[R] M'),
  IsAssociatedPrime I M ↔ IsAssociatedPrime I M'
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_alter_eq_sub_one : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      m.contains k = true → (f (m.get? k)).isNone = true → (↑(m.alter k f)).size = (↑m).size - 1
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E →L[𝕜] F) {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F] [T2Space F], UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (⇑f) s x = f
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.leftQuotientEquiv.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : AddSubgroup.IsComplement S ↑H),
  hS.leftQuotientEquiv = (Equiv.ofBijective (S.domRestrict QuotientAddGroup.mk) ⋯).symm
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesToE.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂),
  X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ =
    X.descOpcycles f₁₂ f₃ n₀ n₁ hn₁
      (CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)) ⋯
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpoint.ref : Lean.Elab.PartialFixpoint → Lean.Syntax
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The function `Real.exp` is real analytic.  -/
analyticOn_rexp : AnalyticOn ℝ Real.exp Set.univ
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.subset_iUnion : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), J ∈ π → ↑J ⊆ π.iUnion
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_update_smul_left : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (m : (i : ι) → M₁ i)
  (i : ι) (c : R) (x : M₁ i), f (Function.update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (Function.update m i x)
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.isAlgebraic_adjoin_simple_X' : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K), (¬∃ c, f = RatFunc.C c) → Algebra.IsAlgebraic (↥K⟮f⟯) (RatFunc K)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- Whiskering right of a `CatCospanTransformMorphism` by a `CatCospanTransform`.  -/
CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            {A'' : Type u₇} →
              {B'' : Type u₈} →
                {C'' : Type u₉} →
                  [inst : CategoryTheory.Category.{v₁, u₁} A] →
                    [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                      [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                        {F : CategoryTheory.Functor A B} →
                          {G : CategoryTheory.Functor C B} →
                            [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                              [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                                [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                                  {F' : CategoryTheory.Functor A' B'} →
                                    {G' : CategoryTheory.Functor C' B'} →
                                      [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] →
                                        [inst_7 : CategoryTheory.Category.{v₈, u₈} B''] →
                                          [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] →
                                            {F'' : CategoryTheory.Functor A'' B''} →
                                              {G'' : CategoryTheory.Functor C'' B''} →
                                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                                  (ψ ⟶ ψ') →
                                                    (φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') →
                                                      ψ.comp φ ⟶ ψ'.comp φ
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.instMonoι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.FinitaryExtensive C] {ι : Type u_1}
  [inst_2 : Finite ι] (X : ι → C) (i : ι), CategoryTheory.Mono (CategoryTheory.Limits.Sigma.ι X i)
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinMap.tensorDistrib_tmul : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₁]
  [inst_5 : AddCommMonoid N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁]
  [inst_9 : Module R N₁] [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : SMulCommClass R A N₁] [inst_14 : IsScalarTower R A N₁] [inst_15 : Module R M₂] [inst_16 : Module R N₂]
  (B₁ : LinearMap.BilinMap A M₁ N₁) (B₂ : LinearMap.BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂),
  (((LinearMap.BilinMap.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₁ m₁) m₁' ⊗ₜ[R] (B₂ m₂) m₂'
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) {A : C}
  (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁₂) ⟶ A)
  (h :
    CategoryTheory.CategoryStruct.comp ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) x = 0)
  (hn₁ : n₀ + 1 = n₁) (h' : CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) x = 0)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE._auto_1) {Z : C} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁)
      (CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
        (CategoryTheory.CategoryStruct.comp (X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂) h_1)) =
    CategoryTheory.CategoryStruct.comp x h_1
-- Init.Notation
/-- Boolean equality, notated as `a == b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `==` in identifiers is `beq`. -/
«term_==_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Exponent
/-- A predicate on a monoid saying that there is a positive integer `n` such that `g ^ n = 1`
for all `g`.  -/
Monoid.ExponentExists : (G : Type u) → [Monoid G] → Prop
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.notMem_range_embeddingUpIntGE_iff : ∀ (p n : ℤ), (∀ (i : ℕ), (ComplexShape.embeddingUpIntGE p).f i ≠ n) ↔ n < p
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.instT2Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T2Space M], T2Space Mᵐᵒᵖ
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.Monic = (p.leadingCoeff = 1)
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.isVersoKind : Lean.SyntaxNodeKind → Bool
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.mem_skewAdjointSubmodule : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} (f : Module.End R M),
  f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint ⇑f
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.swap.congr_simp : ∀ (R : Type u_1) {n : Type u_2} [inst : Zero R] [inst_1 : One R] {inst_2 : DecidableEq n} [inst_3 : DecidableEq n]
  (i i_1 : n),
  i = i_1 →
    ∀ (j j_1 : n),
      j = j_1 →
        ∀ (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → Matrix.swap R i j a a_2 = Matrix.swap R i_1 j_1 a_1 a_3
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.map_map : ∀ (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} {γ : Type v₃} (f : α → β) (g : β → γ) (x : ↑P α),
  P.map g (P.map f x) = P.map (g ∘ f) x
-- Init.Data.List.Nat.TakeDrop
List.lt_length_left_of_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {i : ℕ} {l : List α} {l' : List β},
  i < (List.zipWith f l l').length → i < l.length
-- Mathlib.Tactic.NormNum.Inv
/-- Helper function to synthesize a typed `CharZero α` expression given `Ring α`.  -/
Mathlib.Meta.NormNum.inferCharZeroOfRing : {u : Lean.Level} →
  {α : Q(Type u)} →
    (_i : autoParam Q(Ring «$α») Mathlib.Meta.NormNum.inferCharZeroOfRing._auto_1) → Lean.MetaM Q(CharZero «$α»)
-- Init.Data.List.Sublist
List.instDecidableIsPrefixOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : List α) → Decidable (l₁ <+: l₂)
-- Mathlib.Tactic.ToDual
lt_of_eq_of_lt'' : ∀ {α : Type u_1} {a b c : α} [inst : LT α], a = b → c < b → c < a
-- Mathlib.Analysis.Convex.Between
Sbtw.of_lt_of_lt : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {x y z : R},
  x < y → y < z → Sbtw R x y z
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_eq_zero_iff : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (n : ℤ), Mathlib.Tactic.FieldSimp.zpow' a n = 0 ↔ a = 0
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_zero_left : ∀ {R : Type u} [inst : CommSemiring R] {x : R}, IsCoprime 0 x ↔ IsUnit x
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↥X) (hxx' : x = x') {Z : CommRingCat}
  (h : X.presheaf.stalk x' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
      (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap g x') h)
-- Mathlib.GroupTheory.IsSubnormal
/-- The trivial subgroup is subnormal.  -/
Subgroup.IsSubnormal.bot : ∀ {G : Type u_1} [inst : Group G], ⊥.IsSubnormal
-- Lean.Elab.InfoTree.Types
/-- Pending child trees of a node.  -/
Lean.Elab.InfoState.trees : Lean.Elab.InfoState → Lean.PersistentArray Lean.Elab.InfoTree
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {X Y : C}
  (f : X ⟶ Y), Φ.prop f ↔ CategoryTheory.Arrow.mk f = Φ.toSuccArrow X
-- Mathlib.Analysis.InnerProductSpace.Calculus
OpenPartialHomeomorph.contDiff_univUnitBall : ∀ {n : ℕ∞} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E],
  ContDiff ℝ ↑n ↑OpenPartialHomeomorph.univUnitBall
-- Mathlib.Data.Fin.Fin2
/-- `castSucc i` embeds `i : Fin2 n` in `Fin2 (n+1)`.  -/
Fin2.castSucc : {n : ℕ} → Fin2 n → Fin2 (n + 1)
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.Arrow C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
      (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map.eq_1 : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  (p : (b : β) → f b ⟶ g b),
  CategoryTheory.Limits.Sigma.map p = CategoryTheory.Limits.colimMap (CategoryTheory.Discrete.natTrans fun X => p X.as)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toList_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  {f : (a : α) → β a → Option (γ a)},
  (Std.DHashMap.filterMap f m).toList.Perm
    (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) m.toList)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_le_mk_of_dvd : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : M}, a ∣ b → Associates.mk a ≤ Associates.mk b
-- Mathlib.LinearAlgebra.Basis.Defs
/-- `Basis.ofRepr` constructs a basis given an assignment of coordinates to each vector.  -/
Module.Basis.ofRepr : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M ≃ₗ[R] ι →₀ R) → Module.Basis ι R M
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_add : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)]
  {f g : ↑X.functionField},
  f + g ≠ 0 →
    min (AlgebraicGeometry.Scheme.ord f x) (AlgebraicGeometry.Scheme.ord g x) ≤ AlgebraicGeometry.Scheme.ord (f + g) x
-- Mathlib.Algebra.Group.Invertible.Basic
/-- Monoid homs preserve invertibility.  -/
Invertible.map : {R : Type u_1} →
  {S : Type u_2} →
    {F : Type u_3} →
      [inst : MulOneClass R] →
        [inst_1 : MulOneClass S] →
          [inst_2 : FunLike F R S] → [MonoidHomClass F R S] → (f : F) → (r : R) → [Invertible r] → Invertible (f r)
-- Mathlib.Order.Hom.Lex
Prod.Lex.prodLexCongr_apply : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {δ : Type u_7} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] (ea : α ≃o β) (eb : γ ≃o δ) (a : Lex (α × γ)),
  (Prod.Lex.prodLexCongr ea eb) a = toLex (Prod.map (⇑ea) (⇑eb) (ofLex a))
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
/-- The integral of `f (R⁻¹ • x)` with respect to an additive Haar measure is a multiple of the
integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
thanks to the convention that a non-integrable function has integral zero.  -/
MeasureTheory.Measure.integral_comp_inv_smul_of_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F] (f : E → F) {R : ℝ},
  0 ≤ R → ∫ (x : E), f (R⁻¹ • x) ∂μ = R ^ Module.finrank ℝ E • ∫ (x : E), f x ∂μ
-- Mathlib.Algebra.Module.Basic
Set.indicator_smul : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (s : Set α) (r : α → R)
  (f : α → M), (s.indicator fun a => r a • f a) = fun a => r a • s.indicator f a
-- Mathlib.Analysis.Convex.Segment
Convex.combo_le_max : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] {a b : 𝕜} (x y : E),
  0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ≤ max x y
-- Mathlib.Data.Sigma.Lex
Sigma.Lex.decidable : {ι : Type u_1} →
  {α : ι → Type u_2} →
    (r : ι → ι → Prop) →
      (s : (i : ι) → α i → α i → Prop) →
        [DecidableEq ι] → [DecidableRel r] → [(i : ι) → DecidableRel (s i)] → DecidableRel (Sigma.Lex r s)
-- Mathlib.Topology.Order.CountableSeparating
Filter.EventuallyEq.of_forall_eventually_le_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X},
  (∀ (x : X), ∀ᶠ (a : α) in l, f a ≤ x ↔ g a ≤ x) → f =ᶠ[l] g
-- Init.Data.OfScientific
/-- Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite
floating-point value if the range of `Float` is exceeded.
 -/
Nat.toFloat : ℕ → Float
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The quotient `G ⧸ N` of a complete first countable topological group `G` by a normal subgroup
is itself complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Because a topological group is not equipped with a `UniformSpace` instance by default, we must
explicitly provide it in order to consider completeness. See `QuotientGroup.completeSpace_right` for
a version in which `G` is already equipped with a uniform structure.  -/
QuotientGroup.completeSpace_right' : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] [FirstCountableTopology G]
  (N : Subgroup G) [inst_4 : N.Normal] [CompleteSpace G], CompleteSpace (G ⧸ N)
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Multiplication on the left by a nonzero element of a normed division ring tends to infinity at
infinity.  -/
Filter.tendsto_mul_left_cobounded : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {a : α},
  a ≠ 0 → Filter.Tendsto (fun x => a * x) (Bornology.cobounded α) (Bornology.cobounded α)
-- Mathlib.GroupTheory.Sylow
/-- A Sylow p-subgroup has index indivisible by `p`.  -/
Sylow.not_dvd_index : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex], ¬p ∣ (↑P).index
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Evidence that `rightAdjoint f` is a right adjoint of `f`.  -/
CategoryTheory.Bicategory.Adjunction.ofIsLeftAdjoint : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : a ⟶ b) →
        [inst_1 : CategoryTheory.Bicategory.IsLeftAdjoint f] →
          CategoryTheory.Bicategory.Adjunction f (CategoryTheory.Bicategory.rightAdjoint f)
-- Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryPreExtensive C] {F G : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ G)
  [CategoryTheory.Limits.PreservesFiniteProducts F] [CategoryTheory.Limits.PreservesFiniteProducts G],
  CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f →
    CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Ioi_add_eq_sum_Ici : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrderTop α] (a : α), ∑ x > a, f x + f a = ∑ x ≥ a, f x
-- Init.Data.Option.Lemmas
Option.isSome_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α}, (o ⊓ o').isSome = (o.isSome && o'.isSome)