mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalarsRange_apply_eq_zero_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} {M' : Type u_5} {P' : Type u_6} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : SMul S R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] [inst_7 : Module S M] [inst_8 : Module S P] [inst_9 : IsScalarTower S R M]
  [inst_10 : IsScalarTower S R P] [inst_11 : AddCommMonoid M'] [inst_12 : Module S M'] [inst_13 : AddCommMonoid P']
  [inst_14 : Module S P'] (i : M' →ₗ[S] M) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (f : M →ₗ[R] P)
  (hf : ∀ (m : M'), f (i m) ∈ k.range) (m : M'), (i.restrictScalarsRange k hk f hf) m = 0 ↔ f (i m) = 0
-- Mathlib.RingTheory.WittVector.MulCoeff
_private.Mathlib.RingTheory.WittVector.MulCoeff.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Rep.Res
/-- The restriction of `X : Rep k G` associated to a monoid homomorphism `f : H →* G`  -/
Rep.res : {k : Type u} →
  [inst : Semiring k] →
    {G : Type v1} →
      {H : Type v2} → [inst_1 : Monoid G] → [inst_2 : Monoid H] → (H →* G) → Rep.{u_1, u, v1} k G → Rep.{u_1, u, v2} k H
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst_hom_app : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} (X : p.Fiber S),
  CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst.hom.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
/-- If `G` is a topological group and `H` a finite-index subgroup, then `G` is topologically
discrete iff `H` is.  -/
Subgroup.discreteTopology_iff_of_finiteIndex : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H : Subgroup G}
  [H.FiniteIndex], DiscreteTopology ↥H ↔ DiscreteTopology G
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- The compactly generated topology on a topological space `X`. This is the finest topology
which makes all maps from compact Hausdorff spaces to `X`, which are continuous for the original
topology, continuous.

Note: this definition should be used with an explicit universe parameter `u` for the size of the
compact Hausdorff spaces mapping to `X`.
 -/
TopologicalSpace.compactlyGenerated : (X : Type w) → [TopologicalSpace X] → TopologicalSpace X
-- Mathlib.Algebra.Order.Ring.Synonym
toLex_intCast : ∀ {R : Type u_1} [inst : IntCast R] (n : ℤ), toLex ↑n = ↑n
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.vcomp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ ι : F ⟶ G} (Γ : CategoryTheory.Oplax.LaxTrans.Modification η θ)
  (Δ : CategoryTheory.Oplax.LaxTrans.Modification θ ι) (a : B),
  (Γ.vcomp Δ).app a = CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a)
-- Lean.Elab.SetOption
Lean.Elab.linter.deprecated.options : Lean.Option Bool
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitProj : Lean.Expr → Lean.Name → ℕ → Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C}
  (h_1 : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n)
      (CategoryTheory.CategoryStruct.comp (X.opcyclesIsoKernel f g fg h n).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.kernel.ι ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h))) h_1)) =
    CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) h_1
-- Init.Data.Int.DivMod.Lemmas
Int.sub_bmod : ∀ (a b : ℤ) (n : ℕ), (a - b).bmod n = (a.bmod n - b.bmod n).bmod n
-- Std.Http.Data.Body.Basic
/-- Sets the declared size of a body.
 -/
Std.Http.Body.setKnownSize : {α : Type} → [self : Std.Http.Body α] → α → Option Std.Http.Body.Length → Std.Async.Async Unit
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.instHasBinaryBiproductObjEval : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.Limits.HasBinaryBiproduct ((HomologicalComplex.eval C c i).obj K)
    ((HomologicalComplex.eval C c i).obj L)
-- Mathlib.CategoryTheory.Localization.Resolution
/-- a morphism in the source category  -/
CategoryTheory.LocalizerMorphism.RightResolution.Hom.f : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → {R R' : Φ.RightResolution X₂} → R.Hom R' → (R.X₁ ⟶ R'.X₁)
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.toOption.eq_2 : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos),
  String.Slice.Pattern.ForwardSliceSearcher.toOption✝ (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h) =
    some (pos.remainingBytes, 0)
-- Init.Data.List.Pairwise
List.Pairwise.and : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {S : α → α → Prop},
  List.Pairwise R l → List.Pairwise S l → List.Pairwise (fun a b => R a b ∧ S a b) l
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The existence of a left Kan extension of `g` along `f`.  -/
CategoryTheory.Bicategory.HasLeftKanExtension : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b c : B} → (a ⟶ b) → (a ⟶ c) → Prop
-- Std.Time.Format
/-- Parses a date string in the SQL format (`uuuu-MM-dd`) and returns a `PlainDate`.
 -/
