mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- **Alias** of the forward direction of `hasGradientWithinAt_iff_hasFDerivWithinAt`. -/
HasGradientWithinAt.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F},
  HasGradientWithinAt f f' s x → HasFDerivWithinAt f ((InnerProductSpace.toDual 𝕜 F) f') s x
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The trivial norm on a ring `R` is the `RingNorm` taking value `0` at `0` and `1` at every
other element.  -/
RingNorm.instOneOfDecidableEq : (R : Type u_1) → [inst : NonUnitalRing R] → [DecidableEq R] → One (RingNorm R)
-- Mathlib.Order.CompleteLattice.Basic
sInf_eq_iInf' : ∀ {α : Type u_1} [inst : InfSet α] (s : Set α), sInf s = ⨅ a, ↑a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyGE_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, (compare a k).isGE = true},
  Std.DTreeMap.Internal.Impl.getKeyGE k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.getKeyGE k t₂ ⋯ ⋯
-- Mathlib.Data.List.Basic
List.reverse_involutive : ∀ {α : Type u}, Function.Involutive List.reverse
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.comp_summable_norm : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F]
  {f : E → F} {g : ι → E}, f =O[nhds 0] id → (Summable fun x => ‖g x‖) → Summable fun x => ‖f (g x)‖
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.bijOn : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.BijOn (↑e) e.source e.target
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : CategoryTheory.Functor C D) (X_1 : C),
  (((CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso C D).hom.app X).app X_1).f =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.Topology.Order.AtTopBotIxx
comap_coe_nhdsLT_eq_atTop_iff : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {b : X},
  Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop ↔
    s ⊆ Set.Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Set.Ioo a b).Nonempty)
-- Std.Async.Basic
/-- Waits for the result of the `BaseAsync` computation, blocking if necessary.
 -/
Std.Async.BaseAsync.wait : {α : Type} → Std.Async.BaseAsync α → BaseIO α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.instDist : Dist UpperHalfPlane
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.degreeOf_coeff_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ℕ),
  MvPolynomial.degreeOf j (((MvPolynomial.finSuccEquiv R n) p).coeff i) ≤ MvPolynomial.degreeOf j.succ p
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_mul : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (f g : F →WOT[𝕜₂] F), (f * g).toCLM = f.toCLM * g.toCLM
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.div : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [inst : Add α] [inst_1 : DivisionMonoid β]
  [inst_2 : HasDistribNeg β], Function.Antiperiodic f c → Function.Antiperiodic g c → Function.Periodic (f / g) c
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- If a map `f : α → β` sends any two distinct points to point that are **not** related by a fixed
`s ∈ 𝓤 β`, then `f` is uniform inducing with respect to the discrete uniformity on `α`:
the preimage of `𝓤 β` under `Prod.map f f` is the principal filter generated by the diagonal in
`α × α`.  -/
comap_uniformity_of_spaced_out : ∀ {β : Type v} [inst : UniformSpace β] {α : Type u_1} {f : α → β} {s : Set (β × β)},
  s ∈ uniformity β →
    (Pairwise fun x y => (f x, f y) ∉ s) → Filter.comap (Prod.map f f) (uniformity β) = Filter.principal SetRel.id
-- Mathlib.Data.Set.Insert
Set.Nonempty.eq_one : ∀ {α : Type u_1} [Subsingleton α] [inst : One α] {s : Set α}, s.Nonempty → s = {1}
-- Init.Data.Range.Polymorphic.Nat
Std.instLawfulRcoIntersectionNat_7 : Std.Ric.LawfulRcoIntersection ℕ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.ε_comp_map_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε e.inverse)
      (e.inverse.map (CategoryTheory.Functor.LaxMonoidal.ε e.functor)) =
    e.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Init.Data.Rat.Lemmas
