mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.instInjectiveXExtend : ∀ {ι : 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.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (e : c.Embedding c') (K : HomologicalComplex C c)
  [∀ (i : ι), CategoryTheory.Injective (K.X i)] (i' : ι'), CategoryTheory.Injective ((K.extend e).X i')
-- Std.Time.DateTime
/-- The corresponding timestamp for the datetime.
 -/
Std.Time.DateTime.timestamp : Std.Time.DateTime → Std.Time.Timestamp
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_9 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.shiftRight rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_9 w n lhs rhs
-- Mathlib.Order.Minimal
maximal_subtype : ∀ {α : Type u_2} {P Q : α → Prop} [inst : LE α] {x : Subtype Q}, Maximal (fun x => P ↑x) x ↔ Maximal (P ⊓ Q) ↑x
-- Mathlib.Logic.Function.FiberPartition
/-- `y : Y` as a term of the type `Fiber.mk f y`  -/
Function.Fiber.mkSelf : {Y : Type u_2} → {Z : Type u_3} → (f : Y → Z) → (y : Y) → ↑↑(Function.Fiber.mk f y)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_iff_nonpos_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b : α},
  a + b ≤ a ↔ b ≤ 0
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.primrec₂_prec : Primrec₂ Nat.Partrec.Code.prec
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.mk.sizeOf_spec : ∀ (openClose : Bool) (change : Lean.Lsp.TextDocumentSyncKind) (willSave willSaveWaitUntil : Bool)
  (save? : Option Lean.Lsp.SaveOptions),
  sizeOf
      { openClose := openClose, change := change, willSave := willSave, willSaveWaitUntil := willSaveWaitUntil,
        save? := save? } =
    1 + sizeOf openClose + sizeOf change + sizeOf willSave + sizeOf willSaveWaitUntil + sizeOf save?
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- Two subsemirings are equal if they have the same elements.  -/
Subsemiring.ext : ∀ {R : Type u} [inst : NonAssocSemiring R] {S T : Subsemiring R}, (∀ (x : R), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.singleton_span_mem_normalizedFactors_of_mem_normalizedFactors`. -/
singleton_span_mem_normalizedFactors_of_mem_normalizedFactors : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] {a b : R},
  a ∈ UniqueFactorizationMonoid.normalizedFactors b →
    Ideal.span {a} ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {b})
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_coe_eq_top_iff_not_summable_coe : ∀ {α : Type u_1} {f : α → NNReal}, ∑' (a : α), ↑(f a) = ⊤ ↔ ¬Summable fun a => ↑(f a)
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofEq_rfl : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  {p : Submodule R M}, LinearEquiv.ofEq p p ⋯ = LinearEquiv.refl R ↥p
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.mem_iff_of_eqOnSource : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} {e e' : OpenPartialHomeomorph H H},
  e ≈ e' → (e ∈ G ↔ e' ∈ G)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.instCommRingSubtypeMemSubalgebraSubalgebra : (R : Type u_1) →
  [inst : CommRing R] →
    {A : Type u} →
      {B : Type u_2} →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra A B] →
                (D : Algebra.Smooth.DescentAux✝ A B) → CommRing ↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.isUnit_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → (IsUnit p ↔ p = 1)
-- Mathlib.Analysis.Seminorm
Seminorm.ball_bot : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {r : ℝ}
  (x : E), 0 < r → ⊥.ball x r = Set.univ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_eq_fallback : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  {fallback : β}, a ∉ m → m.getD a fallback = fallback
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.congr_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] {g' : β → α}, HasSumUniformlyOn f g s → Set.EqOn g g' s → HasSumUniformlyOn f g' s
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂ : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i₁ i₂ : D.J) (x : PUnit.{u + 1}),
  D.oneHypercover.p₂ x = CategoryTheory.CategoryStruct.comp (D.t i₁ i₂) (D.f i₂ i₁)
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ico a b).OrdConnected
-- Init.Data.Nat.Bitwise.Lemmas
/-- `eq_of_testBit_eq` allows proving two natural numbers are equal
if their bits are all equal.
 -/
Nat.eq_of_testBit_eq : ∀ {x y : ℕ}, (∀ (i : ℕ), x.testBit i = y.testBit i) → x = y
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.free_map : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y : TopCat} (f : X ⟶ Y),
  (TopModuleCat.free R).map f = TopModuleCat.freeMap R f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keys_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (t.get x ⋯))
        t.keys.attach).unattach
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom
        (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv))
-- Mathlib.RepresentationTheory.Submodule
Representation.invtSubmodule.bot_mem : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), ⊥ ∈ ρ.invtSubmodule
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.failedAssign.sizeOf_spec : sizeOf Lean.Meta.Simp.DischargeResult.failedAssign = 1
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.probabilitymeasure_of_probabilitymeasures_conv : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M) [MeasurableAdd₂ M]
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν],
  MeasureTheory.IsProbabilityMeasure (μ.conv ν)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.equiv_of_beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [LawfulBEq α]
  [inst_3 : BEq β] [LawfulBEq β], m₁.WF → m₂.WF → (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.le_def : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupSeminorm E}, p ≤ q ↔ ⇑p ≤ ⇑q
-- Mathlib.Data.PNat.Find
PNat.find_min : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) {m : ℕ+}, m < PNat.find h → ¬p m
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.instCreatesLimitsOfShapeForget : {J : Type w} →
  [inst : CategoryTheory.Category.{v_1, w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.Mon.forget C)
-- Mathlib.NumberTheory.SmoothNumbers
/-- The positive non-`k`-smooth (so "`k`-rough") numbers up to and including `N` as a `Finset`  -/
Nat.roughNumbersUpTo : ℕ → ℕ → Finset ℕ
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (obj : (X : Cᵒᵖ) → ModuleCat ↑(R.obj X)) →
        (map :
            {X Y : Cᵒᵖ} → (f : X ⟶ Y) → obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (obj Y)) →
          autoParam
              (∀ (X : Cᵒᵖ),
                map (CategoryTheory.CategoryStruct.id X) =
                  (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X)))
                          ⋯).inv.app
                    (obj X))
              PresheafOfModules.map_id._autoParam →
            autoParam
                (∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
                  map (CategoryTheory.CategoryStruct.comp f g) =
                    CategoryTheory.CategoryStruct.comp (map f)
                      (CategoryTheory.CategoryStruct.comp
                        ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (map g))
                        ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                                (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
                          (obj Z))))
                PresheafOfModules.map_comp._autoParam →
              PresheafOfModules R
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withoutMacroStackAtErr : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instIsScalarTower : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : SMul R S] [IsScalarTower R S A],
  IsScalarTower R S (MvPowerSeries σ A)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck.match_1.eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)) (h_2 : Unit → motive none),
  (match some c with
    | some c => h_1 c
    | none => h_2 ()) =
    h_1 c
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.lt.sizeOf_spec : sizeOf Lean.Elab.WF.GuessLex.GuessLexRel.lt = 1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.snd : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {F : Type u_9}
  [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → E × F},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => (f x).2) μ
-- Mathlib.Data.Int.Bitwise
Int.bit_coe_nat : ∀ (b : Bool) (n : ℕ), Int.bit b ↑n = ↑(Nat.bit b n)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_eq_mul_iff_eq_and_eq_of_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c d : α} [inst_1 : PartialOrder α] [PosMulStrictMono α]
  [MulPosStrictMono α], a ≤ b → c ≤ d → 0 < a → 0 < d → (a * c = b * d ↔ a = b ∧ c = d)
-- Mathlib.Order.Filter.Pointwise
Filter.pure_div : ∀ {α : Type u_2} [inst : Div α] {g : Filter α} {a : α}, pure a / g = Filter.map (fun x => a / x) g
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.Multifork.toSections_val : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  (c : CategoryTheory.Limits.Multifork I) (x : c.pt) (i : J.L),
  (c.toSections x).val i = (CategoryTheory.ConcreteCategory.hom (c.ι i)) x
-- Mathlib.Algebra.Ring.Equiv
/-- The proposition that the function preserves addition  -/
RingEquiv.map_add' : ∀ {R : Type u_7} {S : Type u_8} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (self : R ≃+* S)
  (x y : R), self.toFun (x + y) = self.toFun x + self.toFun y
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.dvd_iff_not_coprime : ∀ {p n : ℕ}, Nat.Prime p → (p ∣ n ↔ ¬p.Coprime n)
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainBotCoeff_le_chainLength : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  LieModule.chainBotCoeff (⇑α) β ≤ LieAlgebra.IsKilling.chainLength α β
-- Lean.MetavarContext
/-- Set the `BinderInfo` of an fvar. If the given metavariable is not declared or
the given fvar doesn't exist in its context, nothing happens.
 -/
Lean.MVarId.setFVarType : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → Lean.FVarId → Lean.Expr → m Unit
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev_lt : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.startPos}, p.prev h < p
-- Mathlib.CategoryTheory.Abelian.Images
/-- The canonical map from the abelian coimage to the abelian image.
In any abelian category this is an isomorphism.

Conversely, any additive category with kernels and cokernels and
in which this is always an isomorphism, is abelian.  -/
CategoryTheory.Abelian.coimageImageComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            [inst_3 : CategoryTheory.Limits.HasKernel f] →
              [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] →
                [inst_5 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] →
                  CategoryTheory.Abelian.coimage f ⟶ CategoryTheory.Abelian.image f
-- Mathlib.Data.List.Infix
List.map_inits : ∀ {α : Type u_1} {l : List α} {β : Type u_3} (g : α → β), (List.map g l).inits = List.map (List.map g) l.inits
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Submodule.cardQuot.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submodule R M),
  S.cardQuot = S.toAddSubgroup.index
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.IsRegular.mk : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} [toIsProper : h.IsProper], WellFounded h.AncestralRel → h.IsRegular
-- Std.Http.Internal.Char
/-- quoted-string body character class:
( qdtext / quoted-pair payload ) in ASCII-only mode.
 -/
Std.Http.Internal.Char.quotedStringChar : Char → Bool
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      if hkky : compare k ky = Ordering.lt then Std.DTreeMap.Internal.Impl.Const.getEntryGTD k l (ky, y)
      else Std.DTreeMap.Internal.Impl.Const.getEntryGT k r ⋯ ⋯
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₂_obj_obj_obj_obj : ∀ {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₂] {E : Type u_7} [inst_2 : CategoryTheory.Category.{v_7, u_7} E]
  {E' : Type u_8} [inst_3 : CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E')
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) (X_1 : C₁) (X_2 : C₂),
  (((CategoryTheory.Functor.postcompose₂.obj X).obj F).obj X_1).obj X_2 = X.obj ((F.obj X_1).obj X_2)
-- Mathlib.Order.MinMax
min_eq_right_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, min a b = b ↔ b ≤ a
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs_zero : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (N : LieSubmodule R L M)
  [inst_6 : LieModule R L M], LieSubmodule.ucs 0 N = N
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_indicator : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  {a₁ a₂ a₃ : ℝ}, a₂ ∈ Set.Icc a₁ a₃ → ∫ (x : ℝ) in a₁..a₃, {x | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ
-- Mathlib.Computability.EpsilonNFA
εNFA.pumping_lemma : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) [inst : Fintype σ] {x : List α},
  x ∈ M.accepts →
    Fintype.card (Set σ) ≤ x.length →
      ∃ a b c,
        x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * KStar.kstar {b} * {c} ≤ M.accepts
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_of_add_le_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] {a b c d : α}, a + b ≤ c → d ≤ b → a + d ≤ c
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instInhabitedOrigin.default : Lean.Meta.Origin
-- Mathlib.Data.Finset.Insert
/-- The equivalence between pi types on insert and the product.  -/
Finset.insertPiProdEquiv : {α : Type u_1} →
  [inst : DecidableEq α] →
    {s : Finset α} →
      (f : α → Type u_3) → {a : α} → a ∉ s → ((i : α) → i ∈ insert a s → f i) ≃ f a × ((i : α) → i ∈ s → f i)
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_lt_artanh : ∀ {x y : ℝ}, -1 < x → y < 1 → x < y → Real.artanh x < Real.artanh y
-- Lean.Parser
Lean.PrettyPrinter.Parenthesizer.ident.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.Single
ChainComplex.single₀.congr_simp : ∀ (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V], ChainComplex.single₀ V = ChainComplex.single₀ V
-- Mathlib.Order.Category.BddDistLat
BddDistLat.instDistribLatticeCarrier : (X : BddDistLat) → DistribLattice ↑X.toDistLat
-- Aesop.Script.SpecificTactics
Aesop.tryClearManyS : Lean.MVarId → Array Lean.FVarId → Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)
-- Init.Data.SInt.Lemmas
Int32.le_trans : ∀ {a b c : Int32}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.code_is_ok : ∀ (c : Turing.ToPartrec.Code), c.Ok
-- Mathlib.Logic.Equiv.Defs
/-- A family of equivalences `Π a, β₁ a ≃ β₂ a` generates an equivalence between `Σ' a, β₁ a` and
`Σ' a, β₂ a`.  -/
Equiv.psigmaCongrRight : {α : Sort u} → {β₁ : α → Sort u_1} → {β₂ : α → Sort u_2} → ((a : α) → β₁ a ≃ β₂ a) → (a : α) ×' β₁ a ≃ (a : α) ×' β₂ a
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The pairing is continuous in the left argument.

Note that since `𝓢(E, F)` is not a normed space, uncurried and curried continuity do not
coincide.  -/
SchwartzMap.pairing_continuous_left : ∀ {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedAddCommGroup D]
  [inst_7 : NormedSpace ℝ D] [inst_8 : NormedAddCommGroup G] [inst_9 : NormedSpace ℝ G] [inst_10 : NormedSpace 𝕜 F]
  [inst_11 : NormedSpace 𝕜 E] [inst_12 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (g : SchwartzMap D F),
  Continuous fun x => ((SchwartzMap.pairing B) x) g
-- Lean.Data.KVMap
Lean.DataValue.ofString.sizeOf_spec : ∀ (v : String), sizeOf (Lean.DataValue.ofString v) = 1 + sizeOf v
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- Via `S.rightHomologyι : S.rightHomology ⟶ S.opcycles`, the object `S.rightHomology` identifies
to the kernel of `S.fromOpcycles : S.opcycles ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.rightHomologyIsKernel : {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.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.rightHomologyι ⋯)
-- Lean.Meta.Constructions.CtorIdx
_private.Lean.Meta.Constructions.CtorIdx.0.Lean.genCtorIdx : Lean.Option Bool
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
exteriorPower.pairingDual_ιMulti_ιMulti : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  (f : Fin n → Module.Dual R M) (v : Fin n → M),
  ((exteriorPower.pairingDual R M n) ((exteriorPower.ιMulti R n) f)) ((exteriorPower.ιMulti R n) v) =
    (Matrix.of fun i j => (f j) (v i)).det
-- Mathlib.CategoryTheory.Generator.Indization
CategoryTheory.Ind.isSeparator_range_yoneda : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteColimits C], CategoryTheory.IsSeparator (∐ CategoryTheory.Ind.yoneda.obj)