mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_le_of_sum_le : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} [L.NeBot],
  Summable f L → (∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂) → ∑'[L] (i : ι), f i ≤ a₂
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) [F.Faithful],
  (P.lift F hF).Faithful
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_zipWithAll.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (h_1 : Unit → motive none none)
  (h_2 : (a? : Option α) → (b? : Option β) → motive a? b?),
  (match none, none with
    | none, none => h_1 ()
    | a?, b? => h_2 a? b?) =
    h_1 ()
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.π₁_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.ι K) (HomologicalComplex.pathObject.π₁ K) =
    CategoryTheory.CategoryStruct.id K
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
/-- This lemma demonstrates the origin of the `foldr` name.  -/
CliffordAlgebra.foldr_prod_map_ι : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (l : List M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N),
  ((CliffordAlgebra.foldr Q f hf) n) (List.map (⇑(CliffordAlgebra.ι Q)) l).prod = List.foldr (fun m n => (f m) n) n l
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_apply_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : M),
  Monoid.Coprod.snd (Monoid.Coprod.inl x) = 1
-- Mathlib.Tactic.Linarith.Preprocessing
/-- **Alias** of `Mathlib.Tactic.Linarith.rearrangeComparison?`.

---

`rearrangeComparison e` takes a proof `e` of an equality, inequality, or negation thereof,
and turns it into a proof of a comparison `_ R 0`, where `R ∈ {=, ≤, <}`.
 -/
Mathlib.Tactic.Linarith.rearrangeComparison : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_gen' : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {C : ℝ}
  {f : (i : α) → E i}, (∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C) → Memℓp f p
-- Mathlib.Topology.Perfect
Perfect.closed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α}, Perfect C → IsClosed C
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.homeomorph_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (hf : IsHomeomorph f) (b : Y), (IsHomeomorph.homeomorph f hf).symm b = Function.surjInv ⋯ b
-- Mathlib.SetTheory.Cardinal.Finite
ENat.exists_ne_ne_of_three_le : ∀ {α : Type u_1}, 3 ≤ ENat.card α → ∀ (x y : α), ∃ z, z ≠ x ∧ z ≠ y
-- Mathlib.Lean.Meta.RefinedDiscrTree
/-- Returns candidates from all imported modules that match the expression.  -/
Lean.Meta.RefinedDiscrTree.findImportMatches : {α : Type} →
  Lean.EnvExtension (IO.Ref (Option (Lean.Meta.RefinedDiscrTree α))) →
    (Lean.Name →
        Lean.ConstantInfo →
          Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
      Lean.Expr → optParam ℕ 1000 → optParam ℕ 128 → Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult α)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.instForInSigmaOfMonad : {α : Type u} →
  {β : α → Type v} → {m : Type w → Type w'} → [Monad m] → ForIn m (Std.DTreeMap.Internal.Impl α β) ((a : α) × β a)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).maxKey? = t.maxKey?
-- Batteries.Data.ByteSlice
ByteSlice.stop_eq_start_add_size : ∀ (s : ByteSlice), s.stop = s.start + s.size
-- Init.Data.Dyadic.Basic
Dyadic.zero_add : ∀ (x : Dyadic), 0 + x = x
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The constant edge on a `0`-simplex.  -/
SSet.Edge.id : {X : SSet} → (x₀ : X.obj (Opposite.op { len := 0 })) → SSet.Edge x₀ x₀
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β]
  [inst_4 : Max γ] [inst_5 : Bot γ] (g : InfTopHom βᵒᵈ γᵒᵈ) (f : InfTopHom αᵒᵈ βᵒᵈ),
  SupBotHom.dual.symm (g.comp f) = (SupBotHom.dual.symm g).comp (SupBotHom.dual.symm f)
-- Mathlib.Order.Defs.Unbundled
/-- The carrier of a `LowerSet` is a lower set.  -/
LowerSet.lower' : ∀ {α : Type u_1} [inst : LE α] (self : LowerSet α), IsLowerSet self.carrier
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
ValueDistribution.proximity.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (a : WithTop E),
  ValueDistribution.proximity f a =
    if h : a = ⊤ then Real.circleAverage (fun x => ‖f x‖.posLog) 0
    else Real.circleAverage (fun x => ‖f x - a.untop₀‖⁻¹.posLog) 0
