mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Extension.Linear
/-- **Szpilrajn extension theorem**: any partial order can be extended to a linear order.  -/
extend_partialOrder : ∀ {α : Type u} (r : α → α → Prop) [IsPartialOrder α r], ∃ s, IsLinearOrder α s ∧ r ≤ s
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- The cardinality of the set of `k`-rough numbers `≤ N` is bounded by `N` times the sum
of `1/p` over the primes `k ≤ p ≤ N`.  -/
Nat.roughNumbersUpTo_card_le' : ∀ (N k : ℕ), ↑(N.roughNumbersUpTo k).card ≤ ↑N * ∑ p ∈ N.succ.primesBelow \ k.primesBelow, 1 / ↑p
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.trans_conj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (β : Y ≅ Z)
  (f : CategoryTheory.End X), (α ≪≫ β).conj f = β.conj (α.conj f)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.mk'_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {fst snd : S.Arrow} (r : fst.Relation snd),
  (CategoryTheory.GrothendieckTopology.Cover.Relation.mk' r).r = r
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure.below.basic : ∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → FiniteInter.finiteInterClosure S a → Prop} {s : Set α}
  (a : s ∈ S), FiniteInter.finiteInterClosure.below ⋯
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.innerProductForm_ιMulti_self : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (x : Fin n → E),
  (exteriorPower.innerProductForm✝ ((exteriorPower.ιMulti ℝ n) x)) ((exteriorPower.ιMulti ℝ n) x) =
    (Matrix.gram ℝ x).det
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.eq_false_of_isUnsat : ∀ (ctx : Nat.Internal.Linear.Context) (c : Nat.Internal.Linear.ExprCnstr),
  c.toNormPoly.isUnsat = true → Nat.Internal.Linear.ExprCnstr.denote ctx c = False
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.num_pow : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (n : ℕ), ↑(c ^ n).num = ↑c.num ^ n
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.holderₗ_apply_apply_coe : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal)
  [hpqr : p.HolderTriple q r] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K)
  (m : ↥(lp E p)) (f : ↥(lp F q)) (i : ι), ↑(((lp.holderₗ r B hBK) m) f) i = ((B i) (↑m i)) (↑f i)
-- Mathlib.NumberTheory.Fermat
/-- **Goldbach's theorem** : no two distinct Fermat numbers share a common factor greater than one.

From a letter to Euler, see page 37 in [juskevic2022].
 -/
Nat.coprime_fermatNumber_fermatNumber : ∀ {m n : ℕ}, m ≠ n → m.fermatNumber.Coprime n.fermatNumber
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_combine : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (p₁.combine p₂) =
        Lean.Grind.CommRing.Poly.denoteS ctx p₁ + Lean.Grind.CommRing.Poly.denoteS ctx p₂
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instMonoidWithZero : {α : Type u_1} → [MonoidWithZero α] → MonoidWithZero αᵐᵒᵖ
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.sub : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Sub β]
  [ContinuousSub β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f - g)
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx : Type
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinitesimal.neg : ∀ {x : ℝ*}, x.Infinitesimal → (-x).Infinitesimal
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The underlying category of a `BasedCategory`.  -/
CategoryTheory.BasedCategory.category : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (self : CategoryTheory.BasedCategory 𝒮) → CategoryTheory.Category.{v₂, u₂} self.obj
-- Mathlib.Dynamics.Minimal
IsOpen.iUnion_smul : ∀ (G : Type u_2) {α : Type u_3} [inst : Group G] [inst_1 : TopologicalSpace α] [inst_2 : MulAction G α]
  [MulAction.IsMinimal G α] {U : Set α}, IsOpen U → U.Nonempty → ⋃ g, g • U = Set.univ
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The natural isomorphism expressing that functors `Karoubi C ⥤ Karoubi D` obtained
using `functorExtension₁` actually extend the original functors `C ⥤ Karoubi D`.  -/
CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso : (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] →
        (CategoryTheory.Idempotents.functorExtension₁ C D).comp
            ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C)
                  (CategoryTheory.Idempotents.Karoubi D)).obj
              (CategoryTheory.Idempotents.toKaroubi C)) ≅
          CategoryTheory.Functor.id (CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D))
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- **Alias** of `CategoryTheory.comp_apply`. -/
CategoryTheory.comp_apply' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) (x : CategoryTheory.ToType X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.FieldTheory.Perfect
PerfectRing.toPerfectField : ∀ (K : Type u_1) (p : ℕ) [inst : Field K] [ExpChar K p] [PerfectRing K p], PerfectField K
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G],
  (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).Faithful
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instContMDiffInv₀OfNatWithTopENat : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] [ContMDiffInv₀ I 2 G],
  ContMDiffInv₀ I 1 G
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.mem_corootSpace' : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} [inst_3 : LieRing.IsNilpotent ↥H] [inst_4 : H.IsCartanSubalgebra] [inst_5 : IsNoetherian R L]
  (α : ↥H → R) {x : ↥H},
  x ∈ LieAlgebra.corootSpace α ↔
    x ∈ Submodule.span R {x | ∃ y ∈ LieAlgebra.rootSpace H α, ∃ z ∈ LieAlgebra.rootSpace H (-α), ⁅y, z⁆ = ↑x}
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.dist : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : PseudoMetricSpace β]
  {f g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => dist (f x) (g x)) μ
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialEvalσ.eq_def : ∀ (L : List ℕ) (j : ℕ),
  SimplexCategoryGenRel.simplicialEvalσ L j =
    match L with
    | [] => j
    | a :: L =>
      if a < SimplexCategoryGenRel.simplicialEvalσ L j then SimplexCategoryGenRel.simplicialEvalσ L j - 1
      else SimplexCategoryGenRel.simplicialEvalσ L j
