mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesColimit_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D), Subsingleton (CategoryTheory.Limits.PreservesColimit K F)
-- Mathlib.RingTheory.Valuation.ValuationSubring
Valuation.mem_valuationSubring_iff : ∀ {K : Type u} [inst : Field K] {Γ : Type u_1} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (x : K),
  x ∈ v.valuationSubring ↔ v x ≤ 1
-- Mathlib.ModelTheory.Substructures
/-- The inf of two substructures is their intersection.  -/
FirstOrder.Language.Substructure.instInf : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → Min (L.Substructure M)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTransposeAlgEquiv_apply : ∀ (n : Type u_3) {R : Type u_7} (α : Type v) [inst : Fintype n] [inst_1 : CommSemiring R] [inst_2 : StarRing R]
  [inst_3 : TrivialStar R] [inst_4 : Semiring α] [inst_5 : StarRing α] [inst_6 : Algebra R α] [inst_7 : StarModule R α]
  (a : Matrix n n α), (Matrix.conjTransposeAlgEquiv n α) a = MulOpposite.op a.conjTranspose
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_eq_iff_eq' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S}, f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (x₁ + ↑y₂) = f (x₂ + ↑y₁)
-- Init.Data.SInt.Lemmas
UInt8.toInt8_add : ∀ (a b : UInt8), (a + b).toInt8 = a.toInt8 + b.toInt8
-- Mathlib.Order.Disjoint
Codisjoint.ne_bot_of_ne_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a b : α}, Codisjoint a b → a ≠ ⊤ → b ≠ ⊥
-- Mathlib.Algebra.Category.Grp.Basic
/-- The underlying type.  -/
AddGrpCat.carrier : AddGrpCat → Type u
-- Init.Tactics
/-- `and_intros` applies `And.intro` until it does not make progress.  -/
Lean.Parser.Tactic.tacticAnd_intros : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Morphisms.Descent
/-- If `P` is local at the target, to show `P` descends along `P'` we may assume
the base to be affine.  -/
AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong : ∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  [P'.IsStableUnderBaseChange],
  (∀ {R : CommRingCat} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec R)
      (g : Y ⟶ AlgebraicGeometry.Spec R), P' f → P (CategoryTheory.Limits.pullback.fst f g) → P g) →
    P.DescendsAlong P'
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_pow : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α} {n : ℕ}, 1 ∈ s → n ≠ 0 → s ⊆ s ^ n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Complex.continuousAt_tan : ∀ {x : ℂ}, ContinuousAt Complex.tan x ↔ Complex.cos x ≠ 0
-- Init.Control.Lawful.Instances
StateT.run_set : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] (s s' : σ), (set s').run s = pure (PUnit.unit, s')
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Let `M` be an `R`-module, and `f` an `R`-linear endomorphism of `M`.
Then `μ : R` and `k : ℕ∞` satisfy `HasUnifEigenvalue f μ k` if
`f.genEigenspace μ k ≠ ⊥`.

For `k = 1`, this means that `μ` is an eigenvalue of `f`.  -/
Module.End.HasUnifEigenvalue : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ∞ → Prop
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceFrom_inj : ∀ {s : String.Slice} {p₀ : s.Pos} {pos pos' : (s.sliceFrom p₀).Pos},
  String.Slice.Pos.ofSliceFrom pos = String.Slice.Pos.ofSliceFrom pos' ↔ pos = pos'
-- Mathlib.RingTheory.Smooth.StandardSmooth
/-- The relative dimension of a standard smooth `R`-algebra `S` is
the dimension of an arbitrarily chosen submersive `R`-presentation of `S`.

Note: If `S` is non-trivial, this number is independent of the choice of the presentation as it is
equal to the `S`-rank of `Ω[S/R]`
(see `IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential`).
 -/
Algebra.IsStandardSmooth.relativeDimension : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [Algebra.IsStandardSmooth R S] → ℕ
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.lt_add_of_pos_left : ∀ {α : Type u_1} [inst : CommSemiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] (a : α) {b : α},
  0 < b → a < b + a
-- Mathlib.Computability.EpsilonNFA
εNFA.mk : {α : Type u} → {σ : Type v} → (σ → Option α → Set σ) → Set σ → Set σ → εNFA α σ
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.truncate_eq_of_agree : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} (x : PFunctor.Approx.CofixA F n) (y : PFunctor.Approx.CofixA F n.succ),
  PFunctor.Approx.Agree x y → PFunctor.Approx.truncate y = x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M : C} [inst_3 : CategoryTheory.MonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
          CategoryTheory.MonObj.mul))
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom)
      CategoryTheory.MonObj.mul
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_two_of_utf8Size_eq_four : ∀ {c : Char} (h : c.utf8Size = 4), (String.utf8EncodeChar c)[2].toBitVec = 2#2 ++ BitVec.extractLsb' 6 6 c.val.toBitVec
-- Mathlib.FieldTheory.ChevalleyWarning
MvPolynomial.sum_eval_eq_zero : ∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ] [inst_3 : DecidableEq σ]
  (f : MvPolynomial σ K), f.totalDegree < (Fintype.card K - 1) * Fintype.card σ → ∑ x, (MvPolynomial.eval x) f = 0
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The morphim `K ⟶ S K n₁` which in degree `n₁` corresponds to
the composition `K.X n₁ ⟶ K.opcycles n₁ ⟶ Injective.under (K.opcycles n₁)`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.i : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (K : CochainComplex C ℤ) →
        [inst_2 : CategoryTheory.EnoughInjectives C] →
          (n₁ : ℤ) → K ⟶ CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.S✝ K n₁