-- Mathlib.CategoryTheory.GradedObject
/-- Given `X : GradedObject I C`, `p : I → J` and `j : J`,
`CofanMapObjFun X p j` is the type `Cofan (X.mapObjFun p j)`. The point object of
such colimits cofans are isomorphic to `X.mapObj p j`, see `CofanMapObjFun.iso`.  -/
CategoryTheory.GradedObject.CofanMapObjFun : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [CategoryTheory.Category.{v_1, u_4} C] →
        CategoryTheory.GradedObject I C → (I → J) → J → Type (max (max u_4 v_1) u_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_hom_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.zero = iX.hom
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Evaluation of a `σ₁₂`-linear map at a fixed `a`, as an `AddMonoidHom`.  -/
LinearMap.evalAddMonoidHom : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ M₂] → {σ₁₂ : R₁ →+* R₂} → M → (M →ₛₗ[σ₁₂] M₂) →+ M₂
-- Mathlib.CategoryTheory.Action.Limits
Action.nsmul_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {X Y : Action V G} (n : ℕ) (f : X ⟶ Y), (n • f).hom = n • f.hom
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measureUnivNNReal_eq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.measureUnivNNReal μ = 0 ↔ μ = 0
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT),
  AlgebraicGeometry.IsAffineOpen US →
    AlgebraicGeometry.IsAffineOpen UT →
      AlgebraicGeometry.IsAffineOpen UX → CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instForInSigmaOfTransCmpOfLawfulMonad : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} →
        [Std.TransCmp cmp] → [inst : Monad m] → [LawfulMonad m] → ForIn m (Std.ExtDTreeMap α β cmp) ((a : α) × β a)
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroup.normedAddGroup.eq_1 : ∀ {E : Type u_1} [inst : NormedAddGroup E] {s : AddSubgroup E},
  AddSubgroup.normedAddGroup =
    { toNorm := AddSubgroup.seminormedAddGroup.toNorm, toAddGroup := s.toAddGroup, toMetricSpace := Subtype.metricSpace,
      dist_eq := ⋯ }
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.small_op_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  CategoryTheory.ObjectProperty.Small.{w, v, u} P.op ↔ CategoryTheory.ObjectProperty.Small.{w, v, u} P
-- Mathlib.Topology.Sheaves.Presheaf
IsOpenMap.pullbackObjIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (ℱ : TopCat.Presheaf C Y)
  (X_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (hf.pullbackObjIso ℱ).hom.app X_1 = (TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ (Opposite.unop X_1) ⋯).hom
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of a function `f` evaluates to zero if `f` is not meromorphic.  -/
MeromorphicOn.divisor_eq_zero_of_not_meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E}, ¬MeromorphicOn f U → (MeromorphicOn.divisor f U) z = 0
-- Mathlib.Algebra.Group.Action.Defs
AddAction.mk : {G : Type u_9} →
  {P : Type u_10} →
    [inst : AddMonoid G] → [toAddSemigroupAction : AddSemigroupAction G P] → (∀ (p : P), 0 +ᵥ p = p) → AddAction G P
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_anti : ∀ {α : Type u_1} [inst : EDist α] {s t : Set α}, s ⊆ t → t.einfsep ≤ s.einfsep
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.homMk'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f : A.toMon ⟶ B.toMon), CategoryTheory.Grp.homMk' f = { hom := f }
-- Mathlib.Order.RelIso.Basic
RelEmbedding.isTrans : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [IsTrans β s], IsTrans α r
-- Std.Sat.CNF.RelabelFin
_private.Std.Sat.CNF.RelabelFin.0.Std.Sat.CNF.not_exists_mem : ∀ {α : Type u_1} {f : Std.Sat.CNF α}, (¬∃ v, Std.Sat.CNF.VarMem v f) ↔ ∃ n, f.clauses = Array.replicate n []
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A local diffeomorphism on `s` is a local homeomorphism on `s`.  -/
IsLocalDiffeomorphOn.isLocalHomeomorphOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {s : Set M},
  IsLocalDiffeomorphOn I J n f s → IsLocalHomeomorphOn f s
-- Init.Notation
Lean.guardMsgsPositionsArg : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- The edge of `Λ[n, i]` with endpoints `j` and `j+1`.