Std.Time.PlainDate.fromSQLDateString : String → Except String Std.Time.PlainDate
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context : Type
-- Init.Data.Vector.Lemmas
Vector.toList_mk : ∀ {α : Type u_1} {xs : Array α} {a : ℕ} {h : xs.size = a}, (Vector.mk xs h).toList = xs.toList
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.ext_iff : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} {x y : Metric.Snowflaking X α hα₀ hα₁}, x = y ↔ x.val = y.val
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- compatibility condition  -/
CategoryTheory.Endofunctor.Algebra.Hom.h_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (self : A₀.Hom A₁) {Z : C} (h : A₁.a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map self.f) (CategoryTheory.CategoryStruct.comp A₁.str h) =
    CategoryTheory.CategoryStruct.comp A₀.str (CategoryTheory.CategoryStruct.comp self.f h)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yoneda_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (x : Cᵒᵖ),
  (CategoryTheory.yoneda.map f).app x = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp g f
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.iUnion_split : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ), (BoxIntegral.Prepartition.split I i x).iUnion = ↑I
-- Mathlib.Data.Set.Prod
Set.offDiag_eq_sep_prod : ∀ {α : Type u_1} (s : Set α), s.offDiag = {x | x ∈ s ×ˢ s ∧ x.1 ≠ x.2}
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The mixed space `ℝ^r₁ × ℂ^r₂`, with `(r₁, r₂)` the signature of `K`, as a Euclidean space.  -/
NumberField.mixedEmbedding.euclidean.mixedSpace : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_mul : ∀ {a b : ENNReal}, (a * b).toNNReal = a.toNNReal * b.toNNReal
-- Mathlib.Algebra.Order.GroupWithZero.Basic
StrictAnti.const_mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [inst_2 : Preorder α]
  {f : α → M₀} [PosMulStrictMono M₀], StrictAnti f → 0 < a → StrictAnti fun x => a * f x
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedHGFunSeries_coeff : ∀ {a b : Multiset ℂ}, (Complex.regularizedHGFunSeries a b).coeff = Complex.regularizedHGFunCoeff a b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitArg.type : Lean.Meta.Grind.SplitArg → Lean.Expr
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : Inhabited α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey! k = m₁.getKey! k
-- Batteries.Data.List.Basic
List.swapAtTR.go.eq_3 : ∀ {α : Type u_1} (l : List α) (v : α) (a : Array α) (x_3 : α) (xs : List α) (n : ℕ),
  List.swapAtTR.go l v (x_3 :: xs) n.succ a = List.swapAtTR.go l v xs n (a.push x_3)
-- Init.Data.List.Nat.Sum
List.min_mul_length_le_sum_nat : ∀ {xs : List ℕ} (h : xs ≠ []), xs.min h * xs.length ≤ xs.sum
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_ext_iff : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R)
  (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R), A₁.fromCols A₂ = B₁.fromCols B₂ ↔ A₁ = B₁ ∧ A₂ = B₂
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.ZNum.ofInt'.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_nat_eq_addSubmonoidClosure : ∀ {M : Type u_4} [inst : AddCommMonoid M] (s : Set M), (Submodule.span ℕ s).toAddSubmonoid = AddSubmonoid.closure s
-- Init.Data.Function
Function.LeftInverse.id : ∀ {α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β}, Function.LeftInverse g f → g ∘ f = id
-- Init.Data.String.Lemmas.Basic
String.sliceTo_sliceTo : ∀ {s : String} {pos : s.Pos} {pos' : (s.sliceTo pos).Pos},
  (s.sliceTo pos).sliceTo pos' = s.sliceTo (String.Pos.ofSliceTo pos')
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_coe_finset : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α] (s : Finset α),
  MulAction.stabilizer G ↑s = MulAction.stabilizer G s
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.erase_aux : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLE α] (x : α) {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α},
  Ordnode.Valid' a₁ t a₂ → Ordnode.Valid' a₁ (Ordnode.erase x t) a₂ ∧ Ordnode.Raised (Ordnode.erase x t).size t.size
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalRing.toContinuousNeg : ∀ {R : Type u_1} {inst : TopologicalSpace R} {inst_1 : NonUnitalNonAssocRing R} [self : IsTopologicalRing R],
  ContinuousNeg R
