mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
slope_pos_iff_gt : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜},
  b < x₀ → (0 < slope f x₀ b ↔ f b < f x₀)
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_toInt64 : ∀ (x : Int16), x.toInt64.toNatClampNeg = x.toNatClampNeg
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.ball_subset_closedBall : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E}
  {r : ℝ}, Euclidean.ball x r ⊆ Euclidean.closedBall x r
-- Mathlib.Data.Part
Part.map_Dom : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (o : Part α), (Part.map f o).Dom = o.Dom
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_eq_zero : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) {x : ↥S}, ↑x = 0 ↔ x = 0
-- Init.Data.Rat.Lemmas
Rat.mul_assoc : ∀ (a b c : ℚ), a * b * c = a * (b * c)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableDiv.measurable_const_div : ∀ {G₀ : Type u_2} {inst : MeasurableSpace G₀} {inst_1 : Div G₀} [self : MeasurableDiv G₀] (c : G₀),
  Measurable fun x => c / x
-- Aesop.Forward.State
/-- Remove a hypothesis from the forward state. If `fs` represents a local
context `lctx`, then `fs.eraseHyp h` represents `lctx` with `h` removed.  -/
Aesop.ForwardState.eraseHyp : Lean.FVarId → Aesop.ForwardState → Aesop.ForwardState
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `F' : D ⥤ H` is a right Kan extension of `F : C ⥤ H` along `L : C ⥤ D`, the limit over `F'`
is isomorphic to the limit over `F`.  -/
CategoryTheory.Functor.limitIsoOfIsRightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : L.comp F' ⟶ F) →
                    [F'.IsRightKanExtension α] →
                      [inst_4 : CategoryTheory.Limits.HasLimit F] →
                        [inst_5 : CategoryTheory.Limits.HasLimit F'] →
                          CategoryTheory.Limits.limit F' ≅ CategoryTheory.Limits.limit F
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.hasFactorization : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [self : W₁.IsWeakFactorizationSystem W₂], W₁.HasFactorization W₂
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_tsum_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] (f : ι → M),
  ‖∑' (i : ι), f i‖₊ ≤ ⨆ i, ‖f i‖₊
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.fundSystem.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (i : Fin (NumberField.Units.rank K)),
  NumberField.Units.fundSystem K i = Quotient.out (Additive.toMul ((NumberField.Units.basisModTorsion K) i))
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.instIsMultiplicativeIsColocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P.isColocal.IsMultiplicative
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- This structure contains the data of two right fractions for
`W : MorphismProperty C` that have the same "denominator".  -/
CategoryTheory.MorphismProperty.RightFraction₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → C → C → Type (max u_1 v_1)
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
IntermediateField.algebraicIndependent_adjoin_iff : ∀ {ι : Type u_1} {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [inst : Field F] [inst_1 : Field E]
  [inst_2 : Algebra F E] [inst_3 : CommRing S] [inst_4 : Algebra E S] {x : ι → S},
  AlgebraicIndependent (↥(IntermediateField.adjoin F s)) x ↔ AlgebraicIndependent (↥(Algebra.adjoin F s)) x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g] (hf : S.f = 0),
  CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel S hf =
    CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf
      (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.kernel.ι S.g) ⋯) (CategoryTheory.Limits.kernelIsKernel S.g)
