mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.div₀ : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → (∀ (x : α), g x ≠ 0) → MeasureTheory.StronglyMeasurable (f / g)
-- Mathlib.Logic.Equiv.Defs
Equiv.apply_eq_iff_eq_symm_apply : ∀ {α : Sort u} {β : Sort v} {x : α} {y : β} (f : α ≃ β), f x = y ↔ x = f.symm y
-- Mathlib.Algebra.Ring.Aut
/-- The group of ring automorphisms.  -/
RingAut : (R : Type u_1) → [Mul R] → [Add R] → Type u_1
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.instBEqOrderType.beq : Mathlib.Tactic.Order.OrderType → Mathlib.Tactic.Order.OrderType → Bool
-- Mathlib.LinearAlgebra.Contraction
contractRight_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.Dual R M) (m : M), (contractRight R M) (m ⊗ₜ[R] f) = f m
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_obj_left_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.right = sq.X₂
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Non-unital seminormed commutative ring structure on the product of finitely many non-unital
seminormed commutative rings, using the sup norm.  -/
Pi.nonUnitalSeminormedCommRing : {ι : Type u_3} →
  {R : ι → Type u_4} →
    [Fintype ι] → [(i : ι) → NonUnitalSeminormedCommRing (R i)] → NonUnitalSeminormedCommRing ((i : ι) → R i)
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquivRight_symm_apply_coe : ∀ {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (b : { b // q b }),
  ↑((Equiv.subtypeEquivRight e).symm b) = ↑b
-- Init.Data.BitVec.Lemmas
BitVec.getElem_concat_zero : ∀ {w : ℕ} {b : Bool} {x : BitVec w}, (x.concat b)[0] = b
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f = g` and `f` is an immersion, so is `g`.  -/
Manifold.IsImmersion.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N},
  Manifold.IsImmersion I J n f → f = g → Manifold.IsImmersion I J n g
-- Std.Async.DNS
/-- The service name (e.g., "http" for port 80).
 -/
Std.Async.DNS.NameInfo.service : Std.Async.DNS.NameInfo → String
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.inv_selbergTerms_eq_sum_divisors_moebius_nu : ∀ {s : BoundingSieve} {l : ℕ},
  Squarefree l →
    s.nu l ≠ 0 →
      (BoundingSieve.selbergTerms l)⁻¹ =
        ∑ x ∈ l.divisorsAntidiagonal,
          match x with
          | (d, e) => ↑(ArithmeticFunction.moebius d) * (s.nu e)⁻¹
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousConstVAddCoe : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] {G : Type u_4} [inst_2 : (i : ι) → VAdd G (R i)]
  [inst_3 : ∀ (i : ι), VAddMemClass (S i) G (R i)] [∀ (i : ι), ContinuousConstVAdd G (R i)],
  ContinuousConstVAdd G (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensLegend.mk.injEq : ∀ (tokenTypes tokenModifiers tokenTypes_1 tokenModifiers_1 : Array String),
  ({ tokenTypes := tokenTypes, tokenModifiers := tokenModifiers } =
      { tokenTypes := tokenTypes_1, tokenModifiers := tokenModifiers_1 }) =
    (tokenTypes = tokenTypes_1 ∧ tokenModifiers = tokenModifiers_1)
-- Init.SimpLemmas
of_eq_false : ∀ {p : Prop}, p = False → ¬p
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
/-- A morphism is `QuasiSeparated` if diagonal map is quasi-compact.  -/
AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)
-- Mathlib.Order.Filter.Finite
Set.Finite.eventuallyLE_iUnion : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
  s.Finite → ∀ {f g : ι → Set α}, (∀ i ∈ s, f i ≤ᶠ[l] g i) → ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instAddCommGroup : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] → [IsTopologicalAddGroup F] → AddCommGroup (E →SWOT[σ] F)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates colimits, then `F : C ⥤ Dᵒᵖ` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfSizeOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] →
            CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Order.PiLex
Pi.instLTLexForall : {ι : Type u_1} → {β : ι → Type u_2} → [LT ι] → [(a : ι) → LT (β a)] → LT (Lex ((i : ι) → β i))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey! k = default
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersion.instNormedAddCommGroupComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            (h : Manifold.IsSubmersion I J n f) → NormedAddCommGroup h.complement
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_add : ∀ (x y : ℝ), Real.cos (x + y) = Real.cos x * Real.cos y - Real.sin x * Real.sin y
-- Batteries.Util.ProofWanted
/-- The accessor that reduces `<wrapper> foo` to `foo`'s recorded statement/type.  -/
_private.Batteries.Util.ProofWanted.0.WantedRefKind.accessor : WantedRefKind✝ → Lean.Name
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_sum : ∀ {n : ℕ}, ∑ i ∈ n.divisors, ArithmeticFunction.vonMangoldt i = Real.log ↑n
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.subtypeVal_comp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (s : Set X) {I : Type u_3}
  [inst_2 : TopologicalSpace I],
  IsOpen s → ∀ {x : ↑s} {f : E → ↑s}, IsEvenlyCovered f x I → IsEvenlyCovered (Subtype.val ∘ f) (↑x) I
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGTπ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ (X : C), t.IsGE X n₁ ↔ CategoryTheory.IsIso ((t.truncGTπ n₀).app X)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ext : ∀ {numVarsSucc : ℕ} {x y : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula numVarsSucc},
  x.clauses = y.clauses → x.rupUnits = y.rupUnits → x.ratUnits = y.ratUnits → x.assignments = y.assignments → x = y
-- Mathlib.Topology.Algebra.Group.TopologicalAbelianization
instNormalCommutatorClosure : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  (commutator G).topologicalClosure.Normal
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_transpose : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12}
  (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o), M.transpose.blockDiag' k = (M.blockDiag' k).transpose
-- Mathlib.Data.Finmap
Finmap.union_toFinmap : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (s₁ s₂ : AList β), s₁.toFinmap ∪ s₂.toFinmap = (s₁ ∪ s₂).toFinmap
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUmod : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) {X Y : A} (f : X ⟶ Y) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A] (n : ℕ),
  (Λ.chainComplexMap f).f (n + 2) =
    CategoryTheory.CategoryStruct.comp (Λ.chainComplexXIso X n).hom
      (CategoryTheory.CategoryStruct.comp
        (Λ.F.map
          (CategoryTheory.Limits.kernel.map (ι.map ((Λ.chainComplex X).d (n + 1) n))
            (ι.map ((Λ.chainComplex Y).d (n + 1) n)) (ι.map ((Λ.chainComplexMap f).f (n + 1)))
            (ι.map ((Λ.chainComplexMap f).f n)) ⋯))
        (Λ.chainComplexXIso Y n).inv)
-- Lean.Data.Lsp.Window
Lean.Lsp.instToJsonShowMessageRequestParams.toJson : Lean.Lsp.ShowMessageRequestParams → Lean.Json
-- Mathlib.Algebra.Order.Chebyshev
/-- **Chebyshev's Sum Inequality**: When `f` and `g` antivary together (e.g. one is monotone, the
other is antitone), the product of their sum is greater than the size of the set times their scalar
product.  -/
AntivaryOn.card_mul_sum_le_sum_mul_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {f g : ι → α}, AntivaryOn f g ↑s → ↑s.card * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.ext_iff : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} {x y : hom.InvStruct},
  x = y ↔ x.inv = y.inv ∧ x.homInvId ≍ y.homInvId ∧ x.invHomId ≍ y.invHomId
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.lift_fac : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsClosedImmersion f]
  (H : AlgebraicGeometry.Scheme.Hom.ker f ≤ AlgebraicGeometry.Scheme.Hom.ker g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsClosedImmersion.lift f g H) f = g
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The functor which sends `S : SnakeInput C` to its zeroth line `S.L₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.functorL₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)
-- Mathlib.Topology.CompactOpen
Continuous.compCM : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_6} [inst_4 : TopologicalSpace X']
  {g : X' → C(Y, Z)} {f : X' → C(X, Y)}, Continuous g → Continuous f → Continuous fun x => (g x).comp (f x)
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α},
  Nat.card ↥(Equiv.Perm.OnCycleFactors.toPermHom g).range =
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
/-- The coercion from an elemental algebra to the full algebra is a `IsClosedEmbedding`.  -/
NonUnitalStarAlgebra.elemental.isClosedEmbedding_coe : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] [inst_8 : TopologicalSpace A] [inst_9 : IsSemitopologicalSemiring A]
  [inst_10 : ContinuousConstSMul R A] [inst_11 : ContinuousStar A] (x : A), Topology.IsClosedEmbedding Subtype.val
