mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C] (app : (a : B) → F.obj a ⟶ G.obj a)
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (app a) (G.map f) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (app b))
  (naturality_naturality :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η))
            (naturality g).hom)
      CategoryTheory.Lax.StrongTrans.naturality_naturality._autoParam)
  (naturality_id :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))
            (naturality (CategoryTheory.CategoryStruct.id a)).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).inv
              (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))))
      CategoryTheory.Lax.StrongTrans.naturality_id._autoParam)
  (naturality_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g))
            (naturality (CategoryTheory.CategoryStruct.comp f g)).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (naturality f).hom (G.map g))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g).hom)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).inv
                    (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c)))))))
      CategoryTheory.Lax.StrongTrans.naturality_comp._autoParam),
  sizeOf
      { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
        naturality_id := naturality_id, naturality_comp := naturality_comp } =
    1
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
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]
  [IsNoetherianRing R], IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ x, I = ⊥.colon {x}
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processNullaryOrCat : Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Init.Data.ToString.Name
_private.Init.Data.ToString.Name.0.Lean.Name.needsNoEscapeAsciiRest : String → ℕ → Bool
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  ContDiffOn ℝ 1 f (Set.Icc a b) → a ≤ b → ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Set.Icc a b, ‖deriv f x‖ₑ
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.abs_sub_le_sub_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a b c : α}, a ∈ s → b ∈ s → c ∈ s → b ≤ c → |f c - f b| ≤ variationOnFromTo f s a c - variationOnFromTo f s a b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the right type  -/
CategoryTheory.Limits.MultispanShape.R : CategoryTheory.Limits.MultispanShape → Type w'
-- Mathlib.CategoryTheory.Sites.Canonical
/-- Check that if each `P ∈ Ps` is a sheaf for `J`, then `J` is a subtopology of `finestTopology Ps`.
 -/
CategoryTheory.Sheaf.le_finestTopology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type w)))
  (J : CategoryTheory.GrothendieckTopology C),
  (∀ P ∈ Ps, CategoryTheory.Presieve.IsSheaf J P) → J ≤ CategoryTheory.Sheaf.finestTopology Ps
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.inclCompMap_hom_app : ∀ {I : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I)
  (j : J) (X : C (g j)), (CategoryTheory.Sigma.inclCompMap C g j).hom.app X = CategoryTheory.CategoryStruct.id ⟨g j, X⟩
-- Mathlib.Order.Bounds.Image
AntitoneOn.mem_upperBounds_image_self : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α} {a : α},
  AntitoneOn f t → a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The `SeminormedRing` structure on a ring `R` determined by a `RingSeminorm`.  -/
RingSeminorm.toSeminormedRing : {R : Type u_1} → [inst : Ring R] → RingSeminorm R → SeminormedRing R
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.ext_elem : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) ⦃x y : S⦄, (∀ i < f.natDegree, h.coeff x i = h.coeff y i) → x = y
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.deriv_log : ∀ (x : ℝ), deriv Real.log x = x⁻¹
-- Mathlib.Algebra.Group.Conj
AddMonoidHom.map_isAddConj : ∀ {α : Type u} {β : Type v} [inst : AddMonoid α] [inst_1 : AddMonoid β] (f : α →+ β) {a b : α},
  IsAddConj a b → IsAddConj (f a) (f b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_snd_app : ∀ {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} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [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₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y)
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x : X),
  ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom.app
            X_1).snd.app
      x =
    CategoryTheory.CategoryStruct.id (ψ.right.obj (X_1.snd.obj (U.obj x)))
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.Scheme.IsGermInjectiveAt.mk : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X},
  (∃ U,
      ∃ (hx : x ∈ U),
        AlgebraicGeometry.IsAffineOpen U ∧
          Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))) →
    X.IsGermInjectiveAt x
-- Mathlib.MeasureTheory.Measure.Regular
/-- Outer regular measures are determined by values on bounded open sets.  -/
MeasureTheory.Measure.OuterRegular.ext_isOpen_isBounded : ∀ {α : Type u_3} [inst : PseudoMetricSpace α] {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.OuterRegular]
  [ν.OuterRegular], (∀ (U : Set α), IsOpen U → Bornology.IsBounded U → μ U = ν U) → μ = ν
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.ofAlgEquiv_toPreSubmersivePresentation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) {T : Type u_1} [inst_4 : CommRing T]
  [inst_5 : Algebra R T] (e : S ≃ₐ[R] T), (P.ofAlgEquiv e).toPreSubmersivePresentation = P.ofAlgEquiv e
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_mul : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b : α), ↑(a * b) = ↑a * ↑b
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.ofAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Normal] [inst_2 : H.FiniteIndex],
  FiniteIndexNormalAddSubgroup.ofAddSubgroup H = { toAddSubgroup := H, isNormal' := ⋯, isFiniteIndex' := ⋯ }
