mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.EssentiallySmall.of_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D),
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F) →
    (∀ (Y : D), CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun x => Nonempty (F.obj x ≅ Y))) →
      CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P
-- Mathlib.Topology.Category.Profinite.AsLimit
/-- The isomorphism of cones `X.asLimitCone` and `Profinite.limitCone X.diagram`.
The underlying isomorphism is defeq to `X.isoAsLimitConeLift`.
 -/
Profinite.asLimitConeIso : (X : Profinite) → X.asLimitCone ≅ Profinite.limitCone X.diagram
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.coe_op : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G), ↑H.op = AddOpposite.unop ⁻¹' ↑H
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.lintegral_join : ∀ {α : Type u_1} {mα : MeasurableSpace α} {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {f : α → ENNReal},
  AEMeasurable f m.join → ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : MeasureTheory.Measure α), ∫⁻ (x : α), f x ∂μ ∂m
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.small_coe : ∀ (x : ZFSet.{u}), Small.{u, u + 1} ↥x
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_intCast : ∀ {d : ℤ} (n : ℤ), (↑n).im = 0
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
/-- See `tsub_lt_tsub_iff_left_of_le` for a stronger statement in a linear order.  -/
tsub_lt_tsub_iff_left_of_le_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] [AddLeftReflectLT α],
  b ≤ a → c ≤ a → (a - b < a - c ↔ c < b)
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_add : ∀ {a b : ℤ} {hab₁ : Int64.minValue.toInt ≤ a + b} {hab₂ : a + b ≤ Int64.maxValue.toInt},
  Int64.ofIntLE (a + b) hab₁ hab₂ = Int64.ofInt a + Int64.ofInt b
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_sum_eq_sup_of_pairwise_ne : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M},
  ((↑s).Pairwise fun i j => ‖f i‖₊ ≠ ‖f j‖₊) → ‖∑ i ∈ s, f i‖₊ = s.sup fun i => ‖f i‖₊
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits, then `F : C ⥤ D` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimits F.op],
  CategoryTheory.Limits.PreservesColimits F
-- Mathlib.Geometry.Manifold.DerivationBundle
fdifferential_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  (g : ContMDiffMap I' I'' M' M'' ↑⊤) (f : ContMDiffMap I I' M M' ↑⊤) (x : M),
  fdifferential (g.comp f) x = fdifferential g (f x) ∘ₗ fdifferential f x
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
/-- If `N` is a submodule in an algebra `S` over `R`, there is the natural `R`-linear map
`i(R) ⊗[R] N →ₗ[R] N` induced by multiplication in `S`, here `i : R → S` is the structure map.
This is promoted to an isomorphism of `R`-modules as `Submodule.lTensorOne`. Use that instead.  -/
Submodule.lTensorOne' : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (N : Submodule R S) → TensorProduct R ↥⊥ ↥N →ₗ[R] ↥N
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.lt_of_mk_lt_mk_of_one_le : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a < MulArchimedeanClass.mk b → 1 ≤ a → b < a
-- Lean.SubExpr
Lean.SubExpr.Pos.instToJson : Lean.ToJson Lean.SubExpr.Pos
-- Mathlib.Analysis.ODE.Gronwall
/-- Upper bound used in several Grönwall-like inequalities.  -/
gronwallBound : ℝ → ℝ → ℝ → ℝ → ℝ
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.rootForm_root_self : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (j : ι), (P.RootForm (P.root j)) (P.root j) = ∑ i, P.pairing j i * P.pairing j i
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.coe_toHomeomorph : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  ⇑h.toHomeomorph = ⇑h
-- Mathlib.Topology.MetricSpace.Bounded
Metric.finite_isBounded_inter_isClosed : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α] {K s : Set α},
  IsDiscrete s → Bornology.IsBounded K → IsClosed s → (K ∩ s).Finite
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
/-- The set of `n`-dimensional non-degenerate simplices in a simplicial
set `X` is the complement of `X.degenerate n`.  -/
SSet.nonDegenerate : (X : SSet) → (n : ℕ) → Set (X.obj (Opposite.op { len := n }))
-- Mathlib.Algebra.Order.Group.Synonym
isRightRegular_toColex : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsRightRegular (toColex a) ↔ IsRightRegular a
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.BallPackage.rpos : ∀ {β : Type u_1} {α : Type u_2} (self : Besicovitch.BallPackage β α) (b : β), 0 < self.r b
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_mono_fn' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ ≤ ν → ∀ ⦃f g : α → ENNReal⦄, (∀ (x : α), f x ≤ g x) → ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.id_comp : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  (f : 𝒜 →ₐᵍ[R] ℬ), (GradedAlgHom.id R ℬ).comp f = f
-- Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
/-- A generalized Eisenstein criterion

