mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Config
Lean.Grind.NoopConfig.mk : Lean.Grind.Config → Lean.Grind.NoopConfig
-- Mathlib.RingTheory.Ideal.Operations
/-- If `x` is an `I`-multiple of the submodule spanned by `f '' s`,
then we can write `x` as an `I`-linear combination of the elements of `f '' s`.  -/
Submodule.mem_ideal_smul_span_iff_exists_sum : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (I : Ideal R)
  [I.IsTwoSided] {ι : Type u_4} (f : ι → M) (x : M),
  x ∈ I • Submodule.span R (Set.range f) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_left_strictMono : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddRightStrictMono α] {a : α}, StrictMono fun x => x + a
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.finInsepDegree_top : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Field.finInsepDegree F ↥⊤ = Field.finInsepDegree F K
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_same_then' : ∀ (c t e : Bool), (t == bif c then t else e) = (c || t == e)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isSome_get?_eq_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α},
  (Std.DTreeMap.Const.get? t a).isSome = t.contains a
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_ne_zero : ∀ {α : Type u_1}, Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_real_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.norm x ≠ 0 →
    ∀ {c : ℝ}, c ≠ 0 → NumberField.mixedEmbedding.logMap (c • x) = NumberField.mixedEmbedding.logMap x
-- Mathlib.NumberTheory.Divisors
Nat.prodMk_mem_divisorsAntidiag : ∀ {n x y : ℕ}, n ≠ 0 → ((x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n)
-- Mathlib.Topology.Constructions
isQuotientMap_quotient_mk' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Setoid X}, Topology.IsQuotientMap Quotient.mk'
-- Mathlib.Data.Finsupp.Basic
Finsupp.domCongr_symm : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (e : α ≃ β),
  (Finsupp.domCongr e).symm = Finsupp.domCongr e.symm
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.two_lt_pointCount : ∀ (P : Type u_1) {L : Type u_2} [inst : Membership P L] [Configuration.ProjectivePlane P L] [Finite P] [Finite L]
  (l : L), 2 < Configuration.pointCount P l
-- Init.Data.Option.Lemmas
Option.pmap_some : ∀ {α : Type u_1} {β : Type u_2} {a : α} {p : α → Prop} {f : (a : α) → p a → β}
  {h : ∀ (a_1 : α), some a = some a_1 → p a_1}, Option.pmap f (some a) h = some (f a ⋯)
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  {inst_1 : CategoryTheory.Category.{v', u'} A} {FA : A → A → Type u_1} {CA : A → Type w'}
  {inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)} {inst_3 : CategoryTheory.ConcreteCategory A FA}
  [self : J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y),
  J.W f ↔ CategoryTheory.Presheaf.IsLocallyInjective J f ∧ CategoryTheory.Presheaf.IsLocallySurjective J f
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isHyperbolic_neg_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R},
  (-m).IsHyperbolic ↔ m.IsHyperbolic
-- Mathlib.Order.Minimal
/-- **Alias** of the forward direction of `not_minimal_iff_exists_lt`. -/
exists_lt_of_not_minimal : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : Preorder α], P x → ¬Minimal P x → ∃ y < x, P y
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.RespectsIso],
  (∀ ⦃X Y : C⦄ ⦃f : X ⟶ Y⦄ ⦃R : CategoryTheory.Presieve Y⦄,
      R ∈ K.coverings Y →
        (P f ↔
          ∀ {U : C} (g : U ⟶ Y) [inst_2 : CategoryTheory.Limits.HasPullback f g],
            R g → P (CategoryTheory.Limits.pullback.snd f g))) →
    P.IsLocalAtTarget K