-- Mathlib.Data.Multiset.Replicate
Multiset.nodup_iff_ne_cons_cons : ∀ {α : Type u_1} {s : Multiset α}, s.Nodup ↔ ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
-- Mathlib.Algebra.Category.BoolRing
_private.Mathlib.Algebra.Category.BoolRing.0.BoolRing.Hom.mk : {R : BoolRing} → {S : BoolRing} → (↑R →+* ↑S) → R.Hom S
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- Shows how the entries of the sequence of the computed continued fraction can be obtained by the
fractional parts of the stream of integer and fractional parts.
 -/
GenContFract.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ}
  {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n →
    ifp_n.fr ≠ 0 → (GenContFract.of v).s.get? n = some { a := 1, b := ↑(GenContFract.IntFractPair.of ifp_n.fr⁻¹).b }
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {init : α} [inst : Monad m] {f : α → β → m α},
  List.scanAuxM✝ f init [] = pure [init]
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheck : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Order.Defs.Unbundled
Minimal.le_of_le : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} {x y : α}, Minimal P x → P y → y ≤ x → x ≤ y
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_d_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) h) =
    CategoryTheory.CategoryStruct.comp (G.d i j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) h)
-- Mathlib.Analysis.Normed.Module.Span
LinearIsometryEquiv.toSpanUnitSingleton_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : NormSMulClass 𝕜 E] (x : E) (hx : ‖x‖ = 1) (r : 𝕜),
  (LinearIsometryEquiv.toSpanUnitSingleton x hx) r = ⟨r • x, ⋯⟩
-- Init.Data.Format.Basic
/-- Exits the scope of `count` opened tags.
 -/
Std.Format.MonadPrettyFormat.endTags : {m : Type → Type} → [self : Std.Format.MonadPrettyFormat m] → ℕ → m Unit
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.linearIndepOn_pair : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (D D' : Projectivization K V), LinearIndepOn K id {D.rep, D'.rep}
-- Init.Data.Array.Range
Array.zipIdx_append : ∀ {α : Type u_1} {xs ys : Array α} {k : ℕ}, (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + xs.size)
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.kroneckerTMulStarAlgEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Fintype n]
  [inst_6 : DecidableEq n] [inst_7 : CommSemiring S] [inst_8 : Algebra R S] [inst_9 : Algebra S A]
  [inst_10 : IsScalarTower R S A] [inst_11 : Fintype m] [inst_12 : DecidableEq m] [inst_13 : StarRing R]
  [inst_14 : StarAddMonoid A] [inst_15 : StarAddMonoid B] [inst_16 : StarModule R A] [inst_17 : StarModule R B]
  (x : TensorProduct R (Matrix m m A) (Matrix n n B)),
  (Matrix.kroneckerTMulStarAlgEquiv m n R S A B) x = (kroneckerTMulLinearEquiv m m n n R S A B) x
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabModuleDoc : Lean.Elab.Command.CommandElab
-- Init.Data.String.Termination
String.Slice.Pos.Down.inner : {s : String.Slice} → String.Slice.Pos.Down s → s.Pos
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The `NonUnitalSubring` of elements `x : R` such that `f x = g x`, i.e.,
the equalizer of f and g as a `NonUnitalSubring` of R  -/
NonUnitalRingHom.eqLocus : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] → [inst_1 : NonUnitalNonAssocRing S] → (R →ₙ+* S) → (R →ₙ+* S) → NonUnitalSubring R
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Transport being a left adjoint along a natural isomorphism.  -/
CategoryTheory.Functor.isLeftAdjoint_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [F.IsLeftAdjoint], G.IsLeftAdjoint
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.inf : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β},
  Filter.Tendsto f x₁ y₁ → Filter.Tendsto f x₂ y₂ → Filter.Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂)
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.isOpen_closedBall : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ},
  r ≠ 0 → IsOpen (Metric.closedBall x r)
