mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- An abbreviation for `WeierstrassCurve.Projective.Point.fromAffine` for dot notation.  -/
WeierstrassCurve.Affine.Point.toProjective : {R : Type r} →
  [inst : CommRing R] →
    [Nontrivial R] → {W : WeierstrassCurve.Affine R} → W.Point → (WeierstrassCurve.toProjective W).Point
-- Init.Data.List.Impl
List.erase_eq_eraseTR : @List.erase = @List.eraseTR
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.rel_π₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂)
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), c₁₂.Rel (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁', i₂))
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.inv : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : DivisionCommMonoid β] {A : Set α} {B : Set β}
  {f : α → β} {n : ℕ}, IsMulFreimanHom n A B f → IsMulFreimanHom n A B⁻¹ f⁻¹
-- Mathlib.Algebra.Order.GroupWithZero.Submonoid
Submonoid.coe_pos : ∀ (α : Type u_1) [inst : MulZeroOneClass α] [inst_1 : PartialOrder α] [inst_2 : PosMulStrictMono α]
  [inst_3 : ZeroLEOneClass α] [inst_4 : NeZero 1], ↑(Submonoid.pos α) = Set.Ioi 0
-- Aesop.Util.UnorderedArraySet
/-- O(1)  -/
Aesop.UnorderedArraySet.empty : {α : Type u_1} → [inst : BEq α] → Aesop.UnorderedArraySet α
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The functor `SimplicialObject.Split C ⥤ C` which sends a simplicial object equipped
with a splitting to its nondegenerate `n`-simplices.  -/
CategoryTheory.SimplicialObject.Split.evalN : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → ℕ → CategoryTheory.Functor (CategoryTheory.SimplicialObject.Split C) C
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ⟶ G)
  {X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y),
  ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).map f).f = f.f
-- Mathlib.Computability.Primrec.Basic
/-- The primitive recursive functions `ℕ → ℕ`.  -/
Nat.Primrec : (ℕ → ℕ) → Prop
-- Mathlib.Analysis.Convex.Slope
ConvexOn.secant_mono_aux1 : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (z - x) * f y ≤ (z - y) * f x + (y - x) * f z
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.evalᵢ.eq_1 : ∀ (σ K : Type u) [inst : Fintype K] [inst_1 : CommRing K],
  MvPolynomial.evalᵢ σ K = MvPolynomial.evalₗ K σ ∘ₗ (MvPolynomial.restrictDegree σ K (Fintype.card K - 1)).subtype
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.refl_trans : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β), (Function.Embedding.refl α).trans f = f
-- Mathlib.Topology.Instances.Matrix
Matrix.diagonal_tsum : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [inst_2 : DecidableEq n] [T2Space R] {f : X → n → R},
  Matrix.diagonal (∑'[L] (x : X), f x) = ∑'[L] (x : X), Matrix.diagonal (f x)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
PresheafOfModules.surjective_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Epi f] (X : Cᵒᵖ),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))
-- Init.Data.Array.InsertIdx
Array.getElem_insertIdx_of_lt : ∀ {α : Type u} {xs : Array α} {x : α} {i k : ℕ} (w : i ≤ xs.size) (h : k < i), (xs.insertIdx i x w)[k] = xs[k]
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.instInhabitedEntry.default : Lean.Parser.ParserExtension.Entry
-- Lean.Elab.Do.Legacy
/-- Given two code blocks `c₁` and `c₂`, make sure they have the same set of updated variables.
Let `ws` the union of the updated variables in `c₁‵ and ‵c₂`.
We use `extendUpdatedVars c₁ ws` and `extendUpdatedVars c₂ ws`
 -/
Lean.Elab.Term.Do.homogenize : Lean.Elab.Term.Do.CodeBlock →
  Lean.Elab.Term.Do.CodeBlock → Lean.Elab.TermElabM (Lean.Elab.Term.Do.CodeBlock × Lean.Elab.Term.Do.CodeBlock)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α},
  m.WF → k ∈ Std.DHashMap.Raw.filterMap f m → k ∈ m
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushout_inl_inv_inr_of_right_isIso_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pushout.inr f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Algebra.Group.Hom.Defs
/-- `MulHomClass F M N` states that `F` is a type of multiplication-preserving homomorphisms.

You should declare an instance of this typeclass when you extend `MulHom`.
 -/
