mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_mul : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (s : ℤˣ) (x y : R), s ^ (x * y) = (s ^ x) ^ y
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toList_rcc_eq : ∀ {m n i : ℕ}, ((m...=n).toList[i]?.isNone = true) = (n + 1 ≤ i + m)
-- Mathlib.Logic.Embedding.Basic
/-- The embedding of `β` into the sum `α ⊕ β`.  -/
Function.Embedding.inr : {α : Type u_1} → {β : Type u_2} → β ↪ α ⊕ β
-- Mathlib.Data.Set.Basic
Set.union_right_comm : ∀ {α : Type u} (s₁ s₂ s₃ : Set α), s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.map_mono : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Mono f] [CategoryTheory.Mono g]
  [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct W X] [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct Y Z],
  CategoryTheory.Mono (CategoryTheory.Limits.biprod.map f g)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_intCast : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (z : ℤ), ⇑↑z = z • ⇑(CentroidHom.id α)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_lt : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  {x ∈ Finset.Ico a b | x < c} = Finset.Ico a (min b c)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_sdiff : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s t : TopologicalSpace.Clopens α), ↑(s \ t) = ↑s \ ↑t
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α}, t.WF → k ∈ Std.DTreeMap.Raw.map f t → k ∈ t
-- Mathlib.Algebra.Ring.Parity
natCast_eq_zero_or_one_of_two_eq_zero : ∀ {R : Type u_4} [inst : AddMonoidWithOne R] (n : ℕ), 2 = 0 → ↑n = 0 ∨ ↑n = 1
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toLinearMap_add : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] [inst_7 : IsOrderedAddMonoid E₂] (f g : E₁ →ₚ[R] E₂),
  (f + g).toLinearMap = f.toLinearMap + g.toLinearMap
-- Mathlib.Analysis.Seminorm
Seminorm.instAdd : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → Add (Seminorm 𝕜 E)
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_left_as : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  (t : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)),
  (CategoryTheory.WithInitial.coconeEquiv.inverse.obj t).pt.left.as = PUnit.unit
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.inferForallType : Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.toParentKind : Lean.Expr → Lean.Meta.Grind.NormalizePattern.ParentKind✝
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.uint32.sizeOf_spec : sizeOf Lean.IR.IRType.uint32 = 1
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjointOfDiffUnion_subset : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), ↑(hC.disjointOfDiffUnion hs hI) ⊆ C
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.comp_smul : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {π₃ : ContRepresentation R G U} {S : Type u_7}
  [inst_14 : Monoid S] [inst_15 : DistribMulAction S U] [inst_16 : SMulCommClass R S U]
  [inst_17 : ContinuousConstSMul S U] [inst_18 : LinearMap.CompatibleSMul U U S R] [inst_19 : DistribMulAction S W]
  [inst_20 : SMulCommClass R S W] [inst_21 : ContinuousConstSMul S W] [inst_22 : LinearMap.CompatibleSMul W W S R]
  [LinearMap.CompatibleSMul W U S R] (s : S) (f : ContIntertwiningMap π₂ π₃) (g : ContIntertwiningMap π₁ π₂),
  f.comp (s • g) = s • f.comp g