-- Mathlib.Algebra.Group.ULift
ULift.commSemigroup.eq_1 : ∀ {α : Type u} [inst : CommSemigroup α], ULift.commSemigroup = Function.Injective.commSemigroup ⇑Equiv.ulift ⋯ ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.foldr_eq_foldr_toArray : ∀ {α : Type u} {δ : Type w} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {f : α → β → δ → δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldr f init t =
    Array.foldr (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.Exact.moduleCat_of_range_eq_ker : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker),
  (CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g ⋯).Exact
-- Init.Data.Ord.SInt
Int16.instOrd : Ord Int16
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.quasiCoherentData_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.LocalGeneratorsData) [inst_3 : q.IsLocallyFreeData] (a : q.I), q.quasiCoherentData.X a = q.X a
-- Mathlib.Algebra.Order.Hom.Ring
/-- The inverse of an ordered ring isomorphism as an ordered ring isomorphism.  -/
OrderRingIso.symm : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Mul α] →
      [inst_1 : Add α] → [inst_2 : LE α] → [inst_3 : Mul β] → [inst_4 : Add β] → [inst_5 : LE β] → α ≃+*o β → β ≃+*o α
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Reinterpret an element of a type of semilinear maps as a semilinear map.  -/
SemilinearMapClass.semilinearMap : {R : Type u_1} →
  {S : Type u_5} →
    {M : Type u_8} →
      {M₃ : Type u_11} →
        {F : Type u_14} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₃] →
                      {σ : R →+* S} → F → [inst_6 : FunLike F M M₃] → [SemilinearMapClass F σ M M₃] → M →ₛₗ[σ] M₃
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.op_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), h.op.H = Opposite.op h.H
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAut_bijective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] (G : Type u_1) [inst_2 : Group G]
  [inst_3 : (X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  [inst_5 : TopologicalSpace G] [inst_6 : IsTopologicalGroup G] [inst_7 : CompactSpace G]
  [inst_8 : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G],
  Function.Bijective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.mk.sizeOf_spec : ∀ {n : ℕ} (parts : Multiset ℕ) (parts_pos : ∀ {i : ℕ}, i ∈ parts → 0 < i) (parts_sum : parts.sum = n),
  sizeOf { parts := parts, parts_pos := parts_pos, parts_sum := parts_sum } = 1 + sizeOf parts + sizeOf parts_sum
-- Mathlib.Analysis.Asymptotics.Defs
Filter.EventuallyEq.trans_isLittleO : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g : α → F}, f₁ =ᶠ[l] f₂ → f₂ =o[l] g → f₁ =o[l] g
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.ofNat_lt : ∀ {a : ℤ} {n : ℕ}, a ≥ 0 → a < Int.ofNat n → a.toNat < n
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.le_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), Monotone t.le
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Lean.Data.Lsp.Internal
Lean.Lsp.ImportInfo.mk.sizeOf_spec : ∀ (module : String) (isPrivate isAll isMeta : Bool),
  sizeOf { module := module, isPrivate := isPrivate, isAll := isAll, isMeta := isMeta } =
    1 + sizeOf module + sizeOf isPrivate + sizeOf isAll + sizeOf isMeta
-- Mathlib.Algebra.Group.Invertible.Defs
invertible_unique : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a] [inst_2 : Invertible b], a = b → ⅟a = ⅟b
-- Mathlib.Data.Sym.Basic
/-- `α ∈ s` means that `a` appears as one of the factors in `s`.
 -/
Sym.instMembership : {α : Type u_1} → {n : ℕ} → Membership α (Sym α n)
-- Mathlib.FieldTheory.RatFunc.Basic
/-- The coercion from polynomials to rational functions, implemented as the algebra map from a
domain to its field of fractions  -/
RatFunc.coePolynomial : {K : Type u} → [inst : CommRing K] → [IsDomain K] → Polynomial K → RatFunc K
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_eq_getMsbD : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i))
-- Init.Data.Order.Classes
/-- This typeclass states that the order structure on `α`, represented by an `LE α` instance,
is a preorder. In other words, the less-or-equal relation is reflexive and transitive.
 -/