MulHomClass : (F : Type u_10) → (M : outParam (Type u_11)) → (N : outParam (Type u_12)) → [Mul M] → [Mul N] → [FunLike F M N] → Prop
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalIntro : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α} [inst_1 : SizeOf α] (toOpens : TopologicalSpace.Opens α)
  (mem' : x ∈ toOpens.carrier), sizeOf { toOpens := toOpens, mem' := mem' } = 1 + sizeOf toOpens + sizeOf mem'
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : α}, ∅.contains a = false
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.mk₀_smul : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C] {X Y : C}
  (r : R) (f : X ⟶ Y), CategoryTheory.Abelian.Ext.mk₀ (r • f) = r • CategoryTheory.Abelian.Ext.mk₀ f
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.willInsert.sizeOf_spec : sizeOf Lean.Widget.DiffTag.willInsert = 1
-- Lean.Parser.Term
Lean.Parser.Term.ensureTypeOf : Lean.Parser.Parser
-- Mathlib.Data.List.ReduceOption
List.reduceOption_length_le : ∀ {α : Type u_1} (l : List (Option α)), l.reduceOption.length ≤ l.length
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- Given an algebraic tower of fields `E/L/K` and an element `x : L` whose minimal polynomial `f`
over `K` splits into linear factors over `E`, the `degree(f)`th power of the spectral norm of `x`,
considered as an element of `E`, is equal to the spectral norm of the product of the `E`-valued
roots of `f`.  -/
spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots : ∀ (K : Type u) [inst : NontriviallyNormedField K] (L : Type v) [inst_1 : Field L] [inst_2 : Algebra K L]
  [hu : IsUltrametricDist K] [inst_3 : CompleteSpace K] (x : L) {E : Type u_2} [inst_4 : Field E] [inst_5 : Algebra K E]
  [inst_6 : Algebra L E] [IsScalarTower K L E] [Polynomial.IsSplittingField L E ((Polynomial.mapAlg K L) (minpoly K x))]
  [inst_9 : Algebra.IsAlgebraic K E],
  (spectralMulAlgNorm K E) ((algebraMap L E) x) ^ (minpoly K x).natDegree =
    (spectralMulAlgNorm K E) ((Polynomial.mapAlg K E) (minpoly K x)).roots.prod
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_nonpos_of_nonneg_of_nonpos : ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → a.tdiv b ≤ 0
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.weakEquivalence_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {A : C} (self : HomotopicalAlgebra.PathObject A), HomotopicalAlgebra.WeakEquivalence self.ι
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.mk.sizeOf_spec : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : SizeOf R] [inst_6 : SizeOf M] [inst_7 : SizeOf N]
  (toFun : M → N) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x)
  (exists_companion' : ∃ B, ∀ (x y : M), toFun (x + y) = toFun x + toFun y + (B x) y),
  sizeOf { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' } =
    1 + sizeOf exists_companion'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.pretopology.congr_simp : ∀ (P P_1 : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (e_P : P = P_1) [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative], AlgebraicGeometry.Scheme.pretopology P = AlgebraicGeometry.Scheme.pretopology P_1
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIioIci_symm_apply_of_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} (h : x ≤ y), (OrderIso.sumLexIioIci x).symm y = toLex (Sum.inr ⟨y, h⟩)
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.mul_prod_Ioo_eq_prod_Ico : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a < b → f a * ∏ x ∈ Finset.Ioo a b, f x = ∏ x ∈ Finset.Ico a b, f x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF →
    (m.alter k f).getKey? k' =
      if (k == k') = true then if (f m[k]?).isSome = true then some k else none else m.getKey? k'
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_mul_rpow_neg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {a : A} (x : ℝ),
  autoParam (IsStrictlyPositive a) CFC.rpow_mul_rpow_neg._auto_1 → a ^ x * a ^ (-x) = 1
-- Mathlib.Algebra.GCDMonoid.Nat
Int.strongNormalizationMonoid : StrongNormalizationMonoid ℤ
-- Init.Data.Rat.Lemmas
Rat.lt_of_mul_lt_mul_left : ∀ {a b c : ℚ}, c * a < c * b → 0 ≤ c → a < b
-- Init.Data.List.Find
List.finIdxOf?_cons : ∀ {α : Type u_1} {b : α} [inst : BEq α] {a : α} {xs : List α},
  List.finIdxOf? b (a :: xs) =
    if (a == b) = true then some ⟨0, ⋯⟩ else Option.map (fun x => x.succ) (List.finIdxOf? b xs)
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
PartialHomeomorph.Simps.apply : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → PartialHomeomorph X Y → X → Y
-- Init.Data.BitVec.Lemmas
BitVec.sub_neg : ∀ {w : ℕ} {x y : BitVec w}, x - -y = x + y
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSemigroup.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α], Lex.instSemigroup = { toMul := Lex.instMul, mul_assoc := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasProd.congr_cofinite₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f g : α → K}
  [SeparatelyContinuousMul K] {c : K},
  HasProd f c →
    ∀ {s : Finset α}, (∀ a ∈ s, f a ≠ 0) → (∀ a ∉ s, f a = g a) → HasProd g (c * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i))