-- Mathlib.Order.Partition.Finpartition
Finpartition.instOrderTopOfDecidableEqBot : {α : Type u_1} → [inst : Lattice α] → [inst_1 : OrderBot α] → {a : α} → [Decidable (a = ⊥)] → OrderTop (Finpartition a)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLT.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.lt) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, compare a k = Ordering.lt) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β ky) →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2
-- Mathlib.Data.List.Map2
List.zipRight'_nil_cons : ∀ {α : Type u} {β : Type v} (b : β) (bs : List β),
  [].zipRight' (b :: bs) = ((none, b) :: List.map (fun b => (none, b)) bs, [])
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The pushforward functor for categories of sheaves of modules over schemes.  -/
AlgebraicGeometry.Scheme.Modules.pushforward : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → CategoryTheory.Functor X.Modules Y.Modules
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α], List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Mathlib.Order.Disjoint
disjoint_assoc : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b c : α}, Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)
-- Mathlib.SetTheory.ZFC.PSet
PSet.mk.sizeOf_spec : ∀ (α : Type u) (A : α → PSet.{u}), sizeOf (PSet.mk α A) = 1 + sizeOf α
-- Init.GrindInstances.ToInt
Int8.size.eq_1 : Int8.size = 256
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodComm.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MulEquiv.prodComm = { toEquiv := Equiv.prodComm M N, map_mul' := ⋯ }
-- Mathlib.Util.FormatTable
/-- Align a `String` `s` to the left, right, or center within a field of width `width`.  -/
String.justify : String → Alignment → ℕ → String
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α},
  (m₁ \ m₂).getKeyD k fallback = if k ∈ m₂ then fallback else m₁.getKeyD k fallback
-- Mathlib.Algebra.Star.Basic
/-- When multiplication is commutative, `star` preserves division.  -/
star_div : ∀ {R : Type u} [inst : CommGroup R] [inst_1 : StarMul R] (x y : R), star (x / y) = star x / star y
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.toBilin_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : LinearOrder ι] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  (Q : QuadraticMap R M N) (bm : Module.Basis ι R M) (i j : ι),
  ((Q.toBilin bm) (bm i)) (bm j) =
    if i = j then Q (bm i) else if i < j then QuadraticMap.polar (⇑Q) (bm i) (bm j) else 0
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- `mapGL` is the map from the special linear group over `R` to the general linear group over
`S`, where `S` is an `R`-algebra.  -/
Matrix.SpecialLinearGroup.mapGL : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          (S : Type u_1) → [inst_3 : CommRing S] → [Algebra R S] → Matrix.SpecialLinearGroup n R →* GL n S
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- In a space with the Besicovitch covering property, the set of closed balls with positive radius
forms a Vitali family. This is essentially a restatement of the measurable Besicovitch theorem.  -/
Besicovitch.vitaliFamily : {α : Type u_1} →
  [inst : MetricSpace α] →
    [SecondCountableTopology α] →
      [inst_2 : MeasurableSpace α] →
        [OpensMeasurableSpace α] →
          [HasBesicovitchCovering α] → (μ : MeasureTheory.Measure α) → [MeasureTheory.SFinite μ] → VitaliFamily μ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rio_eq_fallback : ∀ {n i fallback : ℕ}, n ≤ i → (*...n).toArray.getD i fallback = fallback
