mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Defs.Unbundled
MinimalFor.prop : ∀ {ι : Sort u_1} {α : Type u_2} [inst : LE α] {P : ι → Prop} {f : ι → α} {i : ι}, MinimalFor P f i → P i
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapAlgEquiv.eq_1 : ∀ (R : Type u_1) {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (e : A ≃ₐ[R] B),
  MonoidAlgebra.mapAlgEquiv R M e =
    { toFun := (↑↑(MonoidAlgebra.mapAlgHom M ↑e).toRingHom).toFun, invFun := ⇑(MonoidAlgebra.mapAlgHom M ↑e.symm),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.funLike.eq_1 : ∀ {E : Type u_3} [inst : Group E], GroupNorm.funLike = { coe := fun f => f.toFun, coe_injective := ⋯ }
-- Aesop.Rule
Aesop.LocalNormSimpRule.id : Aesop.LocalNormSimpRule → Lean.Name
-- Mathlib.Order.LiminfLimsup
Filter.liminf_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteBooleanAlgebra α] (f : Filter β) (u : β → α),
  (Filter.liminf u f)ᶜ = Filter.limsup (compl ∘ u) f
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)),
  (F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X))
        ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)))
-- Mathlib.Order.Defs.PartialOrder
ne_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → a ≠ b
-- Mathlib.LinearAlgebra.Pi
Pi.mem_span_range_single_inl_iff : ∀ {R : Type u} {ι : Type x} {ι' : Type x'} [inst : DecidableEq ι] [inst_1 : DecidableEq ι'] [Finite ι]
  [inst_3 : Semiring R] {x : ι ⊕ ι' → R},
  x ∈ Submodule.span R (Set.range fun i => Pi.single (Sum.inl i) 1) ↔ ∀ (k : ι'), x (Sum.inr k) = 0
-- Lean.Declaration
Lean.instInhabitedQuotVal : Inhabited Lean.QuotVal
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (P : Algebra.PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀]
  (a : MvPolynomial ι R₀)
  (a_1 : Quotient (Submodule.quotientRel (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀))))),
  SMul.smul a a_1 = Quotient.map' (fun x => a * x) ⋯ a_1
-- Mathlib.RingTheory.TensorProduct.Basic
AlgHom.liftEquiv_tmul : ∀ {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R A] [inst_5 : Algebra S B] [inst_6 : Algebra R S]
  [inst_7 : Algebra R B] [inst_8 : IsScalarTower R S B] (f : A →ₐ[R] B) (s : S) (a : A),
  ((AlgHom.liftEquiv R S A B) f) (s ⊗ₜ[R] a) = s • f a
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
ValueDistribution.logCounting.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (f : 𝕜 → E) (a : WithTop E),
  ValueDistribution.logCounting f a =
    if h : a = ⊤ then Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)⁻
    else Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor (fun x => f x - a.untop₀) Set.univ)⁺
-- Init.Data.Array.Mem
/-- This tactic, added to the `decreasing_trivial` toolbox, proves that `sizeOf a < sizeOf arr`
provided that `a ∈ arr` which is useful for well founded recursions over a nested inductive like
`inductive T | mk : Array T → T`.  -/
Array.tacticArray_mem_dec : Lean.ParserDescr
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.request.sizeOf_spec : ∀ (id : Lean.JsonRpc.RequestID) (method : String),
  sizeOf (Lean.JsonRpc.MessageMetaData.request id method) = 1 + sizeOf id + sizeOf method
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassDiv_zero_right : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f : PowerSeries A)
  [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A], f /ʷ 0 = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesLimitIso_inv_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesLimit F G]
  [inst_4 : CategoryTheory.Limits.HasLimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).inv
      (G.map (CategoryTheory.Limits.limit.π F j)) =
    CategoryTheory.Limits.limit.π (F.comp G) j
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `L` contains both a primitive `p`-th root of unity and `q`-th root of unity, and
`Irreducible (cyclotomic (lcm p q) K)` (in particular for `K = ℚ`), then the `finrank K L` is at
least `(lcm p q).totient`.  -/
IsPrimitiveRoot.lcm_totient_le_finrank : ∀ {K : Type u} {L : Type v} [inst : Field K] [inst_1 : CommRing L] [IsDomain L] [inst_3 : Algebra K L]
  [FiniteDimensional K L] {p q : ℕ} {x y : L},
  IsPrimitiveRoot x p →
    IsPrimitiveRoot y q → Irreducible (Polynomial.cyclotomic (p.lcm q) K) → (p.lcm q).totient ≤ Module.finrank K L
