mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (φ : D₁ ⟶ D₂) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) CategoryTheory.Pseudofunctor.DescentData'.comm._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData'.comm._auto_3),
  CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (φ.hom i₁))
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D₂.hom q f₁ f₂ hf₁ hf₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D₁.hom q f₁ f₂ hf₁ hf₂)
      ((F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂))
-- Mathlib.Order.CompactlyGenerated.Basic
/-- A complete lattice is said to be compactly generated if any
element is the `sSup` of compact elements.  -/
IsCompactlyGenerated : (α : Type u_3) → [CompleteLattice α] → Prop
-- Mathlib.Algebra.Homology.Single
ChainComplex.fromSingle₀Equiv_symm_apply_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {C : ChainComplex V ℕ} {X : V} (f : X ⟶ C.X 0),
  ((C.fromSingle₀Equiv X).symm f).f 0 = f
-- Mathlib.Algebra.Free
instDecidableEqFreeMagma.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : FreeMagma α) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The diagram presenting `B`.  -/
CategoryTheory.IndParallelPairPresentation.F₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} → (self : CategoryTheory.IndParallelPairPresentation f g) → CategoryTheory.Functor self.I C
-- Lean.Expr
Lean.instEmptyCollectionFVarIdSet : EmptyCollection Lean.FVarIdSet
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₂ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₂
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {R₁ R₂ : CategoryTheory.RingObjCat C} →
          (hom : R₁.X ⟶ R₂.X) → [isRingHom : CategoryTheory.IsRingHom hom] → R₁.Hom R₂
-- Init.Grind.AC
Lean.Grind.AC.instBEqExpr : BEq Lean.Grind.AC.Expr
-- Mathlib.Data.Finset.Card
Finset.card_mono : ∀ {α : Type u_1}, Monotone Finset.card
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
/-- The set of numbers satisfying the Liouville condition with some exponent `p > 2` has Lebesgue
measure zero.  -/
volume_iUnion_setOfPred_liouvilleWith : MeasureTheory.volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
MonotoneOn.inv : ∀ {α : Type u} {β : Type u_1} [inst : Group α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, MonotoneOn f s → AntitoneOn (fun x => (f x)⁻¹) s
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- Maps a function `f` on the fractional components of a given pair.
 -/
GenContFract.IntFractPair.mapFr : {K : Type u_1} → {β : Type u_2} → (K → β) → GenContFract.IntFractPair K → GenContFract.IntFractPair β
-- Init.ShareCommon
ShareCommon.instInhabitedState : {σ : ShareCommon.StateFactory} → Inhabited (ShareCommon.State σ)
-- Std.Async.Basic
/-- Converts a `BaseAsync` into a `BaseIO`
 -/
Std.Async.BaseAsync.toRawBaseIO : {α : Type} → Std.Async.BaseAsync α → BaseIO (Std.Async.MaybeTask α)
-- Mathlib.Algebra.Group.Conj
/-- Given an element `a`, `addConjugatesOf a` is the set of additive conjugates.  -/
addConjugatesOf : {α : Type u} → [AddMonoid α] → α → Set α
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaConst_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C] {X Y : C}
  (f : X ⟶ Y) (n : Type w), (CategoryTheory.Limits.sigmaConst.map f).app n = CategoryTheory.Limits.Sigma.map fun x => f
-- Mathlib.RingTheory.Localization.Module
/-- If `A` has an `R`-basis, then localizing `A` at `S` has a basis over `R` localized at `S`.

A suitable instance for `[Algebra A Aₛ]` is `localizationAlgebra`.
 -/
Module.Basis.localizationLocalization : {R : Type u_1} →
  (Rₛ : Type u_2) →
    [inst : CommSemiring R] →
      (S : Submonoid R) →
        [inst_1 : CommSemiring Rₛ] →
          [inst_2 : Algebra R Rₛ] →
            [IsLocalization S Rₛ] →
              {A : Type u_3} →
                [inst_4 : CommSemiring A] →
                  [inst_5 : Algebra R A] →
                    (Aₛ : Type u_4) →
                      [inst_6 : CommSemiring Aₛ] →
                        [inst_7 : Algebra A Aₛ] →
                          [inst_8 : Algebra Rₛ Aₛ] →
                            [inst_9 : Algebra R Aₛ] →
                              [IsScalarTower R Rₛ Aₛ] →
                                [IsScalarTower R A Aₛ] →
                                  [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] →
                                    {ι : Type u_5} → Module.Basis ι R A → Module.Basis ι Rₛ Aₛ