-- Init.Data.List.Lemmas
List.getLast?.eq_1 : ∀ {α : Type u}, [].getLast? = none
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C}
  (φ ψ : W.LeftFraction X Y), φ.map L ⋯ = ψ.map L ⋯ ↔ CategoryTheory.MorphismProperty.LeftFractionRel φ ψ
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- Given a morphism `f : K ⟶ L`, this is the property of factorisations
of `f` consisting of a monomorphism followed by a degreewise epimorphism
with injective kernel.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cofFib : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} → (f : K ⟶ L) → CategoryTheory.ObjectProperty (CategoryTheory.Factorisation f)
-- Mathlib.Data.Nat.Squarefree
/-- The correctness property of the return value of `minSqFac`.
* If `none`, then `n` is squarefree;
* If `some d`, then `d` is a minimal square factor of `n`  -/
Nat.MinSqFacProp : ℕ → Option ℕ → Prop
-- Init.Data.List.Nat.InsertIdx
List.getElem_insertIdx : ∀ {α : Type u} {l : List α} {x : α} {i j : ℕ} (h : j < (l.insertIdx i x).length),
  (l.insertIdx i x)[j] = if h₁ : j < i then l[j] else if h₂ : j = i then x else l[j - 1]
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.cofinite_eq_bot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  μ.cofinite = ⊥
-- Lean.Elab.Tactic.Omega.Core
/-- As for `runOmega`, but assuming the first round of solving equalities has already happened.  -/
Lean.Elab.Tactic.Omega.Problem.elimination : Lean.Elab.Tactic.Omega.Problem → Lean.Elab.Tactic.Omega.OmegaM Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Topology.Connected.Basic
connectedComponent_disjoint : ∀ {α : Type u} [inst : TopologicalSpace α] {x y : α},
  connectedComponent x ≠ connectedComponent y → Disjoint (connectedComponent x) (connectedComponent y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertMany!_list : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β},
  t.WF → (↑(t.insertMany! l)).toListModel.Perm (Std.Internal.List.insertList t.toListModel l)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.nontrivial_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M},
  Nontrivial (M ⧸ p) ↔ p ≠ ⊤
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.instStrongNormalizationMonoid : {k : Type u_2} → [inst : Field k] → StrongNormalizationMonoid (PowerSeries k)
-- Aesop.Script.CtorNames
_private.Aesop.Script.CtorNames.0.Aesop.CtorNames.nameBase : Lean.Name → Lean.Name
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Wide pullback diagrams of equivalent index types are equivalent.  -/
CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv : {J : Type w} →
  (J' : Type w') → J ≃ J' → (CategoryTheory.Limits.WidePullbackShape J ≌ CategoryTheory.Limits.WidePullbackShape J')
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.of_sub_of : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Sub α] (f g : m → n → α),
  Matrix.of f - Matrix.of g = Matrix.of (f - g)
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.slope_le_of_hasDerivWithinAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S x → slope f x y ≤ f'
-- Mathlib.Order.SupClosed
infClosure_univ : ∀ {α : Type u_3} [inst : SemilatticeInf α], infClosure Set.univ = Set.univ
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.instFaithfulActionMapAction : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (F : CategoryTheory.Functor V W) (G : Type u_3) [inst_2 : Monoid G]
  [F.Faithful], (F.mapAction G).Faithful
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.bot_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : OrderBot α], IsLowerSet s → (⊥ ∈ s ↔ s.Nonempty)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (m n : ℤ)
  (hmn : autoParam (m + n = 0) CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app._auto_1)
  {Z : Cᵒᵖ}
  (h :
    (CategoryTheory.shiftFunctor Cᵒᵖ m).obj
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj (Opposite.op X))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor Cᵒᵖ m).map
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op X)))
      h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app
        ((CategoryTheory.shiftFunctor Cᵒᵖ m).obj (Opposite.op X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor Cᵒᵖ n).map
          ((CategoryTheory.shiftFunctor C n).map
              ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n hmn).hom.app (Opposite.op X)).unop).op)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor Cᵒᵖ n).map
            ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n hmn).inv.app
              (Opposite.op ((CategoryTheory.shiftFunctor C n).obj X))))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctorComm Cᵒᵖ n m).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj X)))
            h)))
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instStreamStream : {α : Type u_1} → Std.Stream (RBTree.RBNode.Stream α) α
-- Init.Data.Array.Lemmas
Array.elem_eq_mem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {xs : Array α}, Array.elem a xs = decide (a ∈ xs)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, (Std.TreeMap.map f t).isEmpty = t.isEmpty
-- Mathlib.Analysis.Distribution.DerivNotation
LineDerivLeftSMul.mk : ∀ {R : Type u_11} {V : Type u} {E : Type v} {F : outParam (Type w)} [inst : SMul R V] [inst_1 : SMul R F]
  [inst_2 : LineDeriv V E F],
  (∀ (r : R) (v : V) (x : E), LineDeriv.lineDerivOp (r • v) x = r • LineDeriv.lineDerivOp v x) →
    LineDerivLeftSMul R V E F
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constInsertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.DHashMap α fun x => Unit}
  (l : List α),
  m₁.Equiv m₂ → (Std.DHashMap.Const.insertManyIfNewUnit m₁ l).Equiv (Std.DHashMap.Const.insertManyIfNewUnit m₂ l)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.instContinuousEval : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [LocallyCompactPair A B], ContinuousEval (A →ₜ+ B) A B