-- Mathlib.RingTheory.Polynomial.Vieta
Multiset.esymm_neg : ∀ {R : Type u_1} [inst : CommRing R] (s : Multiset R) (k : ℕ), (Multiset.map Neg.neg s).esymm k = (-1) ^ k * s.esymm k
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Restriction of a `MonoidHom` to a `Submonoid` of the domain.  -/
MonoidHom.domRestrict : {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] → (M →* N) → (s : S) → ↥s →* N
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.mk : {α : Type u_1} → {f : α → α} → ℕ → IterateAddAct f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_erase_eq_of_not_compare_minD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  t.erase k ≠ ∅ → ¬cmp k (t.minD fallback) = Ordering.eq → (t.erase k).minD fallback = t.minD fallback
-- Mathlib.Topology.Defs.Induced
/-- The range of an open embedding is an open set.  -/
Topology.IsOpenEmbedding.isOpen_range : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f → IsOpen (Set.range f)
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Composition of an almost everywhere equal function and a quasi-measure-preserving function.

This is an important special case of `AEEqFun.compQuasiMeasurePreserving`. We use a separate
definition so that lemmas that need `f` to be measure preserving can be `@[simp]` lemmas.  -/
MeasureTheory.AEEqFun.compMeasurePreserving : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace γ] →
            [inst_2 : MeasurableSpace β] →
              {ν : MeasureTheory.Measure β} →
                (β →ₘ[ν] γ) → (f : α → β) → MeasureTheory.MeasurePreserving f μ ν → α →ₘ[μ] γ
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.isHoleRHS : Lean.Syntax → Bool
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.instValuationRingFiniteElement : ∀ (K : Type u_1) [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  ValuationRing (ArchimedeanClass.FiniteElement K)
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A map is a homeomorphism iff it is a quotient map and injective.  -/
isHomeomorph_iff_isQuotientMap_injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f ↔ Topology.IsQuotientMap f ∧ Function.Injective f
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_bot : ∀ {V : Type u} {G : SimpleGraph V}, ⊥.edgeSet = ∅
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.le_tsum : ∀ {α : Type u_1} {f : α → ENNReal} (a : α), f a ≤ ∑' (a : α), f a
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).inverse =
    TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.shiftLeft.sizeOf_spec : ∀ {m n : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : Std.Tactic.BVDecide.BVExpr n),
  sizeOf (lhs.shiftLeft rhs) = 1 + sizeOf m + sizeOf n + sizeOf lhs + sizeOf rhs
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.map_neg : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x : M), f (-x) = -f x
-- Mathlib.Data.ENNReal.Real
ENNReal.one_le_ofReal : ∀ {p : ℝ}, 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p
-- Init.Data.Dyadic.Basic
Dyadic.roundDown.eq_2 : ∀ (prec n k : ℤ) (hn : n % 2 = 1),
  (Dyadic.ofOdd n k hn).roundDown prec =
    match k - prec with
    | Int.ofNat l => Dyadic.ofIntWithPrec (n >>> l) prec
    | Int.negSucc a => Dyadic.ofOdd n k hn
-- Mathlib.CategoryTheory.Equivalence.Symmetry
/-- The `inverse` functor sends an equivalence to its inverse.  -/
CategoryTheory.Equivalence.inverseFunctorObjIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (e : C ≌ D) → (CategoryTheory.Equivalence.inverseFunctor C D).obj e ≅ Opposite.op e.inverse
-- Mathlib.Data.Set.Image
IsCompl.preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {s t : Set β}, IsCompl s t → IsCompl (f ⁻¹' s) (f ⁻¹' t)
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.VersionedHtml.mk : ProofWidgets.Html → ℕ → ProofWidgets.RefreshComponent.VersionedHtml
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₂_obj_p_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
  (Δ : SimplexCategoryᵒᵖ),
  (AlgebraicTopology.DoldKan.Γ₂.obj P).p.app Δ =
    (AlgebraicTopology.DoldKan.Γ₀.splitting P.X).desc Δ fun A =>
      CategoryTheory.CategoryStruct.comp (P.p.f (Opposite.unop A.fst).len)
        (((AlgebraicTopology.DoldKan.Γ₀.splitting P.X).cofan Δ).inj A)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPBeta : Lean.Options → Bool
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
/-- More linear version of `TensorProduct.tensorQuotientEquiv`.  -/
TensorProduct.AlgebraTensorModule.tensorQuotientEquiv : {R : Type u_1} →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra R B] →
                (M : Type u_4) →
                  [inst_5 : AddCommGroup M] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module A M] →
                        [inst_8 : IsScalarTower R A M] →
                          {N : Type u_5} →
                            [inst_9 : AddCommGroup N] →
                              [inst_10 : Module R N] →
                                [inst_11 : Module B N] →
                                  [inst_12 : IsScalarTower R B N] →
                                    (n : Submodule B N) →
                                      TensorProduct R M (N ⧸ n) ≃ₗ[A]
                                        TensorProduct R M N ⧸
                                          ((TensorProduct.AlgebraTensorModule.lTensor A M) (↑R n.subtype)).range