-- Init.NotationExtra
«termΣ'_,_» : Lean.ParserDescr
-- Lean.LocalContext
/-- Low-level function for updating every declaration in the local context.
Assumptions about `f`, the resulting nested expressions must be definitionally equal to their original values,
and neither the `index` nor `fvarId` are modified.
 -/
Lean.LocalContext.modifyLocalDecls : Lean.LocalContext → (Lean.LocalDecl → Lean.LocalDecl) → Lean.LocalContext
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.mk.inj : ∀ {unfolds : Lean.NameMap Lean.Meta.SimpTheorem} {casts : Lean.NameMap (Lean.Name × Lean.Name)}
  {insertionFuns : Lean.NameSet} {unfolds_1 : Lean.NameMap Lean.Meta.SimpTheorem}
  {casts_1 : Lean.NameMap (Lean.Name × Lean.Name)} {insertionFuns_1 : Lean.NameSet},
  { unfolds := unfolds, casts := casts, insertionFuns := insertionFuns } =
      { unfolds := unfolds_1, casts := casts_1, insertionFuns := insertionFuns_1 } →
    unfolds = unfolds_1 ∧ casts = casts_1 ∧ insertionFuns = insertionFuns_1
-- Mathlib.Data.Fintype.Parity
/-- The cardinality of `Fin 2` is even, `Fact` version.
This `Fact` is needed as an instance by `Matrix.SpecialLinearGroup.instNeg`.  -/
Fintype.card_fin_two : Fact (Even (Fintype.card (Fin 2)))
-- Mathlib.CategoryTheory.Localization.Composition
CategoryTheory.Functor.IsLocalization.comp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
  (W₃ : CategoryTheory.MorphismProperty C₁),
  W₃.IsInvertedBy (L₁.comp L₂) → W₁ ≤ W₃ → W₂ ≤ W₃.map L₁ → (L₁.comp L₂).IsLocalization W₃
-- Init.Data.List.Nat.Basic
List.length_rightpad : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, (List.rightpad n a l).length = max n l.length
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.get?.match_1.eq_1 : ∀ (motive : String → String.Pos.Raw → Sort u_1) (s : String) (p : String.Pos.Raw)
  (h_1 : (s : String) → (p : String.Pos.Raw) → motive s p),
  (match s, p with
    | s, p => h_1 s p) =
    h_1 s p
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.Extension.not_isReal_of_not_isReal : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] {ψ : K →+* ℂ} [inst_2 : Algebra K L]
  (φ : NumberField.ComplexEmbedding.Extension L ψ),
  ¬NumberField.ComplexEmbedding.IsReal ψ → ¬NumberField.ComplexEmbedding.IsReal ↑φ
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.compHahnSeries_add : ∀ {Γ : Type u_5} {Γ' : Type u_6} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ'] {R : Type u_7} [inst_2 : CommRing R]
  {U : Type u_8} {V : Type u_9} {W : Type u_10} [inst_3 : AddCommGroup U] [inst_4 : Module R U]
  [inst_5 : AddCommGroup V] [inst_6 : Module R V] [inst_7 : AddCommGroup W] [inst_8 : Module R W]
  (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (u v : U),
  A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.eq_image_iff_symm_image_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β)
  (t : Set α), s = ⇑e '' t ↔ ⇑e.symm '' s = t
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.pointwise_smul_le_pointwise_smul_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ {S T : Subsemiring R}, a • S ≤ a • T ↔ S ≤ T
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the
pseudometric space structure from the seminorm properties. Note that in most cases this instance
creates bad definitional equalities (e.g., it does not take into account a possibly existing
`UniformSpace` instance on `E`).  -/
GroupSeminorm.toSeminormedCommGroup : {E : Type u_5} → [inst : CommGroup E] → GroupSeminorm E → SeminormedCommGroup E
-- Init.Data.AC
Lean.Data.AC.Context : Sort u → Type u
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instSMulCauchyOfIsScalarTower : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] →
            {abv : β → α} →
              [inst_4 : IsAbsoluteValue abv] →
                {γ : Type u_3} → [inst_5 : SMul γ β] → [IsScalarTower γ β β] → SMul γ (CauSeq.Completion.Cauchy abv)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
      AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The span of `univ` is `⊤`.  -/