-- Mathlib.Tactic.ModCases
/-- Int case of `mod_cases h : e % n`.
 -/
Mathlib.Tactic.ModCases.IntMod.modCases : Lean.TSyntax `Lean.binderIdent → Q(ℤ) → ℕ → Lean.Elab.Tactic.TacticM Unit
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.startsWith_char_iff_get : ∀ {c : Char} {s : String}, s.startsWith c = true ↔ ∃ (h : s.startPos ≠ s.endPos), s.startPos.get h = c
-- Mathlib.CategoryTheory.Monoidal.Conv
CategoryTheory.Conv.instMul : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : C} → [CategoryTheory.ComonObj M] → [CategoryTheory.MonObj N] → Mul (CategoryTheory.Conv M N)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_T_le : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ), (LaurentPolynomial.T n).degree ≤ ↑n
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The Fréchet derivative of the Fourier transform of `f` is the Fourier transform of
`fun v ↦ -2 * π * I ⟪v, ⬝⟫ f v`.  -/
Real.fderiv_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) MeasureTheory.volume →
      fderiv ℝ (FourierTransform.fourier f) = FourierTransform.fourier (VectorFourier.fourierSMulRight (innerSL ℝ) f)
-- Mathlib.CategoryTheory.FinCategory.Basic
CategoryTheory.FinCategory.mk : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    autoParam (Fintype J) CategoryTheory.FinCategory.fintypeObj._autoParam →
      autoParam ((j j' : J) → Fintype (j ⟶ j')) CategoryTheory.FinCategory.fintypeHom._autoParam →
        CategoryTheory.FinCategory J
-- Mathlib.Analysis.Calculus.TangentCone.Basic
mem_tangentConeAt_of_add_smul_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} {x y : E} {α : Type u_3}
  {l : Filter α} [l.NeBot] {c : α → 𝕜},
  Filter.Tendsto c l (nhdsWithin 0 {0}ᶜ) → (∀ᶠ (n : α) in l, x + c n • y ∈ s) → y ∈ tangentConeAt 𝕜 s x
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.sheafFiber.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A],
  Φ.sheafFiber = (CategoryTheory.sheafToPresheaf J A).comp Φ.presheafFiber
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- The natural order isomorphism between the two ways to represent invariant submodules.  -/
Module.AEval.mapSubmodule : (R : Type u_1) →
  {A : Type u_2} →
    (M : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          (a : A) →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] →
                    [inst_6 : IsScalarTower R A M] →
                      ↥((Algebra.lsmul R R M) a).invtSubmodule ≃o Submodule (Polynomial R) (Module.AEval R M a)
-- Mathlib.Algebra.Group.Semiconj.Units
SemiconjBy.units_val_iff : ∀ {M : Type u_1} [inst : Monoid M] {a x y : Mˣ}, SemiconjBy ↑a ↑x ↑y ↔ SemiconjBy a x y
-- Mathlib.GroupTheory.Index
/-- The index of an additive subgroup as a natural number.
Returns 0 if the index is infinite. 

[Wikidata Q1464168](https://www.wikidata.org/wiki/Q1464168) -/
AddSubgroup.index : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → ℕ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT'_volume : ∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w // w.IsComplex })
  [inst_1 : NumberField K],
  MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀) =
    ↑(NumberField.mixedEmbedding.convexBodyLT'Factor K) * ↑(∏ w, f w ^ w.mult)
-- Mathlib.Data.ENNReal.Real
/-- `ENNReal.toNNReal` as a `MonoidHom`.  -/
ENNReal.toNNRealHom : ENNReal →*₀ NNReal
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x x_1 : R),
  x = x_1 → ∀ (y y_1 : ↥M), y = y_1 → IsLocalization.mk' S x y = IsLocalization.mk' S x_1 y_1
-- Mathlib.Topology.ContinuousMap.CompactlySupported
_private.Mathlib.Topology.ContinuousMap.CompactlySupported.0.CompactlySupportedContinuousMap.«term_→co_» : Lean.TrailingParserDescr
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.toList_inj : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtTreeMap α β cmp},
  t₁.toList = t₂.toList ↔ t₁ = t₂
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.comm`.

