mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finsupp.Indicator
Finsupp.indicator_singleton : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (a : ι) (f : (j : ι) → j ∈ {a} → α),
  Finsupp.indicator {a} f = fun₀ | a => f a ⋯
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.lt_iff : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  {x y : α},
  Std.PRange.UpwardEnumerable.LT x y ↔ Std.PRange.UpwardEnumerable.LT (HasModel.encode✝ x) (HasModel.encode✝ y)
-- Mathlib.Data.Nat.Log
Nat.clog_of_right_le_one : ∀ {n : ℕ}, n ≤ 1 → ∀ (b : ℕ), Nat.clog b n = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.ord_cof_le : ∀ (o : Ordinal.{u_1}), o.cof.ord ≤ o
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.coe_basis : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε), ⇑h.basis = e
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformation : Type
-- Lean.Meta.GetUnfoldableConst
/-- Look up a constant name, returning the `ConstantInfo`
if it is a def/theorem that should be unfolded at the current reducibility settings,
or `none` otherwise.

This is part of the implementation of `whnf`.
External users wanting to look up names should be using `Lean.getConstInfo`.
 -/
Lean.Meta.getUnfoldableConst? : Lean.Name → Lean.MetaM (Option Lean.ConstantInfo)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The multifork `presheafObjMultifork` is a limit.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjIsLimit : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                    [inst_3 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                      (G₀ : CategoryTheory.Sheaf J₀ A) →
                        (X : C) →
                          CategoryTheory.Limits.IsLimit
                            (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjMultifork data G₀ X)
-- Mathlib.Algebra.Ring.Hom.Defs
/-- The proposition that the function preserves 0  -/
RingHom.map_zero' : ∀ {α : Type u_5} {β : Type u_6} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (self : α →+* β),
  (↑↑self).toFun 0 = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_replaceEntry_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k},
  (k == a) = false →
    Std.Internal.List.getEntry? a (Std.Internal.List.replaceEntry k v l) = Std.Internal.List.getEntry? a l
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkMVarS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → Lean.MVarId → m Lean.Expr
-- Lean.Meta.Tactic.Grind.AC.PP
_private.Lean.Meta.Tactic.Grind.AC.PP.0.Lean.Meta.Grind.AC.ppStruct? : Lean.Meta.Grind.AC.M✝ (Option Lean.MessageData)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
KaehlerDifferential.cotangentComplexBaseChange.congr_simp : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] (P : Type u_2) (A : Type u_3)
  [inst_2 : CommRing P] [inst_3 : CommRing A] [inst_4 : Algebra P S] [inst_5 : Algebra P A] [inst_6 : Algebra R P]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower P S A],
  KaehlerDifferential.cotangentComplexBaseChange R S P A = KaehlerDifferential.cotangentComplexBaseChange R S P A
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.opOpEquivalence_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.opOpEquivalence C).inverse = CategoryTheory.opOp C
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_of_card_mul_and_disjoint : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [Finite G],
  Nat.card ↥H * Nat.card ↥K = Nat.card G → Disjoint H K → H.IsComplement' K
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.eq_append_of_dropPrefix?_string_eq_some : ∀ {s pat : String} {res : String.Slice}, s.dropPrefix? pat = some res → s = pat ++ res.copy
-- Init.Data.SInt.Lemmas
Int8.ne_of_lt : ∀ {a b : Int8}, a < b → a ≠ b
-- Mathlib.Data.Multiset.Count
Multiset.count_cons_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), Multiset.count a (a ::ₘ s) = Multiset.count a s + 1
-- Mathlib.RepresentationTheory.Maschke
LinearMap.sumOfConjugates.congr_simp : ∀ {k : Type u_1} [inst : CommRing k] (G : Type u_2) [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π π_1 : W →ₗ[k] V),
  π = π_1 → ∀ [inst_10 : Fintype G], LinearMap.sumOfConjugates G π = LinearMap.sumOfConjugates G π_1
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.fvar.injEq : ∀ (moduleName id moduleName_1 id_1 : String),
  (Lean.Lsp.RefIdent.fvar moduleName id = Lean.Lsp.RefIdent.fvar moduleName_1 id_1) =
    (moduleName = moduleName_1 ∧ id = id_1)
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_zmodeq : ∀ (b : ℤ) (k : ℕ) (L : List ℕ), Nat.ofDigits b L ≡ Nat.ofDigits (b % ↑k) L [ZMOD ↑k]
-- Mathlib.Topology.Order.LowerUpperTopology
OrderDual.instIsUpper : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α], Topology.IsUpper αᵒᵈ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Special case of `integral_deriv_mul_eq_sub_of_hasDeriv_right` where the functions have a
derivative at the endpoints.  -/
intervalIntegral.integral_deriv_mul_eq_sub : ∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  (∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x) →
      IntervalIntegrable u' MeasureTheory.volume a b →
        IntervalIntegrable v' MeasureTheory.volume a b →
          ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