AffineSubspace.span_univ : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], affineSpan k Set.univ = ⊤
-- Mathlib.Data.Num.ZNum
Num.div.eq_1 : ∀ (x : Num), Num.zero.div x = 0
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
RealRMK.rieszMeasure.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [inst_4 : LocallyCompactSpace X],
  RealRMK.rieszMeasure Λ = (rieszContent (CompactlySupportedContinuousMap.toNNRealLinear Λ)).measure
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.instGetElemOptionTrue : {α : Type u_1} →
  {β : Type u_2} →
    {x : BEq α} → {x_1 : Hashable α} → GetElem (Lean.PersistentHashMap α β) α (Option β) fun x x_2 => True
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.mk : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {k : ℕ}, ζ ^ k = 1 → (∀ (l : ℕ), ζ ^ l = 1 → k ∣ l) → IsPrimitiveRoot ζ k
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.isCollinear_of_card_eq_two : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (S : Set (Projectivization K V)), S.ncard = 2 → Projectivization.IsCollinear S
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function of a positive function with locally finite support is
asymptotically strictly monotone.
 -/
Function.locallyFinsuppWithin.logCounting_strictMono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : DecidableEq E] [inst_2 : ProperSpace E]
  {D : Function.locallyFinsupp E ℤ} {e : E},
  Function.locallyFinsuppWithin.single e 1 ≤ D →
    StrictMonoOn (Function.locallyFinsuppWithin.logCounting D) (Set.Ioi ‖e‖)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_C : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) (r : R), (Polynomial.expand R p) (Polynomial.C r) = Polynomial.C r