-- Init.Data.List.Lemmas
List.replace_append_right : ∀ {α : Type u_1} [inst : BEq α] {a b : α} [LawfulBEq α] {l₁ l₂ : List α},
  a ∉ l₁ → (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b
-- Mathlib.Data.Nat.ModEq
Nat.add_modEq_right_iff : ∀ {n a b : ℕ}, a + b ≡ b [MOD n] ↔ n ∣ a
-- Mathlib.RingTheory.Valuation.Basic
Valuation.mk.sizeOf_spec : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedCommMonoidWithZero Γ₀] [inst_1 : Ring R] [inst_2 : SizeOf R]
  [inst_3 : SizeOf Γ₀] (toMonoidWithZeroHom : R →*₀ Γ₀)
  (map_add_le_max' :
    ∀ (x y : R),
      (↑toMonoidWithZeroHom).toFun (x + y) ≤ max ((↑toMonoidWithZeroHom).toFun x) ((↑toMonoidWithZeroHom).toFun y)),
  sizeOf { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' } =
    1 + sizeOf toMonoidWithZeroHom
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The inclusion from `X.AffineZariskiSite` to `X.Opens`.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens : {X : AlgebraicGeometry.Scheme} → X.AffineZariskiSite → X.Opens
-- Mathlib.RepresentationTheory.Intertwining
/-- `centralAlgebraMul` as monoid homomorphism from the center of `A[G]` to intertwining map
from any representation of `G` to itself.  -/
Representation.IntertwiningMap.centralAlgebraMulHom : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module A V] →
              (ρ : Representation A G V) → ↥(Submonoid.center (MonoidAlgebra A G)) →* ρ.IntertwiningMap ρ
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} {Y X : (CategoryTheory.Limits.Cocone F)ᵒᵖ} (f : Y ⟶ X),
  (CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.functor.map f).hom = f.unop.hom.unop
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The forgetful functor from group objects to monoid objects.  -/
CategoryTheory.Grp.forget₂Mon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.Grp C) (CategoryTheory.Mon C)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_subset_sub : ∀ {α : Type u_2} [inst : Sub α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ - s₂ ⊆ t₁ - t₂
-- Mathlib.Order.SuccPred.Basic
Order.Icc_pred_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Icc b (Order.pred a) = Set.Ico b a
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Convenience constructor for a subobject.  -/
CategoryTheory.Subobject.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X A : C} → (f : A ⟶ X) → [CategoryTheory.Mono f] → CategoryTheory.Subobject X
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The algebra isomorphism between multivariable polynomials in a single variable and
polynomials over the ground ring.  -/
MvPolynomial.pUnitAlgEquiv : (R : Type u) → [inst : CommSemiring R] → MvPolynomial PUnit.{u_2 + 1} R ≃ₐ[R] Polynomial R
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanIso.bijOn : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β}, IsAddFreimanIso n A B f → Set.BijOn f A B
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.Condensed.TopCatAdjunction
/-- The object part of the functor `CondensedSet ⥤ TopCat`  -/
CondensedSet.toTopCat : CondensedSet → TopCat
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.cancel_natIso_hom_right_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} (α : F ≅ G) {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ F.obj Y) (f' : W ⟶ X')
  (g' : X' ⟶ F.obj Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (α.hom.app Y)) =
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (α.hom.app Y)) ↔
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
/-- A continuous function `f` has bounded range if and only if it is `O(1)` with respect to the
cocompact filter.
 -/
Continuous.isBounded_range_iff_isBigO : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {D : Type u_2} [inst_1 : TopologicalSpace D] {f : D → E},
  Continuous f → (Bornology.IsBounded (Set.range f) ↔ f =O[Filter.cocompact D] 1)
-- Init.Tactics
/-- A `rwRuleSeq` is a list of `rwRule` in brackets.  -/
Lean.Parser.Tactic.rwRuleSeq : Lean.ParserDescr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ Std.DHashMap.Raw.filter f m}
  (h : m.WF), Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.filter f m) k h' = Std.DHashMap.Raw.Const.get m k ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)},
      (t.alter k f).getD k' fallback =
        if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback else t.getD k' fallback
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.coe_span_singleton_eq_closedBall : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] (x : ↥(Valued.integer K)),
  ↑(Ideal.span {x}) = Metric.closedBall 0 ‖x‖
-- Mathlib.Topology.Sheaves.LocallySurjective
/-- A map of presheaves `T : ℱ ⟶ 𝒢` is **locally surjective** if for any open set `U`,
section `t` over `U`, and `x ∈ U`, there exists an open set `x ∈ V ⊆ U` and a section `s` over `V`
such that `$T_*(s_V) = t|_V$`.

See `TopCat.Presheaf.isLocallySurjective_iff` below.
 -/
