mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The inverse of an equivalence of additive group extensions is an equivalence.  -/
AddGroupExtension.Equiv.symm : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            {S : AddGroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : AddGroup E'] → {S' : AddGroupExtension N E' G} → S.Equiv S' → S'.Equiv S
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.liftAddEquiv_symm_apply : ∀ {α : Type u} {G : Type u_1} [inst : AddCommGroup G] (a : FreeAbelianGroup α →+ G) (a_1 : α),
  FreeAbelianGroup.liftAddEquiv.symm a a_1 = (MonoidHom.toAdditive.symm a) (Abelianization.of (FreeGroup.of a_1))
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.mapFinIdxM.map.match_1.splitter : {α : Type u_1} →
  (as : Array α) →
    (j : ℕ) →
      (motive : (i : ℕ) → i + j = as.size → Sort u_2) →
        (i : ℕ) →
          (inv : i + j = as.size) →
            ((x : 0 + j = as.size) → motive 0 x) →
              ((i : ℕ) → (inv : i + 1 + j = as.size) → motive i.succ inv) → motive i inv
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Iic_sdiff_Ioc_self_of_le`. -/
Finset.Iic_diff_Ioc_self_of_le : ∀ {α : Type u_2} {a b : α} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : LocallyFiniteOrderBot α],
  a ≤ b → Finset.Iic b \ Finset.Ioc a b = Finset.Iic a
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_isCycles : ∀ {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph} {M' : G'.Subgraph},
  M.IsPerfectMatching → M'.IsPerfectMatching → (symmDiff M.spanningCoe M'.spanningCoe).IsCycles
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.inf : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : SemilatticeInf β] [ContinuousInf β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f ⊓ g) μ
-- Mathlib.Algebra.Category.Ring.Under.Property
RingHom.HasFiniteProducts.hasFiniteProducts : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀ (R : CommRingCat),
        CategoryTheory.Limits.HasFiniteProducts
          ((RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).Under ⊤ R)
-- Std.Http.Protocol.H1.Event
/-- Signals that an `Expect: 100-continue` decision is pending.
 -/
Std.Http.Protocol.H1.Event.continue : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Event dir
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.isometry_toBCF : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β],
  Isometry ZeroAtInftyContinuousMap.toBCF
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The isomorphism from the point of a colimit cokernel cofork of `S.f` to `S.opcycles`.  -/
CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit : {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] →
          {cc : CategoryTheory.Limits.CokernelCofork S.f} → CategoryTheory.Limits.IsColimit cc → (cc.pt ≅ S.opcycles)
-- Mathlib.Algebra.Group.Units.Defs
/-- The element of the group of units, corresponding to an element of a monoid which is a unit. When
`α` is a `DivisionMonoid`, use `IsUnit.unit'` instead.  -/
IsUnit.unit : {M : Type u_1} → [inst : Monoid M] → {a : M} → IsUnit a → Mˣ
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.rightOp_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Dᵒᵖ C} (a : F.rightOp ⊣ G),
  a.rightOp.counit = CategoryTheory.NatTrans.op a.unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The univariate polynomials `preΨₙ` for `n ∈ ℕ`, which are auxiliary to the bivariate polynomials
