mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Function.Conjugate
/-- Two maps `f g : α → α` commute if `f (g x) = g (f x)` for all `x : α`.
Given `h : Function.commute f g` and `a : α`, we have `h a : f (g a) = g (f a)` and
`h.comp_eq : f ∘ g = g ∘ f`.
 -/
Function.Commute : {α : Type u_1} → (α → α) → (α → α) → Prop
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialProd_zero : ∀ {M : Type u_2} [inst : Monoid M] {n : ℕ} (f : Fin n → M), Fin.partialProd f 0 = 1
-- Mathlib.CategoryTheory.Idempotents.Biproducts
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_3 : Finite J]
  (F : J → CategoryTheory.Idempotents.Karoubi C),
  (CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).pt.p = CategoryTheory.Limits.biproduct.map fun j => (F j).p
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- (Implementation) Given a cone in the base category, raise it to a cone in
`CostructuredArrow K B`. Note this is where the connected assumption is used.
 -/
CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
            {K : CategoryTheory.Functor C D} →
              [CategoryTheory.IsConnected J] →
                {B : D} →
                  {F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow K B)} →
                    CategoryTheory.Limits.Cone (F.comp (CategoryTheory.CostructuredArrow.proj K B)) →
                      CategoryTheory.Limits.Cone F
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- A chosen right adjoint to a functor that is a left adjoint.  -/
CategoryTheory.Functor.rightAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) → [R.IsLeftAdjoint] → CategoryTheory.Functor C D
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.not_isLeftDescent_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B},
  ¬cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) = cs.length w + 1