Rat.mul_pos_iff_of_pos_right : ∀ {a b : ℚ}, 0 < b → (0 < a * b ↔ 0 < a)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.of_obj : ∀ {B : Type u} [inst : Quiver B] (a : B), CategoryTheory.FreeBicategory.of.obj a = id a
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.ext_iff : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {f g : TestFunction Ω F n},
  f = g ↔ ∀ (a : E), f a = g a
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (X Y : C) [inst_3 : CategoryTheory.MonObj X]
  [inst_4 : CategoryTheory.MonObj Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (β_ X Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ X Y).hom (β_ X Y).hom)
      CategoryTheory.MonObj.mul
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.filter_mono : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l l' : Filter α},
  l ≤ l' → MeasureTheory.IntegrableAtFilter f l' μ → MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat}
  {x x_1 Z : F.CoGrothendieck} (f : x.Hom x_1) (g : x_1.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).fiber =
    CategoryTheory.CategoryStruct.comp f.fiber
      (CategoryTheory.CategoryStruct.comp ((F.map f.base.op.toLoc).toFunctor.map g.fiber)
        ((F.mapComp g.base.op.toLoc f.base.op.toLoc).inv.toNatTrans.app Z.fiber))
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt32HAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Mathlib.Order.Category.FinBoolAlg
fintypeToFinBoolAlgOp_obj : ∀ (X : FintypeCat), fintypeToFinBoolAlgOp.obj X = Opposite.op (FinBoolAlg.of (Set X.obj))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.toTendstoIxxClass : ∀ {a : outParam ℝ} {outer : Filter ℝ} {inner : outParam (Filter ℝ)} [self : intervalIntegral.FTCFilter a outer inner],
  Filter.TendstoIxxClass Set.Ioc outer inner
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp_const_smul : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {𝕜 : Type u_6} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] {f : α → E} (c : 𝕜) (hf : MeasureTheory.MemLp f p μ),
  MeasureTheory.MemLp.toLp (c • f) ⋯ = c • MeasureTheory.MemLp.toLp f hf
-- Mathlib.CategoryTheory.Category.Basic
/-- Composition of morphisms in a category, written `f ≫ g`.  -/
CategoryTheory.CategoryStruct.comp : {obj : Type u} → [self : CategoryTheory.CategoryStruct.{v, u} obj] → {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
-- Mathlib.Topology.CompactOpen
ContinuousMap.isOpen_setOfPred_range_subset : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {U : Set Y} [CompactSpace X],
  IsOpen U → IsOpen {f | Set.range ⇑f ⊆ U}
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.appr_mono : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), Monotone x.appr
-- Mathlib.Order.RelClasses
wellFoundedGT_dual_iff : ∀ (α : Type u_1) [inst : LT α], WellFoundedGT αᵒᵈ ↔ WellFoundedLT α
-- Mathlib.GroupTheory.Nilpotent
AddGroup.IsNilpotent.mk : ∀ {G : Type u_2} [inst : AddGroup G], (∃ n, AddSubgroup.upperCentralSeries G n = ⊤) → AddGroup.IsNilpotent G
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_addLeft : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [MeasurableAdd G] (g : G),
  MeasurableEmbedding fun x => g + x
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseOffset : Std.Time.Reason✝ → Std.Time.Reason✝ → Bool → Std.Internal.Parsec.String.Parser Std.Time.TimeZone.Offset
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.equivFunOnFinite_symm_eq_sum : ∀ {α : Type u_1} {M : Type u_8} [inst : Fintype α] [inst_1 : AddCommMonoid M] (f : α → M),
  Finsupp.equivFunOnFinite.symm f = ∑ a, fun₀ | a => f a
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.mk''_rightQuotientEquiv : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hT : Subgroup.IsComplement (↑H) T)
  (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' ↑(hT.rightQuotientEquiv q) = q
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.Arrow.Hom.sub_left : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T]
  {u v : CategoryTheory.Arrow T} (α β : u ⟶ v),
  CategoryTheory.Arrow.Hom.left (α - β) = CategoryTheory.Arrow.Hom.left α - CategoryTheory.Arrow.Hom.left β