`Ψₙ` congruent to the bivariate `n`-division polynomials `ψₙ`.  -/
WeierstrassCurve.preΨ' : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → ℕ → Polynomial R
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.node_eq_one : ∀ {n : ℕ}, Polynomial.Chebyshev.node n 0 = 1
-- Mathlib.Topology.JacobsonSpace
JacobsonSpace.of_isOpenEmbedding : ∀ {X : Type u_2} {Y : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [JacobsonSpace Y],
  Topology.IsOpenEmbedding f → JacobsonSpace X
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.denseRange_coe : ∀ {α : Type u_1} [inst : UniformSpace α], DenseRange UniformSpace.Completion.coe'
-- Mathlib.Data.Finset.Max
Finset.coe_max' : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} (hs : s.Nonempty), ↑(s.max' hs) = s.max
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Grind.CommRing.Expr.denoteExpr' : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] →
            Array Lean.Expr → Lean.Meta.Grind.Arith.CommRing.RingExpr → M Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.LaxMonoidalFunctor.of_toFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal], (CategoryTheory.LaxMonoidalFunctor.of F).toFunctor = F
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Subgroup.commutator = { bracket := fun H₁ H₂ => Subgroup.closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g} }
-- Mathlib.Algebra.GroupWithZero.Action.Faithful
/-- `Monoid.toMulAction` is faithful on nontrivial cancellative monoids with zero.  -/
IsRightCancelMulZero.faithfulSMul : ∀ {α : Type u_1} [inst : MonoidWithZero α] [IsRightCancelMulZero α], FaithfulSMul α α
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsOrtho.inr_inl : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₁ : M₁) (m₂ : M₂),
  (Q₁.prod Q₂).IsOrtho (0, m₂) (m₁, 0)
-- Mathlib.NumberTheory.Bernoulli
bernoulli.eq_1 : ∀ (n : ℕ), bernoulli n = (-1) ^ n * bernoulli' n
-- Init.Data.UInt.Bitwise
UInt16.toUSize_shiftRight : ∀ (a b : UInt16), (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 16)
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
_private.Mathlib.LinearAlgebra.AffineSpace.Ordered.0.termC : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.skipSuffix?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  s.skipSuffix? p = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯) = true
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- The quotient by the `dualAnnihilator` of a subspace is isomorphic to the
dual of that subspace.  -/
Subspace.quotAnnihilatorEquiv : {K : Type u_1} →
  {V : Type u_2} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          (W : Subspace K V) → (Module.Dual K V ⧸ Submodule.dualAnnihilator W) ≃ₗ[K] Module.Dual K ↥W
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `fderiv_pow` -/
fderiv_fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E} (n : ℕ),
  DifferentiableAt 𝕜 f x → fderiv 𝕜 (fun i => f i ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp.injEq : ∀ {R : Type u_1} [inst : Semiring R] (toFinsupp toFinsupp_1 : AddMonoidAlgebra R ℕ),
  ({ toFinsupp := toFinsupp } = { toFinsupp := toFinsupp_1 }) = (toFinsupp = toFinsupp_1)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_lt_tsum : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommGroup α] [inst_1 : PartialOrder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α}
  {i : ι} [L.NeBot] [L.LeAtTop],
  f ≤ g → f i < g i → Summable f L → Summable g L → ∑'[L] (n : ι), f n < ∑'[L] (n : ι), g n
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCurry_symm_apply : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] {ι : Type u_5} {κ : ι → Type u_6} (p : ENNReal) [inst_1 : Fact (1 ≤ p)]
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → Fintype (κ i)] (α : (i : ι) → κ i → Type u_7)
  [inst_4 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] [inst_5 : (i : ι) → (k : κ i) → Module 𝕜 (α i k)]
  (f : PiLp p fun i => PiLp p (α i)),
  (LinearIsometryEquiv.piLpCurry 𝕜 p α).symm f = WithLp.toLp p (Sigma.uncurry fun i j => (f.ofLp i).ofLp j)
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], Order.IsPredPrelimit ⊤
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instMaxOfLinearOrder : {α : Type u_1} → [inst : AddMonoid α] → [LinearOrder α] → Max (AddUnits α)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight_assoc : ∀ {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 y : D} (f : x ⟶ y) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x).hom
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso y).inv h))
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) {J : Type w}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c).pt = c.pt.left
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [CategoryTheory.Limits.HasCoproduct Z],
  CategoryTheory.Limits.HasLimit
    ((CategoryTheory.Discrete.opposite α).inverse.comp (CategoryTheory.Discrete.functor Z).op)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticOn.exists_hasFTaylorSeriesUpToOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E},
  AnalyticOn 𝕜 f s → UniqueDiffOn 𝕜 s → ∃ p, HasFTaylorSeriesUpToOn ⊤ f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.compactSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], CompactSpace (TopologicalSpace.Compacts α) ↔ CompactSpace α
