mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.locallyOfFiniteType_specOverSpec : ∀ {R A : CommRingCat} [inst : Algebra ↑R ↑A] [Algebra.FiniteType ↑R ↑A],
  AlgebraicGeometry.LocallyOfFiniteType (AlgebraicGeometry.Spec A ↘ AlgebraicGeometry.Spec R)
-- Init.Data.SInt.Lemmas
ISize.ne_iff_ofBitVec_ne : ∀ {a b : BitVec System.Platform.numBits}, a ≠ b ↔ ISize.ofBitVec a ≠ ISize.ofBitVec b
-- Init.NotationExtra
unexpandMkArray5 : Lean.PrettyPrinter.Unexpander
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getIsPreorderInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_inv_two_pow_lt : ∀ {a : ENNReal}, a ≠ 0 → ∃ n, 2⁻¹ ^ n < a
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toUSize = USize.ofNatLT n ⋯
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumSumSumComm_toEquiv : ∀ (X : Type u) (Y : Type v) (W : Type u_1) (Z : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace W] [inst_3 : TopologicalSpace Z],
  (Homeomorph.sumSumSumComm W X Y Z).toEquiv = Equiv.sumSumSumComm W X Y Z
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞} [inst_11 : SizeOf 𝕜]
  [inst_12 : SizeOf E] [inst_13 : SizeOf E'] [inst_14 : SizeOf H] [inst_15 : SizeOf H'] [inst_16 : SizeOf M]
  [inst_17 : SizeOf M'] (toEquiv : M ≃ M') (contMDiff_toFun : ContMDiff I I' n ⇑toEquiv)
  (contMDiff_invFun : ContMDiff I' I n ⇑toEquiv.symm),
  sizeOf { toEquiv := toEquiv, contMDiff_toFun := contMDiff_toFun, contMDiff_invFun := contMDiff_invFun } =
    1 + sizeOf toEquiv
-- Mathlib.RingTheory.PowerSeries.Schroder
PowerSeries.coeff_X_mul_largeSchroderSeries : ∀ (n : ℕ), 0 < n → (PowerSeries.coeff n) (PowerSeries.X * PowerSeries.largeSchroderSeries) = (n - 1).largeSchroder
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsBigO.trans_isTheta : ∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
  [inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
  f =O[l] g → g =Θ[l] k → f =O[l] k
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Origin.decl.injEq : ∀ (name name_1 : Lean.Name),
  (Mathlib.Meta.FunProp.Origin.decl name = Mathlib.Meta.FunProp.Origin.decl name_1) = (name = name_1)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_congr : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  X =ᵐ[μ] Y → ProbabilityTheory.variance X μ = ProbabilityTheory.variance Y μ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- A set is equivalent to its image under a function `f` as measurable spaces,
if `f` is a measurable embedding  -/
MeasurableEmbedding.equivImage : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → {f : α → β} → (s : Set α) → MeasurableEmbedding f → ↑s ≃ᵐ ↑(f '' s)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Dep.not_indep : ∀ {α : Type u_1} {M : Matroid α} {D : Set α}, M.Dep D → ¬M.Indep D
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_C_iff : ∀ {R : Type u_1} {r : R} [inst : Semiring R], IsNilpotent (Polynomial.C r) ↔ IsNilpotent r
-- Mathlib.Order.Hom.Set
OrderIso.subsingleton_of_wellFoundedGT : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [WellFoundedGT α] [inst_2 : Preorder β], Subsingleton (α ≃o β)
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.Offset.compare_def : compare = compareOn fun x => x.second
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.CandidateKind.pipeArg.sizeOf_spec : sizeOf Lean.Server.FileWorker.SignatureHelp.CandidateKind.pipeArg = 1
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.processPostponed.loop : Bool → Bool → Lean.MetaM Bool
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.injective_map_zero`.

---

If two 0-cells have the same characteristic image point, they are equal.  -/
Topology.CWComplex.injective_map_zero : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D],
  Function.Injective fun x => ↑(Topology.RelCWComplex.map 0 x) ![]
-- Init.Data.Format.Basic
/-- Checks whether a `Format` is the constructor `Format.nil`.

This does not check whether the resulting rendered strings are always empty. To do that, use
`Format.isEmpty`.
 -/
Std.Format.isNil : Std.Format → Bool
-- Mathlib.Data.Complex.Basic
/-- A complex number `z` minus its conjugate `conj z` is `2i` times its imaginary part.  -/
Complex.im_eq_sub_conj : ∀ (z : ℂ), ↑z.im = (z - (starRingEnd ℂ) z) / (2 * Complex.I)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Construct an element of `HomogeneousLocalization 𝒜 x` from a homogeneous fraction.  -/
HomogeneousLocalization.mk : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          {𝒜 : ι → σ} → {x : Submonoid A} → HomogeneousLocalization.NumDenSameDeg 𝒜 x → HomogeneousLocalization 𝒜 x
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isCodetecting_iff_isCoseparating : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Balanced C], P.IsCodetecting ↔ P.IsCoseparating
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C]
  (f : α → β) (a : α), CategoryTheory.CategoryStruct.comp (U.mapPower f) (U.powerπ a) = U.powerπ (f a)
-- Mathlib.Topology.LocallyFinsupp
/-- Taking the positive part of a function with locally finite support commutes with
scalar multiplication by a natural number.
 -/
Function.locallyFinsuppWithin.nsmul_posPart : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y]
  [inst_2 : LinearOrder Y] [IsOrderedAddMonoid Y] (n : ℕ) (f : Function.locallyFinsuppWithin U Y), (n • f)⁺ = n • f⁺
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.ncs_tendsto_const : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {ncs : CauSeq ℤ_[p] norm} {F : Polynomial R} {a : ℤ_[p]},
  (∀ (n : ℕ),
      ‖(Polynomial.aeval (↑ncs n)) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖) →
    Filter.Tendsto (fun i => ‖(Polynomial.aeval (↑ncs i)) (Polynomial.derivative F)‖) Filter.atTop
      (nhds ‖(Polynomial.aeval a) (Polynomial.derivative F)‖)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk'_apply : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (x : G), (QuotientGroup.mk' N) x = ↑x
-- Mathlib.RingTheory.Ideal.Oka
/-- If an ideal is maximal for not satisfying an Oka predicate then it is prime.  -/
Ideal.IsOka.isPrime_of_maximal_not : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Ideal R → Prop},
  Ideal.IsOka P → ∀ {I : Ideal R}, Maximal (fun x => ¬P x) I → I.IsPrime
-- Mathlib.Algebra.Polynomial.Taylor
/-- Taylor's formula.  -/
Polynomial.sum_taylor_eq : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (r : R),
  (((Polynomial.taylor r) f).sum fun i a => Polynomial.C a * (Polynomial.X - Polynomial.C r) ^ i) = f
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.precomp_obj_hom_app : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  (X : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F))
  (X_1 : C'), ((CategoryTheory.Functor.RightExtension.precomp L F G).obj X).hom.app X_1 = X.hom.app (G.obj X_1)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Module.Basis.ExteriorAlgebra.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {I : Type u_3} [inst : LinearOrder I] [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (b : Module.Basis I R M),
  b.ExteriorAlgebra = (⋯.collectedBasis fun n => Module.Basis.exteriorPower n b).reindex Set.powersetCard.prodEquiv
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.instAddHom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → {c : ComplexShape ι} → {C D : HomologicalComplex V c} → Add (C ⟶ D)
-- Aesop.RuleTac.ElabRuleTerm
/-- Elaborate an identifier for a rule that applies to inductive types, e.g.
`cases`. The identifier must unambiguously refer to a global constant that is
either an inductive type or reduces to one. For the reduction test, we use
the larger transparency among `default` and `md`.  -/
Aesop.elabInductiveRuleIdent? : Lean.Term → Lean.Meta.TransparencyMode → Lean.Elab.TermElabM (Option (Lean.Name × Lean.InductiveVal))
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.collectUsed : List Lean.InductiveType → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst.instIsProbabilityMeasure : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} [MeasureTheory.IsProbabilityMeasure ρ], MeasureTheory.IsProbabilityMeasure ρ.fst
-- Mathlib.Topology.MetricSpace.Basic
/-- Metric space structure pulled back by an injective function. Injectivity is necessary to
ensure that `dist x y = 0` only if `x = y`.  -/
MetricSpace.induced : {γ : Type u_2} → {β : Type u_3} → (f : γ → β) → Function.Injective f → MetricSpace β → MetricSpace γ
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.LinearMap.quasiMeasurePreserving : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E →ₗ[ℝ] E),
  LinearMap.det f ≠ 0 → MeasureTheory.Measure.QuasiMeasurePreserving (⇑f) μ μ
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanLocationLink.fromJson : Lean.Json → Except String Lean.Lsp.LeanLocationLink
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.vadd_toHomeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : AddGroup G]
  [inst_12 : AddAction G M] {n : WithTop ℕ∞} [inst_13 : ContMDiffVAdd I I' n G M] (g : G),
  (Diffeomorph.vadd I I' n g).toHomeomorph = Homeomorph.vadd g
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.alphaHash : Lean.Expr → UInt64
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The binary fan constructed from the projection maps is a limit.  -/
CategoryTheory.Limits.prodIsProd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X Y : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] →
        CategoryTheory.Limits.IsLimit
          (CategoryTheory.Limits.BinaryFan.mk CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivialization.coordChangeL.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1)
  (e' e'_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e' : e' = e'_1)
  [inst_8 : Bundle.Trivialization.IsLinear R e] [inst_9 : Bundle.Trivialization.IsLinear R e'] (b b_1 : B),
  b = b_1 → Bundle.Trivialization.coordChangeL R e e' b = Bundle.Trivialization.coordChangeL R e_1 e'_1 b_1
-- Batteries.Recycling.RBTree.Depth
/-- `depthUB c n` is the best upper bound on the depth of any balanced red-black tree
with root colored `c` and black-height `n`.
 -/
RBTree.RBNode.depthUB : RBTree.RBColor → ℕ → ℕ
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.antipode_one : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A],
  (HopfAlgebraStruct.antipode R) 1 = 1
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabLamAux : Lean.NameSet → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Auxiliary definition for `unit'`, to address timeouts.  -/
ModuleCat.RestrictionCoextensionAdj.app' : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (Y : ModuleCat S) → ↑Y →ₗ[S] ↑(((ModuleCat.restrictScalars f).comp (ModuleCat.coextendScalars f)).obj Y)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.mk.inj : ∀ {R : Type u_1} {inst : Add R} {inst_1 : Mul R} {toCon : Con R}
  {add' : ∀ {w x y z : R}, toCon.toSetoid w x → toCon.toSetoid y z → toCon.toSetoid (w + y) (x + z)} {toCon_1 : Con R}
  {add'_1 : ∀ {w x y z : R}, toCon_1.toSetoid w x → toCon_1.toSetoid y z → toCon_1.toSetoid (w + y) (x + z)},
  { toCon := toCon, add' := add' } = { toCon := toCon_1, add' := add'_1 } → toCon = toCon_1
-- Init.Data.Array.Lemmas
Array.all_bne : ∀ {α : Type u_1} {a : α} [inst : BEq α] {xs : Array α}, (xs.all fun x => a != x) = !xs.contains a
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q : M}, Associated p q → Prime p → Prime q
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.identities_of_prop₁_of_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y},
  W₁ f → r.deg X = r.deg Y → CategoryTheory.MorphismProperty.identities C f
-- Mathlib.Analysis.Convex.EGauge
egauge_eq_top : ∀ {𝕜 : Type u_1} [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] {s : Set E} {x : E},
  egauge 𝕜 s x = ⊤ ↔ ∀ (c : 𝕜), x ∉ c • s
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets_singleton_iff : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → Set Ω} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.iIndepSets (fun i => {s i}) κ μ ↔
    ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Finitary.mk : ∀ {α : Type u_1} {M : Matroid α}, (∀ (I : Set α), (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I) → M.Finitary
-- Init.Data.Vector.Lemmas
Vector.count_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {a : α} {xs : Vector α n}, Array.count a xs.toArray = Vector.count a xs
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- Given a natural transformation `F ⟶ G`, get a term of `HomObj F G A` by "ignoring" `A`.  -/
CategoryTheory.Functor.HomObj.ofNatTrans : {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} → {A : CategoryTheory.Functor C (Type w)} → (F ⟶ G) → F.HomObj G A
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_inv_app_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Idempotents.Karoubi C),
  ((CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C).inv.app X).f = X.p
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- Products of completions  -/
AbstractCompletion.prod : {α : Type uα} →
  [inst : UniformSpace α] →
    AbstractCompletion.{vα, uα} α →
      {β : Type uβ} →
        [inst_1 : UniformSpace β] → AbstractCompletion.{vβ, uβ} β → AbstractCompletion.{max vβ vα, max uβ uα} (α × β)
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.hasColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (pres : CategoryTheory.Limits.ColimitPresentation J X), CategoryTheory.Limits.HasColimit pres.diag
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstModInt : Lean.Expr → Lean.MetaM Bool
-- Lean.Elab.Match
Lean.Elab.Term.withPatternElabConfig : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcRef.mk.inj : ∀ {p p_1 : USize}, { p := p } = { p := p_1 } → p = p_1
-- Mathlib.Order.SuccPred.Archimedean
strictAntiOn_of_succ_lt : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f (Order.succ a) < f a) → StrictAntiOn f s
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.obj_eq_of_cons_eq_cons : ∀ {V : Type u} [inst : Quiver V] {a b c d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b ⟶ d} {e' : c ⟶ d},
  p.cons e = p'.cons e' → b = c
-- Lean.Elab.DocString
/-- Retrieves a named argument from the arguments to a documentation extension. Returns `default` if no
such named argument was provided.
 -/
Lean.Doc.getNamed : {α : Type} → [Lean.Doc.FromDocArg α] → Lean.Name → α → StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM α
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.lipschitzOnWith_ofFun_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] [inst_1 : PseudoEMetricSpace β]
  {f : γ → α → β} {K : NNReal} {s : Set γ},
  LipschitzOnWith K (fun x => UniformFun.ofFun (f x)) s ↔ ∀ (c : α), LipschitzOnWith K (fun x => f x c) s
-- Mathlib.Topology.LocallyFinsupp
/-- Restriction commutes with taking negative parts.
 -/
Function.locallyFinsuppWithin.restrict_negPart : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U V : Set X} (D : Function.locallyFinsuppWithin U ℤ) (h : V ⊆ U),
  D⁻.restrict h = (D.restrict h)⁻
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- This is an auxiliary data structure useful for constructing adjunctions.
See `Adjunction.mk'`. This structure won't typically be used anywhere else.
 -/
