mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
/-- A morphism `g : X ⟶ Y` is epi with an injective kernel iff there exists a morphism
`f : I ⟶ X` with `I` injective such that `f ≫ g = 0` and
the short complex `I ⟶ X ⟶ Y` has a splitting.  -/
CategoryTheory.Abelian.epiWithInjectiveKernel_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (g : X ⟶ Y),
  CategoryTheory.Abelian.epiWithInjectiveKernel g ↔
    ∃ I,
      ∃ (_ : CategoryTheory.Injective I),
        ∃ f,
          ∃ (w : CategoryTheory.CategoryStruct.comp f g = 0),
            Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  (self : P.InvariantForm) (i : ι), (self.form (P.root i)) (P.root i) ≠ 0
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.det_refl : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  LinearEquiv.det (LinearEquiv.refl R M) = 1
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- Try to use the universal property of the span (e.g., `Submodule.span_induction`) instead of
this.  -/
Ideal.mem_span_iff_exists_isHomogeneous : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : ι → R) (y : R),
  y ∈ Ideal.span (Set.range x) ↔ ∃ p, p.IsHomogeneous 1 ∧ (MvPolynomial.eval x) p = y
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- If `‖T‖` is not in the spectrum, then `T.rayleighQuotient x` don't reach `‖T‖`.  -/
ContinuousLinearMap.rayleighQuotient_le_of_norm_mem_resolventSet : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) [Nontrivial E],
  (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T → ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Restrict the indexing type to `ι` by precomposing with a function `ι → E.I₀`.  -/
CategoryTheory.PreZeroHypercover.restrictIndex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : C} → (E : CategoryTheory.PreZeroHypercover T) → {ι : Type w'} → (ι → E.I₀) → CategoryTheory.PreZeroHypercover T
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X],
  CategoryTheory.IsIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.createImportedDiscrTree.go.eq_def : ∀ {α : Type} (env : Lean.Environment)
  (act :
    Lean.Name →
      Lean.ConstantInfo →
        Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry))))
  (constantsPerTask capacityPerTask : ℕ) (cctx : Lean.Core.Context) (ngen : Lean.NameGenerator)
  (tasks : Array (Task (Lean.Meta.RefinedDiscrTree.InitResults✝ α))) (start cnt idx : ℕ),
  Lean.Meta.RefinedDiscrTree.createImportedDiscrTree.go✝ env act constantsPerTask capacityPerTask cctx ngen tasks start
      cnt idx =
    let numModules := env.header.moduleData.size;
    if h : idx < numModules then
      have mdata := env.header.moduleData[idx];
      have cnt := cnt + mdata.constants.size;
      if cnt > constantsPerTask then
        match ngen.mkChild with
        | (childNGen, ngen) => do
          let t ←
            liftM
                (Lean.Meta.RefinedDiscrTree.createImportInitResults✝ cctx childNGen env act capacityPerTask start
                    (idx + 1)).asTask
          Lean.Meta.RefinedDiscrTree.createImportedDiscrTree.go✝ env act constantsPerTask capacityPerTask cctx ngen
              (tasks.push t) (idx + 1) 0 (idx + 1)
      else
        Lean.Meta.RefinedDiscrTree.createImportedDiscrTree.go✝ env act constantsPerTask capacityPerTask cctx ngen tasks
          start cnt (idx + 1)
    else
      if start < numModules then
        match ngen.mkChild with
        | (childNGen, snd) => do
          let t ←
            liftM
                (Lean.Meta.RefinedDiscrTree.createImportInitResults✝ cctx childNGen env act capacityPerTask start
                    numModules).asTask
          pure (tasks.push t)
      else pure tasks
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdxTR.eq_1 : ∀ {α : Type u_1} (l : List α) (n : ℕ), l.eraseIdxTR n = List.eraseIdxTR.go✝ l l n #[]
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_comp_map : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q),
  LinearMap.lTensor P g' ∘ₗ TensorProduct.map f g = TensorProduct.map f (g' ∘ₗ g)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.negAt_apply_norm_isReal : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : { w // w.IsReal }), ‖((NumberField.mixedEmbedding.negAt s) x).1 w‖ = ‖x.1 w‖
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, returning `fallback` if no such element exists.
 -/
Std.TreeSet.Raw.getLED : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → α → α
-- Mathlib.CategoryTheory.Preadditive.Transfer
/-- The preadditive structure on `C` induced by a fully faithful functor `F : C ⥤ D` makes `F` an
additive functor.  -/
CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful), F.Additive
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).toNNReal = OfNat.ofNat n
-- Mathlib.GroupTheory.IsSubnormal
/-- The intersection of two subnormal additive subgroups is additive subnormal.  -/
AddSubgroup.IsSubnormal.inf : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.IsSubnormal → K.IsSubnormal → (H ⊓ K).IsSubnormal
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.spanningSets.congr_simp : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1)
  [inst : MeasureTheory.SigmaFinite μ] (i i_1 : ℕ),
  i = i_1 → ∀ (a a_1 : α), a = a_1 → MeasureTheory.spanningSets μ i a = MeasureTheory.spanningSets μ_1 i_1 a_1
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainNonUnitalRingHom_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : Add M],
  AddMonoidAlgebra.mapDomainNonUnitalRingHom R (AddHom.id M) = NonUnitalRingHom.id (AddMonoidAlgebra R M)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.mk.injEq : ∀ (arr : Array Batteries.UFNode) (parentD_lt : ∀ {i : ℕ}, i < arr.size → Batteries.UnionFind.parentD arr i < arr.size)
  (rankD_lt :
    ∀ {i : ℕ},
      Batteries.UnionFind.parentD arr i ≠ i →
        Batteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i))
  (arr_1 : Array Batteries.UFNode)
  (parentD_lt_1 : ∀ {i : ℕ}, i < arr_1.size → Batteries.UnionFind.parentD arr_1 i < arr_1.size)
  (rankD_lt_1 :
    ∀ {i : ℕ},
      Batteries.UnionFind.parentD arr_1 i ≠ i →
        Batteries.UnionFind.rankD arr_1 i < Batteries.UnionFind.rankD arr_1 (Batteries.UnionFind.parentD arr_1 i)),
  ({ arr := arr, parentD_lt := parentD_lt, rankD_lt := rankD_lt } =
      { arr := arr_1, parentD_lt := parentD_lt_1, rankD_lt := rankD_lt_1 }) =
    (arr = arr_1)
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Let `K / A⟮X⟯ / A[X] / R` be a tower. If `K / A[X] / R` is a scalar tower
then so is `K / A⟮X⟯ / R`.  -/
RatFunc.instIsScalarTowerOfPolynomial : ∀ (R : Type u_1) (A : Type u_2) (K : Type u_3) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Field K]
  [inst_3 : Algebra (Polynomial A) K] [inst_4 : FaithfulSMul (Polynomial A) K] [inst_5 : CommSemiring R]
  [inst_6 : Algebra R (Polynomial A)] [inst_7 : SMul R K] [IsScalarTower R (Polynomial A) K],
  IsScalarTower R (RatFunc A) K
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Lattice.BicartSq.le₁₂ : ∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T], Lattice.BicartSq x₁ x₂ x₃ x₄ → x₁ ≤ x₂
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkState.go : {σ : Type} → [BEq σ] → [ToString σ] → String → σ → σ → Lean.CoreM Unit
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The morphism in C underlying the morphism in the Kleisli category.  -/
CategoryTheory.Kleisli.Hom.of : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : CategoryTheory.Monad C} → {c c' : CategoryTheory.Kleisli T} → c.Hom c' → (c.of ⟶ T.obj c'.of)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.opcyclesMap_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology]
  [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.opcyclesMap (φ + φ') =
    CategoryTheory.ShortComplex.opcyclesMap φ + CategoryTheory.ShortComplex.opcyclesMap φ'
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.target.inj : ∀ {a a_1 : Lean.SubExpr.Pos}, Lean.SubExpr.GoalLocation.target a = Lean.SubExpr.GoalLocation.target a_1 → a = a_1
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeInf β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousInf β] (f g : CompactlySupportedContinuousMap α β),
  ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
/-- The yoneda embedding of `CommGrp C` into presheaves of groups.  -/
CategoryTheory.yonedaCommGrpGrp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.CommGrp C) (CategoryTheory.Functor (CategoryTheory.Grp C)ᵒᵖ CommGrpCat)
-- Mathlib.RingTheory.Invariant.Basic
MulSemiringAction.charpoly_eq_prod_smul : ∀ {B : Type u_2} (G : Type u_3) [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B]
  [inst_3 : Fintype G] (b : B), MulSemiringAction.charpoly G b = ∏ g, g • (Polynomial.X - Polynomial.C b)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {fallback : β} {f : β → β},
  (t.modify k f).getD k' fallback =
    if cmp k k' = Ordering.eq then (Option.map f t[k]?).getD fallback else t.getD k' fallback
-- Batteries.Data.Vector.Lemmas
Vector.back?_scanr : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  (Vector.scanr f init as).back? = some init
-- Mathlib.Algebra.BigOperators.Ring.Nat
Finset.card_preimage_eq_sum_card_image_eq : ∀ {ι : Type u_1} {M : Type u_2} {f : ι → M} {s : Finset M},
  (∀ b ∈ s, {a | f a = b}.Finite) → Nat.card ↑(f ⁻¹' ↑s) = ∑ b ∈ s, Nat.card { a // f a = b }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Mathlib.Data.Sym.Sym2
Sym2.instUnique : {α : Type u_1} → [Unique α] → Unique (Sym2 α)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.SemiCartesianMonoidalCategory C] → CategoryTheory.MonoidalCategory C
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃_next : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (pq pq' : κ),
  (c r).Rel pq pq' →
    ∀ (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_47)
      (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_49),
      self.i₃ r' pq' ⋯ = self.i₂ pq
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → (↑ℝ T).IsSymmetric
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.alternatingSum_reverse : ∀ {G : Type u_7} [inst : AddCommGroup G] (l : List G),
  l.reverse.alternatingSum = (-1) ^ (l.length + 1) • l.alternatingSum
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Apply `L(x,-)` pointwise to bilinear maps, as a continuous bilinear map  -/
ContinuousLinearMap.precompR : {𝕜 : 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ₗ] → (E →L[𝕜] Fₗ →L[𝕜] Gₗ) → E →L[𝕜] (Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr f g))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q hP.isoPushout.inv) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inr
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubgroup_fixedPoints_gc : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α],
  GaloisConnection (⇑OrderDual.toDual ∘ fixingAddSubgroup M)
    ((fun P => AddAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.SatelliteConfig.centerAndRescale_center : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {N : ℕ} {τ : ℝ}
  (a : Besicovitch.SatelliteConfig E N τ), a.centerAndRescale.c (Fin.last N) = 0
-- Mathlib.Tactic.Linarith.Datatypes
/-- Some preprocessors perform branching case splits. A `Branch` is used to track one of these case
splits. The first component, an `MVarId`, is the goal corresponding to this branch of the split,
given as a metavariable. The `List Expr` component is the list of hypotheses for `linarith`
in this branch.
 -/
Mathlib.Tactic.Linarith.Branch : Type
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_mod_two_pow : ∀ (x j i : ℕ), (x % 2 ^ j).testBit i = (decide (i < j) && x.testBit i)
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.sub_iff_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 f → (Differentiable 𝕜 (f - g) ↔ Differentiable 𝕜 g)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.continuous_condExpIndL1 : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  Continuous fun x => MeasureTheory.condExpIndL1 hm μ s x
-- Mathlib.CategoryTheory.Monoidal.Center
/-- The Drinfeld center of a monoidal category `C` has as objects pairs `⟨X, b⟩`, where `X : C`
and `b` is a half-braiding on `X`.
 -/
CategoryTheory.Center : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → Type (max u₁ u₁ v₁)
-- Mathlib.Data.Vector.Snoc
_private.Mathlib.Data.Vector.Snoc.0.List.Vector.cons.match_1.splitter : {α : Type u_1} →
  {n : ℕ} →
    (motive : α → List.Vector α n → Sort u_2) →
      (x : α) → (x_1 : List.Vector α n) → ((a : α) → (v : List α) → (h : v.length = n) → motive a ⟨v, h⟩) → motive x x_1
-- Mathlib.Algebra.Group.Prod
/-- Four-way commutativity of `Prod`. The name matches `mul_mul_mul_comm`.  -/
MulEquiv.prodProdProdComm : (M : Type u_3) →
  (N : Type u_4) →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        (M' : Type u_6) →
          (N' : Type u_7) →
            [inst_2 : MulOneClass N'] → [inst_3 : MulOneClass M'] → (M × N) × M' × N' ≃* (M × M') × N × N'
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_add_div : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), p %ₘ q + q * (p /ₘ q) = p
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.val_neg_ofNSMulEqZero : ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ) (ha : n • a = 0) (hn : n ≠ 0),
  ↑(-AddUnits.ofNSMulEqZero a n ha hn) = (n - 1) • a
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is right distributive over addition  -/
Semiring.right_distrib : ∀ {α : Type u} [self : Semiring α] (a b c : α), (a + b) * c = a * c + b * c
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {l : List α} {k : α} {fallback : Unit},
  (m.insertManyIfNewUnit l).getD k fallback = ()
-- Mathlib.Data.Sign.Defs
Right.sign_neg : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [inst_2 : DecidableLT α] [AddRightStrictMono α] (a : α),
  SignType.sign (-a) = -SignType.sign a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k fallback : α},
  k ∈ t → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.apply_eq_iff_eq : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) {x y : M}, e x = e y ↔ x = y
-- Mathlib.Topology.Algebra.Support
hasCompactMulSupport_comp_left : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : One β] [inst_2 : One γ] {g : β → γ}
  {f : α → β}, (∀ {x : β}, g x = 1 ↔ x = 1) → (HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.IsElliptic.isUnit : ∀ {R : Type u} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsElliptic], IsUnit W.Δ
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.domRestrict.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] {N : Type u_5} {S : Type u_6} [inst_1 : MulOneClass N] [inst_2 : SetLike S M]
  [inst_3 : SubmonoidClass S M] (f : M →* N) (s : S), f.domRestrict s = f.comp (SubmonoidClass.subtype s)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 1st object in the complex of inhomogeneous chains of `A : Rep k G` is isomorphic