Let `R` be an integral domain and `K` an `R`-algebra which is a domain.
Let `q : R[X]` be a monic polynomial which is prime in `K[X]`.
Let `f : R[X]` be a primitive polynomial of strictly positive degree
whose leading coefficient is not zero in `K`
and such that the image `f` in `K[X]` is a power of `q`.
Assume moreover that `f.modByMonic q` is not zero in `(R ⧸ (P ^ 2))[X]`,
where `P` is the kernel of `algebraMap R K`.
Then `f` is irreducible.  -/
Polynomial.generalizedEisenstein : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {K : Type u_2} [inst_2 : Field K] [inst_3 : Algebra R K]
  {q f : Polynomial R} {p : ℕ},
  Irreducible (Polynomial.map (algebraMap R K) q) →
    q.Monic →
      f.IsPrimitive →
        0 < f.natDegree →
          (algebraMap R K) f.leadingCoeff ≠ 0 →
            Polynomial.map (algebraMap R K) f =
                Polynomial.C ((algebraMap R K) f.leadingCoeff) * Polynomial.map (algebraMap R K) q ^ p →
              Polynomial.map (Ideal.Quotient.mk (RingHom.ker (algebraMap R K) ^ 2)) (f %ₘ q) ≠ 0 → Irreducible f
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instAddCommGroup : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Ring R] →
          [inst_1 : (i : ι) → AddCommGroup (M₁ i)] →
            [inst_2 : AddCommGroup M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] →
                      [IsTopologicalAddGroup M₂] → AddCommGroup (ContinuousMultilinearMap R M₁ M₂)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.meas_iInter : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {s : ι → Set Ω} [inst : Fintype ι],
  ProbabilityTheory.iIndep m μ → (∀ (i : ι), MeasurableSet (s i)) → μ (⋂ i, s i) = ∏ i, μ (s i)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.ae_zero : ∀ {α : Type u_1} {_m0 : MeasurableSpace α}, MeasureTheory.ae 0 = ⊥
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.instSubsingletonOfIsEmpty : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [IsEmpty X],
  Subsingleton C(X, Y)