-- Init.Data.Option.Lemmas
Option.pfilter_join : ∀ {α : Type u_1} {o : Option (Option α)} {p : (a : α) → o.join = some a → Bool},
  o.join.pfilter p = (o.pfilter fun o' h => o'.pelim false fun a ha => p a ⋯).join
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} (s : CategoryTheory.Limits.CokernelCofork f),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Cofork.π s) = 0
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The iterated derivative within a set of the composition with a linear equiv on the right is
obtained by composing the iterated derivative with the linear equiv.  -/
ContinuousLinearEquiv.iteratedFDerivWithin_comp_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} (g : G ≃L[𝕜] E) (f : E → F),
  UniqueDiffOn 𝕜 s →
    ∀ {x : G},
      g x ∈ s →
        ∀ (i : ℕ),
          iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
            (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
-- Lean.Meta.ArgsPacker
/-- Unpacks a mutually packed argument created with `Mutual.mk` returning the
argument and function index.

Throws an error if the expression is not of that form.
 -/
Lean.Meta.ArgsPacker.Mutual.unpack : ℕ → Lean.Expr → Option (ℕ × Lean.Expr)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.match : Lean.Option Bool
-- Mathlib.Probability.Kernel.Composition.CompProd
/-- Lebesgue integral against the composition-product of two kernels.  -/
ProbabilityTheory.Kernel.lintegral_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal},
  Measurable f → ∫⁻ (bc : β × γ), f bc ∂(κ.compProd η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) ∂η (a, b) ∂κ a
-- Mathlib.CategoryTheory.Shift.Localization
/-- The localization functor `W.Q' : C ⥤ W.Localization'` is compatible with the shift.  -/
CategoryTheory.MorphismProperty.commShift_Q' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (A : Type w) →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] →
            [inst_3 : W.IsCompatibleWithShift A] → [inst_4 : W.HasLocalization] → W.Q'.CommShift A