-- Mathlib.Algebra.DirectSum.Basic
/-- The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`.  -/
DirectSum.sigmaCurryEquiv : {ι : Type v} →
  [DecidableEq ι] →
    {α : ι → Type u} →
      {δ : (i : ι) → α i → Type w} →
        [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
          (DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) ≃+ DirectSum ι fun i => DirectSum (α i) fun j => δ i j
-- Mathlib.Order.Defs.Unbundled
RelUpperSet.mk.injEq : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} (carrier : Set α) (isRelUpperSet' : IsRelUpperSet carrier P)
  (carrier_1 : Set α) (isRelUpperSet'_1 : IsRelUpperSet carrier_1 P),
  ({ carrier := carrier, isRelUpperSet' := isRelUpperSet' } =
      { carrier := carrier_1, isRelUpperSet' := isRelUpperSet'_1 }) =
    (carrier = carrier_1)
-- Std.Http.Internal.IndexMultiMap
/-- Replaces the last value associated with `key` with `value`.
If the key is absent, returns the map unchanged.
 -/
Std.Internal.IndexMultiMap.replaceLast : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → α → β → Std.Internal.IndexMultiMap α β
-- Mathlib.RingTheory.NoetherNormalization
/-- `r` maps `(i : Fin (n + 1))` to `up ^ i`.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.termR : Lean.ParserDescr
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.responseBody : {α β : Type} → Std.Http.Server.Connection.PollSources✝ α β → Option β
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.triangleMorphismId_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.triangleMorphismId T).hom₂ = CategoryTheory.CategoryStruct.id T.obj₂
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_singleton_eq_bot : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
  R ∙ x = ⊥ ↔ x = 0
-- Mathlib.Data.Set.Finite.Basic
/-- The `Set.fintypeInsert` instance requires decidable equality, but when `a ∈ s`
is decidable for this particular `a` we can still get a `Fintype` instance by using
`Set.fintypeInsertOfNotMem` or `Set.fintypeInsertOfMem`.

This instance pre-dates `Set.fintypeInsert`, and it is less efficient.
When `Set.decidableMemOfFintype` is made a local instance, then this instance would
override `Set.fintypeInsert` if not for the fact that its priority has been
adjusted. See Note [lower instance priority].  -/
Set.fintypeInsert' : {α : Type u} → (a : α) → (s : Set α) → [Decidable (a ∈ s)] → [Fintype ↑s] → Fintype ↑(insert a s)
-- Mathlib.NumberTheory.Chebyshev
/-- Extension for the `positivity` tactic: the second Chebyshev function is nonnegative.  -/
Mathlib.Meta.Positivity.evalPsi : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Finsupp.Order
Finsupp.embDomain_le_embDomain_iff_le : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : Zero α] [inst_1 : LE α] [Std.Refl fun x1 x2 => x1 ≤ x2]
  (f : ι ↪ κ) (g₁ g₂ : ι →₀ α), Finsupp.embDomain f g₁ ≤ Finsupp.embDomain f g₂ ↔ g₁ ≤ g₂
-- Mathlib.Data.Finset.Basic
Finset.choose_spec : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a),
  Finset.choose p l hp ∈ l ∧ p (Finset.choose p l hp)
-- Init.Data.Fin.Lemmas
Fin.le_coe_addNat : ∀ {n : ℕ} (m : ℕ) (i : Fin n), m ≤ ↑(i.addNat m)
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_apply : ∀ {α : Type u_1} {f : α → α} {x : α},
  x ∈ Function.periodicPts f → Function.minimalPeriod f (f x) = Function.minimalPeriod f x
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isEmbedding_inclusion_top : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)],
  Topology.IsEmbedding (RestrictedProduct.inclusion R A ⋯)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.toPartialHomeomorph : {X : Type u_7} →
  {Y : Type u_8} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → PartialHomeomorph X Y
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Some `n`-th iterate of `next` is a contracting map, and its associated Lipschitz constant is
independent of the initial point.  -/
ODE.FunSpace.exists_contractingWith_iterate_next : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K),
  ∃ n C, ∀ (x : E) (hx : x ∈ Metric.closedBall x₀ ↑r), ContractingWith C (ODE.FunSpace.next hf hx)^[n]
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- The property of reflecting products expressed in terms of binary fans.  -/
CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {P X Y : C} →
            (f : P ⟶ X) →
              (g : P ⟶ Y) →
                [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.pair X Y) G] →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (G.map f) (G.map g)) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk f g)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The Grothendieck topology on `X.AffineZariskiSite` induced from the topology on `X.Opens`.
Also see `mem_grothendieckTopology_iff_sectionsOfPresieve`.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology : (X : AlgebraicGeometry.Scheme) → CategoryTheory.GrothendieckTopology X.AffineZariskiSite
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Int.trailingZeros.aux.match_1.splitter : (i : ℤ) →
  (motive : (k : ℕ) → k ≠ 0 → i.natAbs ≤ k → Sort u_1) →
    (k : ℕ) →
      (x : k ≠ 0) →
        (hk : i.natAbs ≤ k) → ((k : ℕ) → (x : k + 1 ≠ 0) → (hk : i.natAbs ≤ k + 1) → motive k.succ x hk) → motive k x hk
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- If `f` admits a Taylor series `p` in a set `s`, and `g` is linear, then `f ∘ g` admits a Taylor
series in `g ⁻¹' s`, whose `k`-th term at `x` is given by `p (g x) k (g v₁, ..., g vₖ)` .  -/
HasFTaylorSeriesUpToOn.compContinuousLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞}
  {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s →
    ∀ (g : G →L[𝕜] E),
      HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- The matrix `vecMulVec (star a) a` is always positive semi-definite.  -/
Matrix.posSemidef_vecMulVec_star_self : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [Finite n]
  [StarOrderedRing R] (a : n → R), (Matrix.vecMulVec (star a) a).PosSemidef
-- Mathlib.RingTheory.LaurentSeries
/-- The support of `Cauchy.coeff` has a lower bound.  -/
LaurentSeries.Cauchy.exists_lb_support : ∀ {K : Type u_2} [inst : Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ),
  ∃ N, ∀ n < N, LaurentSeries.Cauchy.coeff hℱ n = 0
-- Mathlib.Geometry.Euclidean.Volume.Measure
_private.Mathlib.Geometry.Euclidean.Volume.Measure.0.MeasureTheory.Measure.addHaarScalarFactor_hausdorffMeasure_eq : (d : ℕ) →
  ProofWanted
    (↑(MeasureTheory.volume.addHaarScalarFactor (MeasureTheory.Measure.hausdorffMeasure ↑d)) =
      MeasureTheory.volume (Metric.ball 0 1) / MeasureTheory.volume (Metric.ball 0 1))
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- A function is almost everywhere strongly measurable if and only if it is almost everywhere
measurable, and up to a zero measure set its range is contained in a separable set.  -/
aestronglyMeasurable_iff_aemeasurable_separable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β],
  MeasureTheory.AEStronglyMeasurable f μ ↔
    AEMeasurable f μ ∧ ∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_erase : ∀ {R : Type u} [inst : Semiring R] (p : AddMonoidAlgebra R ℕ) (n : ℕ),
  { toFinsupp := AddMonoidAlgebra.erase n p } = Polynomial.erase n { toFinsupp := p }