-- Mathlib.Data.List.GetD
List.getD_surjective : ∀ {α : Type u} {l : List α}, (∀ (x : α), x ∈ l) → ∀ (d : α), Function.Surjective fun x => l.getD x d
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.lift.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A],
  TensorAlgebra.lift R =
    { toFun := fun f => (TensorAlgebra.ringCon R M).liftₐ ((FreeAlgebra.lift R) ⇑f) ⋯,
      invFun := fun F => F.toLinearMap ∘ₗ TensorAlgebra.ι R, left_inv := ⋯, right_inv := ⋯ }
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.toStream_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp}, (Std.toStream t).toList = t.toList
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go : {α : Type u} → {β : Type v} → [Ord α] → α → Option (α × β) → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_zero : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  WithVal.ofVal 0 = 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSliceData.treeMap : {α : Type u} →
  {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RooSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.Order.CompleteLattice.Basic
iInf_option : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : Option β → α), ⨅ o, f o = f none ⊓ ⨅ b, f (some b)
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIci.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {b x : α} [inst_1 : Decidable (b ≤ x)], Set.decidableMemIci = inst_1
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeBotOfNonempty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [Nonempty J], ⊥.IsClosedUnderColimitsOfShape J
-- Mathlib.Geometry.Manifold.Immersion
IsOpen.isImmersionAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  IsOpen {x | Manifold.IsImmersionAt I J n f x}
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.directed_ptsOfPeriod_pnat : ∀ {α : Type u_1} (f : α → α), Directed (fun x1 x2 => x1 ⊆ x2) fun n => Function.ptsOfPeriod f ↑n
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- Given a pseudofunctor `F` from `LocallyDiscrete Cᵒᵖ` to `Cat`, a family of
morphisms `f i : X i ⟶ S`, chosen pullbacks `sq i j` of `f i` and `f j` for all `i` and `j`,
and chosen threefold wide pullbacks `sq₃`, this structure contains a description
of objects over the `X i` equipped with a descent data relative to the morphisms `f i`,
where the (iso)morphisms are compatibilities are considered over the chosen pullbacks.  -/
CategoryTheory.Pseudofunctor.DescentData' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)) →
                ((i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) →
                  Type (max (max t u') v')
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
/-- Every object has commutative comonoid structure.  -/
CategoryTheory.CopyDiscardCategory.comonObj : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.CopyDiscardCategory C] → (X : C) → CategoryTheory.ComonObj X
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.openCover.eq_1 : ∀ (D : AlgebraicGeometry.Scheme.GlueData), D.openCover = { I₀ := D.J, X := D.U, f := D.ι, mem₀ := ⋯ }
-- Mathlib.RingTheory.WittVector.StructurePolynomial
/-- `wittStructureRat Φ` is a family of polynomials `ℕ → MvPolynomial (idx × ℕ) ℚ`
that are uniquely characterised by the property that
```
bind₁ (wittStructureRat p Φ) (wittPolynomial p ℚ n) =
bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℚ n))) Φ
```
In other words: evaluating the `n`-th Witt polynomial on the family `wittStructureRat Φ`
is the same as evaluating `Φ` on the (appropriately renamed) `n`-th Witt polynomials.

See `wittStructureRat_prop` for this property,
and `wittStructureRat_existsUnique` for the fact that `wittStructureRat`
gives the unique family of polynomials with this property.

These polynomials turn out to have integral coefficients,
but it requires some effort to show this.
See `wittStructureInt` for the version with integral coefficients,
and `map_wittStructureInt` for the fact that it is equal to `wittStructureRat`
when mapped to polynomials over the rationals.  -/
wittStructureRat : (p : ℕ) → {idx : Type u_2} → [hp : Fact (Nat.Prime p)] → MvPolynomial idx ℚ → ℕ → MvPolynomial (idx × ℕ) ℚ
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.integralClosure_eq_bot_iff : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_3) [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [ifr : IsFractionRing R K], integralClosure R K = ⊥ ↔ IsIntegrallyClosed R
-- Lean.Widget.UserWidget
/-- Every constant `c : α` marked with `@[widget_module]` is registered here.
The registry maps `hash (toModule c).javascript` to ``(`c, `(@toModule α inst c))``
where `inst : ToModule α` is synthesized during registration time
and stored thereafter.  -/
_private.Lean.Widget.UserWidget.0.Lean.Widget.ModuleRegistry : Type
-- Mathlib.Algebra.Category.Ring.Adjunctions
/-- The monoid algebra functor `CommGrpCat ⥤ R-Alg` given by `G ↦ R[G]`.  -/
CommRingCat.monoidAlgebra : (R : CommRingCat) → CategoryTheory.Functor CommMonCat (CategoryTheory.Under R)
-- Mathlib.Data.Finset.Max
Finset.max_eq_sup_withBot : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α), s.max = s.sup WithBot.some
-- Mathlib.Topology.Homotopy.HSpaces
HSpace.eHmul : {X : Type u} →
  {inst : TopologicalSpace X} →
    [self : HSpace X] →
      (HSpace.hmul.comp ((ContinuousMap.const X HSpace.e).prodMk (ContinuousMap.id X))).HomotopyRel (ContinuousMap.id X)
        {HSpace.e}
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.ext : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α}, ↑U = ↑V → U = V
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_le_iff : ∀ {a b : ℝ}, a.sigmoid ≤ b.sigmoid ↔ a ≤ b
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedAddCommGroup.negGen.eq_1 : ∀ (G : Type u_1) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : Nontrivial G] [inst_4 : IsAddCyclic G],
  LinearOrderedAddCommGroup.negGen G = LinearOrderedAddCommGroup.Subgroup.negGen ⊤
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.ofHom_hom : ∀ {X Y : CommGrpCat} (f : X ⟶ Y), CommGrpCat.ofHom (CommGrpCat.Hom.hom f) = f
-- Mathlib.Analysis.Convex.Approximation
ConvexOn.exists_affine_le_of_lt_real : ∀ {s : Set ℝ} {f : ℝ → ℝ} {x a : ℝ},
  x ∈ s →
    a < f x →
      IsClosed s → LowerSemicontinuousOn f s → ConvexOn ℝ s f → ∃ c c', (∀ y ∈ s, c * y + c' ≤ f y) ∧ c * x + c' = a
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.globalName? : Lean.Meta.InstanceEntry → Option Lean.Name
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] (P : CategoryTheory.Idempotents.Karoubi A),
  ((CategoryTheory.Abelian.LeftResolution.karoubi.F Λ).obj P).p = Λ.F.map P.p - Λ.F.map 0
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.yonedaFunctor_preservesLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} CategoryTheory.yoneda
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- The regulator of a family of units of `K`.
 -/
