mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Notation
/-- Defines a syntax for date-only values. The input string represents a date in formats like "YYYY-MM-DD".

Example:
`date("2024-10-13")`
 -/
Std.Time.«termDate(_)» : Lean.ParserDescr
-- Mathlib.Data.Complex.Basic
/-- A complex number `z` plus its conjugate `conj z` is `2` times its real part.  -/
Complex.re_eq_add_conj : ∀ (z : ℂ), ↑z.re = (z + (starRingEnd ℂ) z) / 2
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The restriction natural transformation on presheaves of modules, considered as linear maps
to restriction of scalars.  -/
PresheafOfModules.restriction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (R : CategoryTheory.Functor Cᵒᵖ RingCat) →
      {X Y : Cᵒᵖ} →
        (f : X ⟶ Y) →
          PresheafOfModules.evaluation R X ⟶
            (PresheafOfModules.evaluation R Y).comp (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.Finite.toFiniteType : ∀ {X : Type u_1} {inst : TopologicalSpace X} {C D : Set X} {inst_1 : Topology.RelCWComplex C D}
  [self : Topology.RelCWComplex.Finite C], Topology.RelCWComplex.FiniteType C
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
instNonUnitalNonAssocRingCommutatorRing : (L : Type v) → [LieRing L] → NonUnitalNonAssocRing (CommutatorRing L)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.exists_isFragment : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K < 1 → S.Nonempty → ∃ A, Finset.IsFragment✝ K S A
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k : α},
      Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l) k =
        if k ∈ m ∨ l.contains k = true then some () else none
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
/-- Let `m` be a sub-σ-algebra of `m0`, `f` an `m0`-measurable function and `g` an `m`-measurable
function, such that their integrals coincide on `m`-measurable sets with finite measure.
Then `∫ x in s, ‖g x‖ ∂μ ≤ ∫ x in s, ‖f x‖ ∂μ` on all `m`-measurable sets with finite measure.  -/
MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  m ≤ m0 →
    ∀ {f g : α → ℝ},
      MeasureTheory.StronglyMeasurable f →
        MeasureTheory.IntegrableOn f s μ →
          MeasureTheory.StronglyMeasurable g →
            MeasureTheory.IntegrableOn g s μ →
              (∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ) →
                MeasurableSet s → μ s ≠ ⊤ → ∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_intCast : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (z : ℤ), CauSeq.Completion.ofRat ↑z = ↑z
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey! k = default
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U)
  (V : TopCat.Presheaf.SheafCondition.OpensLeCover U),
  ((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.left = V.obj
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂},
  Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful → Φ.IsLocalizedFullyFaithful
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
intervalIntegral.integral_deriv_smul_deriv_comp : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g g' : ℝ → E}
  [CompleteSpace E],
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivAt g (g' (f x)) (f x)) →
      ContinuousOn f' (Set.uIcc a b) → Continuous g' → ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
-- Mathlib.Algebra.Algebra.Defs
Algebra.compHom_algebraMap_apply : ∀ {R : Type u} {S : Type v} (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (f : S →+* R) (s : S), (algebraMap S A) s = (algebraMap R A) (f s)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- An additive equivalence between commutative additive groups is a linear
equivalence between ℤ-modules  -/
AddEquiv.toIntLinearEquiv : {M : Type u_5} →
  {M₂ : Type u_7} →
    [inst : AddCommGroup M] →
      [inst_1 : AddCommGroup M₂] → {modM : Module ℤ M} → {modM₂ : Module ℤ M₂} → M ≃+ M₂ → M ≃ₗ[ℤ] M₂
-- Mathlib.NumberTheory.LucasLehmer
/-- If `2^p - 1` is prime then the Lucas-Lehmer test holds, `s (p - 2) % (2^p - 1) = 0`.  -/
lucas_lehmer_necessity : ∀ (p : ℕ), 3 ≤ p → Nat.Prime (mersenne p) → LucasLehmerTest p
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_comm_le : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G), ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆
-- Mathlib.CategoryTheory.Center.Basic
/-- The center of a category `C` is the type `End (𝟭 C)` of the endomorphisms
of the identify functor of `C`.  -/
CategoryTheory.CatCenter : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_mul_eq_smul : ∀ {R : Type u_1} {a b : R} [inst : NonUnitalNonAssocSemiring R] (r : R) (x : QuadraticAlgebra R a b),
  QuadraticAlgebra.C r * x = r • x
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the reverse direction of `hasFDerivAtFilter_iff_isLittleO`. -/
HasFDerivAtFilter.of_isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)},
  ((fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[L] fun p => p.1 - p.2) → HasFDerivAtFilter f f' L
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An extensionality lemma in terms of the coercion to a pi-type.
We prove this explicitly rather than deriving it so that it is in terms of the coercion rather than
the projection `.sieves`.
 -/
CategoryTheory.GrothendieckTopology.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
  ⇑J₁ = ⇑J₂ → J₁ = J₂
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Determine whether the explicit parts of two expressions are equal,
and the implicit parts are definitionally equal, up to `reducible_and_instances` transparency.
This says whether two expressions are 'morally equal', and is used for deduplicating suggestions.  -/
Mathlib.Tactic.ClickSuggestions.isExplicitEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.AnchorRef.mk.inj : ∀ {numDigits : ℕ} {anchorPrefix : UInt64} {numDigits_1 : ℕ} {anchorPrefix_1 : UInt64},
  { numDigits := numDigits, anchorPrefix := anchorPrefix } =
      { numDigits := numDigits_1, anchorPrefix := anchorPrefix_1 } →
    numDigits = numDigits_1 ∧ anchorPrefix = anchorPrefix_1
-- Mathlib.Data.ZMod.QuotientGroup
/-- The orbit `(a ^ ℤ) • b` is a cycle of order `minimalPeriod ((•) a) b`.  -/
MulAction.orbitZPowersEquiv : {α : Type u_3} →
  {β : Type u_4} →
    [inst : Group α] →
      (a : α) →
        [inst_1 : MulAction α β] →
          (b : β) → ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b) ≃ ZMod (Function.minimalPeriod (fun x => a • x) b)