-- Mathlib.Tactic.SuppressCompilation
/-- Replacing `def` and `instance` by `noncomputable def` and `noncomputable instance`, designed
to disable the compiler in a given file or a given section.
This is a hack to work around https://github.com/leanprover-community/mathlib4/issues/7103.
Note that it does not work with `notation3`. You need to prefix such a notation declaration with
`unsuppress_compilation` if `suppress_compilation` is active.  -/
commandSuppress_compilation : Lean.ParserDescr
-- Mathlib.Tactic.Linarith.Preprocessing
/-- **Alias** of `Mathlib.Tactic.Linarith.mkNatCastNonnegProof?`.

---

If `e : ℕ`, returns a proof of `0 ≤ (e : C)`.  -/
Mathlib.Tactic.Linarith.mk_natCast_nonneg_prf : Lean.Expr × Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.DTreeMap.ofList l cmp).get? k' = some (cast ⋯ v)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {s : Finset α},
  s ∈ (SzemerediRegularity.chunk hP G ε hU).parts →
    s.card ≤ Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.N_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
  CategoryTheory.Idempotents.DoldKan.N.map f =
    (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map
      (AlgebraicTopology.DoldKan.N₁.map f)
-- Mathlib.MeasureTheory.Measure.OpenPos
Metric.measure_closedEBall_pos : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
  [μ.IsOpenPosMeasure] (x : X) {r : ENNReal}, r ≠ 0 → 0 < μ (Metric.closedEBall x r)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.connected_iff : ∀ {V : Type u} (G : SimpleGraph V), G.Connected ↔ G.Preconnected ∧ Nonempty V
-- Mathlib.GroupTheory.Perm.Centralizer
/-- Cardinality of the centralizer in `Equiv.Perm α` of a permutation given `cycleType`  -/
Equiv.Perm.nat_card_centralizer : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Nat.card ↥(Subgroup.centralizer {g}) =
    (Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial
-- Init.Prelude
/-- The `*>` operator is overloaded using `seqRight`.

When thinking about `f` as potential side effects, `*>` evaluates first the left and then the right
argument for their side effects, discarding the value of the left argument and returning the value
of the right argument.

For most applications, `Applicative` or `Monad` should be used rather than `SeqRight` itself.
 -/
SeqRight : (Type u → Type v) → Type (max (u + 1) v)
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.endPos : Lean.Server.Snapshots.Snapshot → String.Pos.Raw
-- Mathlib.Analysis.Convex.Hull
subset_convexHull : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s : Set E), s ⊆ (convexHull 𝕜) s
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.minEntry.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.isEmpty = false),
  Std.DTreeMap.Internal.Impl.Const.minEntry x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      h_1 => Std.DTreeMap.Internal.Impl.Const.minEntry l ⋯
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : B ⟶ A) (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B ((CategoryTheory.MonoidalClosed.pre f).app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev B).app X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (A ⟹ X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) h)
-- Mathlib.Data.Vector.Mem
List.Vector.notMem_nil : ∀ {α : Type u_1} (a : α), a ∉ List.Vector.nil.toList
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_maxKeyD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.Topology.Separation.Hausdorff
/-- Every two points in a Hausdorff space admit disjoint open neighbourhoods.  -/
T2Space.t2 : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T2Space X],
  Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} {P : β → Prop} {inner : Std.IterM m β}
  {invariant : ∀ (out : β), inner.IsPlausibleIndirectOutput out → P out} {inner_1 : Std.IterM m β}
  {invariant_1 : ∀ (out : β), inner_1.IsPlausibleIndirectOutput out → P out},
  { inner := inner, invariant := invariant } = { inner := inner_1, invariant := invariant_1 } → inner = inner_1
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosReflectLT.toMulPosMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α] [MulPosReflectLT α], MulPosMono α
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.toMvPowerSeries_apply : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] {f : PowerSeries R} (i : σ),
  (PowerSeries.toMvPowerSeries i) f = (MvPowerSeries.rename fun x => i) f