NumberField.Units.regOfFamily : {K : Type u_1} →
  [inst : Field K] → [inst_1 : NumberField K] → (Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) → ℝ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_bot : ∀ {V : Type u} {G : SimpleGraph V} (v : V), ⊥.neighborSet v = ∅
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₄_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.a₄ = 0
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  Continuous MeasureTheory.FiniteMeasure.toWeakDualBCNN
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_eq_smul_add : ∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (x y : V), midpoint R x y = ⅟2 • (x + y)
-- Init.Data.Order.Ord
Array.instTransCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp], Std.TransCmp (Array.compareLex cmp)
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.comp_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (X : C), (F.comp G).obj X = G.obj (F.obj X)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.Bool.or_congr : ∀ (lhs rhs lhs' rhs' : Bool), lhs' = lhs → rhs' = rhs → (lhs' || rhs') = (lhs || rhs)
-- Init.Data.String.Lemmas.Pattern.Memcmp
String.Slice.Pattern.Internal.memcmpSlice_eq_true_iff : ∀ {lhs rhs : String.Slice} {lstart rstart len : String.Pos.Raw} {h₁ : len.offsetBy lstart ≤ lhs.rawEndPos}
  {h₂ : len.offsetBy rstart ≤ rhs.rawEndPos},
  String.Slice.Pattern.Internal.memcmpSlice lhs rhs lstart rstart len h₁ h₂ = true ↔
    lhs.copy.toByteArray.extract lstart.byteIdx (len.offsetBy lstart).byteIdx =
      rhs.copy.toByteArray.extract rstart.byteIdx (len.offsetBy rstart).byteIdx
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_empty_iff : ∀ {m n : ℕ}, (m...n).toArray = #[] ↔ n ≤ m
-- Mathlib.Probability.ProductMeasure
MeasureTheory.lintegral_restrict_infinitePi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : Finset ι} {f : ((i : ↥s) → X ↑i) → ENNReal},
  Measurable f →
    ∫⁻ (y : (i : ι) → X i), f (s.restrict y) ∂MeasureTheory.Measure.infinitePi μ =
      ∫⁻ (y : (i : ↥s) → X ↑i), f y ∂MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.Tactic.FunProp.Theorems
/-- Register theorem `declName` with `fun_prop`.  -/
Mathlib.Meta.FunProp.addTheorem : Lean.Name → optParam Lean.AttributeKind Lean.AttributeKind.global → optParam ℕ 1000 → Lean.MetaM Unit
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_zero : ∀ {K : Type u_1} [inst : RCLike K], ↑0 = 0
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.postcomposing_map_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) {X Y : b ⟶ c} (η : X ⟶ Y) (x : a ⟶ b),
  ((CategoryTheory.Bicategory.postcomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerLeft x η
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- A lower-block-triangular matrix is invertible if its diagonal is.  -/
Matrix.fromBlocksZero₁₂Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (C : Matrix n m α) →
                    (D : Matrix n n α) → [Invertible A] → [Invertible D] → Invertible (Matrix.fromBlocks A 0 C D)
-- Mathlib.Algebra.Order.Monovary
monovary_iff_forall_smul_nonneg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β}, Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_hom_naturality_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L)
  {n n' : ι} (h : n = n') {Z : V} (h_1 : L.X n' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (φ.f n) (CategoryTheory.CategoryStruct.comp (L.XIsoOfEq h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (CategoryTheory.CategoryStruct.comp (φ.f n') h_1)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- If `x : mixedSpace K` is nonzero and the image of an algebraic integer, then there exists a
unit such that `u • x ∈ integerSet K`.  -/
NumberField.mixedEmbedding.fundamentalCone.exists_unitSMul_mem_integerSet : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  x ≠ 0 →
    x ∈ ⇑(NumberField.mixedEmbedding K) '' Set.range ⇑(algebraMap (NumberField.RingOfIntegers K) K) →
      ∃ u, u • x ∈ NumberField.mixedEmbedding.fundamentalCone.integerSet K
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
/-- This lemma expresses `Iter.anyM` in terms of `IterM.anyM`.
It requires all involved types to live in `Type 0`.
 -/
Std.Iter.anyM_eq_anyM_mapM_pure : ∀ {α β : Type} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [inst_6 : Std.IteratorLoop α Id m]
  [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  Std.Iter.anyM p it = ULift.down <$> Std.IterM.anyM (fun x => ULift.up <$> p x) (Std.Iter.mapM pure it)