mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SingleObj
/-- Abbreviation that allows writing `CategoryTheory.SingleObj.star` rather than
`Quiver.SingleObj.star`.
 -/
CategoryTheory.SingleObj.star : (M : Type u) → CategoryTheory.SingleObj M
-- Mathlib.Data.Set.Image
Set.rangeFactorization_coe : ∀ {β : Type u_2} {ι : Sort u_4} (f : ι → β) (a : ι), ↑(Set.rangeFactorization f a) = f a
-- Init.Data.SInt.Lemmas
Int32.sub_left_inj : ∀ {a b : Int32} (c : Int32), a - c = b - c ↔ a = b
-- Mathlib.Order.Filter.Cofinite
Filter.Tendsto.exists_forall_le : ∀ {α : Type u_2} {β : Type u_3} [Nonempty α] [inst : LinearOrder β] {f : α → β},
  Filter.Tendsto f Filter.cofinite Filter.atTop → ∃ a₀, ∀ (a : α), f a₀ ≤ f a
-- Lean.Expr
/-- `.lit l` is now the preferred form.
 -/
Lean.mkLit : Lean.Literal → Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
/-- `WithCStarModule.equiv` as a uniform equivalence between `C⋆ᵐᵒᵈ(A, E)` and `E`.  -/
WithCStarModule.uniformEquiv : {A : Type u_3} → {E : Type u_4} → [inst : UniformSpace E] → WithCStarModule A E ≃ᵤ E
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.realize_imp : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {φ ψ : L.Sentence},
  M ⊨ FirstOrder.Language.Formula.imp φ ψ ↔ M ⊨ φ → M ⊨ ψ
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Ioo_eq_of_Icc_succ_pred_eq : ∀ {m n : ℕ} {s : Finset ℕ}, Finset.Icc (m + 1) (n - 1) = s → Finset.Ioo m n = s
-- Mathlib.Analysis.InnerProductSpace.Reproducing
_private.Mathlib.Analysis.InnerProductSpace.Reproducing.0.RKHS.kernel.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V],
  RKHS.kernel H = Matrix.of fun x y => ContinuousLinearMap.adjoint (RKHS.kerFun H x) ∘SL RKHS.kerFun H y
-- Mathlib.Data.List.Infix
List.IsInfix.flatMap : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α},
  l₁ <:+: l₂ → ∀ (f : α → List β), List.flatMap f l₁ <:+: List.flatMap f l₂
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.eval₂Hom_comp_bind₂ : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (f : S →+* T) (g : σ → T) (h : R →+* MvPolynomial σ S),
  (MvPolynomial.eval₂Hom f g).comp (MvPolynomial.bind₂ h) = MvPolynomial.eval₂Hom ((MvPolynomial.eval₂Hom f g).comp h) g
-- Aesop.Search.Expansion.Norm
Aesop.NormStep.runPostSimpRules : Aesop.UnorderedArraySet Lean.MVarId → Aesop.NormStep
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.norm_precompR_le : ∀ {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Eₗ] [inst_2 : SeminormedAddCommGroup Fₗ] [inst_3 : SeminormedAddCommGroup Gₗ]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedSpace 𝕜 Eₗ]
  [inst_7 : NormedSpace 𝕜 Fₗ] [inst_8 : NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ),
  ‖ContinuousLinearMap.precompR Eₗ L‖ ≤ ‖L‖
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_map_equiv : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {β : Type u_7} [inst_6 : MeasurableSpace β] {e : X ≃ᵐ β} {f : β → E} {s : Set β},
  MeasurableSet s → ∫ᵛ (y : β) in s, f y ∂[B; μ.map ⇑e] = ∫ᵛ (x : X) in ⇑e ⁻¹' s, f (e x) ∂[B; μ]
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
/-- If `f` is a morphism of monoid objects internal to `C`,
then `f.mop` is a morphism of monoid objects internal to `Cᴹᵒᵖ`.  -/
MonObj.mop_isMonHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {N : C} [inst_3 : CategoryTheory.MonObj N] (f : M ⟶ N) [CategoryTheory.IsMonHom f],
  CategoryTheory.IsMonHom f.mop
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ),
  AlgebraicTopology.DoldKan.PInfty.f n = (AlgebraicTopology.DoldKan.P n).f n
-- Batteries.Data.List.Basic
List.Forall₂.below.nil : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  {motive : (a : List α) → (a_1 : List β) → List.Forall₂ R a a_1 → Prop}, List.Forall₂.below ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_le_maxKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {he : t ≠ ∅}, (cmp (t.maxKey he) ((t.insert k v).maxKey ⋯)).isLE = true
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_erase_bot : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (s : Finset α),
  (s.erase ⊥).sup id = s.sup id