-- Mathlib.NumberTheory.ZetaValues
hasSum_one_div_nat_pow_mul_sin : ∀ {k : ℕ},
  k ≠ 0 →
    ∀ {x : ℝ},
      x ∈ Set.Icc 0 1 →
        HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * Real.pi * ↑n * x))
          ((-1) ^ (k + 1) * (2 * Real.pi) ^ (2 * k + 1) / 2 / ↑(2 * k + 1).factorial *
            Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
-- Mathlib.RingTheory.Unramified.Locus
Algebra.IsUnramifiedAt.of_restrictScalars : ∀ (R : Type u_1) {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] (P : Ideal B)
  [inst_7 : P.IsPrime] [Algebra.IsUnramifiedAt R P], Algebra.IsUnramifiedAt A P
-- Mathlib.Data.Fintype.Inv
Function.Injective.right_inv_of_invOfMemRange : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β} (hf : Function.Injective f)
  (a : α), hf.invOfMemRange ⟨f a, ⋯⟩ = a
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_dfinsuppProd : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Add M] [inst_2 : CommMonoid M]
  [inst_3 : (i : ι) → Zero (β i)] [inst_4 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : RingCon M)
  (h : (i : ι) → β i → M) (f : Π₀ (i : ι), β i), ↑(f.prod h) = f.prod fun i b => ↑(h i b)
-- Std.Data.TreeMap.Basic
Std.TreeMap.instInter : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Inter (Std.TreeMap α β cmp)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a fallback : α}, m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coe_mapRingHom : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S), ⇑(MonoidAlgebra.mapRingHom M f) = MonoidAlgebra.map ↑f
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipWithTR.go.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (a : α) (as : List α)
  (b : β) (bs : List β) (acc : Array γ)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc)
  (h_2 : (x : List α) → (x_1 : List β) → (acc : Array γ) → motive x x_1 acc),
  (match a :: as, b :: bs, acc with
    | a :: as, b :: bs, acc => h_1 a as b bs acc
    | x, x_1, acc => h_2 x x_1 acc) =
    h_1 a as b bs acc
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_insert : ∀ {X : Type u_2} {s : Set X} {x : X} [inst : PseudoEMetricSpace X],
  Metric.ediam (insert x s) = max (⨆ y ∈ s, edist x y) (Metric.ediam s)