-- Lean.Data.Lsp.Internal
Lean.Lsp.OpenNamespace.renamed.sizeOf_spec : ∀ («from» «to» : Lean.Name), sizeOf (Lean.Lsp.OpenNamespace.renamed «from» «to») = 1 + sizeOf «from» + sizeOf «to»
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `isOpen_setOfPred_eventually_nhdsWithin`. -/
isOpen_setOf_eventually_nhdsWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {p : X → Prop},
  IsOpen {x | ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y}
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.isGroupLikeElem_iff_mem_range_single_one : ∀ {R : Type u_1} {M : Type u_8} [inst : CommRing R] [IsDomain R] {x : MonoidAlgebra R M},
  IsGroupLikeElem R x ↔ x ∈ Set.range fun x => MonoidAlgebra.single x 1
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Flip the second and third arguments in a trifunctor, as a functor.
 -/
CategoryTheory.Functor.flip₂₃Functor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {E : Type u_9} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
              [inst_3 : CategoryTheory.Category.{v_9, u_9} E] →
                CategoryTheory.Functor
                  (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
                  (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₃ (CategoryTheory.Functor C₂ E)))
-- Lean.Elab.Tactic.Grind.Basic
/-- Elaborate `x` with `stx` on the macro stack  -/
Lean.Elab.Tactic.Grind.withMacroExpansion : {α : Type} → Lean.Syntax → Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_add : ∀ {R : Type u} {σ : Type u_1} {a a' : R} [inst : CommSemiring R],
  MvPolynomial.C (a + a') = MvPolynomial.C a + MvPolynomial.C a'
-- Mathlib.Order.RelSeries
LTSeries.instFintypeOfDecidableLT : {α : Type u_1} → [inst : Preorder α] → [Fintype α] → [DecidableLT α] → Fintype (LTSeries α)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Mathlib.Topology.Instances.CantorSet
/-- The order `n` pre-Cantor set, defined starting from `[0, 1]` and successively removing the
middle third of each interval. Formally, the order `n + 1` pre-Cantor set is the
union of the images under the functions `(· / 3)` and `((2 + ·) / 3)` of `preCantorSet n`.
 -/
preCantorSet : ℕ → Set ℝ
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.id_star_whiskerRight : ∀ {x : AugmentedSimplexCategory},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star)
      x =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.WithInitial.star x)
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- The type of the parameter created in a telescope for logging.
We always expect this to be `some _` normally, but allow `none` as a failsafe.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter.type? : Mathlib.Linter.UnusedInstancesInType.Parameter✝ → Option Lean.Expr
-- Lean.Meta.MkIffOfInductiveProp
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.Shape.mk.inj : ∀ {variablesKept : List Bool} {neqs : Option ℕ} {variablesKept_1 : List Bool} {neqs_1 : Option ℕ},
  { variablesKept := variablesKept, neqs := neqs } = { variablesKept := variablesKept_1, neqs := neqs_1 } →
    variablesKept = variablesKept_1 ∧ neqs = neqs_1
-- Mathlib.RingTheory.Nilpotent.Basic
isReduced_iff_pow_one_lt : ∀ {R : Type u_1} [inst : MonoidWithZero R] (k : ℕ), 1 < k → (IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0)
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.ext_iff : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  {f g : Convexity.ConvexSpace.AffineMap R X Y}, f = g ↔ ⇑f = ⇑g
-- Init.Data.String.Lemmas.Iterate
String.Slice.mem_toList_copy_iff_exists_get : ∀ {s : String.Slice} {c : Char}, c ∈ s.copy.toList ↔ ∃ p, ∃ (h : p ≠ s.endPos), p.get h = c
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
HomotopyCategory.commShiftQuotient : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (HomotopyCategory.quotient C (ComplexShape.up ℤ)).CommShift ℤ
-- Init.GetElem
Array.getInternal_eq_getElem : ∀ {α : Type u_1} (a : Array α) (i : ℕ) (h : i < a.size), a.getInternal i h = a[i]
-- Init.Data.List.Lemmas
List.reverseAux_eq : ∀ {α : Type u_1} {as bs : List α}, as.reverseAux bs = as.reverse ++ bs
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_le_of_lt'`. -/
LE.le.trans_lt' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b ≤ a → c < b → c < a
-- Mathlib.Algebra.Lie.Basic
LieHom.coe_zero : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], ⇑0 = 0
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- **Alias** of the forward direction of `hasFDerivWithinAt_iff_hasGradientWithinAt`. -/
HasFDerivWithinAt.hasGradientWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : StrongDual 𝕜 F} {s : Set F},
  HasFDerivWithinAt f frechet s x → HasGradientWithinAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) s x