-- Lean.Expr
/-- Like `Expr.updateLet!` but preserves the `nondep` flag.  -/
Lean.Expr.updateLetE! : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_top : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Top β], ↑⊤ = ⊤
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation.eq_1 : ∀ {X : Type u_1} {mX : MeasurableSpace X} {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V),
  μ.variation = MeasureTheory.preVariation (fun x => ‖μ x‖ₑ) ⋯ ⋯
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.addConj_conjugator_reduceCyclically : ∀ {α : Type u} [inst : DecidableEq α] (L : List (α × Bool)),
  FreeAddGroup.reduceCyclically.conjugator L ++ FreeAddGroup.reduceCyclically L ++
      FreeAddGroup.negRev (FreeAddGroup.reduceCyclically.conjugator L) =
    L
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The right dual of a tensor product is isomorphic to the reversed tensor product of
the right duals.  -/
CategoryTheory.rightDualTensorIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.HasRightDual X] →
          [inst_3 : CategoryTheory.HasRightDual Y] →
            [inst_4 : CategoryTheory.HasRightDual (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)] →
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)ᘁ ≅
                CategoryTheory.MonoidalCategoryStruct.tensorObj Yᘁ Xᘁ
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.forgetMapConeLimitConeIso_hom_hom : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Mon.forgetMapConeLimitConeIso F c hc).hom.hom = CategoryTheory.CategoryStruct.id c.pt
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Week.Offset` to a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.addWeeks : Std.Time.PlainDateTime → Std.Time.Week.Offset → Std.Time.PlainDateTime
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- The filtration of a simplicial set given by a rank function
for a proper pairing of a subcomplex.  -/
SSet.Subcomplex.Pairing.RankFunction.filtration : {X : SSet} →
  {A : X.Subcomplex} → {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → P.RankFunction ι → ι → X.Subcomplex
-- Mathlib.LinearAlgebra.TensorProduct.Free
Algebra.TensorProduct.equivFinsuppOfBasis_apply : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring R] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] {ι : Type u_4} (b : Module.Basis ι R V) (x : TensorProduct R A V),
  (Algebra.TensorProduct.equivFinsuppOfBasis A b) x =
    (TensorProduct.finsuppScalarRight R A A ι) ((LinearMap.baseChange A ↑b.repr) x)
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusCompIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F],
  J.plusCompIso F P = J.plusCompIso F P
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveViewToCoinductiveElab : Lean.Elab.Command.InductiveElabStep1 → Lean.Elab.Command.CoinductiveElabData
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instSub : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddGroup β] → [IsTopologicalAddGroup β] → Sub (ZeroAtInftyContinuousMap α β)
-- Init.Data.List.Lemmas
/-- This differs from `getElem?_set_self` by monadically mapping `Function.const _ a` over the `Option`
returned by `l[i]?`.  -/
List.getElem?_set_self' : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α}, (l.set i a)[i]? = Function.const α a <$> l[i]?
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_map : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α → β} (hf : Function.Injective f), (M.map f ⋯).comap f = M
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_univ : ∀ {M : Type u_1} [inst : Group M], SimpleGraph.mulCayley Set.univ = ⊤
-- Mathlib.Order.Filter.ENNReal
Real.limsSup_of_not_isCobounded : ∀ {f : Filter ℝ}, ¬Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f → f.limsSup = 0
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalRing : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalRing A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → (S : NonUnitalStarSubalgebra R A) → NonUnitalRing ↥S
-- Init.Data.String.Lemmas.Intercalate
String.intercalate_cons_cons : ∀ {s t u : String} {l : List String}, s.intercalate (t :: u :: l) = t ++ s ++ s.intercalate (u :: l)
-- Mathlib.GroupTheory.MonoidLocalization.Away
Localization.Away.mulEquivOfQuotient.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] (x : M)
  (f : Submonoid.LocalizationMap.AwayMap x N),
  Localization.Away.mulEquivOfQuotient x f = Localization.mulEquivOfQuotient f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, k ∈ m → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey? k = m.getKey? k
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
/-- The functor of free groupoid induced by a prefunctor of quivers  -/
Quiver.freeGroupoidFunctor : {V : Type u} →
  [inst : Quiver V] →
    {V' : Type u'} →
      [inst_1 : Quiver V'] → V ⥤q V' → CategoryTheory.Functor (Quiver.FreeGroupoid V) (Quiver.FreeGroupoid V')
-- Init.Data.Nat.Lemmas
Nat.add_mod_eq_add_mod_right : ∀ {a d b : ℕ} (c : ℕ), a % d = b % d → (a + c) % d = (b + c) % d
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- **Alias** of `isClosed_setOfPred_lipschitzWith`. -/
isClosed_setOf_lipschitzWith : ∀ {α : Type u_4} {β : Type u_5} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal),
  IsClosed {f | LipschitzWith K f}
-- Mathlib.MeasureTheory.Order.Lattice
Measurable.const_inf : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : α → M} [inst_1 : Min M]
  [MeasurableInf M], Measurable f → ∀ (c : M), Measurable fun x => c ⊓ f x
-- Mathlib.NumberTheory.NumberField.ProductFormula
/-- The Product Formula for the Number Field `K`.  -/
NumberField.prod_abs_eq_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : K},
  x ≠ 0 → (∏ w, w x ^ w.mult) * ∏ᶠ (w : NumberField.FinitePlace K), w x = 1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget₂AddMon_comp_forget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.AddGrp.forget₂Mon C).comp (CategoryTheory.AddMon.forget C) = CategoryTheory.AddGrp.forget C
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.mahlerSeries.congr_simp : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] (a a_1 : ℕ → E), a = a_1 → PadicInt.mahlerSeries a = PadicInt.mahlerSeries a_1
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Context.mk : Lean.Try.Config → Lean.Meta.Try.Collector.Context
-- Std.Data.TreeMap.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.
If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`,
then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.TreeMap.containsThenInsertIfNew : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → β → Bool × Std.TreeMap α β cmp
-- Mathlib.Order.Completion
DedekindCut.upperBounds_left : ∀ {α : Type u_1} [inst : Preorder α] (A : DedekindCut α), upperBounds A.left = A.right
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
/-- Identity morphisms are left identities for composition.  -/
CategoryTheory.Bicategory.Strict.id_comp : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f = f
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeightsUnnorm_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂),
  (s.map f.toAffineMap ⋯).excenterWeightsUnnorm = s.excenterWeightsUnnorm
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse_initial : ∀ {T : Type u_1} (g : ContextFreeGrammar T), g.reverse.initial = g.initial
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.equivPi_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsArtinianRing R] [inst_2 : IsReduced R] (x : R) (m : MaximalSpectrum R),
  (IsArtinianRing.equivPi R) x m = (Ideal.Quotient.mk m.asIdeal) x
-- Mathlib.Data.List.AList
AList.union_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s₁ s₂ : AList β),
  AList.erase a (s₁ ∪ s₂) = AList.erase a s₁ ∪ AList.erase a s₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Complex.instContinuousMapUniqueHom : ∀ {A : Type u_2} [inst : TopologicalSpace A] [T2Space A] [inst_2 : Ring A] [inst_3 : StarRing A] [inst_4 : Algebra ℂ A],
  ContinuousMap.UniqueHom ℂ A