-- Init.Grind.Tactics
/-- `grind_order` solves simple goals about partial orders and linear orders.

It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `order` solver.
Please use `grind` instead if you need additional capabilities.
 -/
Lean.Parser.Tactic.grind_order : Lean.ParserDescr
-- Batteries.Lean.EStateM
EStateM.run_getModify : ∀ {σ ε : Type u_1} {s : σ} (f : σ → σ), (getModify f).run s = EStateM.Result.ok s (f s)
-- Init.Data.Array.DecidableEq
Array.instDecidableEmpEqImpl : {α : Type u_1} → (xs : Array α) → Decidable (#[] = xs)
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mem_toSubmodule : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) {x : L}, x ∈ L'.toSubmodule ↔ x ∈ L'
-- Mathlib.CategoryTheory.Types.Basic
_private.Mathlib.CategoryTheory.Types.Basic.0.TypeCat.Hom.mk.injEq : ∀ {X Y : Type u} (hom' hom'_1 : TypeCat.Fun X Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.contains t.maxKey! = true
-- Mathlib.Order.Filter.Extr
/-- `IsExtrOn f s a` means `IsMinOn f s a` or `IsMaxOn f s a`  -/
IsExtrOn : {α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Set α → α → Prop
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mapRange_smul : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {N : Type u_4} [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R : Type u_5} [inst_4 : Semiring R]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : ContinuousConstSMul R M] [inst_8 : ContinuousConstSMul R N]
  {v : MeasureTheory.VectorMeasure α M} {f : M →ₗ[R] N} (hf : Continuous ⇑f) {c : R},
  (c • v).mapRange f.toAddMonoidHom hf = c • v.mapRange f.toAddMonoidHom hf
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_inj : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {x y : (i : Fin n) → α (p.succAbove i)} {xₚ yₚ : α p},
  p.insertNth xₚ x = p.insertNth yₚ y ↔ xₚ = yₚ ∧ x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The type of objects for the diagram indexing a (co)equalizer.  -/
CategoryTheory.Limits.WalkingParallelPair : Type
-- Mathlib.Topology.Neighborhoods
closure_sdiff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, closure s \ closure t ⊆ closure (s \ t)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
CFC.nnrpow_le_nnrpow : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : NNReal},
  p ∈ Set.Icc 0 1 → ∀ {a b : A}, a ≤ b → a ^ p ≤ b ^ p
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- Using `standardσ_simplicialInsert`, we can prove that every morphism satisfying `P_σ` is equal
to some `standardσ` for some admissible list of indices.  -/
SimplexCategoryGenRel.exists_normal_form_P_σ : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y),
  SimplexCategoryGenRel.P_σ f →
    ∃ L m b,
      ∃ (h₁ : SimplexCategoryGenRel.mk m = y) (h₂ : x = SimplexCategoryGenRel.mk (m + b)) (h : L.length = b),
        SimplexCategoryGenRel.IsAdmissible m L ∧ f = SimplexCategoryGenRel.standardσ L ⋯
