mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e =
    {
      hom :=
        CategoryTheory.Limits.coprod.desc
          (AlgebraicGeometry.Scheme.Hom.normalizationDesc (CategoryTheory.CategoryStruct.comp iU f)
            (CategoryTheory.CategoryStruct.comp iU (AlgebraicGeometry.Scheme.Hom.toNormalization f))
            (AlgebraicGeometry.Scheme.Hom.fromNormalization f) ⋯)
          (AlgebraicGeometry.Scheme.Hom.normalizationDesc (CategoryTheory.CategoryStruct.comp iV f)
            (CategoryTheory.CategoryStruct.comp iV (AlgebraicGeometry.Scheme.Hom.toNormalization f))
            (AlgebraicGeometry.Scheme.Hom.fromNormalization f) ⋯),
      inv :=
        AlgebraicGeometry.Scheme.Hom.normalizationDesc f
          (CategoryTheory.CategoryStruct.comp
            (e.coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.pair U V))).hom
            (CategoryTheory.Limits.coprod.map
              (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iU f))
              (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iV f))))
          (CategoryTheory.Limits.coprod.desc
            (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iU f))
            (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iV f)))
          ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryLE! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap α (fun x => β) cmp → α → α × β
-- Std.Data.String.ToNat
String.Slice.toNat?_comp_copy : String.toNat? ∘ String.Slice.copy = String.Slice.toNat?
-- Mathlib.Order.Lattice
Bool.instPartialOrder : PartialOrder Bool
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.of_symm_eq : ∀ {M : Type u_1}, MulArchimedeanOrder.of.symm = MulArchimedeanOrder.val
-- Mathlib.Data.PNat.Xgcd
/-- `z = zp + 1`  -/
PNat.XgcdType.z : PNat.XgcdType → ℕ+
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- If `I` is a nonzero fractional ideal, `a ∈ R`, and `J` is an ideal of `R` such that
`I = a⁻¹J`, then `a` is nonzero.  -/
FractionalIdeal.constant_factor_ne_zero : ∀ {R : Type u_6} [inst : CommRing R] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ {a : R} {J : Ideal R},
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J → Ideal.span {a} ≠ 0
-- Mathlib.Algebra.Homology.CochainComplexPlus
CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_X : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : F.PreservesZeroMorphisms] (X : CochainComplex.Plus C) (i : ℤ),
  (F.mapCochainComplexPlus.obj X).obj.X i = F.obj (X.obj.X i)
-- Aesop.Tree.Data
Aesop.instDecidableEqRappId : DecidableEq Aesop.RappId
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalSemiring.toContinuousMul : ∀ {R : Type u_1} {inst : TopologicalSpace R} {inst_1 : NonUnitalNonAssocSemiring R} [self : IsTopologicalSemiring R],
  ContinuousMul R
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {ra rb : Lean.Meta.Grind.Arith.CommRing.RingExpr} {a_1 b_1 : Lean.Expr}
  {ra_1 rb_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr},
  Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core a b ra rb =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core a_1 b_1 ra_1 rb_1 →
    a = a_1 ∧ b = b_1 ∧ ra = ra_1 ∧ rb = rb_1
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.associator_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H I : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B),
  (CategoryTheory.Oplax.LaxTrans.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivInverse_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) {J : Type w}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).obj c =
    CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c