-- Init.Data.SInt.Bitwise
instCommutativeInt32HOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instIsZeroApplyForall : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂], IsZeroApply (MultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- A finite place of a number field `K` is a place associated to an embedding into a completion
with respect to a maximal ideal.  -/
NumberField.FinitePlace : (K : Type u_3) → [inst : Field K] → [NumberField K] → Type (max 0 u_3)
-- Mathlib.Algebra.Group.Units.Equiv
AddEquiv.neg_apply : ∀ (G : Type u_6) [inst : SubtractionCommMonoid G] (a : G), (AddEquiv.neg G) a = -a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- The supremum of an intersection of two sets is bounded by the minimum of the suprema of each
set, if all sets are bounded above and nonempty.  -/
csSup_inter_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  BddAbove s → BddAbove t → (s ∩ t).Nonempty → sSup (s ∩ t) ≤ sSup s ⊓ sSup t
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rco_eq_add : ∀ {m n i : ℕ}, i < n - m → (m...n).toList[i]! = m + i
-- Mathlib.Order.BooleanAlgebra.Basic
/-- Pullback a `GeneralizedBooleanAlgebra` along an injection.  -/
Function.Injective.generalizedBooleanAlgebra : {α : Type u} →
  {β : Type u_1} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : Bot α] →
              [inst_5 : SDiff α] →
                [inst_6 : GeneralizedBooleanAlgebra β] →
                  (f : α → β) →
                    Function.Injective f →
                      (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                        (∀ {x y : α}, f x < f y ↔ x < y) →
                          (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                            (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                              f ⊥ = ⊥ → (∀ (a b : α), f (a \ b) = f a \ f b) → GeneralizedBooleanAlgebra α
-- Lean.Structure
/-- Gets information for all the parents that appear in the `extends` clause.  -/
Lean.getStructureParentInfo : Lean.Environment → Lean.Name → Array Lean.StructureParentInfo
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hom_ext_iff : ∀ {X Y : BoolAlg} {f g : X ⟶ Y}, f = g ↔ BoolAlg.Hom.hom f = BoolAlg.Hom.hom g
-- Mathlib.Combinatorics.Enumerative.Composition
/-- When one splits a list along a composition `c`, the lengths of the sublists thus created are
given by the block sizes in `c`.  -/
List.map_length_splitWrtComposition : ∀ {α : Type u_1} (l : List α) (c : Composition l.length), List.map List.length (l.splitWrtComposition c) = c.blocks
-- Mathlib.Algebra.Group.Hom.Defs
/-- Additive group homomorphisms preserve integer scaling.  -/
map_zsmul : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
  [inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (n : ℤ) (g : G), f (n • g) = n • f g
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (x : R),
  (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'
-- Mathlib.Analysis.Real.Hyperreal
Filter.hyperfilter.congr_simp : ∀ (α : Type u) [inst : Infinite α], Filter.hyperfilter α = Filter.hyperfilter α
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
right_le_lineMap_iff_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r : k}, r < 1 → (b ≤ (AffineMap.lineMap a b) r ↔ b ≤ a)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.denote_toPoly_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (e : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Poly.denote ctx e.toPoly_nc = Lean.Grind.CommRing.Expr.denote ctx e
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
/-- For a spectral object indexed by a preorder, this is the isomorphism
`E^{n₁}(i₀ ≤ i₁ ≤ i₂ ≤ i₃) ≅ E^{n₁}(i₀ ≤ i₁ ≤ i₂ ≤ i₄)`
when `H^{n₁-1}(i₃ ≤ i₄)` is a zero object.  -/
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃' : {C : Type u_1} →
  {ι' : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : Preorder ι'] →
          (X' : CategoryTheory.Abelian.SpectralObject C ι') →
            (i₀ i₁ i₂ i₃ i₄ : ι') →
              (hi₀₁ : i₀ ≤ i₁) →
                (hi₁₂ : i₁ ≤ i₂) →
                  (hi₂₃ : i₂ ≤ i₃) →
                    (hi₃₄ : i₃ ≤ i₄) →
                      (n₀ n₁ n₂ : ℤ) →
                        CategoryTheory.Limits.IsZero
                            ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₃₄))) →
                          (hn₁ :
                              autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃'._auto_1) →
                            (hn₂ :
                                autoParam (n₁ + 1 = n₂)
                                  CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃'._auto_3) →
                              X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂)
                                  (CategoryTheory.homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂ ≅
                                X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂)
                                  (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forM_eq_forM : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit.{w + 1}},
  Std.DTreeMap.forM f t = forM t fun a => f a.fst a.snd
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G]
  {ν : MeasureTheory.Measure α},
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂ν
-- Mathlib.Order.Lattice
/-- A lattice with total order is a linear order.

See note [reducible non-instances].  -/
Lattice.toLinearOrder : (α : Type u) →
  [inst : Lattice α] →
    [DecidableEq α] → [DecidableLE α] → [DecidableLT α] → [Std.Total fun x1 x2 => x1 ≤ x2] → LinearOrder α
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The left unitor in the localized monoidal category `LocalizedMonoidal L W ε`.  -/
CategoryTheory.Localization.Monoidal.leftUnitor : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).obj unit ≅
                        CategoryTheory.Functor.id (CategoryTheory.LocalizedMonoidal L W ε)
-- Mathlib.Analysis.BoxIntegral.Basic
/-- Reinterpret `BoxIntegral.HasIntegral` as `Filter.Tendsto`, e.g., dot-notation theorems
that are shadowed in the `BoxIntegral.HasIntegral` namespace.  -/
BoxIntegral.HasIntegral.tendsto : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
  BoxIntegral.HasIntegral I l f vol y →
    Filter.Tendsto (BoxIntegral.integralSum f vol) (BoxIntegral.IntegrationParams.toFilteriUnion I ⊤) (nhds y)
-- Mathlib.Topology.MetricSpace.Thickening
/-- For the equality, see `cthickening_thickening`.  -/
Metric.cthickening_thickening_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ε : ℝ},
  0 ≤ ε → ∀ (δ : ℝ) (s : Set α), Metric.cthickening ε (Metric.thickening δ s) ⊆ Metric.cthickening (ε + δ) s
-- Mathlib.RingTheory.SimpleModule.Isotypic
isotypicComponent_eq_top_iff : ∀ {R : Type u_2} {M : Type u} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSimpleModule R S] [IsSemisimpleModule R M],
  isotypicComponent R M S = ⊤ ↔ IsIsotypicOfType R M S
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback_toSquare : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (sq : CategoryTheory.Square C)
  [inst_2 : CategoryTheory.Mono sq.f₂₄] [inst_3 : CategoryTheory.Mono sq.f₃₄] (h₁ : sq.IsPullback)
  (h₂ : CategoryTheory.Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄),
  (CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback sq h₁ h₂).toSquare = sq
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.inf_subgroupOf_left : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), (K ⊓ H).subgroupOf K = H.subgroupOf K
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
/-- The structure morphism `Φ.r ⟶ 𝟭 C` of a preradical `Φ`.  -/
CategoryTheory.Abelian.Preradical.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.Abelian.Preradical C) → Φ.r ⟶ CategoryTheory.Functor.id C
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.pincerRecursion.match_1.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (n n_1 : ℕ) (h_1 : (m : ℕ) → motive m 0) (h_2 : (n : ℕ) → motive 0 n)
  (h_3 : (n n_2 : ℕ) → motive n.succ n_2.succ),
  (match n.succ, n_1.succ with
    | m, 0 => h_1 m
    | 0, n => h_2 n
    | n.succ, n_2.succ => h_3 n n_2) =
    h_3 n n_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Copy of a `ZeroAtInftyContinuousMap` with a new `toFun` equal to the old one. Useful
