mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.stabilizerEquiv_symm_apply_smul : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {N : Type u_4}
  [inst_3 : Group N] [inst_4 : MulSemiringAction N R] (I : Ideal R) (e : M ≃* N)
  (he : ∀ (m : M) (x : R), e m • x = m • x) (n : ↥(MulAction.stabilizer N I)) (x : R),
  (I.stabilizerEquiv e he).symm n • x = n • x
-- Lean.Elab.App
/-- Context of the `elab_as_elim` elaboration procedure.  -/
Lean.Elab.Term.ElabElim.Context : Type
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.reassignToTerm : Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_hom : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U), hU.isoSpec.hom = U.toSpecΓ
-- Mathlib.CategoryTheory.Comma.Basic
/-- A natural isomorphism `L₁ ≅ L₂` induces an equivalence of categories
`Comma L₁ R ≌ Comma L₂ R`.  -/
CategoryTheory.Comma.mapLeftIso : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (R : CategoryTheory.Functor B T) →
              {L₁ L₂ : CategoryTheory.Functor A T} → (L₁ ≅ L₂) → (CategoryTheory.Comma L₁ R ≌ CategoryTheory.Comma L₂ R)
-- Init.Data.Nat.Control
_private.Init.Data.Nat.Control.0.Nat.forM.loop : {m : Type → Type u_1} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → m Unit) → (i : ℕ) → i ≤ n → m Unit
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R],
  (CategoryTheory.forget₂ (TopModuleCat R) TopCat).IsRightAdjoint
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.trunc_pderiv : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : DecidableEq σ] {i : σ} (f : MvPowerSeries σ R)
  (n : σ →₀ ℕ),
  (MvPowerSeries.trunc R n) ((MvPowerSeries.pderiv R i) f) =
    (MvPolynomial.pderiv i) ((MvPowerSeries.trunc R (n + fun₀ | i => 1)) f)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- Let `F` be a functor from sheaf of `R`-module to sheaf of `S`-module, if `F` preserves