-- Mathlib.RingTheory.Trace.Basic
Algebra.embeddingsMatrixReindex_eq_vandermonde : ∀ {A : Type u} {B : Type v} (C : Type z) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : CommRing C] [inst_4 : Algebra A C] (pb : PowerBasis A B) (e : Fin pb.dim ≃ (B →ₐ[A] C)),
  Algebra.embeddingsMatrixReindex A C (⇑pb.basis) e = (Matrix.vandermonde fun i => (e i) pb.gen).transpose
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.coe_zero : ∀ {𝕜 : Type u_1} [inst : Zero 𝕜] [inst_1 : PseudoMetricSpace 𝕜], ↑0 = 0
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.destruct_join.aux.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Sort u_2) (s : Stream'.WSeq α)
  (S : Stream'.WSeq (Stream'.WSeq α)) (h_1 : Unit → motive none)
  (h_2 : (s : Stream'.WSeq α) → (S : Stream'.WSeq (Stream'.WSeq α)) → motive (some (s, S))),
  (match some (s, S) with
    | none => h_1 ()
    | some (s, S) => h_2 s S) =
    h_2 s S
-- Mathlib.RingTheory.LocalProperties.Basic
/-- If `P` is stable under base change and holds for `f`, then `P` holds for `f` localized
at any submonoid `M` of `R`.  -/
RingHom.IsStableUnderBaseChange.isLocalization_map : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.IsStableUnderBaseChange P →
    ∀ {R S Rᵣ Sᵣ : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing Rᵣ] [inst_3 : CommRing Sᵣ]
      [inst_4 : Algebra R Rᵣ] [inst_5 : Algebra S Sᵣ] (M : Submonoid R) [inst_6 : IsLocalization M Rᵣ] (f : R →+* S)
      [inst_7 : IsLocalization (Submonoid.map f M) Sᵣ], P f → P (IsLocalization.map Sᵣ f ⋯)
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the largest element of the tree set, panicking if the set is empty.
 -/
Std.TreeSet.max! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet α cmp → α
-- Mathlib.Data.EReal.Basic
instCharZeroEReal : CharZero EReal
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.injective : ∀ {ι : Type u_1} {G : Type u_3} [inst : AddGroup G] (b : FreeAddGroupBasis ι G), Function.Injective ⇑b
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.getMatchGeneralizing? : Lean.Syntax → Option Bool
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapIso_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (e : G ≃* H) (e' : ↑B ≃ₗ[k] ↑A) (he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e') (n : ℕ),
  (groupCohomology.mapIso e e' he n).hom =
    groupCohomology.map (↑e.symm) (Rep.ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLift.eq_1 : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : Algebra.IsAlgebraic K L] (σ : B →ₐ[A] B₂),
  galLift K L L₂ σ = { toRingHom := IsLocalization.lift ⋯, commutes' := ⋯ }
-- Lean.Server.Requests
Lean.Server.RequestError.methodNotFound : String → Lean.Server.RequestError
-- Mathlib.NumberTheory.Rayleigh
/-- Generalization of Rayleigh's theorem on Beatty sequences. Let `r` be a real number greater
than 1, and `1/r + 1/s = 1`. Then the complement of `B_r` is `B'_s`.  -/
compl_beattySeq : ∀ {r s : ℝ}, r.HolderConjugate s → {x | ∃ k, beattySeq r k = x}ᶜ = {x | ∃ k, beattySeq' s k = x}
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.age.jointEmbedding : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M], FirstOrder.Language.JointEmbedding (L.age M)
-- Batteries.Data.List.Basic
List.sections.eq_1 : ∀ {α : Type u_1}, [].sections = [[]]
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impArrow : Lean.Parser.Parser
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.instCoeTCOfAddActionSemiHomClass : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : VAdd M X] →
          {Y : Type u_6} →
            [inst_1 : VAdd N Y] →
              {F : Type u_8} → [inst_2 : FunLike F X Y] → [AddActionSemiHomClass F φ X Y] → CoeTC F (X →ₑ[φ] Y)
-- Mathlib.RingTheory.PrincipalIdealDomain
dvd_or_isCoprime : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] (x y : R), Irreducible x → x ∣ y ∨ IsCoprime x y
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.localNormSimpRule.sizeOf_spec : ∀ (r : Aesop.LocalNormSimpRule), sizeOf (Aesop.LocalRuleSetMember.localNormSimpRule r) = 1 + sizeOf r
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A tree is 2-colorable.  -/
SimpleGraph.IsTree.colorable_two : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → G.Colorable 2
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_sum_single : ∀ {ι : Type u_3} (s : Finset ι) (n : ℕ), Finsupp.toMultiset (∑ i ∈ s, fun₀ | i => n) = n • s.val
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.HeightOneSpectrum.span_natGenerator : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  (v : IsDedekindDomain.HeightOneSpectrum R),
  Ideal.span {↑(Rat.HeightOneSpectrum.natGenerator v)} = Ideal.map (Rat.IsIntegralClosure.intEquiv R) v.asIdeal
-- Mathlib.Data.Set.Sigma
Set.mk_preimage_sigma_eq_empty : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι}, i ∉ s → Sigma.mk i ⁻¹' s.sigma t = ∅
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.instGroupoidαCategoryObjCatForgetToCat : (X : CategoryTheory.Grpd) → CategoryTheory.Groupoid ↑(CategoryTheory.Grpd.forgetToCat.obj X)
-- Init.Data.UInt.Bitwise
UInt64.and_neg_one : ∀ {a : UInt64}, a &&& -1 = a
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- The **Plünnecke-Ruzsa inequality**. Multiplication version. Note that this is genuinely harder
than the division version because we cannot use a double counting argument.  -/
Finset.pluennecke_ruzsa_inequality_pow_div_pow_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] {A : Finset G},
  A.Nonempty → ∀ (B : Finset G) (m n : ℕ), ↑(B ^ m / B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.isComplex_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂), S₁.IsComplex ↔ S₂.IsComplex
-- Mathlib.Algebra.Order.Hom.Monoid
monotone_iff_map_nonpos : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], Monotone ⇑f ↔ ∀ a ≤ 0, f a ≤ 0
-- Mathlib.Control.Fold
Monoid.foldrM : (m : Type u → Type u) → [Monad m] → Type u → Type u
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.unitGroup_strictMono : ∀ {K : Type u} [inst : Field K], StrictMono ValuationSubring.unitGroup
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.Polynomial.quotQuotEquivComm I f).symm
      ((Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f}))
        ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) p)) =
    (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.CheckCoverageResult.missing.inj : ∀ {pos pos_1 : List ℕ},
  Lean.Meta.Grind.CheckCoverageResult.missing pos = Lean.Meta.Grind.CheckCoverageResult.missing pos_1 → pos = pos_1
-- Mathlib.Data.List.Sort
List.orderedInsert_count : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : DecidableEq α] (L : List α) (a b : α),
  List.count a (List.orderedInsert r b L) = List.count a L + if b = a then 1 else 0