-- Init.Grind.AC
Lean.Grind.AC.Seq.var.inj : ∀ {x x_1 : Lean.Grind.AC.Var}, Lean.Grind.AC.Seq.var x = Lean.Grind.AC.Seq.var x_1 → x = x_1
-- Mathlib.Algebra.Group.TypeTags.Basic
instIsAddTorsionFreeAdditiveOfIsMulTorsionFree : ∀ {α : Type u} [inst : Monoid α] [IsMulTorsionFree α], IsAddTorsionFree (Additive α)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.get_EStateM : ∀ {ε σ : Type u_1} {Q : Std.Do.PostCond σ (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))},
  ⦃fun s => Q.1 s s⦄ MonadStateOf.get ⦃Q⦄
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- The defining ideal.  -/
FGAlgCatSkeleton.I : {R : Type u} → [inst : CommRing R] → (self : FGAlgCatSkeleton R) → Ideal (MvPolynomial (Fin self.n) R)
-- Std.Data.HashSet.Lemmas
Std.HashSet.diff_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.diff m₂ = m₁ \ m₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_eq_getD_get? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} {fallback : β a}, m.getD a fallback = (m.get? a).getD fallback
-- Mathlib.RingTheory.WittVector.Basic
/-- `WittVector.coeff x 0` as a `RingHom`  -/
WittVector.constantCoeff : {p : ℕ} → {R : Type u_1} → [inst : CommRing R] → [inst_1 : Fact (Nat.Prime p)] → WittVector p R →+* R
-- Mathlib.MeasureTheory.Measure.Prod
/-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
Tonelli's theorem is measurable.
This version has the argument `f` in curried form.  -/
Measurable.lintegral_prod_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {f : α → β → ENNReal},
  Measurable (Function.uncurry f) → Measurable fun x => ∫⁻ (y : β), f x y ∂ν
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instLieAddGroupOfNatWithTopENat : ∀ {𝕜 : 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 : AddGroup G] [LieAddGroup I 2 G], LieAddGroup I 1 G
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_add : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b : α), ↑(a + b) = ↑a + ↑b
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- Multiplicativity of the ideal norm in number rings.  -/
cardQuot_mul : ∀ {S : Type u_1} [inst : CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] (I J : Ideal S),
  Submodule.cardQuot (I * J) = Submodule.cardQuot I * Submodule.cardQuot J
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.ScopedEntries.mk.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β] (map : Lean.SMap Lean.Name (Lean.PArray β)), sizeOf { map := map } = 1 + sizeOf map
-- Mathlib.RingTheory.LocalProperties.Basic
/-- An ideal is trivial if its localization at every maximal ideal is trivial.  -/
ideal_eq_bot_of_localization' : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R),
  (∀ (J : Ideal R) (x : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥) → I = ⊥
-- Mathlib.Data.Fin.VecNotation
Matrix.head_fin_const : ∀ {α : Type u} {n : ℕ} (a : α), (Matrix.vecHead fun x => a) = a
-- Mathlib.CategoryTheory.Quotient
/-- The quotient of a groupoid is a groupoid.  -/
CategoryTheory.Quotient.groupoid : {G : Type u_2} →
  [inst : CategoryTheory.Groupoid G] → (r : HomRel G) → CategoryTheory.Groupoid (CategoryTheory.Quotient r)
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_mul_mem_unitary : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] (A : E) {U : E},
  U ∈ unitary E → ‖A * U‖ = ‖A‖
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mem_commonNeighbors : ∀ {V : Type u} (G : SimpleGraph V) {u v w : V}, u ∈ G.commonNeighbors v w ↔ G.Adj v u ∧ G.Adj w u
-- Lean.Meta.Basic
/-- `resultDeps` contains the function result type backwards dependencies.
That is, the (0-indexed) position of parameters that the result type depends on.
 -/
Lean.Meta.FunInfo.resultDeps : Lean.Meta.FunInfo → Array ℕ
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is convex on `S` and differentiable within `S` at `x`, then the slope of any
secant line with left endpoint at `x` is bounded below by the derivative of `f` within `S` at `x`.

This is fractionally weaker than `ConvexOn.le_slope_of_hasDerivWithinAt_Ioi` but simpler to apply
under a `DifferentiableOn S` hypothesis.  -/
ConvexOn.le_slope_of_hasDerivWithinAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S x → f' ≤ slope f x y
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.prodEquiv_symm_apply_fst : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  (f : ContinuousMultilinearMap R M₁ (M₂ × M₃)),
  (ContinuousMultilinearMap.prodEquiv.symm f).1 = (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f
-- Init.Data.UInt.Basic
/-- Decides whether one 64-bit unsigned integer is less than or equal to another. Usually accessed via the
`DecidableLE UInt64` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (15 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : UInt64) ≤ 5 then "yes" else "no") = "no"`
 * `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
 * `show (7 : UInt64) ≤ 7 by decide`
 -/