colimits and `F.obj (unit R) ≅ unit S`, given generating sections `G : M.GeneratingSections`,
then we obtain generating sections of `F.obj M`.  -/
SheafOfModules.GeneratingSections.map : {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] →
            {C' : Type u₁} →
              [inst_3 : CategoryTheory.Category.{v₁, u₁} C'] →
                {J' : CategoryTheory.GrothendieckTopology C'} →
                  {S : CategoryTheory.Sheaf J' RingCat} →
                    [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] →
                      [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat] →
                        {M : SheafOfModules R} →
                          M.GeneratingSections →
                            (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) →
                              [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁,
                                      max (max (u + 1) u') v', max (max (u + 1) u₁) v₁}
                                    F] →
                                (SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) → (F.obj M).GeneratingSections
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- The complex unit disc, denoted as `𝔻` within the Complex namespace  -/
Complex.UnitDisc : Type
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instInfSet : {G : Type u_1} → [inst : Group G] → InfSet (Subgroup G)
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.limit_mon_mul : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.MonObj.mul =
    hc.lift
      { pt := CategoryTheory.MonoidalCategoryStruct.tensorObj c.1 c.1,
        π :=
          {
            app := fun X =>
              CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.tensorHom (c.π.app X) (c.π.app X)) CategoryTheory.MonObj.mul,
            naturality := ⋯ } }
-- Mathlib.Data.Set.Function
/-- **Alias** of the forward direction of `Set.eqOn_range`. -/
Set.EqOn.comp_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_7} {f : ι → α} {g₁ g₂ : α → β},
  Set.EqOn g₁ g₂ (Set.range f) → g₁ ∘ f = g₂ ∘ f
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.instMeasurableAdd₂ : ∀ {α : Type u_3} {m : MeasurableSpace α}, MeasurableAdd₂ (MeasureTheory.Measure α)
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_div_cancel_right'` for a stronger version.  -/
ENNReal.mul_div_cancel_right : ∀ {a b : ENNReal}, b ≠ 0 → b ≠ ⊤ → a * b / b = a
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntryD.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (fallback : (a : α) × β a)
  (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getEntryD a fallback x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => fallback
    | Std.DHashMap.Internal.AssocList.cons k v es =>
      if (k == a) = true then ⟨k, v⟩ else Std.DHashMap.Internal.AssocList.getEntryD a fallback es
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.coeff_comp_degree_mul_degree : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  q.natDegree ≠ 0 → (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.valuation_Δ_aux.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K),
  WeierstrassCurve.valuation_Δ_aux R W =
    if h : WeierstrassCurve.IsIntegral R W then
      ⟨(IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ, ⋯⟩
    else ⟨⊥, WeierstrassCurve.valuation_Δ_aux._proof_4⟩
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_empty : ∀ {X : Type u_2} [inst : EMetricSpace X], dimH ∅ = 0
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Restriction along open immersions commutes with taking stalks.  -/
AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      (x : ↥X) →
        (AlgebraicGeometry.Scheme.Modules.restrictFunctor f).comp
            ((AlgebraicGeometry.Scheme.Modules.toPresheaf X).comp (TopCat.Presheaf.stalkFunctor Ab x)) ≅
          (AlgebraicGeometry.Scheme.Modules.toPresheaf Y).comp (TopCat.Presheaf.stalkFunctor Ab (f x))
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodal_insert_eq_nodal : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [inst_1 : DecidableEq ι] {i : ι},
  i ∉ s → Lagrange.nodal (insert i s) v = (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal s v
-- Init.Prelude
/-- `a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. -/
HDiv.hDiv : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HDiv α β γ] → α → β → γ
-- Mathlib.RingTheory.Valuation.Basic
Valuation.toMonoidWithZeroHom : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : LinearOrderedCommMonoidWithZero Γ₀] → [inst_1 : Ring R] → Valuation R Γ₀ → R →*₀ Γ₀
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_modify_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k} {h : k ∈ m.modify k f}, (m.modify k f).get k h = f (m.get k ⋯)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.nonempty_orbit : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] (a : α), (AddAction.orbit M a).Nonempty
-- Mathlib.Topology.Defs.Basic
/-- Notation for `closure` with respect to a non-standard topology.  -/
Topology.closure_of : Lean.ParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure'.below.id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure' x → Prop} (x : C),
  CategoryTheory.MorphismProperty.multiplicativeClosure'.below ⋯
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instCommMonoid : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [CommMonoid Y] → CommMonoid (LocallyConstant X Y)
-- Mathlib.Algebra.Star.Conjneg
conjneg_inj : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] {f g : G → R},
  conjneg f = conjneg g ↔ f = g
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.IntFractPair.stream_zero : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K),
  GenContFract.IntFractPair.stream v 0 = some (GenContFract.IntFractPair.of v)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The trivial monoid algebra is the base ring.  -/
AddMonoidAlgebra.uniqueAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : AddMonoid M] → [Subsingleton M] → AddMonoidAlgebra A M ≃ₐ[R] A
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.addHaarMeasure.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G),
  MeasureTheory.Measure.addHaarMeasure K₀ =
    ((MeasureTheory.Measure.haar.addHaarContent K₀).measure ↑K₀)⁻¹ •
      (MeasureTheory.Measure.haar.addHaarContent K₀).measure
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} (self : F.HomObj G A) {c d : C} (f : c ⟶ d)
  (a : A.obj c) {Z : D} (h : G.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f)
      (CategoryTheory.CategoryStruct.comp (self.app d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) h) =
    CategoryTheory.CategoryStruct.comp (self.app c a) (CategoryTheory.CategoryStruct.comp (G.map f) h)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.getElimExprInfo : Lean.Expr → optParam (Option Lean.Name) none → Lean.MetaM Lean.Meta.ElimInfo
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.mk.injEq : ∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier : Set α) (isIrreducible' : IsIrreducible carrier)
  (isClosed' : IsClosed carrier) (carrier_1 : Set α) (isIrreducible'_1 : IsIrreducible carrier_1)
  (isClosed'_1 : IsClosed carrier_1),
  ({ carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' } =
      { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 }) =
    (carrier = carrier_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory)
      (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.counitIso.hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.nhds_hasBasis : ∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {a : α}, (nhds a).HasBasis (fun t => t ∈ b ∧ a ∈ t) fun t => t
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommRing.mk.inj : ∀ {toRing : Lean.Meta.Sym.Arith.Ring} {invFn? : Option Lean.Expr} {semiringId? : Option ℕ}
  {commSemiringInst commRingInst : Lean.Expr} {noZeroDivInst? fieldInst? : Option Lean.Expr}
  {toRing_1 : Lean.Meta.Sym.Arith.Ring} {invFn?_1 : Option Lean.Expr} {semiringId?_1 : Option ℕ}
  {commSemiringInst_1 commRingInst_1 : Lean.Expr} {noZeroDivInst?_1 fieldInst?_1 : Option Lean.Expr},
  { toRing := toRing, invFn? := invFn?, semiringId? := semiringId?, commSemiringInst := commSemiringInst,
        commRingInst := commRingInst, noZeroDivInst? := noZeroDivInst?, fieldInst? := fieldInst? } =
      { toRing := toRing_1, invFn? := invFn?_1, semiringId? := semiringId?_1, commSemiringInst := commSemiringInst_1,
        commRingInst := commRingInst_1, noZeroDivInst? := noZeroDivInst?_1, fieldInst? := fieldInst?_1 } →
    toRing = toRing_1 ∧
      invFn? = invFn?_1 ∧
        semiringId? = semiringId?_1 ∧
          commSemiringInst = commSemiringInst_1 ∧
            commRingInst = commRingInst_1 ∧ noZeroDivInst? = noZeroDivInst?_1 ∧ fieldInst? = fieldInst?_1
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- UV-compression reduces the size of the shadow of `𝒜` if, for all `x ∈ u` there is `y ∈ v` such
that `𝒜` is `(u.erase x, v.erase y)`-compressed. This is the key fact about compression for
Kruskal-Katona.  -/
UV.shadow_compression_subset_compression_shadow : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} (u v : Finset α),
  (∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) →
    (UV.compression u v 𝒜).shadow ⊆ UV.compression u v 𝒜.shadow
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_ext_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {X Y : C} {f : J → C}
  {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Y},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) g =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h) →
    g = h
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.submoduleOf_sup_of_le : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N₁ N₂ N : Submodule R M}, N₁ ≤ N → N₂ ≤ N → (N₁ ⊔ N₂).submoduleOf N = N₁.submoduleOf N ⊔ N₂.submoduleOf N
-- Mathlib.Analysis.Distribution.Support
Distribution.TemperedDistribution.IsVanishingOn.lineDerivOp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] {f : TemperedDistribution E F} {s : Set E},
  Distribution.IsVanishingOn (⇑f) s → ∀ (m : E), Distribution.IsVanishingOn (⇑(LineDeriv.lineDerivOp m f)) s
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.compHom'_apply_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddCommMonoid P]
  (f : M →+ N) (y : N →+ P) (x : M), (f.compHom' y) x = y (f x)
-- Lean.MetavarContext
Lean.MetavarContext.incDepth : Lean.MetavarContext → optParam Bool false → Lean.MetavarContext
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_col_zero_eq : ∀ {α : Type u_1} {n : Type u_3} [inst : SubtractionMonoid n] (v : n → α) (i : n), Matrix.circulant v i 0 = v i
-- Mathlib.CategoryTheory.Skeletal
/-- The class of an object in the skeleton.  -/
CategoryTheory.toSkeleton : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → C → CategoryTheory.Skeleton C
-- Mathlib.Algebra.Module.Equiv.Defs
/-- The equivalence of types underlying a linear equivalence.  -/
LinearEquiv.toEquiv : {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₂] →
                {modM : Module R M} →
                  {modM₂ : Module S M₂} →
                    {σ : R →+* S} →
                      {σ' : S →+* R} →
                        [inst_4 : RingHomInvPair σ σ'] → [inst_5 : RingHomInvPair σ' σ] → (M ≃ₛₗ[σ] M₂) → M ≃ M₂
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.radical_le_jacobson : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.radical ≤ I.jacobson
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.fiber_eqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (h : X = Y), (CategoryTheory.eqToHom h).fiber = CategoryTheory.eqToHom ⋯
-- Lean.Data.KVMap
Lean.DataValue.ofString.injEq : ∀ (v v_1 : String), (Lean.DataValue.ofString v = Lean.DataValue.ofString v_1) = (v = v_1)
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.PostponeBehavior.partial.sizeOf_spec : sizeOf Lean.Elab.Term.PostponeBehavior.partial = 1
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The functor `uliftFunctor : AddCommGrpCat.{u} ⥤ AddCommGrpCat.{max u v}` creates `u`-small colimits.
 -/
AddCommGrpCat.instCreatesColimitsOfSizeUliftFunctor : CategoryTheory.CreatesColimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} AddCommGrpCat.uliftFunctor
-- Mathlib.Data.Stream.Init
Stream'.get_even : ∀ {α : Type u} (n : ℕ) (s : Stream' α), s.even.get n = s.get (2 * n)
-- Mathlib.Algebra.Group.Action.Units
Units.coe_smul : ∀ {M : Type u_6} {N : Type u_7} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulDistribMulAction M N] (m : M)
  (u : Nˣ), ↑(m • u) = m • ↑u
-- Mathlib.Data.List.Lattice
List.bagInter.match_1.congr_eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x x_1 : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x []) (h_3 : (a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂) (a : α) (l₁ l₂ : List α),
  x = a :: l₁ →
    x_1 = l₂ →
      (l₂ = [] → False) →
        (match x, x_1 with
          | [], x => h_1 x
          | x, [] => h_2 x
          | a :: l₁, l₂ => h_3 a l₁ l₂) ≍
          h_3 a l₁ l₂
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.measurableEmbedding_coe : MeasurableEmbedding UpperHalfPlane.coe
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
/-- Lower bound on the **Ruzsa-Szemerédi problem** in terms of 3AP-free sets.

If there exists a 3AP-free subset of `[1, ..., (n - 3) / 6]` of size `m`, then there exists a graph
with `n` vertices and `(n / 3 - 2) * m` edges such that each edge belongs to exactly one triangle.
 -/
rothNumberNat_le_ruzsaSzemerediNumberNat' : ∀ (n : ℕ), (↑n / 3 - 2) * ↑(rothNumberNat ((n - 3) / 6)) ≤ ↑(ruzsaSzemerediNumberNat n)
-- Batteries.Data.Nat.Lemmas
/-- Strong case analysis on `a < b ∨ b ≤ a`  -/
Nat.lt_sum_ge : (a b : ℕ) → a < b ⊕' b ≤ a
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₃_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.ShortComplex.SnakeInput.functorL₃.obj S = S.L₃
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The face of a face of a cone is also a face of the cone.  -/
PointedCone.IsFaceOf.trans : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F₁ F₂ : PointedCone R M},
  F₂.IsFaceOf F₁ → F₁.IsFaceOf C → F₂.IsFaceOf C
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.monotone : ∀ (f : CircleDeg1Lift), Monotone ⇑f
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.elabBlock.withSpace : String → String
-- Mathlib.Data.Setoid.Basic
Setoid.instPartialOrder : {α : Type u_1} → PartialOrder (Setoid α)
-- Mathlib.Algebra.Lie.OfAssociative
AlgHom.toLieHom_apply : ∀ {A : Type v} [inst : Ring A] {R : Type u} [inst_1 : CommRing R] [inst_2 : Algebra R A] {B : Type w} [inst_3 : Ring B]
  [inst_4 : Algebra R B] (f : A →ₐ[R] B) (x : A), f.toLieHom x = f x
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- If `f : R^n → R^m` is an `R`-linear map and `I ⊆ R` is an ideal, then the image of `I^n` is
contained in `I^m`.  -/
Ideal.map_pi : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [inst : Ring R] (I : Ideal R) [I.IsTwoSided] [Finite ι] (x : ι → R),
  (∀ (i : ι), x i ∈ I) → ∀ (f : (ι → R) →ₗ[R] ι' → R) (i : ι'), f x i ∈ I
-- Mathlib.Data.ENat.Basic
ENat.pow_ne_top_iff : ∀ {a : ℕ∞} {n : ℕ}, a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0
-- Mathlib.Data.Nat.Count
Nat.count_strict_mono : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → m < n → Nat.count p m < Nat.count p n
-- Mathlib.Probability.Process.Stopping
/-- A stopping time with respect to some filtration `f` is a function
`τ` such that for all `i`, the preimage of `{j | j ≤ i}` along `τ` is measurable
with respect to `f i`.

Intuitively, the stopping time `τ` describes some stopping rule such that at time
`i`, we may determine it with the information we have at time `i`.  -/
MeasureTheory.IsStoppingTime : {Ω : Type u_1} →
  {ι : Type u_3} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → MeasureTheory.Filtration ι m → (Ω → WithTop ι) → Prop
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_smul_of_tower : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  [inst_6 : SMul S A] [inst_7 : SMul S M] [LinearMap.CompatibleSMul A M S R] (D : Derivation R A M) (r : S) (a : A),
  D (r • a) = r • D a
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lequivCongrLeft_symm_lof : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {κ : Type u_1} [inst_3 : DecidableEq ι] [inst_4 : DecidableEq κ] {h : ι ≃ κ}
  {k : κ} {x : M (h.symm k)},
  (DirectSum.lequivCongrLeft R h).symm ((DirectSum.lof R κ (fun k => M (h.symm k)) k) x) =
    (DirectSum.lof R ι M (h.symm k)) x
-- Init.Data.List.Basic
/-- Permutation is transitive: `l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃`.
 -/
List.Perm.trans : ∀ {α : Type u} {l₁ l₂ l₃ : List α}, l₁.Perm l₂ → l₂.Perm l₃ → l₁.Perm l₃
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.isLocalization : ∀ {R : Type u_1} [inst : CommSemiring R], IsLocalization.Away Polynomial.X (LaurentPolynomial R)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball_subset`. -/
EMetric.ball_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal},
  edist x y + ε₁ ≤ ε₂ → edist x y ≠ ⊤ → Metric.eball x ε₁ ⊆ Metric.eball y ε₂
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_anti_of_ediam_ne_top : ∀ {α : Type u_1} {G G' : SimpleGraph α}, G ≤ G' → G.ediam ≠ ⊤ → G'.diam ≤ G.diam