Std.IsPreorder : (α : Type u) → [LE α] → Prop
-- Mathlib.Data.Set.Basic
/-- **Alias** of the forward direction of `Set.nonempty_iff_ne_empty`.

---

See also `Set.not_nonempty_iff_eq_empty`.  -/
Set.Nonempty.ne_empty : ∀ {α : Type u} {s : Set α}, s.Nonempty → s ≠ ∅
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressProcessingInfo.mk : Lean.Lsp.Range → Lean.Lsp.LeanFileProgressKind → Lean.Lsp.LeanFileProgressProcessingInfo
-- Mathlib.Algebra.Order.Monoid.ToMulBot
WithZero.toMulBot_coe_ofAdd : ∀ {α : Type u} [inst : Add α] (x : α), WithZero.toMulBot.symm (Multiplicative.ofAdd ↑x) = ↑(Multiplicative.ofAdd x)
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {inst_1 : CategoryTheory.Category.{t, w} J}
  {X : C} {diag : CategoryTheory.Functor J C} {ι : diag ⟶ (CategoryTheory.Functor.const J).obj X}
  {isColimit : CategoryTheory.Limits.IsColimit { pt := X, ι := ι }} {diag_1 : CategoryTheory.Functor J C}
  {ι_1 : diag_1 ⟶ (CategoryTheory.Functor.const J).obj X}
  {isColimit_1 : CategoryTheory.Limits.IsColimit { pt := X, ι := ι_1 }},
  { diag := diag, ι := ι, isColimit := isColimit } = { diag := diag_1, ι := ι_1, isColimit := isColimit_1 } →
    diag = diag_1 ∧ ι ≍ ι_1 ∧ isColimit ≍ isColimit_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          aig.RefVec w →
            aig.RefVec w →
              ℕ →
                ℕ →
                  aig.RefVec w →
                    aig.RefVec w → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput aig w
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.visit : Lean.Expr → StateRefT' IO.RealWorld Lean.Meta.Try.Collector.Cache Lean.Meta.Try.Collector.M Unit
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
/-- The action of `GL(2, ℝ)` on `ℍ` is jointly continuous.  -/
UpperHalfPlane.instContinuousSMulGL2R : ContinuousSMul (GL (Fin 2) ℝ) UpperHalfPlane
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.comp_continuous : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {g : Y → Z}
  {f : X → Y}, IsLocallyConstant g → Continuous f → IsLocallyConstant (g ∘ f)
-- Mathlib.Algebra.Ring.Invertible
AddUnits.neg_mul_neg : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {x y : AddUnits R}, ↑(-x) * ↑(-y) = ↑x * ↑y
-- Mathlib.Order.BooleanAlgebra.Defs
BooleanAlgebra.toCompl : {α : Type u} → [self : BooleanAlgebra α] → Compl α
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.blockDiagonal'.eq_1 : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : (i : o) → Matrix (m' i) (n' i) α),
  Matrix.blockDiagonal' M =
    Matrix.of fun x x_1 =>
      match x with
      | ⟨k, i⟩ =>
        match x_1 with
        | ⟨k', j⟩ => if h : k = k' then M k i (cast ⋯ j) else 0
-- Aesop.Stats.Basic
Aesop.instInhabitedRuleStats : Inhabited Aesop.RuleStats
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.collectDeps : Array Lean.Expr → Lean.Expr → Array ℕ
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangle_map_hom₃ : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₃ = F.map f.hom₃
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.inv' : ∀ {G : Type u} {inst : Group G} [self : GroupFilterBasis G] {U : Set G},
  U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun x => x⁻¹) ⁻¹' U
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- See also `SkewPolynomial.sum_smul_index'` for a version using `smul` on the RHS.  -/
SkewPolynomial.sum_smul_index : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] (p : SkewPolynomial R) (b : R)
  (f : ℕ → R → S), (∀ (i : ℕ), f i 0 = 0) → (b • p).sum f = p.sum fun n a => f n (b * a)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
_private.Mathlib.RingTheory.Valuation.Discrete.Basic.0.Valuation.termK₀ : Lean.ParserDescr
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_inv : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f⁻¹.SameCycle x y ↔ f.SameCycle x y
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.instMonoid : {α : Type u_1} → {rels : FreeMonoid α → FreeMonoid α → Prop} → Monoid (PresentedMonoid rels)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.lift_ι'_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g}
  (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.IsLimit.lift hs k h)
      (CategoryTheory.CategoryStruct.comp s.ι h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.fromOpposite.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N)
  (hf : ∀ (x y : M), AddCommute (f x) (f y)), f.fromOpposite hf = { toFun := ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }