mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.one_lt_mul_of_le_of_lt`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul_of_le_of_lt`.  -/
one_lt_mul_of_le_of_lt' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b : α}, 1 ≤ a → 1 < b → 1 < a * b
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- A free group basis `FreeGroupBasis ι G` is a structure recording the isomorphism between a
group `G` and the free group over `ι`. One may think of such a basis as a function from `ι` to `G`
(which is registered through a `FunLike` instance) together with the fact that the morphism induced
by this function from `FreeGroup ι` to `G` is an isomorphism.  -/
FreeGroupBasis : Type u_1 → (G : Type u_2) → [Group G] → Type (max u_1 u_2)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_eq_bot_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] {I : Ideal S}, Ideal.spanNorm R I = ⊥ ↔ I = ⊥
-- Lean.DocString.Types
/-- Rewrites using proofs that two inline element types and two block types are equal.  -/
Lean.Doc.Block.cast : {i i' : Type u_1} → {b b' : Type u_2} → i = i' → b = b' → Lean.Doc.Block i b → Lean.Doc.Block i' b'
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_of_card_le_orderOf : ∀ {α : Type u_1} [inst : Group α] [Finite α] (x : α), Nat.card α ≤ orderOf x → IsCyclic α
-- Init.Data.Array.GetLit
Array.getLit : {α : Type u} → {n : ℕ} → (xs : Array α) → (i : ℕ) → xs.size = n → i < n → α
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- This is the subgroup of `nxn` matrices with entries over a
linear ordered ring and positive determinant.  -/
MatrixGroups.«termGL(_,_)⁺» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.hasProd_of_prod_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {g : γ → α},
  (∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) →
    HasProd g a → HasProd f a
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.map_inv_hom_id_eval : ∀ {C : Type u_1} {D : Type u_2} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X Y : CategoryTheory.GradedObject J C} (e : X ≅ Y)
  (F : CategoryTheory.Functor C D) (j : J),
  CategoryTheory.CategoryStruct.comp (F.map (e.inv j)) (F.map (e.hom j)) =
    CategoryTheory.CategoryStruct.id (F.obj (Y j))
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_le_op_iff : ∀ {M : Type u_2} [inst : MulOneClass M] {S₁ S₂ : Submonoid M}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- Over a division ring, `dilatransvections` correspond to linear
equivalences `e` such that the linear map `e - id` has rank at most 1.

See also `LinearEquiv.mem_dilatransvections_iff_rank`.  -/
LinearEquiv.mem_dilatransvections_iff_finrank : ∀ {V : Type u_2} [inst : AddCommGroup V] {K : Type u_3} [inst_1 : DivisionRing K] [inst_2 : Module K V]
  [Module.Finite K V] {e : V ≃ₗ[K] V},
  e ∈ LinearEquiv.dilatransvections K V ↔ Module.finrank K ↥(↑e - LinearMap.id).range ≤ 1
-- Mathlib.Data.Finset.PiInduction
/-- Given a predicate on functions `∀ i, Finset (α i)` defined on a finite type, it is true on all
maps provided that it is true on `fun _ ↦ ∅` and for any function `g : ∀ i, Finset (α i)`, an index
`i : ι`, and `x ∉ g i`, `p g` implies `p (update g i (insert x (g i)))`.

See also `Finset.induction_on_pi_max` and `Finset.induction_on_pi_min` for specialized versions
that require `∀ i, LinearOrder (α i)`.  -/
Finset.induction_on_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)),
  (p fun x => ∅) →
    (∀ (g : (i : ι) → Finset (α i)) (i : ι), ∀ x ∉ g i, p g → p (Function.update g i (insert x (g i)))) → p f