TopCat.Presheaf.IsLocallySurjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type v} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] → {X : TopCat} → {ℱ 𝒢 : TopCat.Presheaf C X} → (ℱ ⟶ 𝒢) → Prop
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.pow : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} {m n : ℕ}, IsCoprime x y → IsCoprime (x ^ m) (y ^ n)
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- Let `s ⊆ X`. Suppose that `X` is Hausdorff, and that to prove that `s` is open,
it suffices to show that for every compact set `K ⊆ X`, `s ∩ K` is open in `K`.
Then `X` is compactly generated.  -/
compactlyGeneratedSpace_of_isOpen_of_t2 : ∀ {X : Type u} [inst : TopologicalSpace X] [T2Space X],
  (∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' s)) → IsOpen s) → CompactlyGeneratedSpace X
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀`.

---

More explicit constructor in case `Ω₀` is already known to be a terminal object.  -/
CategoryTheory.Classifier.mkOfTerminalΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Ω₀ : C) →
      (t : CategoryTheory.Limits.IsTerminal Ω₀) →
        (Ω : C) →
          (truth : Ω₀ ⟶ Ω) →
            (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) →
              (∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m],
                  CategoryTheory.IsPullback m (t.from U) (χ m) truth) →
                (∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] (χ' : X ⟶ Ω),
                    CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) →
                  CategoryTheory.Subobject.Classifier C
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
  (RingHom.id β).comp f = f
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.equivOfEq_symm : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Subalgebra R A)
  (h : S = T), (S.equivOfEq T h).symm = T.equivOfEq S ⋯
-- Mathlib.Data.Nat.Count
Nat.count_one : ∀ (p : ℕ → Prop) [inst : DecidablePred p], Nat.count p 1 = if p 0 then 1 else 0
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_add_div_same : ∀ {a b c : ENNReal}, a / c + b / c = (a + b) / c
-- Mathlib.Analysis.InnerProductSpace.LinearMap
norm_innerSL_le : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ‖innerSL 𝕜‖ ≤ 1
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoid.mem_closure_finset : ∀ {M : Type u_1} [inst : AddCommMonoid M] {x : M} {s : Finset M},
  x ∈ AddSubmonoid.closure ↑s ↔ ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_smul : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : SMul M β] (c : M) (f : α → β),
  UniformFun.ofFun (c • f) = c • UniformFun.ofFun f
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
CommRingCat.KaehlerDifferential.ext_iff : ∀ {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} {α β : CommRingCat.KaehlerDifferential f ⟶ M},
  α = β ↔
    ∀ (b : ↑B),
      (CategoryTheory.ConcreteCategory.hom α) (CommRingCat.KaehlerDifferential.d b) =
        (CategoryTheory.ConcreteCategory.hom β) (CommRingCat.KaehlerDifferential.d b)
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.BlockMem.instNontrivial : ∀ (G : Type u_1) [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [Nontrivial X] (a : X),
  Nontrivial (AddAction.BlockMem G a)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If the (coproduct-like) biproduct comparison for `F` and `f` is an epimorphism, then `F`
preserves the biproduct of `F` and `f`. For the converse, see `mapBiproduct`.  -/
CategoryTheory.Limits.preservesBiproduct_of_epi_biproductComparison' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C}
  [inst_6 : CategoryTheory.Limits.HasBiproduct f] [inst_7 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)]
  [CategoryTheory.Epi (F.biproductComparison' f)], CategoryTheory.Limits.PreservesBiproduct f F
-- Mathlib.Order.Heyting.Basic
himp_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), a ⇨ aᶜ = aᶜ
-- Lean.ResolveName
_private.Lean.ResolveName.0.Lean.resolveLocalName.go : Lean.LocalDecl → Lean.MacroScopesView → Lean.Name → Lean.Name → Option Lean.LocalDecl
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- If c.norm = 0, return a certificate with proof `x * c.subject = 0` without
recursively certifying `x`.  -/
Mathlib.Tactic.Determinant.zeroProdCert : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Q(«$α») → Mathlib.Tactic.Determinant.Cert rα → Lean.MetaM (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_isCoprime_of_dvd_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime z y → x ∣ y → IsCoprime z x
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_oneMore_iff : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.oneMore ↔ b &&& 224 = 192
-- Mathlib.Util.Export
Lean.Export.Entry : Type
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.pow_apply : ∀ {k n : ℕ}, (ArithmeticFunction.pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.instNonemptyFreeGroupoid : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [Nonempty C], Nonempty (CategoryTheory.FreeGroupoid C)
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a `NormedAddGroup` from a `SeminormedAddGroup`
satisfying `∀ x, ‖x‖ = 0 → x = 0`. This avoids having to go back to the `(Pseudo)MetricSpace`
level when declaring a `NormedAddGroup` instance as a special case of a more general
`SeminormedAddGroup` instance.  -/
NormedAddGroup.ofSeparation : {E : Type u_5} → [inst : SeminormedAddGroup E] → (∀ (x : E), ‖x‖ = 0 → x = 0) → NormedAddGroup E
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).p = CategoryTheory.Limits.cokernel.π S.f
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.tensorProductMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_4}
  {B : Type u_5} {C : Type u_6} {D : Type u_7} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : CommRing C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : CommRing D]
  [inst_14 : Algebra R D] {f : A →ₐ[S] C} {g : B →ₐ[R] D}, f.Flat → g.Flat → (Algebra.TensorProduct.map f g).Flat
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod
-- Std.Time.Format.Modifier
Std.Time.OffsetX.hourMinuteColon.sizeOf_spec : sizeOf Std.Time.OffsetX.hourMinuteColon = 1
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedMul_one : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (x : TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)),
  ((TensorProduct.gradedMul R 𝒜 ℬ) x) 1 = x
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y}
  {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [inst_2 : F.Full]
  {Z : D} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (hf.lift i h hi)) (CategoryTheory.CategoryStruct.comp (hf.fst g) h_1) =
    CategoryTheory.CategoryStruct.comp i h_1
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.instOrderTop : {R : Type u_1} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → OrderTop (Submodule R M)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.union_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ m₃ m₄ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∪ m₂).Equiv (m₃ ∪ m₄)
-- Init.Data.List.TakeDrop
List.take_succ_eq_append_getElem : ∀ {α : Type u_1} {i : ℕ} {l : List α} (h : i < l.length), List.take (i + 1) l = List.take i l ++ [l[i]]
-- Std.Data.String.ToNat
String.isNat_toSlice : ∀ {s : String}, s.toSlice.isNat = s.isNat
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_single_neg : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {p : ι → Prop}
  [inst_2 : DecidablePred p] (i : ι) (x : β i), ¬p i → (DFinsupp.filter p fun₀ | i => x) = 0
-- Init.Data.Sum.Basic
Sum.elim_inr : ∀ {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : α → γ) (g : β → γ) (x : β), Sum.elim f g (Sum.inr x) = g x
-- Init.Prelude
instHAppendOfAppend : {α : Type u_1} → [Append α] → HAppend α α α
-- Aesop.Rule.Name
Aesop.ScopeName.noConfusionType : Sort v✝ → Aesop.ScopeName → Aesop.ScopeName → Sort v✝
-- Batteries.Data.List.Basic
/-- Inner loop for `dropInfix?`.  -/
List.dropInfix?.go : {α : Type u_1} → [BEq α] → List α → List α → List α → Option (List α × List α)
-- Mathlib.Order.BooleanAlgebra.Defs
BooleanAlgebra.mk : {α : Type u} →
  [toDistribLattice : DistribLattice α] →
    [toCompl : Compl α] →
      [toSDiff : SDiff α] →
        [toHImp : HImp α] →
          [toTop : Top α] →
            [toBot : Bot α] →
              (∀ (x : α), x ⊓ xᶜ ≤ ⊥) →
                (∀ (x : α), ⊤ ≤ x ⊔ xᶜ) →
                  (∀ (a : α), a ≤ ⊤) →
                    (∀ (a : α), ⊥ ≤ a) →
                      autoParam (∀ (x y : α), x \ y = x ⊓ yᶜ) BooleanAlgebra.sdiff_eq._autoParam →
                        autoParam (∀ (x y : α), x ⇨ y = y ⊔ xᶜ) BooleanAlgebra.himp_eq._autoParam → BooleanAlgebra α
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roi.toArray_iter : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roi α}, r.iter.toArray = r.toArray
-- Mathlib.Algebra.Order.IsBotOne
NeZero.of_gt' : ∀ {α : Type u_1} {a : α} [inst : Zero α] [inst_1 : Preorder α] [IsBotZeroClass α] [inst_3 : One α] [Fact (1 < a)],
  NeZero a
-- Std.Time.Format.Modifier
Std.Time.instReprOffsetX : Repr Std.Time.OffsetX
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
OrderIso.divRight₀_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : MulPosReflectLT G₀] (a : G₀)
  (ha : 0 < a) (x : G₀), (OrderIso.divRight₀ a ha) x = x / a
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.root : {n : ℕ} →
  {P : MvPFunctor.{u} (n + 1)} →
    (x : P.last.M) →
      (a : P.A) → (f : P.last.B a → P.last.M) → x.dest = ⟨a, f⟩ → (i : Fin2 n) → P.drop.B a i → MvPFunctor.M.Path P x i
-- Mathlib.Algebra.Group.Action.Defs
IsCancelVAdd.mk : ∀ {G : Type u_9} {P : Type u_10} [inst : VAdd G P] [toIsLeftCancelVAdd : IsLeftCancelVAdd G P],
  (∀ (a b : G) (c : P), a +ᵥ c = b +ᵥ c → a = b) → IsCancelVAdd G P
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.toSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] (A B : Subgroup G) (u : ℤˣ), HNNExtension.toSubgroup A B u = if u = 1 then A else B