-- Mathlib.NumberTheory.ModularForms.SlashActions
/-- `SlashAction` induced by a monoid homomorphism.  -/
monoidHomSlashAction : {β : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      {α : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : AddMonoid α] → [inst_2 : Monoid H] → [SlashAction β G α] → (H →* G) → SlashAction β H α
-- Init.Data.Option.List
Option.toList_join : ∀ {α : Type u_1} {o : Option (Option α)}, o.join.toList = List.flatMap Option.toList o.toList
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.ofHom_hom : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)}
  {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} [self : CategoryTheory.ConcreteCategory C FC]
  {X Y : C} (f : X ⟶ Y), CategoryTheory.ConcreteCategory.ofHom (CategoryTheory.ConcreteCategory.hom f) = f
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.toNF.match_1.splitter : {v : Lean.Level} →
  {M : Q(Type v)} →
    (motive : (ℤ × Q(«$M»)) × ℕ → Sort u_1) →
      (x : (ℤ × Q(«$M»)) × ℕ) → ((a : ℤ) → (x : Q(«$M»)) → (snd : ℕ) → motive ((a, x), snd)) → motive x
-- Mathlib.RingTheory.HahnSeries.Cardinal
/-- The cardinality of the support of a Hahn series.  -/
HahnSeries.cardSupp : {Γ : Type u_1} → {R : Type u_2} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → HahnSeries Γ R → Cardinal.{u_1}
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_comp_self : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ⇑e.symm ∘ ⇑e = id
-- Mathlib.Topology.Algebra.Module.Basic
LinearMap.continuous_on_pi : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Finite ι] [inst : Semiring R] [inst_1 : TopologicalSpace R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M]
  (f : (ι → R) →ₗ[R] M), Continuous ⇑f
-- Mathlib.Tactic.DeprecateTo
/-- Writing
```lean
deprecate to new_name new_name₂ ... new_nameₙ
theorem old_name : True := .intro
```
where `new_name new_name₂ ... new_nameₙ` is a sequence of identifiers produces the
`Try this` suggestion:
```lean
theorem new_name : True := .intro

@[deprecated (since := "YYYY-MM-DD")] alias old_name := new_name

@[deprecated (since := "YYYY-MM-DD")] alias old_name₂ := new_name₂
...

@[deprecated (since := "YYYY-MM-DD")] alias old_nameₙ := new_nameₙ
```
where `old_name old_name₂ ... old_nameₙ` are the non-blacklisted declarations
(auto)generated by the initial command.

The "YYYY-MM-DD" entry is today's date and it is automatically filled in.

`deprecate to` makes an effort to match `old_name`, the "visible" name, with
`new_name`, the first identifier produced by the user.
The "old", autogenerated declarations `old_name₂ ... old_nameₙ` are retrieved in alphabetical order.
In the case in which the initial declaration produces at most 1 non-blacklisted
declarations besides itself, the alphabetical sorting is irrelevant.

Technically, the command also take an optional `String` argument to fill in the date in `since`.
However, its use is mostly intended for debugging purposes, where having a variable date would
make tests time-dependent.
 -/
Mathlib.Tactic.DeprecateTo.commandDeprecateTo______ : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
`x * M`.  -/
QuotientGroup.groupSeminorm : {M : Type u_1} → [inst : SeminormedCommGroup M] → {S : Subgroup M} → GroupSeminorm (M ⧸ S)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.HomogeneousLocalization.awayMapAux.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {f x : A} (hx : f ∣ x),
  HomogeneousLocalization.awayMapAux✝ 𝒜 hx = HomogeneousLocalization.awayMapAux✝ 𝒜 hx
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D) {y z : C} (f : y ≅ z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f.inv)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f.hom) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.isIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂),
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.τ₁ ∧ CategoryTheory.IsIso f.τ₂ ∧ CategoryTheory.IsIso f.τ₃
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.Gamma_conj : ∀ (s : ℂ), Complex.Gamma ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Complex.Gamma s)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_some_getD_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α} {fallback : β},
  m.contains a = true → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.getD m a fallback)
-- Mathlib.GroupTheory.Index
/-- If `J` has finite index in `K`, then `J ⊓ L` has finite index in `K ⊓ L` for any `L`.  -/
Subgroup.relIndex_inter_ne_zero : ∀ {G : Type u_1} [inst : Group G] {J K : Subgroup G},
  J.relIndex K ≠ 0 → ∀ (L : Subgroup G), (J ⊓ L).relIndex (K ⊓ L) ≠ 0
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuousWithinAt.inf : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α} {a : α},
  UpperSemicontinuousWithinAt f s a →
    UpperSemicontinuousWithinAt g s a → UpperSemicontinuousWithinAt (fun x => min (f x) (g x)) s a
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The universal property of the direct limit: maps from the components to another
NonUnitalNonAsssocSemiRing that respect the directed system structure
(i.e. make some diagram commute) give rise to a unique map out of the direct limit.
 -/