-- Mathlib.RingTheory.PowerSeries.Exp
PowerSeries.derivative_exp : ∀ (A : Type u_3) [inst : CommRing A] [inst_1 : Algebra ℚ A],
  (PowerSeries.derivative A) (PowerSeries.exp A) = PowerSeries.exp A
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- Two embedding `e₁` and `e₂` into a complex shape `c : ComplexShape ι`
are complementary when the range of `e₁.f` and `e₂.f` form a partition of `ι`.  -/
ComplexShape.Embedding.AreComplementary : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} → {c₁ : ComplexShape ι₁} → {c₂ : ComplexShape ι₂} → c₁.Embedding c → c₂.Embedding c → Prop
-- Mathlib.Order.Sublattice
Sublattice.pi_bot : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] {s : Set κ},
  s.Nonempty → (Sublattice.pi s fun x => ⊥) = ⊥
-- Init.Data.SInt.Lemmas
Int16.neg_eq_neg_one_mul : ∀ (a : Int16), -a = -1 * a
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.ofContinuousOpen_toPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source),
  (OpenPartialHomeomorph.ofContinuousOpen e hc ho hs).toPartialHomeomorph =
    PartialHomeomorph.ofContinuousOpenRestrict e hc ⋯
-- Std.Http.Protocol.H1
/-- Output data ready to be sent to the socket.
 -/
Std.Http.Protocol.H1.StepResult.output : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.StepResult dir → Std.Http.Internal.ChunkedBuffer
-- Init.Data.UInt.Bitwise
UInt16.toNat_or : ∀ (a b : UInt16), (a ||| b).toNat = a.toNat ||| b.toNat
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.Subtype.volume_univ : ∀ {δ : Type u_4} {u : Set δ} [inst : MeasureTheory.MeasureSpace δ],
  MeasureTheory.NullMeasurableSet u MeasureTheory.volume → MeasureTheory.volume Set.univ = MeasureTheory.volume u
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Functor.toCatHom_toFunctor : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (F : CategoryTheory.Functor C D), F.toCatHom.toFunctor = F
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- a `d`-simplex in the target of the monomorphism  -/
SSet.relativeCellComplexOfMono.Cell.simplex : {X Y : SSet} → {i : X ⟶ Y} → {d : ℕ} → SSet.relativeCellComplexOfMono.Cell i d → Y.obj (Opposite.op { len := d })
-- Mathlib.NumberTheory.SmoothNumbers
/-- `m` is an `n`-smooth number if and only if `m ≠ 0` and the `Finset` of its prime factors
is contained in the `Finset` of primes below `n`  -/
Nat.mem_smoothNumbers_iff_primeFactors_subset : ∀ {m n : ℕ}, m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ m.primeFactors ⊆ n.primesBelow
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is zero or `π` if and only if the three points are collinear.  -/
EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ Collinear ℝ {p₁, p₂, p₃}
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_div_eq_mk_right : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk b < MulArchimedeanClass.mk a → MulArchimedeanClass.mk (a / b) = MulArchimedeanClass.mk b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesIso₀_inv_comp_iCycles_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 0 → G) →₀ ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).inv
      (CategoryTheory.CategoryStruct.comp (groupHomology.iCycles A 0) h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ A).inv h
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {f : β → m γ}
  (it : Std.IterM Id β), (Std.IterM.mapM f it).toArray = Array.mapM f it.toArray.run
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (X : C) (i : ↑(Set.Iic j)),
  CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso F X i = CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.Order.Group.MinMax
max_neg_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b : α),
  max (-a) (-b) = -min a b
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- The tensor product of two bialgebra morphisms as a bialgebra morphism.  -/
Bialgebra.TensorProduct.map : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        {C : Type u_5} →
          {D : Type u_6} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring S] →
                [inst_2 : Semiring A] →
                  [inst_3 : Semiring B] →
                    [inst_4 : Bialgebra S A] →
                      [inst_5 : Bialgebra R B] →
                        [inst_6 : Algebra R A] →
                          [inst_7 : Algebra R S] →
                            [inst_8 : IsScalarTower R S A] →
                              [inst_9 : Semiring C] →
                                [inst_10 : Semiring D] →
                                  [inst_11 : Bialgebra S C] →
                                    [inst_12 : Bialgebra R D] →
                                      [inst_13 : Algebra R C] →
                                        [inst_14 : IsScalarTower R S C] →
                                          (A →ₐc[S] C) → (B →ₐc[R] D) → TensorProduct R A B →ₐc[S] TensorProduct R C D