This constructor assumes `0 < i < n`,
which is the type of horn that occurs in the horn-filling condition of quasicategories.  -/
SSet.horn.primitiveEdge : {n : ℕ} → {i : Fin (n + 1)} → 0 < i → i < Fin.last n → Fin n → (SSet.horn n i).toSSet.obj (Opposite.op { len := 1 })
-- Mathlib.RingTheory.FiniteType
Module.Finite.finiteType : ∀ {R : Type u_1} (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [hRA : Module.Finite R A], Algebra.FiniteType R A
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.coe_transPartialEquiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ≃ β} {g : PartialEquiv β γ}, ↑(f.transPartialEquiv g) = ↑g ∘ ⇑f
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtension_iff_of_iso : ∀ {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' F'' : CategoryTheory.Functor D H} (e : F' ≅ F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) (α' : L.comp F'' ⟶ F),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft e.hom) α' = α →
    (F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α')
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Every Schwartz function is continuous.  -/
SchwartzMap.continuous : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F), Continuous ⇑f
-- Lean.Data.Lsp.LanguageFeatures
/-- Identifier that is sent from the server to the client as part of the `CompletionItem.data?` field.
Needed to resolve the `CompletionItem` when the client sends a `completionItem/resolve` request
for that item, again containing the `data?` field provided by the server.
 -/
Lean.Lsp.CompletionIdentifier : Type
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_mul_subset_left : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] (f g : ι → M₀),
  (Function.support fun x => f x * g x) ⊆ Function.support f
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.iIndepFun.cgf_sum : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), Measurable (X i)) →
      ∀ {s : Finset ι},
        (∀ i ∈ s, MeasureTheory.Integrable (fun ω => Real.exp (t * X i ω)) μ) →
          ProbabilityTheory.cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, ProbabilityTheory.cgf (X i) μ t
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.fibreIncl_apply : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × Option X) (σ : Option X → S → T)
  (x : ↑(Prod.snd ∘ InternalProjectivityProof.π_r✝ π σ ⁻¹' {none})), InternalProjectivityProof.fibreIncl✝ π σ x = ↑x
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.IsSFiniteKernel.piecewise : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsSFiniteKernel η], ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.piecewise hs κ η)
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.snd_inl_apply_of_ne_zero : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] {x : G₀},
  x ≠ 0 → (MonoidWithZeroHom.snd G₀ H₀) ((MonoidWithZeroHom.inl G₀ H₀) x) = 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictAntiOn.const_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [MulLeftStrictMono α], StrictAntiOn f s → ∀ (c : α), StrictAntiOn (fun x => c * f x) s
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- Given a submodule `M ⊆ R` and a prime ideal `p` of `S = M⁻¹R`, with `f : R →+* S` the localization
map, then `T = Sₚ` is the localization of `R` at `f⁻¹(p)`.
 -/
IsLocalization.isLocalization_isLocalization_atPrime_isLocalization : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (T : Type u_3) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [IsScalarTower R S T] [IsLocalization M S] (p : Ideal S) [Hp : p.IsPrime] [IsLocalization.AtPrime T p],
  IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)
-- Mathlib.Data.Finsupp.Antidiagonal
Finsupp.image_prodMap_embDomain_antidiagonal : ∀ {α : Type u} [inst : DecidableEq α] {β : Type u_1} [inst_1 : DecidableEq β] (f : α ↪ β) (y : α →₀ ℕ),
  Finset.image (Prod.map (Finsupp.embDomain f) (Finsupp.embDomain f)) (Finset.HasAntidiagonal.antidiagonal y) =
    Finset.HasAntidiagonal.antidiagonal (Finsupp.embDomain f y)
-- Init.Data.Rat.Lemmas
Rat.mk'.congr_simp : ∀ (num num_1 : ℤ) (e_num : num = num_1) (den den_1 : ℕ) (e_den : den = den_1) (den_nz : den ≠ 0)
  (reduced : num.natAbs.Coprime den),
  { num := num, den := den, den_nz := den_nz, reduced := reduced } =
    { num := num_1, den := den_1, den_nz := ⋯, reduced := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.eval_umod : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinOp.umod.eval = fun x1 x2 => x1 % x2
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
IicProdIoc.eq_1 : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] (a b : ι) (x : ((i : ↥(Finset.Iic a)) → X ↑i) × ((i : ↥(Finset.Ioc a b)) → X ↑i))
  (i : ↥(Finset.Iic b)), IicProdIoc a b x i = if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_zero_of_lt_two : ∀ {x : ℝ}, x < 2 → Chebyshev.psi x = 0
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.mk.inj : ∀ {additionalRules erasedRules : Array Aesop.Frontend.RuleExpr} {enabledRuleSets : Std.HashSet Aesop.RuleSetName}
  {options : Aesop.Options} {simpConfig : Lean.Meta.Simp.Config} {simpConfigSyntax? : Option Lean.Term}
  {additionalRules_1 erasedRules_1 : Array Aesop.Frontend.RuleExpr} {enabledRuleSets_1 : Std.HashSet Aesop.RuleSetName}
  {options_1 : Aesop.Options} {simpConfig_1 : Lean.Meta.Simp.Config} {simpConfigSyntax?_1 : Option Lean.Term},
  { additionalRules := additionalRules, erasedRules := erasedRules, enabledRuleSets := enabledRuleSets,
        options := options, simpConfig := simpConfig, simpConfigSyntax? := simpConfigSyntax? } =
      { additionalRules := additionalRules_1, erasedRules := erasedRules_1, enabledRuleSets := enabledRuleSets_1,
        options := options_1, simpConfig := simpConfig_1, simpConfigSyntax? := simpConfigSyntax?_1 } →
    additionalRules = additionalRules_1 ∧
      erasedRules = erasedRules_1 ∧
        enabledRuleSets = enabledRuleSets_1 ∧
          options = options_1 ∧ simpConfig = simpConfig_1 ∧ simpConfigSyntax? = simpConfigSyntax?_1