-- Mathlib.Topology.Algebra.Group.Basic
inv_mem_connectedComponent_one : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : DivisionMonoid G] [ContinuousInv G] {g : G},
  g ∈ connectedComponent 1 → g⁻¹ ∈ connectedComponent 1
-- Std.Sat.AIG.CNF
/-- The central invariant for the `Cache`.

Relate satisfiability results about our produced CNF to satisfiability results about the AIG that
we are processing. The intuition for this is: if a node is marked, its CNF is already part of the
current CNF. Thus the current CNF is already mirroring the semantics of the marked node.
This means that if the CNF is satisfiable at some assignment, we can evaluate the marked node under
the atom part of that assignment and will get the value that was assigned to the corresponding
auxiliary variable as a result.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.Inv : (aig : Std.Sat.AIG ℕ) → Std.Sat.CNF ℕ → (marks : Array Bool) → marks.size = aig.decls.size → Prop
-- Mathlib.Topology.Category.Stonean.Basic
/-- A finite discrete space as a Stonean space.
 -/
Stonean.mkFinite : (X : Type u_1) → [Finite X] → [inst : TopologicalSpace X] → [DiscreteTopology X] → Stonean
-- Mathlib.Topology.Order.IsLocallyClosed
isLocallyClosed_Ici : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a : X} [inst_1 : Preorder X] [ClosedIciTopology X],
  IsLocallyClosed (Set.Ici a)
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.coe_one : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⇑1 = id
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α → β) [Subsingleton (AddUnits M)]
  (x : α →₀ M), Finsupp.mapDomain f x = 0 ↔ x = 0
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.A_transpose : ∀ (n : ℕ), (CartanMatrix.A n).transpose = CartanMatrix.A n
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Given an `S`-linear map `g : M → M'` between `S`-modules, `g` is also `R`-linear between `M` and
`M'` by means of restriction of scalars.
 -/