CategoryTheory.Adjunction.CoreHomEquivUnitCounit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)
-- Init.Data.List.Lemmas
List.cons_ne_self : ∀ {α : Type u_1} (a : α) (l : List α), a :: l ≠ l
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.instEquivLike : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] → [inst_2 : Mul M] → [inst_3 : Mul N] → EquivLike (M ≃ₜ* N) M N
-- Batteries.Data.String.Lemmas
/-- Validity for a substring.  -/
Substring.Raw.Valid : Substring.Raw → Prop
-- Init.Data.Dyadic.Basic
Dyadic.ble.eq_3 : ∀ (n k : ℤ) (hn : n % 2 = 1), (Dyadic.ofOdd n k hn).ble Dyadic.zero = decide (n ≤ 0)
-- Std.Data.TreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the largest key that is
less than or equal to the given key.
 -/
Std.TreeMap.getKeyLE : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.TreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α
-- Init.Data.Ord.Basic
Ordering.isLE_of_eq_eq : ∀ {o : Ordering}, o = Ordering.eq → o.isLE = true
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
alternatingGroup.normalClosure_swap_mul_swap_five : Subgroup.normalClosure {⟨Equiv.swap 0 4 * Equiv.swap 1 3, ⋯⟩} = ⊤
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHomClass.map_comp_comul : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : AddCommMonoid A} {inst_2 : Module R A} {inst_3 : AddCommMonoid B} {inst_4 : Module R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : FunLike F A B} [self : CoalgHomClass F R A B]
  (f : F), TensorProduct.map ↑f ↑f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ ↑f