DirectLimit.NonUnitalRing.lift : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)] →
                  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                    [inst_6 : Nonempty ι] →
                      (P : Type u_7) →
                        [inst_7 : NonUnitalNonAssocSemiring P] →
                          (g : (i : ι) → G i →ₙ+* P) →
                            (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                              DirectLimit G f →ₙ+* P
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.ker_mapRingHom : ∀ {R : Type u} {S : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring S] (f : R →+* S),
  RingHom.ker (Polynomial.mapRingHom f) = Ideal.map Polynomial.C (RingHom.ker f)
-- Mathlib.Algebra.Category.ModuleCat.Subobject
ModuleCat.toKernelSubobject.eq_1 : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {f : M ⟶ N},
  ModuleCat.toKernelSubobject =
    ModuleCat.Hom.hom (CategoryTheory.Limits.kernelSubobjectIso f ≪≫ ModuleCat.kernelIsoKer f).inv
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.congr_arg : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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 : M →ₛₗ[σ] M₃} {x x' : M}, x = x' → f x = f x'
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.norm_seminormedAddCommGroupToProd : ∀ (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : α × β), ‖x‖ = ‖WithLp.toLp p x‖
-- Mathlib.RingTheory.WittVector.InitTail
/-- The polynomial that witnesses that `WittVector.select` is a polynomial function.
`selectPoly n` is `X n` if `P n` holds, and `0` otherwise.  -/
WittVector.selectPoly : (ℕ → Prop) → ℕ → MvPolynomial ℕ ℤ
-- Mathlib.Data.List.Basic
List.map_injective_iff : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective (List.map f) ↔ Function.Injective f
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyι_comp_fromOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp S.rightHomologyι S.fromOpcycles = 0
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_ite_zero : ∀ {M : Type u_1} {A : Type u_7} [inst : Zero A] [inst_1 : SMulZeroClass M A] (p : Prop) [inst_2 : Decidable p] (a : M)
  (b : A), (a • if p then b else 0) = if p then a • b else 0
-- Init.Data.Range.Polymorphic.UInt
UInt8.succ?_ofBitVec : ∀ {x : BitVec 8}, Std.PRange.succ? { toBitVec := x } = UInt8.ofBitVec <$> Std.PRange.succ? x
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalNonAssocRing : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → [Mul M] → NonUnitalNonAssocRing (MonoidAlgebra R M)
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_le_of_dvd : ∀ {n m : ℕ}, 2 ≤ m → m ∣ n → n.minFac ≤ m
-- Mathlib.Computability.RegularExpressions
RegularExpression.instInhabited : {α : Type u_1} → Inhabited (RegularExpression α)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y Z : C} (p : X = Y)
  (q : Y = Z) (x : F.obj X),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom q)))
      ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom p))) x) =
    (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) x
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
  (fun x => |u x|) =O[l] g ↔ u =O[l] g
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.sum_le_lift_mk_mul_iSup_lift : ∀ {ι : Type u} (f : ι → Cardinal.{v}),
  Cardinal.sum f ≤ Cardinal.lift.{v, u} (Cardinal.mk ι) * ⨆ i, Cardinal.lift.{u, v} (f i)
-- Mathlib.GroupTheory.OrderOfElement
finEquivPowers_apply : ∀ {G : Type u_1} [inst : Monoid G] {x : G} (hx : IsOfFinOrder x) {n : Fin (orderOf x)},
  (finEquivPowers hx) n = ⟨x ^ ↑n, ⋯⟩
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.union : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Analysis.Calculus.VectorField
/-- The pullback of a vector field under a function, defined
as `(f^* V) (x) = Df(x)^{-1} (V (f x))`. If `Df(x)` is not invertible, we use the junk value `0`.
 -/
VectorField.pullback : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → (F → F) → E → E
-- Mathlib.Data.Fin.Fin2
Fin2.rev_involutive : ∀ {n : ℕ}, Function.Involutive Fin2.rev
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.instIsSemitopologicalRing : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [IsSemitopologicalRing A] (s : NonUnitalSubalgebra R A), IsSemitopologicalRing ↥s
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mk : {ι : Type u_2} → (lower upper : ι → ℝ) → (∀ (i : ι), lower i < upper i) → BoxIntegral.Box ι
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.not_nhds_le_map : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α}
  [inst_2 : TopologicalSpace β],
  IsLocalExtrOn f s a →
    ∀ [(nhdsWithin (f a) (Set.Iio (f a))).NeBot] [(nhdsWithin (f a) (Set.Ioi (f a))).NeBot],
      ¬nhds (f a) ≤ Filter.map f (nhdsWithin a s)