mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to an `AddGroupSeminorm`.  -/
GroupSeminorm.instSMul : {R : Type u_1} →
  {E : Type u_3} →
    [inst : Group E] →
      [inst_1 : SMul R ℝ] → [inst_2 : SMul R NNReal] → [IsScalarTower R NNReal ℝ] → SMul R (GroupSeminorm E)
-- Mathlib.Topology.Algebra.IsOpenUnits
/-- We say that a topological monoid `M` has open units if `Mˣ` is open in `M` and
has the subspace topology (i.e. inverse is continuous).

Typical examples include monoids with discrete topology, topological groups (or fields),
and rings `R` equipped with the `I`-adic topology where `I ≤ J(R)`.
 -/
IsOpenUnits : (M : Type u_1) → [Monoid M] → [TopologicalSpace M] → Prop
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_true_of_eq_clzAuxRec_of_ne_zero : ∀ {w n : ℕ} {x : BitVec w},
  ¬x = 0#w → (∀ (i : ℕ), n < i → x.getLsbD i = false) → x.getLsbD (w - 1 - (x.clzAuxRec n).toNat) = true
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.existsUnique_toNπ : ∀ {X : SSet} {x : X.S} {y : X.N},
  x.toN = y → ∃! f, CategoryTheory.Epi f ∧ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`.  -/
UpperSemicontinuousWithinAt.add' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] {f g : α → γ},
  UpperSemicontinuousWithinAt f s x →
    UpperSemicontinuousWithinAt g s x →
      ContinuousAt (fun p => p.1 + p.2) (f x, g x) → UpperSemicontinuousWithinAt (fun z => f z + g z) s x
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.homMk_eq_id_iff : ∀ {X : FintypeCat} (f : X.obj → X.obj), FintypeCat.homMk f = CategoryTheory.CategoryStruct.id X ↔ f = id
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.dom_fg_iff_cod_fg : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {N : Type u_1} [inst_1 : L.Structure N]
  (f : L.PartialEquiv M N), f.dom.FG ↔ f.cod.FG
-- Lean.Level
_private.Lean.Level.0.Lean.mkLevelIMaxCore : Lean.Level → Lean.Level → (Unit → Lean.Level) → Lean.Level
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
/-- The pseudofunctor from `LocallyDiscrete CommRingCatᵒᵖ` to `Cat` which sends
a commutative ring `R` to its category of modules. The functoriality is given by
the restriction of scalars.  -/
CommRingCat.moduleCatRestrictScalarsPseudofunctor : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ) CategoryTheory.Cat
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_mod_of_dvd : ∀ (a b : UInt64), b.toNat ∣ 4294967296 → (a % b).toUInt32 = a.toUInt32 % b.toUInt32
-- Init.Core
iff_not_self : ∀ {a : Prop}, ¬(a ↔ ¬a)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.isHomotopyInvariant_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (HP : TopPair.HomologyPretheory C c),
  TopPair.HomologyPretheory.isHomotopyInvariant C c HP ↔ HP.IsHomotopyInvariant
-- Init.Sym.Lemmas
Lean.Sym.Int.eq_eq_false : ∀ (a b : ℤ), decide (a = b) = false → (a = b) = False
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleDocumentSymbol.toDocumentSymbols.popStack : Lean.FileMap →
  Lean.Syntax →
    List Lean.Syntax →
      ℕ →
        Array Lean.Lsp.DocumentSymbol →
          List Lean.Server.FileWorker.NamespaceEntry → Lean.Server.RequestM (Array Lean.Lsp.DocumentSymbol)
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Complex.hasDerivAt_Gamma_nat : ∀ (n : ℕ), HasDerivAt Complex.Gamma (↑n.factorial * (-↑Real.eulerMascheroniConstant + ↑(harmonic n))) (↑n + 1)
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso_inv : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0),
  (CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).inv =
    CategoryTheory.CategoryStruct.comp (e.inv.app (Y a.2))
      ((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).inv).app (Y a.2))
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y) {F : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F] (x_1 : carrier (Y.presheaf.stalk ((TopCat.Hom.hom f.base) y))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) x_1) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y)) x_1)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.toUnfoldThms.injEq : ∀ (a : Lean.Name) (a_1 : Array Lean.Name) (a_2 : Lean.Name) (a_3 : Array Lean.Name),
  (Lean.Meta.SimpEntry.toUnfoldThms a a_1 = Lean.Meta.SimpEntry.toUnfoldThms a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_add : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r₁ r₂ : k),
  AffineMap.homothety c (r₁ + r₂) = r₁ • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.homothety c r₂
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_withDensity_eq_integral_smul₀ : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {f : X → NNReal},
  AEMeasurable f μ → ∀ (g : X → E), (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ
-- Std.Http.Data.Headers.Basic
/-- Validates the chunked placement rules for the Transfer Encoding header. Returns `false` if the
encoding list violates the constraints.

Reference: https://www.rfc-editor.org/rfc/rfc9112#section-6.1
 -/
Std.Http.Header.TransferEncoding.Validate : Array String → Bool
-- Mathlib.Data.Nat.Nth
Nat.count_nth_zero : ∀ (p : ℕ → Prop) [inst : DecidablePred p], Nat.count p (Nat.nth p 0) = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.inl_iso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {Z : D} (h : CategoryTheory.Limits.pushout (G.map f) (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inl f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (G.map f) (G.map g)) h
-- Mathlib.Algebra.Group.Action.Option
Option.vadd_none : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] (a : M), a +ᵥ none = none
-- Mathlib.Analysis.Convex.Basic
Convex_subadditive_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : LinearOrder 𝕜]
  [IsOrderedRing 𝕜] [inst_4 : SMul 𝕜 E] {f : E → 𝕜},
  (∀ (x y : E), f (x + y) ≤ f x + f y) →
    (∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x) → ∀ (B : 𝕜), Convex 𝕜 {x | f x ≤ B}
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- Set of edges incident to a given vertex, aka incidence set.  -/
SimpleGraph.incidenceSet : {V : Type u} → SimpleGraph V → V → Set (Sym2 V)
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The `p`-adic valuation on `ℚ_[p]`, as a `Valuation`, bundled `Padic.valuation`.  -/
Padic.mulValuation : {p : ℕ} → [hp : Fact (Nat.Prime p)] → Valuation ℚ_[p] (WithZero (Multiplicative ℤ))
-- Mathlib.AlgebraicTopology.DoldKan.Projections
/-- For each `q`, `Q q` is a natural transformation.  -/
AlgebraicTopology.DoldKan.natTransQ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      ℕ → (AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.LHom.coe_substructureReduct : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {L' : FirstOrder.Language} [inst_1 : L'.Structure M]
  (φ : L →ᴸ L') [inst_2 : φ.IsExpansionOn M] {S : L'.Substructure M}, ↑(φ.substructureReduct S) = ↑S
-- Mathlib.Data.Part
Part.toOption.congr_simp : ∀ {α : Type u_1} (o o_1 : Part α),
  o = o_1 → ∀ {inst : Decidable o.Dom} [inst_1 : Decidable o_1.Dom], o.toOption = o_1.toOption
-- Mathlib.Data.Holor
Holor.instAddSemigroup : {α : Type} → {ds : List ℕ} → [AddSemigroup α] → AddSemigroup (Holor α ds)
-- Mathlib.Tactic.Widget.CommDiag
/-- Construct a commutative diagram from a Penrose `sub`stance program and expressions `embeds` to
display as labels in the diagram.  -/
Mathlib.Tactic.Widget.mkCommDiag : String → Mathlib.Tactic.Widget.ExprEmbeds → Lean.MetaM ProofWidgets.Html
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.inter_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∩ t₂).Equiv (t₃ ∩ t₄)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `AEMeasurable.inv` -/
AEMeasurable.fun_inv : ∀ {G : Type u_2} {α : Type u_3} [inst : Inv G] [inst_1 : MeasurableSpace G] [MeasurableInv G] {m : MeasurableSpace α}
  {f : α → G} {μ : MeasureTheory.Measure α}, AEMeasurable f μ → AEMeasurable (fun i => (f i)⁻¹) μ
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instIsCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsCancelAdd α], IsCancelAdd (Colex α)
-- Init.Data.Int.OfNat
Nat.ToInt.div_congr : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a / b) = a' / b'
-- Init.Prelude
/-- Add a new macro scope to the name `n`.  -/
Lean.Macro.addMacroScope : Lean.Name → Lean.MacroM Lean.Name
-- Init.Data.List.ToArray
List.back_toArray : ∀ {α : Type u_1} (l : List α) (h : 0 < l.toArray.size), l.toArray.back h = l.getLast ⋯
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map.eq_1 : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ),
  groupHomology.map f φ n = HomologicalComplex.homologyMap (groupHomology.chainsMap f φ) n
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *non-unital ⋆-algebra homomorphism* is a non-unital algebra homomorphism between
non-unital `R`-algebras `A` and `B` equipped with a `star` operation, and this homomorphism is
also `star`-preserving.  -/
NonUnitalStarAlgHom : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [DistribMulAction R A] →
            [Star A] → [inst_4 : NonUnitalNonAssocSemiring B] → [DistribMulAction R B] → [Star B] → Type (max u_2 u_3)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsThetaOTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsThetaTVS 𝕜 l) (Asymptotics.IsThetaTVS 𝕜 l)
                                  (Asymptotics.IsThetaTVS 𝕜 l)
-- Mathlib.Data.Finset.Max
Finset.max'_eq_iff : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) (a : α), s.max' H = a ↔ a ∈ s ∧ ∀ b ∈ s, b ≤ a
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- A map `f : α → β` is called a *measurable embedding* if it is injective, measurable, and sends
measurable sets to measurable sets. The latter assumption can be replaced with “`f` has measurable
inverse `g : Set.range f → α`”, see `MeasurableEmbedding.measurable_rangeSplitting`,
`MeasurableEmbedding.of_measurable_inverse_range`, and
`MeasurableEmbedding.of_measurable_inverse`.

One more interpretation: `f` is a measurable embedding if it defines a measurable equivalence to its
range and the range is a measurable set. One implication is formalized as
`MeasurableEmbedding.equivRange`; the other one follows from
`MeasurableEquiv.measurableEmbedding`, `MeasurableEmbedding.subtype_coe`, and
`MeasurableEmbedding.comp`.  -/
MeasurableEmbedding : {α : Type u_1} → {β : Type u_2} → [MeasurableSpace α] → [MeasurableSpace β] → (α → β) → Prop
-- Mathlib.Algebra.Module.Injective
Module.Baer.instMinExtensionOf : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → (i : M →ₗ[R] N) → (f : M →ₗ[R] Q) → Min (Module.Baer.ExtensionOf i f)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_def : ∀ (a b : Ordinal.{u_4}), a % b = a - b * (a / b)
-- Mathlib.Data.List.PeriodicityLemma
/-- This is the equivalent definition of `HasPeriod w p` by indices.  -/
List.hasPeriod_iff_getElem? : ∀ {α : Type u_1} {p : ℕ} {w : List α}, w.HasPeriod p ↔ ∀ i < w.length - p, w[i]? = w[i + p]?
-- Mathlib.LinearAlgebra.Dual.BaseChange
IsBaseChange.toDual_comp_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) (f : Module.Dual R V)
  (v : V), (ibc.toDual f) (j v) = (algebraMap R A) (f v)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Build an isomorphism in the category `AddMonCat` from
an `AddEquiv` between `AddMonoid`s.  -/
AddEquiv.toAddMonCatIso : {X Y : Type u} → [inst : AddMonoid X] → [inst_1 : AddMonoid Y] → X ≃+ Y → (AddMonCat.of X ≅ AddMonCat.of Y)
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instMonoidWithZero : {α : Type u_1} → [MonoidWithZero α] → MonoidWithZero αᵒᵈ
-- Mathlib.Data.Sign.Defs
SignType.coe_neg_one : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Neg α], ↑(-1) = -1
-- Lean.Meta.Sym.SymM
/-- Cache for `inferType` results, keyed by pointer equality.
`SymM` uses a fixed configuration, so we can use a simpler key than `MetaM`.
Remark: type inference is a bottleneck on `Meta.Tactic.Simp` simplifier.
 -/
Lean.Meta.Sym.State.inferType : Lean.Meta.Sym.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.addHom_ext'_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {N : Type u_8} [inst_1 : AddZeroClass N]
  {f g : AddMonoidAlgebra R M →+ N},
  f = g ↔ ∀ (m : M), f.comp (AddMonoidAlgebra.singleAddHom m) = g.comp (AddMonoidAlgebra.singleAddHom m)
-- Mathlib.Analysis.Convex.Between
/-- The segment of points weakly between `x` and `y`. When convexity is refactored to support
abstract affine combination spaces, this will no longer need to be a separate definition from
`segment`. However, lemmas involving `+ᵥ` or `-ᵥ` will still be relevant after such a
refactoring, as distinct from versions involving `+` or `-` in a module.  -/
affineSegment : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring R] → [PartialOrder R] → [inst_2 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → P → P → Set P
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.comp_add_assoc : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y Z : C} {X' Y' Z' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y')
  (eZ : L.obj Z ≅ Z') (f : X' ⟶ Y') (g₁ g₂ : Y' ⟶ Z') {Z_1 : D} (h : Z' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add W eY eZ g₁ g₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Localization.Preadditive.add W eX eZ (CategoryTheory.CategoryStruct.comp f g₁)
        (CategoryTheory.CategoryStruct.comp f g₂))
      h
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Distance as a nonnegative real number.  -/
PseudoMetricSpace.toNNDist : {α : Type u} → [PseudoMetricSpace α] → NNDist α
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Parameters of caller (including fixed prefix)  -/
Lean.Elab.WF.GuessLex.RecCallWithContext.params : Lean.Elab.WF.GuessLex.RecCallWithContext → Array Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.starGraph.eq_1 : ∀ {V : Type u_1} (r : V), SimpleGraph.starGraph r = SimpleGraph.fromRel fun v x => v = r
-- Batteries.Tactic.PrintPrefix
_private.Batteries.Tactic.PrintPrefix.0.Batteries.Tactic.instEvalExprPrintPrefixConfig.evalExpr : Lean.Expr → Lean.MetaM Batteries.Tactic.PrintPrefixConfig
-- Lean.InternalExceptionId
Lean.InternalExceptionId.idx : Lean.InternalExceptionId → ℕ
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int8.intCast : IntCast Int8
-- Mathlib.Data.Multiset.Fintype
Multiset.map_univ_coeEmbedding : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Finset.map m.coeEmbedding Finset.univ = m.toEnumFinset
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- The union of all bounded set is the whole space.  -/
Bornology.sUnion_isVonNBounded_eq_univ : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E], ⋃₀ Set.ofPred (Bornology.IsVonNBounded 𝕜) = Set.univ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Limits.IsTerminal.ofUniqueHom.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} (h h_1 : (X : C) → X ⟶ Y) (e_h : h = h_1)
  (uniq : ∀ (X : C) (m : X ⟶ Y), m = h X),
  CategoryTheory.Limits.IsTerminal.ofUniqueHom h uniq = CategoryTheory.Limits.IsTerminal.ofUniqueHom h_1 ⋯
-- Mathlib.Algebra.Regular.Pow
IsLeftRegular.prod : ∀ {ι : Type u_2} {R : Type u_3} [inst : CommMonoid R] {s : Finset ι} {f : ι → R},
  (∀ i ∈ s, IsLeftRegular (f i)) → IsLeftRegular (∏ i ∈ s, f i)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.edist_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E), edist (f x) (f y) = edist x y
-- Mathlib.Data.Fintype.Order
Finite.map_iInf_of_antitone : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] (f : ι → α) {g : α → β},
  Antitone g → g (⨅ i, f i) = ⨆ i, g (f i)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.toEquivalence_unitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_2 : ∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
  [inst_3 : ∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : C),
  adj.toEquivalence.unitIso.hom.app X = adj.unit.app X
-- Mathlib.Analysis.Calculus.VectorField
Filter.EventuallyEq.lieBracketWithin_vectorField_eq_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E},
  V₁ =ᶠ[nhds x] V → W₁ =ᶠ[nhds x] W → VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x
-- Init.Data.SInt.Lemmas
UInt32.toInt32_sub : ∀ (a b : UInt32), (a - b).toInt32 = a.toInt32 - b.toInt32
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
sSetTopAdj_homEquiv_stdSimplex_zero : ∀ {X : TopCat} (f : SSet.toTop.obj (SSet.stdSimplex.obj { len := 0 }) ⟶ X),
  (sSetTopAdj.homEquiv (SSet.stdSimplex.obj { len := 0 }) X) f =
    SSet.const (TopCat.toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) default))
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_pow : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : Pow G M] (a : G) (n : M), ↑(a ^ n) = ↑a ^ n
-- Mathlib.Algebra.Group.Action.Defs
/-- Auxiliary definition for `SMul.comp`, `MulAction.compHom`,
`DistribMulAction.compHom`, `Module.compHom`, etc.  -/
SMul.comp.smul : {M : Type u_1} → {N : Type u_2} → {α : Type u_5} → [SMul M α] → (N → M) → N → α → α
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The sum over the values of the trivial additive character is the cardinality of the source.  -/
AddChar.sum_eq_card_of_eq_one : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : Fintype R] {R' : Type u_2} [inst_2 : CommRing R'] {ψ : AddChar R R'},
  ψ = 1 → ∑ a, ψ a = ↑(Fintype.card R)
-- Mathlib.CategoryTheory.Localization.Construction
/-- The object in the path category of `LocQuiver W` attached to an object in
the category `C`  -/
CategoryTheory.Localization.Construction.ιPaths : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      C → CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_dvd1 : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ) (b : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_right_split ctx p₁ p₂ p₃ d k →
    Int.Internal.Linear.cooper_dvd_right_split_dvd1_cert p₂ p' b ↑k = true → b ∣ Int.Internal.Linear.Poly.denote' ctx p'
-- Mathlib.InformationTheory.Hamming
Hamming.toHamming_neg : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Neg (β i)] {x : (i : ι) → β i},
  Hamming.toHamming (-x) = -Hamming.toHamming x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMonObjRepresentableBy.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.yonedaMonObjRepresentableBy M =
    CategoryTheory.Functor.representableByEquiv.symm (CategoryTheory.Iso.refl (CategoryTheory.yoneda.obj M))
-- Lean.Environment
_private.Lean.Environment.0.Lean.readIRPartsOfMod.unsafe_4 : Lean.ModuleData × Lean.CompactedRegion → System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)