-- Mathlib.Algebra.Algebra.Unitization
/-- If `φ : A →⋆ₙₐ[R] B` is injective, the lift `starMap φ : Unitization R A →⋆ₐ[R] Unitization R B`
is also injective.  -/
Unitization.starMap_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : NonUnitalSemiring B] [inst_8 : StarRing B] [inst_9 : Module R B]
  [inst_10 : SMulCommClass R B B] [inst_11 : IsScalarTower R B B] [inst_12 : StarModule R B] {φ : A →⋆ₙₐ[R] B},
  Function.Injective ⇑φ → Function.Injective ⇑(Unitization.starMap φ)
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.pmap.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : (x : List α) → (∀ a ∈ x, P a) → Sort u_2) (x : ∀ a ∈ [], P a)
  (h_1 : (x : ∀ a ∈ [], P a) → motive [] x)
  (h_2 : (a : α) → (l : List α) → (H : ∀ a_1 ∈ a :: l, P a_1) → motive (a :: l) H),
  (match [], x with
    | [], x => h_1 x
    | a :: l, H => h_2 a l H) =
    h_1 x
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.IsQuotientMap.isGeneratedBy`. -/
Topology.IsQuotientMap.deltaGeneratedSpace : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] {f : Y → Z},
  Topology.IsQuotientMap f → ∀ [Topology.IsGeneratedBy X Y], Topology.IsGeneratedBy X Z
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_mul_le_one : ∀ (a : ENNReal), a⁻¹ * a ≤ 1
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.seq.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ}
  (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B),
  NumberField.Units.dirichletUnitTheorem.seq K w₁ hB 0 = ⟨1, ⋯⟩
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivInvOneMonoid` if it admits an injective
map that preserves `1`, `*`, `⁻¹`, and `/` to a `DivInvOneMonoid`. See note
[reducible non-instances].  -/
Function.Injective.divInvOneMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : DivInvOneMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → DivInvOneMonoid M₁
-- Mathlib.Topology.Path
/-- Pointwise addition of paths in a topological additive group.  -/
Path.add : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [inst_1 : Add X] → [ContinuousAdd X] → {a₁ b₁ a₂ b₂ : X} → Path a₁ b₁ → Path a₂ b₂ → Path (a₁ + a₂) (b₁ + b₂)
-- Mathlib.Data.Set.Piecewise
Set.piecewise_compl : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
  [inst_1 : (i : α) → Decidable (i ∈ sᶜ)], sᶜ.piecewise f g = s.piecewise g f
-- Mathlib.GroupTheory.Abelianization.Defs
abelianizationCongr_trans : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] {I : Type v} [inst_2 : Group I] (e : G ≃* H)
  (e₂ : H ≃* I), e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr
-- Init.Data.SInt.Lemmas
Int8.neg_nonpos_iff : ∀ (n : Int8), -n ≤ 0 ↔ n = Int8.minValue ∨ 0 ≤ n
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- `includeLeftSubRight` is compatible with `distribBaseChange` and `lTensor`.  -/
Algebra.TensorProduct.distribBaseChange_comp_includeLeftSubRight : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T],
  ↑(LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)) ∘ₗ
      LinearMap.lTensor T (Algebra.TensorProduct.includeLeftSubRight R S) =
    ↑R (Algebra.TensorProduct.includeLeftSubRight T (TensorProduct R T S))
-- Lean.Data.PersistentArray
Lean.PersistentArray.mkNewTail : {α : Type u} → Lean.PersistentArray α → Lean.PersistentArray α
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- If `C` has enough injectives, we may choose an injective presentation of `X : C`
which is given by a zero object when `X` is a zero object.  -/
CategoryTheory.Injective.exists_presentation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EnoughInjectives C] (X : C),
  ∃ p, CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero p.J
-- Mathlib.SetTheory.ZFC.PSet
PSet.instInsert : Insert PSet.{u_1} PSet.{u_1}
-- Mathlib.RingTheory.HahnSeries.Basic
/-- Change a `HahnSeries` on a Lex product to a `HahnSeries` with coefficients in a `HahnSeries`.  -/
HahnSeries.toIterate : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      [inst : PartialOrder Γ] →
        [inst_1 : Zero R] → [inst_2 : PartialOrder Γ'] → HahnSeries (Lex (Γ × Γ')) R → HahnSeries Γ (HahnSeries Γ' R)
-- Mathlib.NumberTheory.DirichletCharacter.GaussSum
/-- If `gaussSum χ e ≠ 0`, and `d` is such that `e.mulShift d = 1`, then `χ` must factor through
`d`. (This will be used to show that Gauss sums vanish when `χ` is primitive and `e` is not.)  -/
factorsThrough_of_gaussSum_ne_zero : ∀ {N : ℕ} [inst : NeZero N] {R : Type u_1} [inst_1 : CommRing R] (e : AddChar (ZMod N) R) [IsDomain R]
  {χ : DirichletCharacter R N} {d : ℕ}, d ∣ N → e.mulShift ↑d = 1 → gaussSum χ e ≠ 0 → χ.FactorsThrough d
-- Lean.Server.FileWorker.SemanticHighlighting
/-- A debugging utility for inspecting sets of collected tokens, classified by line and sorted by
column.
 -/
Lean.Server.FileWorker.dbgShowTokens : Lean.FileMap → Array Lean.Server.FileWorker.LeanSemanticToken → String
-- Init.Data.List.Lemmas
List.filterMap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Option γ} {l : List α},
  List.filterMap g (List.map f l) = List.filterMap (g ∘ f) l
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.πTruncGE_naturality : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.CategoryStruct.comp (K.πTruncGE e) (HomologicalComplex.truncGEMap φ e) =
    CategoryTheory.CategoryStruct.comp φ (L.πTruncGE e)