-- Mathlib.CategoryTheory.Yoneda
/-- The curried version of coyoneda lemma when `C` is small.  -/
CategoryTheory.curriedCoyonedaLemma' : {C : Type u₁} →
  [inst : CategoryTheory.SmallCategory C] →
    CategoryTheory.yoneda.comp
        ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Functor C (Type u₁))ᵒᵖ (Type u₁)).obj
          CategoryTheory.coyoneda.rightOp) ≅
      CategoryTheory.Functor.id (CategoryTheory.Functor C (Type u₁))
-- Lean.Elab.Util
Lean.Elab.MonadMacroAdapter : (Type → Type) → Type 1
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_ciInf_eq_right_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {b : β} {f : (x : β) → b = x → α},
  ⨅ x, ⨅ (h : b = x), f x h ≤ f b ⋯
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.ExtDHashMap.Const.unitOfList l).getKey! k = default
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- (Implementation) Given a diagram in `CostructuredArrow K B`, produce a natural transformation
from the diagram legs to the specific object.
 -/
CategoryTheory.CostructuredArrow.CreatesConnected.natTransInCostructuredArrow : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
            {K : CategoryTheory.Functor C D} →
              {B : D} →
                (F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow K B)) →
                  F.comp ((CategoryTheory.CostructuredArrow.proj K B).comp K) ⟶ (CategoryTheory.Functor.const J).obj B
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_none : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, a ∉ t → Std.DTreeMap.Internal.Impl.Const.get? t a = none
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addLECancellable_coe : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [AddLeftReflectLE α] (a : α), AddLECancellable ↑a
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_castPred_self : ∀ {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ Fin.last n), (p.castPred hp).predAbove p = p.castPred hp
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.nat_mul_neg : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {f : ℤ → M},
  Multipliable f → Multipliable fun n => f ↑n * f (-↑n)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Reify.0.Lean.Meta.Grind.Arith.Linear.reify?.asVar : ℕ → Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM Lean.Meta.Grind.Arith.Linear.LinExpr
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.q_pos : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsAEKolmogorovProcess X P p q M → 0 < q
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanIndex_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] (x : (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).R),
  (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z).right x = CategoryTheory.OrthogonalReflection.step W Z
-- Init.Notation
/-- The attribute `@[deprecated_arg old new]` marks a named parameter as deprecated.

When a caller uses the old name with a replacement available, a deprecation warning is emitted
and the argument is silently forwarded to the new parameter. When no replacement is provided,
the parameter is treated as removed and using it produces an error.

* `@[deprecated_arg old new (since := "2026-03-18")]` marks `old` as a deprecated alias for `new`.
* `@[deprecated_arg old new "use foo instead" (since := "2026-03-18")]` adds a custom message.
* `@[deprecated_arg old (since := "2026-03-18")]` marks `old` as a removed parameter (no replacement).
* `@[deprecated_arg old "no longer needed" (since := "2026-03-18")]` removed with a custom message.

A warning is emitted if `(since := "...")` is omitted.
 -/