-- Lean.Parser.Do
Lean.Parser.Term.notFollowedByRedefinedTermToken.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.zpow_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] (a : ℤ) (a_1 : X ≃ₜ X), ZPow.zpow a a_1 = zpowRec npowRec a a_1
-- Mathlib.Topology.MetricSpace.Antilipschitz
antilipschitzWith_iff_le_mul_dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
AffineEquiv.map_midpoint : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : Invertible 2]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] (f : P ≃ᵃ[R] P') (a b : P),
  f (midpoint R a b) = midpoint R (f a) (f b)
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.noetherianSpace_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.NoetherianSpace α] (f : α → β),
  Continuous f → Function.Surjective f → TopologicalSpace.NoetherianSpace β
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_congr : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H),
  G.vertexCoverNum = H.vertexCoverNum
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.le_ker_iff_map : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] {f : M →ₗ⁅R,L⁆ N} (M' : LieSubmodule R L M),
  M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.lift'_obj : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  (obj : V → D) (map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w))
  (map_id : ∀ (v : V), map (CategoryTheory.ReflQuiver.id v) = CategoryTheory.CategoryStruct.id (obj v)) (v : V),
  (CategoryTheory.Cat.FreeRefl.lift' obj (fun {v w} => map) map_id).obj (CategoryTheory.Cat.FreeRefl.mk v) = obj v
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.toNonUnitalSubsemiring_inj : ∀ {R : Type u} [inst : NonAssocSemiring R] {S₁ S₂ : Subsemiring R},
  S₁.toNonUnitalSubsemiring = S₂.toNonUnitalSubsemiring ↔ S₁ = S₂
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongr_smul : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} {S : Type u_12} [inst_5 : Monoid S]
  [inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass R S N] (σ : ι ≃ ι') (c : S) (f : M [⋀^ι]→ₗ[R] N),
  AlternatingMap.domDomCongr σ (c • f) = c • AlternatingMap.domDomCongr σ f
-- Mathlib.Tactic.ModCases
/-- The end point is that once we have reduced to `∃ z, n ≤ z < n ∧ a ≡ z (mod n)`
there are no more cases to consider.
 -/
Mathlib.Tactic.ModCases.IntMod.onModCases_stop : (p : Sort u_1) → (n : ℕ) → (a : ℤ) → Mathlib.Tactic.ModCases.IntMod.OnModCases n a n p
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.instNonemptyStrictLimitsClosureIter : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {β : Type w'} [inst_2 : LinearOrder β]
  [OrderBot β] [inst_4 : SuccOrder β] [inst_5 : WellFoundedLT β] (b : β) [P.Nonempty],
  (P.strictLimitsClosureIter J b).Nonempty
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- `f` has the derivative `f'` at the point `x` along the direction `v` in the set `s`.
That is, `f (x + t v) = f x + t • f' + o (t)` when `t` tends to `0` and `x + t v ∈ s`.
Note that this definition is less well behaved than the total Fréchet derivative, which
should generally be favored over this one.  -/
HasLineDerivWithinAt : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} →
      [inst_1 : NormedAddCommGroup F] →
        [NormedSpace 𝕜 F] →
          {E : Type u_3} → [inst_3 : AddCommGroup E] → [Module 𝕜 E] → (E → F) → F → Set E → E → E → Prop
-- Init.Data.Vector.Basic
_private.Init.Data.Vector.Basic.0.Vector.mapM.go.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f : α → m β) (xs : Vector α n)
  (k : ℕ) (h : k ≤ n) (acc : Vector β k),
  Vector.mapM.go✝ f xs k h acc =
    if h' : k < n then do
      let __do_lift ← f xs[k]
      Vector.mapM.go✝ f xs (k + 1) ⋯ (acc.push __do_lift)
    else pure (Vector.cast ⋯ acc)
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_mul_unit_right_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsUnit x → (IsRelPrime (y * x) z ↔ IsRelPrime y z)
-- Mathlib.Order.LatticeIntervals
Set.Icc.semilatticeInf : {α : Type u_1} → {a b : α} → [inst : SemilatticeInf α] → SemilatticeInf ↑(Set.Icc a b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_inter_le_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₁.size
-- Mathlib.Data.Tree.Basic
BinaryTree.height_le_numNodes : ∀ {α : Type u} (x : BinaryTree α), x.height ≤ x.numNodes
-- Init.Data.String.Basic
String.str_slice : ∀ {s : String} {startInclusive endExclusive : s.Pos} {h : startInclusive ≤ endExclusive},
  (s.slice startInclusive endExclusive h).str = s
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteEdges_empty : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.deleteEdges ∅ = G
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- A continuous function `f` is locally integrable with respect to any locally finite measure.  -/
Continuous.locallyIntegrable : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [SecondCountableTopologyEither X E], Continuous f → MeasureTheory.LocallyIntegrable f μ
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.nat_lt_univ : ∀ (n : ℕ), ↑n < Cardinal.univ.{u, v}
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atTop_iInf : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : CompleteLattice α]
  [InfConvergenceClass α] {f : ι → α}, Antitone f → Filter.Tendsto f Filter.atTop (nhds (⨅ i, f i))
-- Mathlib.CategoryTheory.Limits.Indization.Equalizers
/-- Suppose `F : J ⥤ I ⥤ C` is a finite diagram in the functor category `I ⥤ C`, where `I` is small
and filtered. If `i : I`, we can apply the Yoneda embedding to `F(·, i)` to obtain a
diagram of presheaves `J ⥤ Cᵒᵖ ⥤ Type v`. Suppose that the limits of this diagram is always an
ind-object.

For `j : J` we can apply the Yoneda embedding to `F(j, ·)` and take colimits to obtain a finite
diagram `J ⥤ Cᵒᵖ ⥤ Type v` (which is actually a diagram `J ⥤ Ind C`). The theorem states that
the limit of this diagram is an ind-object.

This theorem will be used to construct equalizers in the category of ind-objects. It can be
interpreted as saying that ind-objects are closed under finite limits as long as the diagram
we are taking the limit of comes from a diagram in a functor category `I ⥤ C`. We will show (TODO)
that this is the case for any parallel pair of morphisms in `Ind C` and deduce that ind-objects
are closed under equalizers.

This is Proposition 6.1.16(i) in [Kashiwara2006].
 -/
CategoryTheory.Limits.isIndObject_limit_comp_yoneda_comp_colim : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  [CategoryTheory.IsFiltered I] {J : Type} [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor I C)),
  (∀ (i : I),
      CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit ((F.flip.obj i).comp CategoryTheory.yoneda))) →
    CategoryTheory.Limits.IsIndObject
      (CategoryTheory.Limits.limit
        (F.comp
          (((CategoryTheory.Functor.whiskeringRight I C (CategoryTheory.Functor Cᵒᵖ (Type v))).obj
                CategoryTheory.yoneda).comp
            CategoryTheory.Limits.colim)))
-- Mathlib.GroupTheory.Abelianization.Defs
abelianizationCongr_symm : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (e : G ≃* H),
  e.abelianizationCongr.symm = e.symm.abelianizationCongr
-- Init.While
/-- Computational core of `repeatM`: returns the loop value paired with its
`repeatM.Pred` proof.  -/
_private.Init.While.0.repeatM.impl : {α : Type u} →
  {m : Type u → Type v} →
    [inst : Monad m] → {β : Type u} → [Nonempty β] → (f : α → m (α ⊕ β)) → (a : α) → Subtype (repeatM.Pred✝ f a)