to `G →₀ A` as a `k`-module.  -/
groupHomology.chainsIso₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → (groupHomology.inhomogeneousChains A).X 1 ≅ ModuleCat.of k (G →₀ ↑A)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.nonsingularPointEquivSubtype_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} {h : W'.Nonsingular x y}
  {p : W'.Point → Prop} (p0 : p WeierstrassCurve.Affine.Point.zero) (ph : p (WeierstrassCurve.Affine.Point.some x y h)),
  (WeierstrassCurve.Affine.nonsingularPointEquivSubtype p0) ⟨WeierstrassCurve.Affine.Point.some x y h, ph⟩ =
    some ⟨(x, y), ⋯⟩
-- Mathlib.Order.Category.Lat
/-- Constructs an isomorphism of lattices from an order isomorphism between them.  -/
Lat.Iso.mk : {α β : Lat} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.support.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (p : SkewMonoidAlgebra k G), p.support = p.coeff.support
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntryD.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (fallback : (a : α) × β a) (k : α) (v : β k)
  (l : List ((a : α) × β a)),
  Std.Internal.List.getEntryD a fallback (⟨k, v⟩ :: l) =
    bif k == a then ⟨k, v⟩ else Std.Internal.List.getEntryD a fallback l
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_injective : ∀ {α : Type u_1} [inst : HeytingAlgebra α], Function.Injective Heyting.Regular.val
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.repeatEq.match_1.eq_2 : ∀ (motive : (x : ℕ) → TypeVec.{u_1} x → Sort u_2) (n : ℕ) (α : TypeVec.{u_1} n.succ)
  (h_1 : (x : TypeVec.{u_1} 0) → motive 0 x) (h_2 : (n : ℕ) → (α : TypeVec.{u_1} n.succ) → motive n.succ α),
  (match n.succ, α with
    | 0, x => h_1 x
    | n.succ, α => h_2 n α) =
    h_2 n α
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isNoetherian_coeIdeal : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K] [IsNoetherianRing R₁]
  (I : Ideal R₁), IsNoetherian R₁ ↥↑↑I
-- Mathlib.Order.Lattice.Nat
Nat.sInf_def : ∀ {s : Set ℕ} (h : s.Nonempty), sInf s = Nat.find h
-- Mathlib.GroupTheory.Abelianization.Defs
/-- The map operation of the `Abelianization` functor  -/
Abelianization.map : {G : Type u} → [inst : Group G] → {H : Type v} → [inst_1 : Group H] → (G →* H) → Abelianization G →* Abelianization H
-- Lean.Data.SMap
/-- Imported constants.  -/
Lean.SMap.map₁ : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → Std.HashMap α β
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.tensorQuotientEquiv_apply_mk_tmul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (n : Submodule R N) (x : M) (y : N),
  (TensorProduct.tensorQuotientEquiv M n) (x ⊗ₜ[R] Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
totallyBounded_iff_subset_finite_iUnion_nhds_zero : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {s : Set α},
  TotallyBounded s ↔ ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.instNegHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → Neg (S₁ ⟶ S₂)
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Functor.instPreservesLimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type u_1))
  [F.IsCorepresentable], CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, u_1, u, u_1 + 1} F
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.instInhabitedR : (σ K : Type u) → [inst : Fintype K] → [inst_1 : CommRing K] → Inhabited (MvPolynomial.R σ K)
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.disjoint_iff_inter_eq_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint s t ↔ s ∩ t = ∅