---

The diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
commutes.
 -/
CategoryTheory.HasClassifier.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp m (CategoryTheory.HasSubobjectClassifier.χ m) =
    CategoryTheory.CategoryStruct.comp (⋯.some.χ₀ U) (CategoryTheory.HasSubobjectClassifier.truth C)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.instIsStrictlySupportedTruncGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], (K.truncGE e).IsStrictlySupported e
-- Mathlib.Data.Sum.Interval
Sum.Lex.locallyFiniteOrder : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [LocallyFiniteOrder α] →
          [LocallyFiniteOrder β] → [LocallyFiniteOrderTop α] → [LocallyFiniteOrderBot β] → LocallyFiniteOrder (α ⊕ₗ β)
-- Mathlib.Algebra.Group.Defs
nsmul_left_comm : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (m n : ℕ), n • m • a = m • n • a
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.findAux : {α : Type u_1} → {β : Type u_2} → [BEq α] → Lean.PersistentHashMap.Node α β → USize → α → Option β
-- Mathlib.Probability.Process.Stopping
MeasureTheory.integrable_stoppedValue_of_mem_finset : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [inst_1 : PartialOrder ι] {ℱ : MeasureTheory.Filtration ι m}
  [inst_2 : NormedAddCommGroup E],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.Integrable (u n) μ) →
      ∀ {s : Finset ι},
        (∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s) → MeasureTheory.Integrable (MeasureTheory.stoppedValue u τ) μ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The infimum edistance is invariant under isometries  -/