-- Std.Http.Protocol.H1
/-- Checks whether adding `extra` bytes would exceed configured per-message body
limits.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.fitsBodyLimit : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → ℕ → Bool
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- The category of finitely generated modules.  -/
FGModuleCat : (R : Type u) → [Ring R] → Type (max u (v + 1))
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommGroupWithZero.toZPow : {α : Type u_3} → [self : LinearOrderedCommGroupWithZero α] → ZPow α
-- Init.Data.BitVec.Lemmas
BitVec.signExtend_not : ∀ {w v : ℕ} {x : BitVec w}, 0 < w → BitVec.signExtend v (~~~x) = ~~~BitVec.signExtend v x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_eq_iff : ∀ {ψ θ : Real.Angle}, 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑Real.pi
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- An effective presentation of an object with respect to an equivalence of categories.  -/
CategoryTheory.Functor.equivalenceEffectivePresentation : {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] → (e : C ≌ D) → (X : D) → e.functor.EffectivePresentation X
-- Mathlib.Tactic.ComputeAsymptotics.Lemmas
Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eq : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] (f : 𝕜 → α) (c : 𝕜) [inst_5 : TopologicalSpace α] {a b : α},
  Filter.Tendsto (fun x => f (c - x⁻¹)) Filter.atTop (nhds a) →
    Filter.Tendsto (fun x => f (c + x⁻¹)) Filter.atTop (nhds b) → a = b → Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds a)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isIso_homologyι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι),
  c.next i = j → K.d i j = 0 → ∀ [inst_2 : K.HasHomology i], CategoryTheory.IsIso (K.homologyι i)
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) ⦃m n : ℕ⦄, m ≤ n → K m ⊆ K n
-- Mathlib.Data.UInt
UInt16.toBitVec_intCast : ∀ (z : ℤ), (↑z).toBitVec = ↑z
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.left`.  -/
Tree.left : {α : Type u_1} → Tree α → Tree α
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreserving_comp_apply : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β}
  {γ : Type u_8} {mγ : MeasurableSpace γ} {μc : MeasureTheory.Measure γ} (g : ↥(MeasureTheory.Lp E p μc)) {f : β → γ}
  (hf : MeasureTheory.MeasurePreserving f μb μc) {f' : α → β} (hf' : MeasureTheory.MeasurePreserving f' μ μb),
  (MeasureTheory.Lp.compMeasurePreserving (f ∘ f') ⋯) g =
    (MeasureTheory.Lp.compMeasurePreserving f' hf') ((MeasureTheory.Lp.compMeasurePreserving f hf) g)
-- Lean.Environment
Lean.Kernel.Exception.letTypeMismatch.inj : ∀ {env : Lean.Kernel.Environment} {lctx : Lean.LocalContext} {name : Lean.Name} {givenType expectedType : Lean.Expr}
  {env_1 : Lean.Kernel.Environment} {lctx_1 : Lean.LocalContext} {name_1 : Lean.Name}
  {givenType_1 expectedType_1 : Lean.Expr},
  Lean.Kernel.Exception.letTypeMismatch env lctx name givenType expectedType =
      Lean.Kernel.Exception.letTypeMismatch env_1 lctx_1 name_1 givenType_1 expectedType_1 →
    env = env_1 ∧ lctx = lctx_1 ∧ name = name_1 ∧ givenType = givenType_1 ∧ expectedType = expectedType_1
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
/-- **Vieta's formula** for quadratics.  -/
Polynomial.eq_mul_mul_of_roots_quadratic_eq_pair : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {a b c x1 x2 : R},
  (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).roots = {x1, x2} →
    c = a * x1 * x2
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of `intrinsicClosure_sdiff_intrinsicInterior`. -/
intrinsicClosure_diff_intrinsicInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicClosure 𝕜 s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
ofMul_multiset_prod : ∀ {M : Type u_3} [inst : CommMonoid M] (s : Multiset M), Additive.ofMul s.prod = (Multiset.map (⇑Additive.ofMul) s).sum
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.Hom.mk.inj : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X Y : F.Grothendieck}
  {base : X.base ⟶ Y.base} {fiber : (F.map base.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber} {base_1 : X.base ⟶ Y.base}
  {fiber_1 : (F.map base_1.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber},
  { base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 } → base = base_1 ∧ fiber ≍ fiber_1
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_ι_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (j : J),
  ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).ι.app j).f = c.ι.app j
-- Mathlib.Topology.Category.CompHaus.EffectiveEpi
CompHaus.effectiveEpiFamily_tfae : ∀ {α : Type} [inst : Finite α] {B : CompHaus} (X : α → CompHaus) (π : (a : α) → X a ⟶ B),
  [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π),
      ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_iff_norm_neg_add_lt : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r ↔ ‖-b + a‖ < r
-- Mathlib.Tactic.GCongr.Core
/-- Remove any redundant eta expansions in the arguments on either side of the relation `e`.
As a result, the corresponding binder names are removed, so they cannot end up in the expression
produced by `grw`.  -/
_private.Mathlib.Tactic.GCongr.Core.0.Mathlib.Tactic.GCongr.applyGCongrLemma.preprocess : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.SetTheory.Ordinal.Exponential
/-- The ordinal exponential, defined by transfinite recursion.

We call this `opow` in theorems in order to disambiguate from other exponentials.  -/
Ordinal.instPow : Pow Ordinal.{u_1} Ordinal.{u_1}
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranCompLimIso_inv_app : ∀ {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] {H : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  (L : CategoryTheory.Functor C D) [inst_3 : ∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape C H] [inst_5 : CategoryTheory.Limits.HasLimitsOfShape D H]
  (X : CategoryTheory.Functor C H),
  L.ranCompLimIso.inv.app X = ((L.ran.obj X).limitIsoOfIsRightKanExtension (L.ranCounit.app X)).inv
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_subset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t u : Finset α}, s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u
-- Init.Data.List.Basic
/-- Two lists are permutations of each other if they contain the same elements, each occurring the same
number of times but not necessarily in the same order.

One list can be proven to be a permutation of another by showing how to transform one into the other
by repeatedly swapping adjacent elements.

`List.isPerm` is a Boolean equivalent of this relation.
 -/
List.«term_~_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A continuous linear equivalence of two modules restricts to a continuous linear equivalence
from any submodule `p` of the domain onto the image of that submodule.

This is the continuous linear version of `LinearEquiv.submoduleMap`.
This is `ContinuousLinearEquiv.ofSubmodule'` but with map on the right instead of comap on the left.
 -/