-- Lean.Parser.Term
/-- Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
An empty type ascription `(e :)` elaborates `e` without the expected type.
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
do not yield the right result.
 -/
Lean.Parser.Term.typeAscription : Lean.Parser.Parser
-- Mathlib.Topology.Sober
QuasiSober.inter_of_isClosed_of_quasiSober_left : ∀ {α : Type u_1} [inst : TopologicalSpace α] {V : Set α} (W : Set α) [QuasiSober ↑W], IsClosed V → QuasiSober ↑(W ∩ V)
-- Mathlib.Data.Quot
/-- `Quotient.mk''` is a surjective function.  -/
Quotient.mk''_surjective : ∀ {α : Sort u_1} {s₁ : Setoid α}, Function.Surjective Quotient.mk''
-- Mathlib.Order.SupClosed
latticeClosure_univ : ∀ {α : Type u_3} [inst : Lattice α], latticeClosure Set.univ = Set.univ
-- Mathlib.Algebra.Ring.NonZeroDivisors
dvd_cancel_left_coe_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] {x y : R} {c : ↥(nonZeroDivisors R)}, ↑c * x ∣ ↑c * y ↔ x ∣ y
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_filterMap_eq_false : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l).isEmpty = false ↔
      ∃ k,
        ∃ (h : Std.Internal.List.containsKey k l = true),
          (f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h)).isSome = true)