UInt64.decLe : (a b : UInt64) → Decidable (a ≤ b)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.uniqueDiffOn_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n),
  n ≠ 0 → ∀ {s : Set E}, UniqueDiffOn 𝕜 (⇑h '' s) ↔ UniqueDiffOn 𝕜 s
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.symm_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (h : Homotopy f g) (i j : ι),
  h.symm.hom i j = -h.hom i j
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- The covering number of the image of a set under an injective isometry is equal to
the covering number of the set.
See `Isometry.coveringNumber_image` for the version in an `EMetricSpace`, in which injectivity is
a consequence of being an isometry.  -/
Isometry.coveringNumber_image' : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {A : Set X} {ε : NNReal}
  {f : X → Y}, Isometry f → Set.InjOn f A → Metric.coveringNumber ε (f '' A) = Metric.coveringNumber ε A
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey! k = t₂.getKey! k
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_one : ∀ (n : ℕ), Nat.digits 1 n = List.replicate n 1
-- Init.Data.UInt.Lemmas
UInt32.sub_right_inj : ∀ {a b : UInt32} (c : UInt32), c - a = c - b ↔ a = b
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.hasSheafify_of_isEquivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasSheafify J A]
  [CategoryTheory.Limits.HasFiniteLimits A], CategoryTheory.HasSheafify K A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.DTreeMap.Raw.filter f t} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).getKey k h' = t.getKey k ⋯
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeId_inv_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (X : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Cone.postcomposeId.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.invertible_iff_generator_nonzero : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [inst_5 : (↑I).IsPrincipal],
  I * I⁻¹ = 1 ↔ Submodule.IsPrincipal.generator ↑I ≠ 0
-- Lean.Parser.Command
Lean.Parser.Command.computedField.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasDerivAtFilter.hasGradientAtFilter' : ∀ {g : ℝ → ℝ} {g' u : ℝ} {L' : Filter ℝ}, HasDerivAtFilter g g' (L' ×ˢ pure u) → HasGradientAtFilter g g' u L'
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast? a (Std.Internal.List.eraseKey k l) =
      if (k == a) = true then none else Std.Internal.List.getValueCast? a l
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Any discrete space is a charted space over a singleton set.
We keep this as a definition (not an instance) to avoid instance search trying to search for
`DiscreteTopology` or `Unique` instances.
 -/
ChartedSpace.ofDiscreteTopology : {H : Type u} →
  {M : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace H] → [DiscreteTopology M] → [h : Unique H] → ChartedSpace H M
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instSingleton : {α : Type u} → {cmp : α → α → Ordering} → Singleton α (Std.TreeSet.Raw α cmp)
-- Init.Data.Array.Monadic
Array.map_toList_inj : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {xs ys : m (Array α)},
  Array.toList <$> xs = Array.toList <$> ys ↔ xs = ys
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherianRing_rangeS : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S) [IsNoetherianRing R],
  IsNoetherianRing ↥f.rangeS
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- The resolution maps intertwine the descent of a morphism and that morphism.  -/
CategoryTheory.InjectiveResolution.desc_commutes : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Z ⟶ Y)
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp J.ι (CategoryTheory.InjectiveResolution.desc f I J) =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) I.ι
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mul_mem_left : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x y : R), y ∈ I → x * y ∈ I
-- Mathlib.Algebra.Algebra.Tower
Algebra.lsmul_apply : ∀ (R : Type u) {A : Type w} (B : Type u₁) (M : Type v₁) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M] [inst_6 : Module R M]
  [inst_7 : Module A M] [inst_8 : Module B M] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (a : A) (m : M), ((Algebra.lsmul R B M) a) m = a • m
-- Mathlib.Algebra.DirectSum.Module
/-- If a collection of submodules has just two indices, `i` and `j`, then
`DirectSum.IsInternal` is equivalent to `isCompl`.  -/
DirectSum.isInternal_submodule_iff_isCompl : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] (A : ι → Submodule R M) {i j : ι},
  i ≠ j → Set.univ = {i, j} → (DirectSum.IsInternal A ↔ IsCompl (A i) (A j))
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.SMulBracketCommClass.mk : ∀ {S : Type u_4} {L : Type u_5} {α : Type u_6} [inst : SMul S α] [inst_1 : LieRing L] [inst_2 : AddCommGroup α]
  [inst_3 : LieRingModule L α],
  (∀ (s : S) (l : L) (a : α), s • ⁅l, a⁆ = ⁅l, s • a⁆) → LieDerivation.SMulBracketCommClass S L α
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Icc_left_eq_Icc_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  Order.pred a ≤ b → insert (Order.pred a) (Set.Icc a b) = Set.Icc (Order.pred a) b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → (↑m).toArray.isEmpty = (↑m).isEmpty
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.decidableLT.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α} [inst_3 : DecidableLT α] (a b : AddLocalization s),
  a.decidableLT b = a.recOnSubsingleton₂ b fun x x_1 x_2 x_3 => decidable_of_iff' (↑x_3 + x < ↑x_2 + x_1) ⋯
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.toGaloisInsertion.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (gc : GaloisConnection l u) (h : ∀ (b : β), b ≤ l (u b)),
  gc.toGaloisInsertion h = { choice := fun x x_1 => l x, gc := gc, le_l_u := h, choice_eq := ⋯ }