-- Lean.Message
/-- Calls `withExprHover`, but uses the current local context if one is not given.
See `withExprHover` for a description of each parameter.
 -/
Lean.MessageData.withExprHoverM : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLCtx m] →
      Std.Format →
        Lean.Expr →
          optParam (Option Lean.LocalContext) none →
            optParam (Option Lean.DeclarationLocation) none →
              optParam (Option String) none →
                optParam (Option (Lean.PPContext → IO String)) none → optParam Bool false → m Lean.MessageData
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctor_obj_d' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n i j : ℤ),
  ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j =
    n.negOnePow • K.d (i + { as := n }.as) (j + { as := n }.as)
-- Mathlib.Logic.Equiv.List
/-- If `α` is countable, then so is `Multiset α`.  -/
Multiset.countable : ∀ {α : Type u_1} [Countable α], Countable (Multiset α)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instOneHom : (G H : CommGrpCat) → One (G ⟶ H)
-- Mathlib.Order.CompleteLattice.PiLex
_private.Mathlib.Order.CompleteLattice.PiLex.0.Pi.Lex.inf.congr_simp : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] (s s_1 : Set (Lex ((i : ι) → (fun i => α i) i))),
  s = s_1 → ∀ (i : ι), Pi.Lex.inf✝ s i = Pi.Lex.inf✝ s_1 i
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.finite_support : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i), {i | f i ≠ 0}.Finite
-- Lean.Elab.InfoTree.Basic
/-- Applies `s.lazyAssignment` to `s.trees`, asynchronously.  -/
Lean.Elab.InfoState.substituteLazy : Lean.Elab.InfoState → Task Lean.Elab.InfoState
-- Mathlib.Order.SymmDiff
le_symmDiff_sup_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ≤ symmDiff a b ⊔ b
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
isCyclic_left_of_prod : ∀ (M : Type u_4) (N : Type u_5) [inst : Group M] [inst_1 : Group N] [cyc : IsCyclic (M × N)], IsCyclic M
-- Mathlib.Order.Atoms
IsAtom.ne_bot_iff_eq : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, IsAtom a → b ≤ a → (b ≠ ⊥ ↔ b = a)
-- ProofWidgets.Data.Html
/-- Interpolates an expression into a JSX attribute literal.  -/
ProofWidgets.Jsx.«proofWidgetsJsxAttrVal{_}» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If for any finitely generated submodules `M'` of `M`, `M'` and `N` are linearly disjoint,
then `M` and `N` themselves are linearly disjoint.  -/
Submodule.LinearDisjoint.of_linearDisjoint_fg_left : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  (∀ M' ≤ M, M'.FG → M'.LinearDisjoint N) → M.LinearDisjoint N
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.of_comap : ∀ {R : Type u} {M : Type v} {N : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] N),
  Function.Surjective ⇑f → ∀ (S : Submodule R N) [hI : (Submodule.comap f S).IsPrincipal], S.IsPrincipal
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map : ∀ {X : AlgebraicGeometry.Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat)
  (α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F)
  (H : CategoryTheory.NatTrans.Coequifibered α) {U : X.AffineZariskiSite} (r : ↑(X.presheaf.obj (Opposite.op ↑U))),
  AlgebraicGeometry.Scheme.Hom.opensRange
      ((AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData H).functor.map (CategoryTheory.homOfLE ⋯)) =
    PrimeSpectrum.basicOpen ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U))) r)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.domCongr_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N) (m : M) (a : A),
  (AddMonoidAlgebra.domCongr R A e) (AddMonoidAlgebra.single m a) = AddMonoidAlgebra.single (e m) a