ContinuousLinearEquiv.submoduleMap : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_3} →
      {M₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid M₂] →
                  [inst_5 : TopologicalSpace M₂] →
                    {module_M : Module R M} →
                      {module_M₂ : Module R₂ M₂} →
                        {σ₁₂ : R →+* R₂} →
                          {σ₂₁ : R₂ →+* R} →
                            {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                              {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                                (e : M ≃SL[σ₁₂] M₂) → (p : Submodule R M) → ↥p ≃SL[σ₁₂] ↥(Submodule.map (↑↑e) p)
-- Mathlib.MeasureTheory.SetSemiring
/-- In a semi-ring of sets `C`, for all sets `s, t ∈ C`, `s \ t` is equal to a disjoint union of
finitely many sets in `C`. The finite set of sets in the union is not unique, but this definition
gives an arbitrary `Finset (Set α)` that satisfies the equality.

We remove the empty set to ensure that `t ∉ hC.disjointOfDiff hs ht` even if `t = ∅`.  -/
MeasureTheory.IsSetSemiring.disjointOfDiff : {α : Type u_1} → {C : Set (Set α)} → {s t : Set α} → MeasureTheory.IsSetSemiring C → s ∈ C → t ∈ C → Finset (Set α)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y P : C} {f g : X ⟶ Y} (π π' : Y ⟶ P)
  (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
  (w' : CategoryTheory.CategoryStruct.comp π'.op f.op = CategoryTheory.CategoryStruct.comp π'.op g.op) (h : π = π'),
  CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp π π' w w' h =
    CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp π π' w w' h
-- Mathlib.Topology.MetricSpace.Dilation
/-- The composition of dilations is a dilation  -/
Dilation.comp : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : PseudoEMetricSpace α] →
        [inst_1 : PseudoEMetricSpace β] → [inst_2 : PseudoEMetricSpace γ] → β →ᵈ γ → α →ᵈ β → α →ᵈ γ
-- Mathlib.Order.Concept
Order.IsIntent.iInter₂ : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} {r : α → β → Prop} (f : (i : ι) → κ i → Set β),
  (∀ (i : ι) (j : κ i), Order.IsIntent r (f i j)) → Order.IsIntent r (⋂ i, ⋂ j, f i j)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.map : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {G'' : G'.coe.Subgraph} (f : G'.coe →g G),
  G''.Connected → (SimpleGraph.Subgraph.map f G'').Connected
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.compClosure_iff_self : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C)
  [CategoryTheory.HomRel.IsStableUnderPrecomp r] [CategoryTheory.HomRel.IsStableUnderPostcomp r] {X Y : C}
  (f g : X ⟶ Y), CategoryTheory.HomRel.CompClosure r f g ↔ r f g