Lean.deprecated_arg : Lean.ParserDescr
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
/-- The non-canonical representation `ofFinite` of a finite module is actually isomorphic to
the given module.  -/
FGModuleRepr.ofFiniteEquiv : (R : Type u) →
  [inst : Ring R] →
    (M : Type v) →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → [inst_3 : Module.Finite R M] → (FGModuleRepr.ofFinite R M).repr ≃ₗ[R] M
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.sup' : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : SemilatticeSup M] {ι : Type u_3} {f : ι → α → M}
  (s : Finset ι),
  (∀ i ∈ s, Function.HasFiniteSupport (f i)) →
    ∀ (hs : s.Nonempty), Function.HasFiniteSupport fun a => s.sup' hs fun x => f x a
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which monovary together on `s`, is unchanged by a permutation if and only if `f ∘ σ` and `g`
monovary together on `s`. Stated by permuting the entries of `f`.  -/
MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ MonovaryOn (f ∘ ⇑σ) g ↑s)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_singleton_eq_self : ∀ {α : Type u_2} [inst : DecidableEq α] (s : Finset α), s.sup singleton = s
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanLiftUnit_desc_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g) {Z : c ⟶ a}
  (h : CategoryTheory.CategoryStruct.comp s.lift f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.lanLiftDesc s) f) h) =
    CategoryTheory.CategoryStruct.comp s.unit h
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.mem_primesOverFinset_iff`. -/
mem_primesOverFinset_iff : ∀ {A : Type u_4} [inst : CommRing A] {p : Ideal A},
  p ≠ ⊥ →
    ∀ [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B] [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B]
      [IsDomain A] [Module.IsTorsionFree A B] {P : Ideal B},
      P ∈ IsDedekindDomain.primesOverFinset p B ↔ P ∈ p.primesOver B
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {H : LieSubalgebra R L} (α χ : ↥H → R) (p q : ℤ) [inst_7 : LieRing.IsNilpotent ↥H],
  LieModule.genWeightSpace M (q • α + χ) = ⊥ →
    ∀ {x : L},
      x ∈ LieAlgebra.rootSpace H α →
        ∀ {y : M}, y ∈ LieModule.genWeightSpaceChain M α χ p q → ⁅x, y⁆ ∈ LieModule.genWeightSpaceChain M α χ p q
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
CategoryTheory.NatTrans.instIsClosedUnderColimitsOfShapeUnderFunctorCoequifiberedHomOfHasProductsOfShapeHom : ∀ {J : Type u_1} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F : CategoryTheory.Functor C D) [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D],
  CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape (fun f => CategoryTheory.NatTrans.Coequifibered f.hom) J
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (P : C),
  CategoryTheory.Projective P ↔ (CategoryTheory.preadditiveCoyonedaObj P).PreservesEpimorphisms
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_map_eq_of_injective : ∀ {R : Type u_1} {S : Type u_2} {M N : Type u} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module S N]
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] N),
  Function.Injective ⇑f → ∀ (p : Submodule R M), (Submodule.map f p).spanRank = p.spanRank
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- The underlying linear map.  -/
SemimoduleCat.Hom.hom' : {R : Type u} → [inst : Semiring R] → {M N : SemimoduleCat R} → M.Hom N → ↑M →ₗ[R] ↑N
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instVAddForall.eq_1 : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} [inst : VAdd M α],
  DomAddAct.instVAddForall = { vadd := fun c f a => f (DomAddAct.mk.symm c +ᵥ a) }
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.hom_comp : ∀ {R S T : SemiRingCat} (f : R ⟶ S) (g : S ⟶ T),
  SemiRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (SemiRingCat.Hom.hom g).comp (SemiRingCat.Hom.hom f)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.finsetProd : ∀ {α : Type u_1} {l : Filter α} {ι : Type u_17} {R : Type u_18} {𝕜 : Type u_19} [inst : SeminormedCommRing R]
  [inst_1 : NormedField 𝕜] {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜},
  (∀ i ∈ s, f i =O[l] g i) → (∃ i ∈ s, f i =o[l] g i) → (fun x => ∏ i ∈ s, f i x) =o[l] fun x => ∏ i ∈ s, g i x
-- Mathlib.Logic.Pairwise
Subsingleton.pairwise : ∀ {α : Type u_1} {r : α → α → Prop} [Subsingleton α], Pairwise r
-- Mathlib.Logic.Equiv.Fin.Basic
finProdFinEquiv_symm_apply : ∀ {m n : ℕ} (x : Fin (m * n)), finProdFinEquiv.symm x = (x.divNat, x.modNat)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the denominator of the left fractions  -/
CategoryTheory.MorphismProperty.LeftFraction₃.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction₃ X Y) → Y ⟶ self.Y'
-- Mathlib.Topology.EMetricSpace.Defs
instEDistAdditive : {X : Type u_1} → [EDist X] → EDist (Additive X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F],
  CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i →
    CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i) → CategoryTheory.IsPullback f g h i