-- Mathlib.Order.CompleteLattice.Basic
inf_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α}, a ⊓ ⨅ x, f x = ⨅ x, a ⊓ f x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_eq_getKey! : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {a : α} {h : m.contains a = true}, m.getKey a h = m.getKey! a
-- Lean.Meta.Tactic.Simp.Attr
Lean.Meta.getSEvalTheorems : Lean.CoreM Lean.Meta.SimpTheorems
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprSyntax_mathlib.toExpr : Lean.Syntax → Lean.Expr
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.ofHom_id : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : CommRing X] [inst_2 : Bialgebra R X],
  CommBialgCat.ofHom (BialgHom.id R X) = CategoryTheory.CategoryStruct.id (CommBialgCat.of R X)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.map : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat} (j j' : J) (f : j ⟶ j')
  (x : ↑(F.obj j)),
  MonCat.Colimits.Relation F (MonCat.Colimits.Prequotient.of j' ((CategoryTheory.ConcreteCategory.hom (F.map f)) x))
    (MonCat.Colimits.Prequotient.of j x)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.LaxBraided] [inst_7 : F'.LaxBraided] (e : F ≅ F')
  [inst_8 : CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.CommMon C),
  ((CategoryTheory.Functor.mapCommMonNatIso e).hom.app X).hom.hom = e.hom.app X.X
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α] {k : α}
  {v : β}, (k, v) ∈ Std.DHashMap.Const.toList m ↔ Std.DHashMap.Const.get? m k = some v
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.isGLB_ciInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → IsGLB (Set.range f) (⨅ i, f i)
-- Lean.Meta.HaveTelescope
/-- Previous `have`s that the value of this `have` depends on, as indices into `HaveTelescopeInfo.haveInfo`.
Used in `computeFixedUsed` to compute used `have`s.  -/
Lean.Meta.HaveInfo.valueBackDeps : Lean.Meta.HaveInfo → Std.HashSet ℕ
-- Std.Do.SPred.SPred
/-- Existential quantifier in `SPred`.  -/
Std.Do.SPred.exists : {α : Sort u} → {σs : List (Type v)} → (α → Std.Do.SPred σs) → Std.Do.SPred σs
-- Mathlib.Order.Lattice
/-- The binary supremum, used to derive `Max α`  -/
SemilatticeSup.sup : {α : Type u} → [self : SemilatticeSup α] → α → α → α
-- Mathlib.Topology.Algebra.GroupWithZero
/-- Left multiplication by a nonzero element in a `GroupWithZero` with continuous multiplication
is a homeomorphism of the underlying type.  -/
Homeomorph.mulLeft₀ : {α : Type u_1} →
  [inst : TopologicalSpace α] → [inst_1 : GroupWithZero α] → [SeparatelyContinuousMul α] → (c : α) → c ≠ 0 → α ≃ₜ α
-- Init.Data.Int.Gcd
Int.gcd_left_comm : ∀ (a b c : ℤ), a.gcd ↑(b.gcd c) = b.gcd ↑(a.gcd c)
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.algHom_ext_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {S : Type u_5} [Finite ι] [inst_4 : DecidableEq ι] [inst_5 : Semiring S]
  [inst_6 : Algebra R S] {f g : (PiTensorProduct R fun i => A i) →ₐ[R] S},
  f = g ↔ ∀ (i : ι), f.comp (PiTensorProduct.singleAlgHom i) = g.comp (PiTensorProduct.singleAlgHom i)
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- The basis constructed by `unitsSMul` has vectors given by a diagonal matrix.  -/
Module.Basis.toMatrix_unitsSMul : ∀ {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂]
  [inst_3 : DecidableEq ι] (e : Module.Basis ι R₂ M₂) (w : ι → R₂ˣ),
  e.toMatrix ⇑(e.unitsSMul w) = Matrix.diagonal (Units.val ∘ w)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.instFunLikeContinuousHom : {α : Type u_2} →
  {β : Type u_3} → [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → FunLike (α →𝒄 β) α β
-- Mathlib.RingTheory.PrincipalIdealDomain
Ideal.irreducible_iff_isMaximal_span_singleton : ∀ {R : Type u} [inst : CommSemiring R] [IsPrincipalIdealRing R] [IsDomain R] {p : R},
  p ≠ 0 → (Irreducible p ↔ Ideal.IsMaximal (R ∙ p))
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.desc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α α_1 : CochainComplex.HomComplex.Cochain K M 0) (e_α : α = α_1) (β β_1 : CochainComplex.HomComplex.Cocycle L M 1)
  (e_β : β = β_1) (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0),
  CochainComplex.mappingCocone.desc φ α β hαβ = CochainComplex.mappingCocone.desc φ α_1 β_1 ⋯