-- Lean.Attributes
Lean.TagAttribute.hasTag : Lean.TagAttribute → Lean.Environment → Lean.Name → Bool
-- Lean.Meta.Tactic.Simp.Arith.Util
Lean.Meta.Simp.Arith.isDvdCnstr : Lean.Expr → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.le_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((∀ (k' : α), Std.Internal.List.minKey? l = some k' → (compare k k').isLE = true) ↔
      ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Fintype.linearCombination_apply_single : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : α → M) [inst_4 : DecidableEq α] (i : α) (r : R),
  (Fintype.linearCombination R v) (Pi.single i r) = r • v i
-- Mathlib.RingTheory.Congruence.Hom
/-- A ring homomorphism `f` induces an injective homomorphism on the quotient by `f`'s kernel.  -/
RingCon.kerLift_injective : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] (f : M →+* P),
  Function.Injective ⇑(RingCon.kerLift f)
-- Init.Data.UInt.Lemmas
UInt64.mul_comm : ∀ (a b : UInt64), a * b = b * a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  (contains_eq_false : m₁.contains k = false) {h' : (m₁.union m₂).contains k = true},
  (m₁.union m₂).getKey k h' = m₂.getKey k ⋯
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Ric.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Ric α}, r.toArray = (Std.Ric.Internal.iter r).toArray
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.instIsMonoidalFunctorCongrLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u_1) [inst_2 : CategoryTheory.Category.{v_1, u_1} E] [inst_3 : CategoryTheory.MonoidalCategory E]
  (e : C ≌ D), e.congrLeft.IsMonoidal