-- Init.Data.List.Basic
List.dropLast_nil : ∀ {α : Type u}, [].dropLast = []
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- If `π` is a partition of `I`, then there exists a finite set `s` of hyperplanes such that
`splitMany I s ≤ π`.  -/
BoxIntegral.Prepartition.IsPartition.exists_splitMany_le : ∀ {ι : Type u_1} [Finite ι] {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I},
  π.IsPartition → ∃ s, BoxIntegral.Prepartition.splitMany I s ≤ π
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.tacticEval_simp : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- Auxiliary definition for `bifunctorComp₂₃Functor`.  -/
CategoryTheory.bifunctorComp₂₃FunctorMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₂₃ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] →
                    {F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} →
                      (F ⟶ F') →
                        (CategoryTheory.bifunctorComp₂₃FunctorObj F ⟶ CategoryTheory.bifunctorComp₂₃FunctorObj F')
-- Mathlib.Logic.Basic
/-- As mathlib is primarily classical,
if the type signature of a `def` or `lemma` does not require any `Decidable` instances to state,
it is preferable not to introduce any `Decidable` instances that are needed in the proof
as arguments, but rather to use the `classical` tactic as needed.

In the other direction, when `Decidable` instances do appear in the type signature,
it is better to use explicitly introduced ones rather than allowing Lean to automatically infer
classical ones, as these may cause instance mismatch errors later.

Various types that (almost) never have provable decidability, such as `ℝ`, `Set α` or `Ideal R`,
are given global `DecidableEq` instances, so that no decidable arguments have to be provided.
 -/
LibraryNote.decidable_arguments : Batteries.Util.LibraryNote
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (∀ (a : α), m.contains a = true → (List.map Prod.fst l).contains a = false) →
          (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).size = (↑m).size + l.length
-- Lean.Elab.DefView
Lean.Elab.instToSnapshotTreeDefsParsedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.DefsParsedSnapshot
-- Mathlib.GroupTheory.Congruence.Hom
Con.ker_apply : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {f : M →* P} {x y : M},
  (Con.ker f) x y ↔ f x = f y
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- `@[simp]`-normal form of `pushforward_obj_map_apply`.  -/
PresheafOfModules.pushforward_obj_map_apply' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y)
  (m : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))),
  (ModuleCat.Hom.hom (((PresheafOfModules.pushforward φ).obj M).map f)) m =
    (CategoryTheory.ConcreteCategory.hom (M.map (F.map f.unop).op)) m
-- Init.Data.Array.Attach
List.attach_toArray : ∀ {α : Type u_1} {l : List α}, l.toArray.attach = (l.attachWith (fun x => x ∈ l.toArray) ⋯).toArray
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.zero : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → W'.Point
-- Mathlib.Data.Set.Basic
Set.union_left_comm : ∀ {α : Type u} (s₁ s₂ s₃ : Set α), s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getEntryD_eq_getEntryDₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (fallback : (a : α) × β a), m.getEntryD a fallback = m.getEntryDₘ a fallback
-- Mathlib.Combinatorics.Additive.Dissociation
addDissociated_singleton : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α}, AddDissociated {a} ↔ a ≠ 0
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_iff_sdiff_not_spanning : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
HomologicalComplex.shortComplexTruncLEX₃ToTruncGE.congr_simp : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Abelian C]
  (K : HomologicalComplex C c) {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} [inst_2 : e₁.IsTruncLE]
  [inst_3 : e₂.IsTruncGE] (ac : e₁.AreComplementary e₂),
  K.shortComplexTruncLEX₃ToTruncGE ac = K.shortComplexTruncLEX₃ToTruncGE ac
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- If `M` is commutative, we only need to check the left condition `x ∈ s`.  -/
AddSubmonoid.AddSaturated.of_left : ∀ {M : Type u_2} [inst : AddCommMonoid M] {s : AddSubmonoid M}, (∀ ⦃x y : M⦄, x + y ∈ s → x ∈ s) → s.AddSaturated
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.isoMk_hom_out : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget),
  (CategoryTheory.EnrichedFunctor.isoMk h).hom.out = h.hom
-- Mathlib.Data.Fintype.Sigma
Set.biInter_finsetSigma_univ : ∀ {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_3} [inst : (i : ι) → Fintype (κ i)] (s : Finset ι)
  (f : Sigma κ → Set α), ⋂ ij ∈ s.sigma fun x => Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.combine.go.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (k₁ k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂ : Lean.Grind.CommRing.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_2 :
    (k₁ k₂ : ℤ) →
      (m₂ : Lean.Grind.CommRing.Mon) →
        (p₂ : Lean.Grind.CommRing.Poly) →
          motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (h_3 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_4 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) →
            (m₂ : Lean.Grind.CommRing.Mon) →
              (p₂ : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)),
  (match Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ with
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => h_1 k₁ k₂
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_2 k₁ k₂ m₂ p₂
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ => h_3 k₁ m₁ p₁ k₂
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_4 k₁ m₁ p₁ k₂ m₂ p₂) =
    h_2 k₁ k₂ m₂ p₂
-- Mathlib.RingTheory.SimpleModule.Isotypic
instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent : ∀ {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] [IsSemisimpleModule R S], IsSemisimpleModule R ↥(isotypicComponent R M S)