-- Lean.Elab.DefView
/-- Universe level parameter names explicitly provided by the user.  -/
Lean.Elab.DefViewElabHeaderData.levelNames : Lean.Elab.DefViewElabHeaderData → List Lean.Name
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroUSizeUintNumBits : Lean.Grind.ToInt.Zero USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology],
  CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.CategoryStruct.id S) =
    CategoryTheory.CategoryStruct.id S.opcycles
-- Mathlib.LinearAlgebra.RootSystem.Reduced
/-- See also `RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent`.  -/
RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent : ∀ {ι : 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) {i j : ι} [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M],
  P.coxeterWeight i j = 4 ↔ ¬LinearIndependent R ![P.root i, P.root j]
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMk_X₁_carrier : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : Type v} [inst_1 : AddCommGroup X₁] [inst_2 : AddCommGroup X₂]
  [inst_3 : AddCommGroup X₃] [inst_4 : Module R X₁] [inst_5 : Module R X₂] [inst_6 : Module R X₃] (f : X₁ →ₗ[R] X₂)
  (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0), ↑(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₁ = X₁
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.getElem_toList_eq : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least).get ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- `f : X ⟶ Y` is right homotopic to itself relative to any pre-path object.  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy.refl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} → (P : HomotopicalAlgebra.PrepathObject Y) → {X : C} → (f : X ⟶ Y) → P.RightHomotopy f f
-- Mathlib.Data.Stream.Init
Stream'.drop_succ : ∀ {α : Type u} (n : ℕ) (s : Stream' α), Stream'.drop n.succ s = Stream'.drop n s.tail
-- Init.Data.List.Lemmas
List.map_tail : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, List.map f l.tail = (List.map f l).tail
-- Mathlib.Topology.Irreducible
PreirreducibleSpace.of_forall_nonempty_inter : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (∀ ⦃U V : Set X⦄, IsOpen U → IsOpen V → U.Nonempty → V.Nonempty → (U ∩ V).Nonempty) → PreirreducibleSpace X
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.parallelPairObj_one : ∀ {C : Type u} {X Y : C},
  CategoryTheory.Limits.parallelPair.parallelPairObj X Y CategoryTheory.Limits.WalkingParallelPair.one = Y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.mk : String →
  Lean.Lsp.SymbolKind →
    Option (Array Lean.Lsp.SymbolTag) →
      Option String →
        Lean.Lsp.DocumentUri → Lean.Lsp.Range → Lean.Lsp.Range → Option Lean.Json → Lean.Lsp.CallHierarchyItem
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDecls.mk.inj : ∀ {decls decls_1 : Lean.Meta.DiscrTree Mathlib.Meta.FunProp.FunPropDecl},
  { decls := decls } = { decls := decls_1 } → decls = decls_1
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.mk.inj : ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {I₁₂ : Type u_11}
  {p : I₁ × I₂ → I₁₂} {q : I₁₂ × I₃ → J} {hpq : ∀ (i : I₁ × I₂ × I₃), q (p (i.1, i.2.1), i.2.2) = r i}
  {I₁₂_1 : Type u_11} {p_1 : I₁ × I₂ → I₁₂_1} {q_1 : I₁₂_1 × I₃ → J}
  {hpq_1 : ∀ (i : I₁ × I₂ × I₃), q_1 (p_1 (i.1, i.2.1), i.2.2) = r i},
  { I₁₂ := I₁₂, p := p, q := q, hpq := hpq } = { I₁₂ := I₁₂_1, p := p_1, q := q_1, hpq := hpq_1 } →
    I₁₂ = I₁₂_1 ∧ p ≍ p_1 ∧ q ≍ q_1