-- Mathlib.Order.KrullDimension
Order.height_le_krullDim : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑(Order.height a) ≤ Order.krullDim α
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows : ∀ {X : AlgebraicGeometry.Scheme} (U : X.AffineZariskiSite) (s : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))),
  U.presieveOfSections s = CategoryTheory.Presieve.ofArrows (fun i => U.basicOpen ↑i) fun i => CategoryTheory.homOfLE ⋯
-- Mathlib.Logic.Embedding.Basic
/-- Transfer an embedding along a pair of equivalences.  -/
Function.Embedding.congr : {α : Sort u} → {β : Sort v} → {γ : Sort w} → {δ : Sort x} → α ≃ β → γ ≃ δ → (α ↪ γ) → β ↪ δ
-- Mathlib.Order.Filter.AtTopBot.ModEq
/-- Infinitely many natural numbers are equal to `d` mod `n`.  -/
Nat.frequently_modEq : ∀ {n : ℕ}, n ≠ 0 → ∀ (d : ℕ), ∃ᶠ (m : ℕ) in Filter.atTop, m ≡ d [MOD n]
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Functor.reflectsLimits_of_isEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : CategoryTheory.Functor D C) [E.IsEquivalence],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.withNewMutableVars : {α : Type} → Array Lean.Elab.Term.Do.Var → Bool → Lean.Elab.Term.Do.ToCodeBlock.M α → Lean.Elab.Term.Do.ToCodeBlock.M α
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_eq : ∀ {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ : Ω → ℕ∞} [inst : AddCommMonoid β] (n : ℕ),
  MeasureTheory.stoppedProcess u τ n =
    {a | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range n, {ω | τ ω = ↑i}.indicator (u i)
-- Mathlib.CategoryTheory.Noetherian
CategoryTheory.Artinian.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [toEssentiallySmall : CategoryTheory.EssentiallySmall.{u_2, v_1, u_1} C],
  (∀ (X : C), CategoryTheory.IsArtinianObject X) → CategoryTheory.Artinian C
-- Mathlib.Data.Nat.Cast.Order.Ring
Nat.cast_eq_neg_cast : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] {m n : ℕ}, ↑m = -↑n ↔ m = 0 ∧ n = 0
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- Given `E` and `F` two topological vector spaces and `𝔖 : Set (Set E)`, then
`UniformConvergenceCLM σ F 𝔖` (denoted `E →SLᵤ[σ, 𝔖] F`) is a type synonym of `E →SL[σ] F` equipped
with the "topology of uniform convergence on the elements of `𝔖`".

If the continuous linear image of any element of `𝔖` is bounded, this makes `E →SL[σ] F` a
topological vector space.  -/
UniformConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [Module 𝕜₁ E] →
                  [TopologicalSpace E] →
                    [inst : AddCommGroup F] → [Module 𝕜₂ F] → [TopologicalSpace F] → Set (Set E) → Type (max u_3 u_4)
-- Batteries.Data.String.Lemmas
/-- A string position is valid if it is equal to the UTF-8 length of an initial substring of `s`.  -/
String.Pos.Raw.Valid : String → String.Pos.Raw → Prop
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withLetBody : {α : Type} →
  [Inhabited α] →
    {m : Type → Type} →
      [Monad m] →
        [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → [MonadControlT Lean.MetaM m] → m α → m α
-- Mathlib.Algebra.Ring.BooleanRing
BoundedLatticeHom.asBoolRing_id : ∀ {α : Type u_1} [inst : BooleanAlgebra α], (BoundedLatticeHom.id α).asBoolRing = RingHom.id (AsBoolRing α)
-- Mathlib.CategoryTheory.Comma.Basic
/-- The canonical functor from `Comma L.op R.op` to `(Comma R L)ᵒᵖ`.  -/
CategoryTheory.Comma.unopFunctor : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                CategoryTheory.Functor (CategoryTheory.Comma L.op R.op) (CategoryTheory.Comma R L)ᵒᵖ
-- Init.Try
/-- Helper internal tactic for implementing the tactic `try?` with parallel execution, returning first success.  -/
Lean.Parser.Tactic.firstPar : Lean.ParserDescr