-- Mathlib.Data.Set.Finite.Range
Finite.Set.finite_range : ∀ {α : Type u} {ι : Sort w} (f : ι → α) [Finite ι], Finite ↑(Set.range f)
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_iSup_le_lift : ∀ {ι : Type u} {c : Cardinal.{v}} {f : ι → Ordinal.{v}},
  Cardinal.lift.{v, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, v} c → (∀ (i : ι), (f i).card ≤ c) → (⨆ i, f i).card ≤ c
-- Init.Data.Array.Count
Array.countP_empty : ∀ {α : Type u_1} {p : α → Bool}, Array.countP p #[] = 0
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- The cone `finiteSubproductsCone` is a limit cone.  -/
CategoryTheory.Limits.ProductsFromFiniteCofiltered.isLimitFiniteSubproductsCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
        (f : α → C) →
          [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C] →
            [inst_3 : CategoryTheory.Limits.HasProduct f] →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.mem_prepartition_iff : ∀ {ι : Type u_1} {n : ℕ} [inst : NeZero n] [inst_1 : Fintype ι] {B I : BoxIntegral.Box ι},
  I ∈ BoxIntegral.unitPartition.prepartition n B ↔
    ∃ ν ∈ BoxIntegral.unitPartition.admissibleIndex n B, BoxIntegral.unitPartition.box n ν = I
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_conj_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.isLocalizationMap_of_group : ∀ {M : Type u_1} {G : Type u_2} [inst : CommMonoid M] [inst_1 : CommGroup G] {S : Submonoid M} {f : M → G},
  Function.Injective f → (∀ (g : G), ∃ x, ∃ y ∈ S, g = f x / f y) → S.IsLocalizationMap f
-- Mathlib.Data.Multiset.Fintype
Multiset.map_univ_coe : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Multiset.map (fun x => x.fst) Finset.univ.val = m
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsRamified.ne_conjugate : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w₁ w₂ : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsRamified k w₂ → w₁.embedding ≠ NumberField.ComplexEmbedding.conjugate w₂.embedding
-- Init.Core
/-- A dependent recursion principle for `Quotient` that uses [heterogeneous
equality](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=HEq), analogous to a [recursor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=recursors) for
a structure.

`Quotient.recOn` is a version of this recursor that uses `Eq` instead of `HEq`.
 -/
Quotient.hrecOn : {α : Sort u} →
  {s : Setoid α} →
    {motive : Quotient s → Sort v} →
      (q : Quotient s) → (f : (a : α) → motive ⟦a⟧) → (∀ (a b : α), a ≈ b → f a ≍ f b) → motive q
-- Std.Http.Protocol.H1
/-- Returns `true` if the reader is in a failed state.
 -/
Std.Http.Protocol.H1.Machine.failed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app : ∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))
  (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso X Y).hom.app
      (SSet.Truncated.HomotopyCategory.mk (x, y)) =
    CategoryTheory.CategoryStruct.id
      (((SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y).comp
            (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y)).obj
        (SSet.Truncated.HomotopyCategory.mk (x, y)))
-- Mathlib.Data.Nat.Nth
/-- When `s` is an infinite set, `nth` agrees with `Nat.Subtype.orderIsoOfNat`.  -/
Nat.nth_apply_eq_orderIsoOfNat : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Infinite) (n : ℕ), Nat.nth p n = ↑((Nat.Subtype.orderIsoOfNat (Set.ofPred p)) n)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.intCast : ℤ → Lean.Grind.CommRing.Expr
-- Lean.Parser.Term
Lean.Parser.Term.configItem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roi_eq_mkSlice_roo : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ},
  Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Roo.Sliceable.mkSlice xs lo<...xs.size
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
/-- The projective spectrum of a graded commutative ring is the subtype of all homogeneous ideals
that are prime and do not contain the irrelevant ideal.  -/
ProjectiveSpectrum : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] → [inst_2 : AddSubmonoidClass σ A] → (𝒜 : ℕ → σ) → [GradedRing 𝒜] → Type u_1
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.abs_mem_subalgebra_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A),
  |↑f| ∈ A.topologicalClosure