-- Mathlib.Order.WithBotTop
WithBotTop.rec_coe : ∀ {ι : Type u_1} {motive : WithBotTop ι → Sort u_2} (bot : motive ⊥) (coe : (a : ι) → motive (WithBotTop.coe a))
  (top : motive ⊤) (a : ι), WithBotTop.rec bot coe top (WithBotTop.coe a) = coe a
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- If a wide coequalizer of `f` exists, we can access an arbitrary choice of such by
saying `wideCoequalizer f`.  -/
CategoryTheory.Limits.wideCoequalizer : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} → (f : J → (X ⟶ Y)) → [CategoryTheory.Limits.HasWideCoequalizer f] → C
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.quotientEquiv.symm_apply : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (x : ↑(ZSpan.fundamentalDomain b)),
  (ZSpan.quotientEquiv b).symm x = Submodule.Quotient.mk ↑x
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.val_posSubmonoid_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : ↥(ValuativeRel.posSubmonoid R)), ↑x ≠ 0
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuous_iff_IsClosed_hypograph : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [ClosedIicTopology γ] {f : α → γ}, UpperSemicontinuous f ↔ IsClosed {p | p.2 ≤ f p.1}
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.range_mul : ∀ {α : Type u_2} [inst : Mul α] {ι : Sort u_7} (a : α) (f : ι → α), (Set.range fun i => a * f i) = a • Set.range f
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insert'.valid : ∀ {α : Type u_1} [inst : Preorder α] [Std.Total fun x1 x2 => x1 ≤ x2] [inst_2 : DecidableLE α] (x : α) {t : Ordnode α},
  t.Valid → (Ordnode.insert' x t).Valid
-- Mathlib.Logic.Relation
Relation.SymmGen.decidableRel : {α : Type u_1} → {r : α → α → Prop} → [DecidableRel r] → DecidableRel (Relation.SymmGen r)
-- Mathlib.LinearAlgebra.Span.Basic
/-- `f` is an explicit argument so we can `apply` this theorem and obtain `h` as a new goal.  -/
Submodule.notMem_span_of_apply_notMem_span_image : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {x : M} {s : Set M},
  f x ∉ Submodule.span R₂ (⇑f '' s) → x ∉ Submodule.span R s
-- Mathlib.CategoryTheory.Monoidal.Opposite
Quiver.Hom.unmop_inj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ}, Function.Injective Quiver.Hom.unmop
-- Mathlib.Topology.Order.Lattice
Continuous.inf : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Min L]
  [ContinuousInf L] {f g : X → L}, Continuous f → Continuous g → Continuous fun x => f x ⊓ g x
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.sum_coeff_single`. -/
MonoidAlgebra.sum_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (f : MonoidAlgebra R M), f.coeff.sum MonoidAlgebra.single = f
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.ext : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  {α β : ODE.FunSpace t₀ x₀ r L}, (∀ (t : ↑(Set.Icc tmin tmax)), α.toFun t = β.toFun t) → α = β
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.le_iff_mem : ∀ {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} {s : NonUnitalStarSubalgebra R A},
  IsClosed ↑s → (NonUnitalStarAlgebra.elemental R x ≤ s ↔ x ∈ s)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.rightKanExtensionUniqueOfIso_inv : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] {G : CategoryTheory.Functor C H} (i : F ≅ G)
  (G' : CategoryTheory.Functor D H) (β : L.comp G' ⟶ G) [inst_4 : G'.IsRightKanExtension β],
  (F'.rightKanExtensionUniqueOfIso α i G' β).inv =
    F'.liftOfIsRightKanExtension α G' (CategoryTheory.CategoryStruct.comp β i.inv)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coeFn_def : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω), ⇑μ = fun s => (↑μ s).toNNReal
-- Init.Data.Order.Ord
Std.LawfulBEqOrd.lawfulBEq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Ord α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α], LawfulBEq α
-- Lean.Server.Rpc.Basic
Lean.Server.RpcObjectStore.mk : Lean.PersistentHashMap Lean.Lsp.RpcRef Lean.Server.ReferencedObject →
  Lean.PersistentHashMap USize Lean.Lsp.RpcRef → USize → Lean.Lsp.RpcWireFormat → Lean.Server.RpcObjectStore
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- A family of maps from `left (J.snd b)` to `right b`  -/
CategoryTheory.Limits.MulticospanIndex.snd : {J : CategoryTheory.Limits.MulticospanShape} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (self : CategoryTheory.Limits.MulticospanIndex J C) → (b : J.R) → self.left (J.snd b) ⟶ self.right b
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X), S.preOneHypercover.sieve₀ = ↑S
-- Mathlib.Data.Set.Countable
Set.countable_pi : ∀ {α : Type u} {π : α → Type u_1} [Finite α] {s : (a : α) → Set (π a)},
  (∀ (a : α), (s a).Countable) → {f | ∀ (a : α), f a ∈ s a}.Countable
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_dvd_of_le_left : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (L : AddSubgroup G), H ≤ K → K.relIndex L ∣ H.relIndex L
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Module.Basis.norm.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] (B B_1 : Module.Basis ι K L),
  B = B_1 → ∀ (x x_1 : L), x = x_1 → B.norm x = B_1.norm x_1
-- Mathlib.Analysis.Normed.Group.Basic
dist_eq_norm_inv_mul' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), dist a b = ‖b⁻¹ * a‖
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.mk.inj : ∀ {B : Type u_1} {M : CoxeterMatrix B} {W : Type u_2} {inst : Group W} {mulEquiv mulEquiv_1 : W ≃* M.Group},
  { mulEquiv := mulEquiv } = { mulEquiv := mulEquiv_1 } → mulEquiv = mulEquiv_1
-- Mathlib.SetTheory.ZFC.Class
Class.coe_inter : ∀ (x y : ZFSet.{u}), ↑(x ∩ y) = ↑x ∩ ↑y
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.map_cast_apply : ∀ {γ γ' : Type u} (h : γ = γ') (x : Option γ), Option.map (cast h) x = cast ⋯ x
-- Mathlib.Order.LiminfLimsup
Filter.limsup_eq_iInf_iSup_of_nat' : ∀ {α : Type u_1} [inst : CompleteLattice α] {u : ℕ → α}, Filter.limsup u Filter.atTop = ⨅ n, ⨆ i, u (i + n)
-- Mathlib.Order.Defs.PartialOrder
le_antisymm_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.int_hom_ext_iff : ∀ {G : AddCommGrpCat} {f g : AddCommGrpCat.of ℤ ⟶ G},
  f = g ↔ (CategoryTheory.ConcreteCategory.hom f) 1 = (CategoryTheory.ConcreteCategory.hom g) 1
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend_exactAt_iff : ∀ {ι : 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]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'},
  e.f j = j' → ∀ [K.HasHomology j] [(K.extend e).HasHomology j'], (K.extend e).ExactAt j' ↔ K.ExactAt j
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_st_of_exists_st : ∀ {x : ℝ*}, (∃ r, x.IsSt r) → x.IsSt x.st
-- Mathlib.Topology.Algebra.GroupCompletion
AddMonoidHom.completion_zero : ∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : IsUniformAddGroup β], AddMonoidHom.completion 0 ⋯ = 0
-- Mathlib.RingTheory.Ideal.Height
IsLocalization.height_map_of_disjoint : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R)
  [IsLocalization M S] (p : Ideal R) [p.IsPrime], Disjoint ↑M ↑p → (Ideal.map (algebraMap R S) p).height = p.height
-- Init.Data.Array.Lemmas
Array.foldrM_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {xs : Array α} {f : α → β → m β} {b : β},
  Array.foldrM f b xs.reverse = Array.foldlM (fun x y => f y x) b xs
-- Mathlib.Data.Finsupp.Weight
Finsupp.image_pow_eq_finsuppProd_image : ∀ {α : Type u_5} {β : Type u_6} [inst : CommMonoid β] {f : α → β} {n : ℕ} {s : Set α},
  (f '' s) ^ n = (fun x => x.prod fun x1 x2 => f x1 ^ x2) '' {x | Finsupp.degree x = n ∧ ↑x.support ⊆ s}