-- Init.Data.SInt.Basic
/-- Converts a word-sized signed integer to a natural number, mapping all negative numbers to `0`.

Use `ISize.toBitVec` to obtain the two's complement representation.
 -/
ISize.toNatClampNeg : ISize → ℕ
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The evaluation natural transformation.  -/
CategoryTheory.ihom.ev : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : C) →
        [inst_2 : CategoryTheory.Closed A] →
          (CategoryTheory.ihom A).comp (CategoryTheory.MonoidalCategory.tensorLeft A) ⟶ CategoryTheory.Functor.id C
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.IsFinite.finite_relations : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (p : M.Presentation) [p.IsFinite],
  Finite p.relations.I
-- Aesop.Forward.Match.Types
Aesop.CompleteMatch.mk.sizeOf_spec : ∀ (clusterMatches : Array Aesop.Match), sizeOf { clusterMatches := clusterMatches } = 1 + sizeOf clusterMatches
-- Std.Data.DHashMap.RawLemmas
/-- Variant of `getD_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Raw.Const.getD_map' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ} (h : m.WF),
  Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.map f m) k fallback =
    (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Raw.Const.get? m k) ⋯).getD fallback
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.domCongr_support : ∀ (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : Semiring A] [inst_3 : CommSemiring k] [inst_4 : Algebra k A] [inst_5 : MulSemiringAction G A]
  [inst_6 : MulSemiringAction H A] [inst_7 : SMulCommClass G k A] [inst_8 : SMulCommClass H k A] {e : G ≃* H}
  (he : ∀ (a : G) (x : A), a • x = e a • x) (f : SkewMonoidAlgebra A G),
  ((SkewMonoidAlgebra.domCongrAlg k A he) f).support = Finset.map (↑e).toEmbedding f.support
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- If `f` is differentiable at `x`, and `L` is `σ`-semilinear, then `L ∘ f ∘ σ⁻¹` is
differentiable at `σ x`.  -/
DifferentiableAt.comp_ringHom : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (σ σ' : 𝕜 →+* 𝕜) [RingHomIsometric σ] [RingHomInvPair σ σ']
  {f : 𝕜 → 𝕜}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (⇑σ ∘ f ∘ ⇑σ') (σ x)
-- Mathlib.CategoryTheory.Limits.Shapes.Equivalence
CategoryTheory.hasInitial_of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : CategoryTheory.Functor D C) [e.IsEquivalence] [CategoryTheory.Limits.HasInitial C],
  CategoryTheory.Limits.HasInitial D
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.DaylightSavingRule.mk.inj : ∀ {name : String} {offset : Std.Time.TimeZone.Offset} {start end_ : Option Std.Time.TimeZone.TransitionRule}
  {name_1 : String} {offset_1 : Std.Time.TimeZone.Offset} {start_1 end__1 : Option Std.Time.TimeZone.TransitionRule},
  { name := name, offset := offset, start := start, end_ := end_ } =
      { name := name_1, offset := offset_1, start := start_1, end_ := end__1 } →
    name = name_1 ∧ offset = offset_1 ∧ start = start_1 ∧ end_ = end__1
-- Lean.InternalExceptionId
/-- Retrieve the name used to register the internal exception.  -/
Lean.InternalExceptionId.getName : Lean.InternalExceptionId → IO Lean.Name
-- Mathlib.Data.EReal.Inv
EReal.div_lt_div_right_of_neg : ∀ {a b c : EReal}, c < 0 → c ≠ ⊥ → a < b → b / c < a / c
-- Lean.Meta.Sym.Arith.Types
/-- Cached `getDecLevel type`  -/
Lean.Meta.Sym.Arith.Ring.u : Lean.Meta.Sym.Arith.Ring → Lean.Level
-- Mathlib.Analysis.Convex.BetweenList
List.exists_map_eq_of_sorted_iff_sbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] [Nontrivial P] {l : List P},
  (∃ p₁ p₂, p₁ ≠ p₂ ∧ ∃ l', l'.SortedLT ∧ List.map (⇑(AffineMap.lineMap p₁ p₂)) l' = l) ↔ List.Sbtw R l
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n)
  (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc)
      (CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (CategoryTheory.Limits.Fork.ι kf)) =
    S.map' (k + 1) (k + 2) ⋯ ⋯
-- Mathlib.RingTheory.Unramified.Basic
Algebra.Unramified.finiteType : ∀ {R : Type u_1} {inst : CommRing R} {A : Type u_2} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.Unramified R A], Algebra.FiniteType R A
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.prod_toAffineMap : ∀ {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃), ↑(f.prod g) = (↑f).prod ↑g
-- Mathlib.Algebra.Group.Basic
zpow_add_one : ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℤ), a ^ (n + 1) = a ^ n * a
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_univ : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Finsupp.supported M R Set.univ = ⊤
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
/-- The Grothendieck group is a group.  -/
Algebra.GrothendieckAddGroup.instAddCommGroup : {M : Type u_1} → [inst : AddCommMonoid M] → AddCommGroup (Algebra.GrothendieckAddGroup M)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns extension states associate with `grind` attributes in use  -/
Lean.Meta.Grind.getExtensions : Lean.Meta.Grind.GrindM Lean.Meta.Grind.ExtensionStateArray
-- Mathlib.LinearAlgebra.Contraction
/-- When `M` is a finite free module, the map `lTensorHomToHomLTensor` is an equivalence. Note
that `lTensorHomEquivHomLTensor` is not defined directly in terms of
`lTensorHomToHomLTensor`, but the equivalence between the two is given by
`lTensorHomEquivHomLTensor_toLinearMap` and `lTensorHomEquivHomLTensor_apply`.  -/
lTensorHomEquivHomLTensor : (R : Type u_2) →
  (M : Type u_3) →
    (P : Type u_5) →
      (Q : Type u_6) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid P] →
              [inst_3 : AddCommMonoid Q] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R P] →
                    [inst_6 : Module R Q] →
                      [Module.Projective R M] →
                        [Module.Finite R M] → TensorProduct R P (M →ₗ[R] Q) ≃ₗ[R] M →ₗ[R] TensorProduct R P Q
-- Std.Sat.AIG.Basic
/-- An `AIG` with an empty AIG and cache.
 -/
Std.Sat.AIG.empty : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α
-- Mathlib.CategoryTheory.Sites.Adjunction
CategoryTheory.Sheaf.instPreservesSheafificationOfIsLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {G : CategoryTheory.Functor E D} [G.IsLeftAdjoint], J.PreservesSheafification G
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.symplComp_symplComp_eq : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] [CompleteSpace H]
  {S : ClosedSubmodule ℝ H}, S.symplComp.symplComp = S
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_add_norm_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (u v : E), ‖u‖ ≤ ‖u + v‖ + ‖v‖
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (base : k.fst ⟶ l.fst)
  (hom : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base) =
        CategoryTheory.CategoryStruct.comp hom ((P l.fst).ι.app l.snd))
      CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam)
  (base_1 : k.fst ⟶ l.fst) (hom_1 : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd)
  (w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base_1) =
        CategoryTheory.CategoryStruct.comp hom_1 ((P l.fst).ι.app l.snd))
      CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam),
  ({ base := base, hom := hom, w := w } = { base := base_1, hom := hom_1, w := w_1 }) = (base = base_1 ∧ hom = hom_1)
-- Mathlib.RingTheory.Jacobson.Semiprimary
IsSemisimpleModule.jacobson_eq_bot : ∀ (R : Type u_1) (M : Type u_3) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M], Module.jacobson R M = ⊥
-- Init.System.CancelToken
/-- Activates a cancellation token. Idempotent.

Resolves the underlying promise *before* setting the `Bool` flag, so that observing `isSet = true`
implies that any synchronously-chained `onSet` callbacks have already run. The reverse implication
does not hold: a callback running synchronously inside `set` may briefly observe `isSet = false`.
 -/
IO.CancelToken.set : IO.CancelToken → BaseIO Unit
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_def : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : α → β} {s : Set β},
  MeasurableSet s ↔ MeasurableSet (f ⁻¹' s)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.insertMany : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ ((a : α) × β a)]
  {m : Std.DHashMap.Raw α β} {l : ρ}, m.WF → (m.insertMany l).WF
-- Lean.Parser.Basic
Lean.Parser.instOrElseParser : OrElse Lean.Parser.Parser
-- Mathlib.Order.InitialSeg
InitialSeg.refl_apply : ∀ {α : Type u_1} {r : α → α → Prop} (x : α), (InitialSeg.refl r) x = x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insert_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, (compare ((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey ⋯) k).isLE = true