to fix definitional equalities.  -/
ZeroAtInftyContinuousMap.copy : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] → (f : ZeroAtInftyContinuousMap α β) → (f' : α → β) → f' = ⇑f → ZeroAtInftyContinuousMap α β
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.Hom.ext_iff : ∀ {A B : MonCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.ofIso_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y}
  (e : QuadraticMap.IsometryEquiv Q₁ Q₂), (QuadraticModuleCat.ofIso e).hom = QuadraticModuleCat.ofHom e.toIsometry
-- Mathlib.Algebra.Group.Hom.Defs
map_eq_zero_iff : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [ZeroHomClass F M N] (f : F), Function.Injective ⇑f → ∀ {x : M}, f x = 0 ↔ x = 0
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Mathlib.Order.Filter.NAry
Filter.NeBot.of_map₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
  (Filter.map₂ m f g).NeBot → f.NeBot
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ι_eq_zero_iff : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  (TensorAlgebra.ι R) x = 0 ↔ x = 0
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.mk : {α : Type w} → List α → Std.Iterators.Types.ListIterator α
-- Lean.Parser.Term.Basic
/-- A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
 -/
Lean.Parser.Term.hole : Lean.Parser.Parser
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.check.injEq : ∀ (e e_1 : Lean.Expr),
  (Lean.Meta.Grind.EMatchTheoremConstraint.check e = Lean.Meta.Grind.EMatchTheoremConstraint.check e_1) = (e = e_1)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.restrictScalars_apply : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Star A]
  [inst_3 : Star B] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : NonUnitalNonAssocSemiring B]
  [inst_6 : MulAction R S] [inst_7 : DistribMulAction S A] [inst_8 : DistribMulAction S B]
  [inst_9 : DistribMulAction R A] [inst_10 : DistribMulAction R B] [inst_11 : IsScalarTower R S A]
  [inst_12 : IsScalarTower R S B] (f : A →⋆ₙₐ[S] B) (x : A), (NonUnitalStarAlgHom.restrictScalars R f) x = f x
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.ContainsZero.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∃ Z, CategoryTheory.Limits.IsZero Z ∧ P Z) → P.ContainsZero
-- Lean.Meta.Tactic.Grind.Injective
_private.Lean.Meta.Tactic.Grind.Injective.0.Lean.Meta.Grind.getSymbols : Lean.Expr → Bool → Lean.MetaM (List Lean.HeadIndex)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_zero_iff_eq_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a : G}, a ≡ 0 [PMOD p] ↔ ∃ z, a = z • p
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Given a right homology map data for morphism `φ`, this is the induced right homology
map data for `-φ`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.neg : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.RightHomologyData} →
            {h₂ : S₂.RightHomologyData} →
              CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.RightHomologyMapData (-φ) h₁ h₂
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.range_inl_sup_range_inr : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H],
  Monoid.Coprod.inl.range ⊔ Monoid.Coprod.inr.range = ⊤
-- Lean.Meta.HasAssignableMVar
_private.Lean.Meta.HasAssignableMVar.0.Lean.Meta.hasAssignableMVar.go : Lean.Expr → StateRefT' IO.RealWorld Lean.ExprSet Lean.MetaM Bool
-- Mathlib.Algebra.LinearRecurrence
/-- The coordinates of a solution in the basis are its first `E.order` values  -/
LinearRecurrence.repr_basis_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (u : ↥E.solSpace),
  E.basis.repr u = Finsupp.ofSupportFinite (↑u ∘ Fin.val) ⋯
-- Mathlib.Algebra.Lie.SemiDirect
/-- The element of L  -/
LieAlgebra.SemiDirectSum.right : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → {x : L →ₗ⁅R⁆ LieDerivation R K K} → K ⋊⁅x⁆ L → L