-- Mathlib.Data.Complex.Basic
Complex.inv_im : ∀ (z : ℂ), z⁻¹.im = -z.im / Complex.normSq z
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_filter_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun k x => f k) t ⋯).impl.getKey? k = Option.filter f (t.getKey? k)
-- Mathlib.CategoryTheory.Idempotents.Basic
CategoryTheory.Idempotents.instIsIdempotentCompleteOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsIdempotentComplete C],
  CategoryTheory.IsIdempotentComplete Cᵒᵖ
-- Mathlib.Order.SuccPred.Basic
Order.pred_eq_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] [inst_1 : PredOrder α] (a : α), Order.pred a = sSup (Set.Iio a)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- `OuterMeasure.trim` is antitone in the σ-algebra.  -/
MeasureTheory.OuterMeasure.trim_anti_measurableSpace : ∀ {α : Type u_2} (m : MeasureTheory.OuterMeasure α) {m0 m1 : MeasurableSpace α}, m0 ≤ m1 → m.trim ≤ m.trim
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
trdeg_eq_iSup_cardinalMk_isTranscendenceBasis : ∀ (R : Type u_1) {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.trdeg R A = ⨆ ι, Cardinal.mk ↑↑ι
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`.  -/
mem_nhdsLT_iff_exists_Ioo_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α}
  {s : Set α}, s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s
-- Mathlib.Data.Vector.Basic
/-- The `last` element of a vector is the `head` of the `reverse` vector.  -/
List.Vector.reverse_get_zero : ∀ {α : Type u_1} {n : ℕ} {v : List.Vector α (n + 1)}, v.reverse.head = v.last
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.ext_continuousLinearMap_iff : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [inst_4 : DecidableEq α] {F : Type u_5} [inst_5 : AddCommMonoid F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F]
  [T2Space F] [inst_9 : Fact (1 ≤ p)] {hp : p ≠ ⊤} {f g : ↥(lp E p) →L[𝕜] F},
  f = g ↔ ∀ (i : α), f ∘SL lp.singleContinuousLinearMap 𝕜 E p i = g ∘SL lp.singleContinuousLinearMap 𝕜 E p i
-- Mathlib.Topology.Algebra.InfiniteSum.Group
hasSum_ite_sub_hasSum : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f : β → α} {a : α} [L.LeAtTop] [inst_4 : DecidableEq β],
  HasSum f a L → ∀ (b : β), HasSum (fun n => if n = b then 0 else f n) (a - f b) L
-- Mathlib.Topology.Homotopy.HSpaces
HSpace.hmul_e_e : ∀ {X : Type u} {inst : TopologicalSpace X} [self : HSpace X], HSpace.hmul (HSpace.e, HSpace.e) = HSpace.e
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_X_pow : ∀ (R : Type u_1) [inst : Semiring R] [Nontrivial R] (n : ℕ), (Polynomial.X ^ n).IsMonicOfDegree n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsAddMonHom.addMonoidHom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.IsAddMonHom.addMonoidHom (CategoryTheory.CategoryStruct.id M) X = AddMonoidHom.id (X ⟶ M)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k a : α} {v : β},
  (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ k ∉ m then k else m.getKey! a
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Expressing `HasFDerivAt f f' x` in terms of `HasDerivAt`  -/
hasFDerivAt_iff_hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F},
  HasFDerivAt f f' x ↔ HasDerivAt f (f' 1) x
-- Init.Data.Range.Polymorphic.UInt
UInt8.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite UInt8
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.descFunLift.eq_def : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (s : CategoryTheory.Limits.Cocone F) (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.descFunLift F s x =
    match x with
    | CommRingCat.Colimits.Prequotient.of j x => (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x
    | CommRingCat.Colimits.Prequotient.zero => 0
    | CommRingCat.Colimits.Prequotient.one => 1
    | x.neg => -CommRingCat.Colimits.descFunLift F s x
    | x.add y => CommRingCat.Colimits.descFunLift F s x + CommRingCat.Colimits.descFunLift F s y
    | x.mul y => CommRingCat.Colimits.descFunLift F s x * CommRingCat.Colimits.descFunLift F s y
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesLimitπ₁ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)],
  CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₁
-- Mathlib.Analysis.Convolution
MeasureTheory.integrable_posConvolution : ∀ {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ E'] [inst_5 : NormedSpace ℝ F]
  {f : ℝ → E} {g : ℝ → E'} {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [μ.IsAddRightInvariant] [MeasureTheory.NullSingletonClass ν],
  MeasureTheory.IntegrableOn f (Set.Ioi 0) ν →
    MeasureTheory.IntegrableOn g (Set.Ioi 0) μ →
      ∀ (L : E →L[ℝ] E' →L[ℝ] F), MeasureTheory.Integrable (MeasureTheory.posConvolution f g L ν) μ