-- Mathlib.Data.Num.Basic
ZNum.pos.sizeOf_spec : ∀ (a : PosNum), sizeOf (ZNum.pos a) = 1 + sizeOf a
-- Batteries.Data.Array.Merge
Array.mergeAdjacentDups.go.eq_def : ∀ {α : Type u_1} [eq : BEq α] (f : α → α → α) (xs acc : Array α) (i : ℕ) (hd : α),
  Array.mergeAdjacentDups.go f xs acc i hd =
    if h : i < xs.size then
      have x := xs[i];
      if (x == hd) = true then Array.mergeAdjacentDups.go f xs acc (i + 1) (f hd x)
      else Array.mergeAdjacentDups.go f xs (acc.push hd) (i + 1) x
    else acc.push hd
-- Mathlib.Topology.Sheaves.Abelian
TopCat.Sheaf.instPreservesFiniteLimitsCompPresheafForgetStalkFunctor : ∀ {C : Type v} [inst : CategoryTheory.Category.{u, v} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  [CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u}
  [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Abelian C] {X : TopCat} (p₀ : ↑X),
  CategoryTheory.Limits.PreservesFiniteLimits ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C p₀))
-- Mathlib.Topology.Algebra.GroupCompletion
AddMonoidHom.continuous_extension : ∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : IsUniformAddGroup β] [inst_6 : CompleteSpace β]
  [inst_7 : T0Space β] (f : α →+ β) (hf : Continuous ⇑f), Continuous ⇑(f.extension hf)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Sieve.pullback.hcongr_6 : ∀ (C C' : Type u₁),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} C) (inst' : CategoryTheory.Category.{v₁, u₁} C'),
      inst ≍ inst' →
        ∀ (X : C) (X' : C'),
          X ≍ X' →
            ∀ (Y : C) (Y' : C'),
              Y ≍ Y' →
                ∀ (h : Y ⟶ X) (h' : Y' ⟶ X'),
                  h ≍ h' →
                    ∀ (S : CategoryTheory.Sieve X) (S' : CategoryTheory.Sieve X'),
                      S ≍ S' → CategoryTheory.Sieve.pullback h S ≍ CategoryTheory.Sieve.pullback h' S'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_eq_none : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α},
  a ∉ m → m.get? a = none
-- Mathlib.Algebra.Order.Group.PosPart
posPart_def : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] (a : α), a⁺ = a ⊔ 0
-- Mathlib.Topology.MetricSpace.Isometry
/-- Turn an element of a type `F` satisfying `EquivLike F α β` and `IsometryClass F α β` into
an actual `IsometryEquiv`. This is declared as the default coercion from `F` to `α ≃ᵢ β`.  -/
IsometryClass.toIsometryEquiv : {F : Type u_1} →
  {α : Type u} →
    {β : Type v} →
      [inst : PseudoEMetricSpace α] →
        [inst_1 : PseudoEMetricSpace β] → [inst_2 : EquivLike F α β] → [IsometryClass F α β] → F → α ≃ᵢ β
-- Mathlib.Topology.List
List.continuous_eraseIdx : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ}, Continuous fun l => l.eraseIdx n
-- Init.Data.BitVec.Lemmas
BitVec.toFin_signExtend_of_le : ∀ {w v : ℕ} {x : BitVec w}, v ≤ w → (BitVec.signExtend v x).toFin = Fin.ofNat (2 ^ v) x.toNat
-- Init.Data.UInt.Lemmas
USize.sub_mul : ∀ {a b c : USize}, (a - b) * c = a * c - b * c
-- Mathlib.Data.Fintype.Pi
/-- **Alias** of the reverse direction of `Fintype.piFinset_nonempty`. -/
Fintype.Aesop.piFinset_nonempty_of_forall_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {γ : α → Type u_3} {s : (a : α) → Finset (γ a)},
  (∀ (a : α), (s a).Nonempty) → (Fintype.piFinset s).Nonempty
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- `ContinuousAlternatingMap.pi` as a `LinearIsometryEquiv`.  -/
ContinuousAlternatingMap.piLIE : (𝕜 : Type u) →
  (E : Type wE) →
    {ι : Type v} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : Fintype ι] →
              {ι' : Type u_1} →
                [inst_4 : Fintype ι'] →
                  {F : ι' → Type u_2} →
                    [inst_5 : (i' : ι') → SeminormedAddCommGroup (F i')] →
                      [inst_6 : (i' : ι') → NormedSpace 𝕜 (F i')] →
                        ((i' : ι') → E [⋀^ι]→L[𝕜] F i') ≃ₗᵢ[𝕜] E [⋀^ι]→L[𝕜] ((i : ι') → F i)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.alterKey.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (v : β k) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
IsNonarchimedean.add_eq_left_of_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} [inst_2 : AddGroup α]
  [inst_3 : FunLike F α R] [AddGroupSeminormClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {x y : α}, f y < f x → f (x + y) = f x
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_unitIso_hom_app_toFun : ∀ (X : Bipointed) (a : ((CategoryTheory.Functor.id Bipointed).obj X).X),
  (Bipointed.swapEquiv.unitIso.hom.app X).toFun a = a
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- Given `X : C`, this is a fibrant object `X'` equipped with a
trivial cofibration `X ⟶ X'` (see `HoCat.iResolutionObj`).  -/
HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → [HomotopicalAlgebra.ModelCategory C] → C → C
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- A linear map **has Noetherian range** if its range is a Noetherian module.  -/
LinearMap.HasNoetherianRange : {K : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_4} →
      [inst : Semiring K] →
        [inst_1 : AddCommMonoid V] →
          [inst_2 : Module K V] → [inst_3 : AddCommMonoid V₂] → [inst_4 : Module K V₂] → (V →ₗ[K] V₂) → Prop
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.InvariantForm.apply_weylGroup_smul : ∀ {ι : 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) {B : P.InvariantForm}
  (g : ↥P.weylGroup) (x y : M), (B.form (g • x)) (g • y) = (B.form x) y
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [inst_8 : RingHomIsometric σ₂₁]
  [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F), Subsingleton E ∨ 0 < ‖↑e.symm‖₊
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- Restrict a ring homomorphism to the nth roots of unity.  -/
restrictRootsOfUnity : {R : Type u_4} →
  {S : Type u_5} →
    {F : Type u_6} →
      [inst : CommMonoid R] →
        [inst_1 : CommMonoid S] →
          [inst_2 : FunLike F R S] → [MonoidHomClass F R S] → F → (n : ℕ) → ↥(rootsOfUnity n R) →* ↥(rootsOfUnity n S)
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit_sub : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α} (ha : IsAddUnit a) (hb : IsAddUnit b),
  ⋯.addUnit = ha.addUnit - hb.addUnit
-- Mathlib.Algebra.Category.CommBialgCat
_private.Mathlib.Algebra.Category.CommBialgCat.0.CommBialgCat.Hom.mk.inj : ∀ {R : Type u} {inst : CommRing R} {A B : CommBialgCat R} {hom' hom'_1 : ↑A →ₐc[R] ↑B},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Algebra.Order.Field.Basic
sub_self_div_two : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] (a : α), a - a / 2 = a / 2