-- Mathlib.Geometry.Manifold.Algebra.Monoid
mdifferentiableAt_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I 1 G] {a b : G},
  (MDiffAt fun x => a + x) b
-- Mathlib.Analysis.Normed.Module.MStructure
/-- This instance was created as an auxiliary definition when defining `Subtype.distribLattice`
all at once would cause a timeout. That is no longer the case. Keeping this as a useful shortcut.
 -/
IsLprojection.instLatticeSubtypeOfFaithfulSMul : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} → [inst_1 : Ring M] → [inst_2 : Module M X] → [FaithfulSMul M X] → Lattice { P // IsLprojection X P }
-- Mathlib.Data.Nat.Basic
Nat.leRecOn_injective : ∀ {C : ℕ → Sort u_1} {n m : ℕ} (hnm : n ≤ m) (next : {k : ℕ} → C k → C (k + 1)),
  (∀ (n : ℕ), Function.Injective next) → Function.Injective (Nat.leRecOn hnm fun {k} => next)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.merge_nil_right : ∀ {α : Type u_1} (t : Ordnode α), Ordnode.nil.merge t = t
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.dvd_choose_pow : ∀ {p n k : ℕ}, Nat.Prime p → k ≠ 0 → k ≠ p ^ n → p ∣ (p ^ n).choose k
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toLogFun.eq_1 : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial) (basis : Tactic.ComputeAsymptotics.Basis) (x : ℝ),
  m.toLogFun basis x = (List.zipWith (fun exp b => exp * Real.log (b x)) m basis).sum
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.NonemptyCompacts.isClosed_in_closeds`.

---

The range of `NonemptyCompacts.toCloseds` is closed in a complete space  -/
EMetric.NonemptyCompacts.isClosed_in_closeds : ∀ {α : Type u_1} [inst : EMetricSpace α] [CompleteSpace α],
  IsClosed (Set.range TopologicalSpace.NonemptyCompacts.toCloseds)
-- Mathlib.RingTheory.Nilpotent.Lemmas
LinearMap.isNilpotent_mulRight_iff : ∀ (R : Type u_1) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A),
  IsNilpotent (LinearMap.mulRight R a) ↔ IsNilpotent a
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `Equiv.toIso_hom_hom_apply`. -/
Equiv.toIso_hom : ∀ {X Y : Type u} (e : X ≃ Y) (x : X), (CategoryTheory.ConcreteCategory.hom e.toIso.hom) x = e x
-- Init.Sym.Lemmas
Lean.Sym.ite_true : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) {ht : c}, (if c then a else b) = a
-- Mathlib.RingTheory.FinitePresentation
AlgHom.FinitePresentation.of_finiteType : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [IsNoetherianRing A] {f : A →ₐ[R] B},
  f.FiniteType ↔ f.FinitePresentation
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
/-- For any compact subset `K ⊆ X`, there exist some compactly supported continuous nonnegative
functions `f` on `X` such that `f ≥ 1` on `K`.  -/
rieszContentAux_image_nonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [T2Space X] [LocallyCompactSpace X] (K : TopologicalSpace.Compacts X), (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}).Nonempty
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measure_preimage_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (g : G) (A : Set G), μ ((fun h => h + g) ⁻¹' A) = μ A
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.Context : Type
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
/-- Simultaneously restrict both the domains and scalars of a perfect pairing with coefficients in a
field.  -/
LinearMap.IsPerfPair.restrictScalars_of_field : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module L M] [inst_6 : Module L N] [inst_7 : Module K M]
  [inst_8 : Module K N] [inst_9 : IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [inst_10 : p.IsPerfPair] {M' : Type u_5}
  {N' : Type u_6} [inst_11 : AddCommGroup M'] [inst_12 : AddCommGroup N'] [inst_13 : Module K M']
  [inst_14 : Module K N'] [inst_15 : IsScalarTower K L N] (i : M' →ₗ[K] M) (j : N' →ₗ[K] N),
  Function.Injective ⇑i →
    Function.Injective ⇑j →
      p.IsPerfectCompl (Submodule.span L ↑i.range) (Submodule.span L ↑j.range) →
        ∀ (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range),
          (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.monotone_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Monotone (MeasurableSpace.map f)