ModuleCat.RestrictScalars.map' : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          {M M' : ModuleCat S} → (M ⟶ M') → (ModuleCat.RestrictScalars.obj' f M ⟶ ModuleCat.RestrictScalars.obj' f M')
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The partial derivative `W_X(X, Y, Z)` with respect to `X` of the polynomial `W(X, Y, Z)`
associated to a Weierstrass curve `W` in Jacobian coordinates.  -/
WeierstrassCurve.Jacobian.polynomialX : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Jacobian R → MvPolynomial (Fin 3) R
-- Mathlib.Data.NNReal.Defs
NNReal.addLeftMono : AddLeftMono NNReal
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [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] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F)
  (n : ℕ), ‖p.compContinuousLinearMap u n‖₊ ≤ ‖p n‖₊ * ‖u‖₊ ^ n
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The submodule `weightedHomogeneousSubmodule R w m` of homogeneous `MvPolynomial`s of
degree `n` is equal to the `R`-submodule of all `p : (σ →₀ ℕ) →₀ R` such that
`p.support ⊆ {d | weight w d = m}`. While equal, the former has a
convenient definitional reduction.  -/
MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M) (m : M),
  MvPolynomial.weightedHomogeneousSubmodule R w m = AddMonoidAlgebra.supported R R {d | (Finsupp.weight w) d = m}
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.instHasFunctorialFactorizationMonomorphismsRlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C],
  (CategoryTheory.MorphismProperty.monomorphisms C).HasFunctorialFactorization
    (CategoryTheory.MorphismProperty.monomorphisms C).rlp
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd.eq_1 : ∀ {α : Type u_1} (G : Type u_4) [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m m0 : MeasurableSpace α}
  (hm : m ≤ m0) (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (s : Set α),
  MeasureTheory.condExpInd G hm μ s =
    { toFun := MeasureTheory.condExpIndL1 hm μ s, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
-- Mathlib.Analysis.Analytic.Basic
AnalyticOn.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  AnalyticOn 𝕜 f s → Set.EqOn g f s → AnalyticOn 𝕜 g s
-- Std.Time.Format
/-- The leanTime24HourNoNanos format, which follows the pattern `HH:mm:ss` for representing time
in a 24-hour clock format. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanTime24HourNoNanos : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.CountableAB4.ofShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasCountableCoproducts C}
  [self : CategoryTheory.CountableAB4 C] (α : Type) [inst_2 : Countable α],
  CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete α) C
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
/-- A non-canonical representation of a finite module (as a quotient of `Rⁿ`).  -/
FGModuleRepr.ofFinite : (R : Type u) →
  [inst : Ring R] →
    (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [Module.Finite R M] → FGModuleRepr R
-- Mathlib.LinearAlgebra.Basis.Cardinality
_private.Mathlib.LinearAlgebra.Basis.Cardinality.0.Option.elim.match_1.eq_1 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (x : α) (x_1 : β) (f : α → β)
  (h_1 : (x : α) → (x_2 : β) → (f : α → β) → motive (some x) x_2 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match some x, x_1, f with
    | some x, x_2, f => h_1 x x_2 f
    | none, y, x => h_2 y x) =
    h_1 x x_1 f
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Function.locallyFinsuppWithin.toClosedBall_eval_within : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {r : ℝ} {z : E} (f : Function.locallyFinsupp E ℤ),
  z ∈ Metric.closedBall 0 |r| → ((Function.locallyFinsuppWithin.toClosedBall r) f) z = f z
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
exteriorPower.basis_apply : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)),
  (Module.Basis.exteriorPower n b) s = exteriorPower.ιMulti_family R n (⇑b) s
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CechNerveTerminalFrom.hasWidePullback' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (ι : Type w)
  [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C),
  CategoryTheory.Limits.HasWidePullback (⊤_ C) (fun x => X) fun x => CategoryTheory.Limits.terminal.from X
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- The canonical linear map from `Dual M ⊗ Dual N` to `Dual (M ⊗ N)`,
sending `f ⊗ g` to the composition of `TensorProduct.map f g` with
the natural isomorphism `R ⊗ R ≃ R`.
 -/
TensorProduct.dualDistrib : (R : Type u_1) →
  (M : Type u_3) →
    (N : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                TensorProduct R (Module.Dual R M) (Module.Dual R N) →ₗ[R] Module.Dual R (TensorProduct R M N)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.OfComp.map_iso_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H)
  [inst_3 : G.Full] [inst_4 : G.Faithful] {A : Type u_5} [inst_5 : AddMonoid A] [inst_6 : CategoryTheory.HasShift C A]
  [inst_7 : CategoryTheory.HasShift D A] [inst_8 : CategoryTheory.HasShift E A] [inst_9 : G.CommShift A]
  [inst_10 : H.CommShift A] (a : A) (X : C),
  G.map ((CategoryTheory.Functor.CommShift.OfComp.iso e a).hom.app X) =
    CategoryTheory.CategoryStruct.comp (e.hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso H a).hom.app X)
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E a).map (e.inv.app X))
          ((CategoryTheory.Functor.commShiftIso G a).inv.app (F.obj X))))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.forIn_eq_forIn_toListModel : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {t : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forIn f init t = forIn t.toListModel init fun a d => f a.fst a.snd d
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.postponed.inj : ∀ {ctx ctx_1 : Lean.Elab.Term.SavedContext},
  Lean.Elab.Term.SyntheticMVarKind.postponed ctx = Lean.Elab.Term.SyntheticMVarKind.postponed ctx_1 → ctx = ctx_1
-- Mathlib.LinearAlgebra.Prod
/-- Multiplying by the trivial module from the right does not change the structure.
This is the `LinearEquiv` version of `AddEquiv.prodUnique`.  -/
LinearEquiv.prodUnique : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → [Unique M₂] → (M × M₂) ≃ₗ[R] M
-- Lean.Server.Completion.CompletionResolution
_private.Lean.Server.Completion.CompletionResolution.0.Lean.Lsp.consumeImplicitPrefix : {α : Type} → Lean.Expr → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_withDensity_iff_integrable_smul₀' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → ENNReal},
  AEMeasurable f μ →
    (∀ᵐ (x : α) ∂μ, f x < ⊤) →
      ∀ {g : α → E},
        MeasureTheory.Integrable g (μ.withDensity f) ↔ MeasureTheory.Integrable (fun x => (f x).toReal • g x) μ