-- Mathlib.Topology.Algebra.FilterBasis
addGroupFilterBasisOfComm.eq_1 : ∀ {G : Type u_1} [inst : AddCommGroup G] (sets : Set (Set G)) (nonempty : sets.Nonempty)
  (inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) (one : ∀ U ∈ sets, 0 ∈ U)
  (mul : ∀ U ∈ sets, ∃ V ∈ sets, V + V ⊆ U) (inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x => -x) ⁻¹' U),
  addGroupFilterBasisOfComm sets nonempty inter_sets one mul inv =
    { sets := sets, nonempty := nonempty, inter_sets := ⋯, zero' := ⋯, add' := ⋯, neg' := ⋯, conj' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_mono_set' : ∀ {α : Type u_1} {x : MeasurableSpace α} ⦃μ : MeasureTheory.Measure α⦄ {s t : Set α} {f : α → ENNReal},
  s ≤ᵐ[μ] t → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroupClass.normedAddCommGroup.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : AddSubgroupClass S E]
  (s : S),
  AddSubgroupClass.normedAddCommGroup s =
    { toNorm := (AddSubgroupClass.seminormedAddCommGroup s).toNorm, toAddCommGroup := AddSubgroupClass.toAddCommGroup s,
      toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
OrthonormalBasis.toBasis_tensorProduct : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι₁ : Type u_6}
  {ι₂ : Type u_7} [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E)
  (b₂ : OrthonormalBasis ι₂ 𝕜 F), (b₁.tensorProduct b₂).toBasis = b₁.toBasis.tensorProduct b₂.toBasis
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructor.match_3.splitter : (motive : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u_1) →
  (ps : List Lean.Elab.Tactic.RCases.RCasesPatt) →
    (Unit → motive []) →
      ((p : Lean.Elab.Tactic.RCases.RCasesPatt) → motive [p]) →
        ((ps : List Lean.Elab.Tactic.RCases.RCasesPatt) →
            (ps = [] → False) → (∀ (p : Lean.Elab.Tactic.RCases.RCasesPatt), ps = [p] → False) → motive ps) →
          motive ps
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.IndepFun.integral_smul_eq_smul_integral : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E]
  [BorelSpace E] {X : Ω → 𝕜} {Y : Ω → E},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.AEStronglyMeasurable X μ →
      MeasureTheory.AEStronglyMeasurable Y μ → ∫ (x : Ω), (X • Y) x ∂μ = (∫ (x : Ω), X x ∂μ) • ∫ (x : Ω), Y x ∂μ
-- Lean.Meta.Tactic.Apply
Lean.MVarId.splitAndCore : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- The field `natToIntMap` contains a mapping
from a `Nat`-term `e` to the pair `(e', he)`, where
`he : NatCast.natCast e = e'`
 -/