-- Mathlib.Data.Finsupp.Single
Finsupp.set_indicator_singleton : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α) (f : α → M), {a}.indicator f = ⇑fun₀ | a => f a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.updateCell.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (k' : α) (v' : β k')
  (h_1 : Unit → motive none) (h_2 : (k' : α) → (v' : β k') → motive (some ⟨k', v'⟩)),
  (match some ⟨k', v'⟩ with
    | none => h_1 ()
    | some ⟨k', v'⟩ => h_2 k' v') =
    h_2 k' v'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k fallback : α},
  k ∈ m → m.getKeyD k fallback = k
-- Mathlib.Algebra.Regular.SMul
/-- The element `0` is `M`-regular when `M` is trivial.  -/
IsSMulRegular.zero : ∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M]
  [sM : Subsingleton M], IsSMulRegular M 0
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
IntermediateField.AdjoinSimple.normal_algebraicClosure : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsIntegral K x → Normal K (AlgebraicClosure ↥K⟮x⟯)
-- Init.Data.SInt.Lemmas
ISize.toInt32_ofInt : ∀ {n : ℤ}, (ISize.ofInt n).toInt32 = Int32.ofInt n
-- Init.Data.Option.Basic
Option.instBEq.beq : {α : Type u_1} → [BEq α] → Option α → Option α → Bool
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Types.ListIterator.stepAsHetT_iterM.match_1.splitter : {β : Type u_1} →
  (motive : List β → Sort u_2) →
    (l : List β) → (Unit → motive []) → ((x : β) → (xs : List β) → motive (x :: xs)) → motive l
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instHasForget₂FiniteAddGrpAddMonoidHomCarrierToAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite.eq_1 : ProfiniteAddGrp.instHasForget₂FiniteAddGrpAddMonoidHomCarrierToAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite =
  {
    forget₂ :=
      { obj := ProfiniteAddGrp.ofFiniteAddGrp, map := fun {X Y} => ProfiniteAddGrp.ofFiniteAddGrpHom,
        map_id :=
          ProfiniteAddGrp.instHasForget₂FiniteAddGrpAddMonoidHomCarrierToAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_1,
        map_comp :=
          @ProfiniteAddGrp.instHasForget₂FiniteAddGrpAddMonoidHomCarrierToAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_2 },
    forget_comp :=
      ProfiniteAddGrp.instHasForget₂FiniteAddGrpAddMonoidHomCarrierToAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_4 }
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II_obj : ∀ (n : SimplexCategory), SimplexCategory.II.obj n = Opposite.op { len := n.len + 1 }
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFun : {α : Type u_3} →
  {E : α → Type u_4} →
    {p : ENNReal} → [inst : (i : α) → NormedAddCommGroup (E i)] → CoeFun ↥(lp E p) fun x => (i : α) → E i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_eq_isSome_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = t[a]?.isSome
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.typeFormerTypeLevel.go : Lean.Expr → Array Lean.Expr → Lean.MetaM (Option Lean.Level)
-- Mathlib.Algebra.Star.Conjneg
conjneg_involutive : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R],
  Function.Involutive conjneg
-- Mathlib.Data.Sum.Order
/-- `Equiv.sumCongr` promoted to an order isomorphism between lexicographic sums.  -/
OrderIso.sumLexCongr : {α₁ : Type u_4} →
  {α₂ : Type u_5} →
    {β₁ : Type u_6} →
      {β₂ : Type u_7} →
        [inst : LE α₁] →
          [inst_1 : LE α₂] → [inst_2 : LE β₁] → [inst_3 : LE β₂] → α₁ ≃o α₂ → β₁ ≃o β₂ → α₁ ⊕ₗ β₁ ≃o α₂ ⊕ₗ β₂
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalRight : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Group.Units.Basic
eq_zero_of_add_left' : ∀ {α : Type u} [inst : AddCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 → b = 0
-- Lean.Util.ParamMinimizer
/-- Found a precise solution.  -/
Lean.Util.ParamMinimizer.Status.precise : Lean.Util.ParamMinimizer.Status
-- Init.Data.Queue
/-- A functional queue data structure, using two back-to-back lists.
If we think of the queue as having elements pushed on the front and
popped from the back, then the queue itself is effectively `eList ++ dList.reverse`.
 -/
Std.Queue : Type u → Type u
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.trans_isLittleO : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
  {c : ℝ} {f : α → E} {g : α → F} {k : α → G} {l : Filter α},
  Asymptotics.IsBigOWith c l f g → g =o[l] k → 0 < c → f =o[l] k