-- Mathlib.Order.Filter.Map
Filter.pure_sets : ∀ {α : Type u_1} (a : α), (pure a).sets = {s | a ∈ s}
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- See also `Matrix.mulVec_injective_iff_isUnit` when working over a field.  -/
Matrix.mulVec_injective_of_det_mem_nonZeroDivisors : ∀ {m : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m R},
  M.det ∈ nonZeroDivisors R → Function.Injective M.mulVec
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.m_le_card_of_mem_chunk_parts : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {s : Finset α},
  s ∈ (SzemerediRegularity.chunk hP G ε hU).parts → Fintype.card α / SzemerediRegularity.stepBound P.parts.card ≤ s.card
-- Mathlib.CategoryTheory.Grothendieck
/-- The inverse functor to build the equivalence `compAsSmallFunctorEquivalence`.  -/
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C CategoryTheory.Cat) →
      CategoryTheory.Functor (CategoryTheory.Grothendieck F)
        (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor))
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.instNatCast : {α : Type u} → [NatCast α] → NatCast (WithBot α)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.prod_div_prod_comm : ∀ {α : Type u_2} {β : Type u_3} [inst : Div α] [inst_1 : Div β] (s₁ s₂ : Set α) (t₁ t₂ : Set β),
  s₁ ×ˢ t₁ / s₂ ×ˢ t₂ = (s₁ / s₂) ×ˢ (t₁ / t₂)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_eq_getLsbD : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i))
-- Mathlib.NumberTheory.LucasLehmer
/-- The Mersenne numbers, 2^p - 1.  -/
mersenne : ℕ → ℕ
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_pow : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [inst : Pow β M] (c : M) (f : α → β),
  (UniformOnFun.ofFun 𝔖) (f ^ c) = (UniformOnFun.ofFun 𝔖) f ^ c
-- Mathlib.Algebra.Group.Subgroup.Even
Subsemigroup.mem_square : ∀ {S : Type u_1} [inst : CommSemigroup S] {a : S}, a ∈ Subsemigroup.square S ↔ IsSquare a
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The torsion submodule of the torsion submodule (viewed as a module) is the full
torsion module.  -/
Submodule.torsion_torsion_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Submodule.torsion R ↥(Submodule.torsion R M) = ⊤
-- Mathlib.Order.InitialSeg
/-- A principal segment embedding is in particular an initial segment embedding.  -/
PrincipalSeg.hasCoeInitialSeg : {α : Type u_1} →
  {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → [IsTrans β s] → Coe (PrincipalSeg r s) (InitialSeg r s)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.simplifyResultingUniverse.simp : (Lean.LevelMap ℕ → Lean.LevelMap ℕ) →
  (Lean.LevelMap ℕ → Lean.Level) →
    (Lean.LevelMap ℕ → Lean.Level → ℕ → Lean.LevelMap ℕ) → Lean.Level → ℕ → Lean.LevelMap ℕ → Lean.LevelMap ℕ
-- Mathlib.Analysis.Convex.Function
/-- Right translation preserves strict convexity.  -/
StrictConvexOn.translate_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCancelCommMonoid E] [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E]
  [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β},
  StrictConvexOn 𝕜 s f → ∀ (c : E), StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
-- Mathlib.Order.Closure
/-- Every element is less than its closure. This property is sometimes referred to as extensivity or
inflationarity.  -/
LowerAdjoint.le_closure : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α),
  x ≤ u (l.toFun x)
-- Mathlib.Data.Int.Order.Basic
Int.mul_pos_iff : ∀ {a b : ℤ}, 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstDivNat : Lean.Expr → Lean.MetaM Bool