Lean.Meta.Grind.Arith.Cutsat.State.natToIntMap : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isNonneg_zero : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {I₁ I₂ : R →+* R} [inst_3 : Preorder R], LinearMap.IsNonneg 0
-- Mathlib.GroupTheory.Complement
Subgroup.smul_leftQuotientEquiv : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {F : Type u_2} [inst_1 : Group F] [inst_2 : MulAction F G]
  [inst_3 : MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H),
  f • ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv (f • q))
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_iff`.

---

Definition of `IsLittleO` in terms of filters.  -/
Asymptotics.IsLittleO.bound : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[l] g → ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Init.Data.SInt.Basic
/-- Signed 64-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 64-bit value.
 -/
Int64 : Type
-- Init.Data.Rat.Lemmas
Rat.add_def' : ∀ (a b : ℚ), a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerTotal_mkQ_single_add : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x y z : S),
  ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | x + y => z) =
    ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | x => z) + (KaehlerDifferential.kerTotal R S).mkQ fun₀ | y => z
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- A version of `fderiv_const_smul` without differentiability hypothesis: in return, the constant
`c` must be invertible, i.e. if `R` is a field.  -/
fderiv_const_smul_of_invertible : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F] (c : R) [Invertible c], fderiv 𝕜 (c • f) x = c • fderiv 𝕜 f x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.mk : {G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} →
      [inst_1 : TopologicalSpace H] →
        [inst_2 : Mul G] →
          [inst_3 : Mul H] →
            (toMulEquiv : G ≃* H) →
              autoParam (Continuous toMulEquiv.toFun) Homeomorph.continuous_toFun._autoParam →
                autoParam (Continuous toMulEquiv.invFun) Homeomorph.continuous_invFun._autoParam → G ≃ₜ* H
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : DecidableEq M] (x y : MonoidAlgebra R M)
  (m : M), (x * y).coeff m = x.coeff.sum fun m₁ r₁ => y.coeff.sum fun m₂ r₂ => if m₁ * m₂ = m then r₁ * r₂ else 0
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- Given `f : X.PtSimplex n x` and `i : Fin n` (note that this implies `n ≠ 0`),
this is the term in `MulStruct f .const f i` corresponding to
`stdSimplex.σ i.succ ≫ f.map`.  -/
SSet.PtSimplex.MulStruct.mulOne : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      (f : X.PtSimplex n x) → (i : Fin n) → f.MulStruct SSet.RelativeMorphism.const f i
-- Mathlib.Data.Fin.Tuple.Basic
/-- Recurse on a tuple by splitting into `Fin.elim0` and `Fin.snoc`.  -/
Fin.snocInduction : {α : Sort u_2} →
  {motive : {n : ℕ} → (Fin n → α) → Sort u_3} →
    motive Fin.elim0 →
      ({n : ℕ} → (x : Fin n → α) → (x₀ : α) → motive x → motive (Fin.snoc x x₀)) → {n : ℕ} → (x : Fin n → α) → motive x
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.sumInl_toMatrix_prod_mul : ∀ {n : Type u_1} (p : Type u_2) {R : Type u₂} [inst : DecidableEq n] [inst_1 : DecidableEq p] [inst_2 : CommRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype p] (M : Matrix n n R) (L : List (Matrix.TransvectionStruct n R))
  (N : Matrix p p R),
  (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.sumInl p) L).prod *
      Matrix.fromBlocks M 0 0 N =
    Matrix.fromBlocks ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M) 0 0 N
-- Mathlib.Combinatorics.SimpleGraph.Basic
Sym2.Mem.other.congr_simp : ∀ {α : Type u_1} {a a_1 : α} (e_a : a = a_1) {z z_1 : Sym2 α} (e_z : z = z_1) (h : a ∈ z),
  Sym2.Mem.other h = Sym2.Mem.other ⋯
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.instFintype : (G : Type u_1) → (R : Type u_3) → [inst : AddCommGroup G] → [inst_1 : RCLike R] → [Finite G] → Fintype (AddChar G R)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.cooper_dvd_left_core : ∀ {a b c d s p q x : ℤ},
  a < 0 →
    0 < b →
      0 < d →
        a * x + p ≤ 0 →
          b * x + q ≤ 0 →
            d ∣ c * x + s →
              Int.Internal.Linear.OrOver (a.lcm (a * d / ↑((a * d).gcd c))) fun k =>
                b * p + -a * q + b * ↑k ≤ 0 ∧ a ∣ p + ↑k ∧ a * d ∣ c * p + -a * s + c * ↑k
-- Mathlib.Topology.UniformSpace.Defs
symm_of_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α}, s ∈ uniformity α → ∃ t ∈ uniformity α, SetRel.IsSymm t ∧ t ⊆ s
-- Init.Data.Nat.Lemmas
Nat.zero_shiftLeft : ∀ (n : ℕ), 0 <<< n = 0
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.smul_const_lt : ∀ {α : Type u_1} {b c : α} {K : Type u_2} [inst : Semiring K] [inst_1 : PartialOrder K] [inst_2 : AddCommMonoid α]
  [inst_3 : PartialOrder α] [inst_4 : Module K α] [PosSMulStrictMono K α], b < c → ∀ {s : K}, 0 < s → s • b < s • c
-- Lean.Elab.InfoTree.Main
Lean.Elab.ErrorNameInfo.format : Lean.Elab.ContextInfo → Lean.Elab.ErrorNameInfo → IO Std.Format
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.mem_primesOver_iff_mem_normalizedFactors : ∀ {R : Type u_1} (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {p : Ideal R}
  [h : p.IsMaximal] [inst_3 : Algebra R A] [IsDomain R] [Module.IsTorsionFree R A],
  p ≠ ⊥ →
    ∀ {P : Ideal A}, P ∈ p.primesOver A ↔ P ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R A) p)
-- Mathlib.Data.Complex.Basic
Complex.smul_re : ∀ {R : Type u_1} [inst : SMul R ℝ] (r : R) (z : ℂ), (r • z).re = r • z.re
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mapAlongMonoidHom.eq_1 : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂}
  {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)]
  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁)
  (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [inst_2 : (i : ι₁) → Monoid (R₁ i)] [inst_3 : (i : ι₂) → Monoid (R₂ i)]
  [inst_4 : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] [inst_5 : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)]
  (φ : (j : ι₂) → R₁ (f j) →* R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)),
  RestrictedProduct.mapAlongMonoidHom R₁ R₂ f hf φ hφ =
    { toFun := RestrictedProduct.mapAlong R₁ R₂ f hf (fun j r => (φ j) r) hφ, map_one' := ⋯, map_mul' := ⋯ }