Metric.infEDist_image : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {x : α} {t : Set α}
  {Φ : α → β}, Isometry Φ → Metric.infEDist (Φ x) (Φ '' t) = Metric.infEDist x t
-- Init.Sym.Lemmas
Lean.Sym.Nat.eq_eq_true : ∀ (a b : ℕ), decide (a = b) = true → (a = b) = True
-- Std.Async.Process
Std.IO.Process.PId.mk : UInt64 → Std.IO.Process.PId
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.toLinearMap_counitAlgHom : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  (Bialgebra.counitAlgHom R A).toLinearMap = CoalgebraStruct.counit
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_add_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T T' : Set α → E →L[ℝ] F) (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.setToL1S (T + T') f =
    MeasureTheory.L1.SimpleFunc.setToL1S T f + MeasureTheory.L1.SimpleFunc.setToL1S T' f
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R))
      (CategoryTheory.ChosenPullbacksAlong.snd T.hom R.hom) =
    CategoryTheory.ChosenPullbacksAlong.snd S.hom R.hom
-- Mathlib.Condensed.Light.Module
instIsRightAdjointLightCondSetLightCondModForget : ∀ (R : Type u) [inst : Ring R], (LightCondensed.forget R).IsRightAdjoint
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1) {M : Type u_2} {M' : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M']
  (f f_1 : M →ₗ[R] M') (e_f : f = f_1) [inst_5 : IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7}
  [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N] [inst_9 : Module R N']
  (g g_1 : N →ₗ[R] N') (e_g : g = g_1) [inst_10 : IsLocalizedModule S g],
  IsLocalizedModule.map S f g = IsLocalizedModule.map S_1 f_1 g_1
-- Mathlib.Algebra.Ring.Subsemiring.Order
/-- A subsemiring of a strict ordered semiring is a strict ordered semiring.  -/
SubsemiringClass.toIsStrictOrderedRing : ∀ {R : Type u_1} {S : Type u_2} [inst : SetLike S R] (s : S) [inst_1 : Semiring R] [inst_2 : PartialOrder R]
  [IsStrictOrderedRing R] [inst_4 : SubsemiringClass S R], IsStrictOrderedRing ↥s