mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.top_prod_top : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S], ⊤.prod ⊤ = ⊤
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.of_fullyFaithful_restrictedULiftYoneda : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.Full] (h : (CategoryTheory.Presheaf.restrictedULiftYoneda F).FullyFaithful),
  F.IsDense
-- Init.Data.Fin.Fold
Fin.foldlM_zero : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (f : α → Fin 0 → m α), Fin.foldlM 0 f = pure
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instPartialOrder : PartialOrder ℚ
-- Mathlib.Order.Filter.Map
Filter.pure_bind : ∀ {α : Type u_1} {β : Type u_2} (a : α) (m : α → Filter β), (pure a).bind m = m a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
IsSelfAdjoint.spectrumRestricts : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [ContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A}, IsSelfAdjoint a → SpectrumRestricts a ⇑Complex.reCLM
-- Std.Http.Data.Headers
/-- Checks if the headers are empty.
 -/
Std.Http.Headers.isEmpty : Std.Http.Headers → Bool
-- Batteries.Data.List.Count
List.snd_idxToSigmaCount : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs : List α} {i : Fin xs.length},
  (xs.idxToSigmaCount i).snd = ⟨List.countBefore xs[↑i] xs ↑i, ⋯⟩
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.mulRightReflectLT : ∀ {α : Type u} [inst : LT α] [inst_1 : Mul α] [c : MulRightReflectLT α], MulRightReflectLT αᵒᵈ
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.mkOfSMul'_smul : ∀ {R : Type u} [inst : Ring R] {A : AddCommGrpCat} (φ : R →+* CategoryTheory.End A) (r : R)
  (x : ↑(ModuleCat.mkOfSMul' φ)),
  r • x =
    (CategoryTheory.ConcreteCategory.hom
        (have this := φ r;
        this))
      x
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_le : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {s t : Submodule R M},
  Submodule.restrictScalars S s ≤ Submodule.restrictScalars S t ↔ s ≤ t
-- Init.Data.List.Range
List.range_sublist : ∀ {m n : ℕ}, (List.range m).Sublist (List.range n) ↔ m ≤ n
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (n : ℤ) (X : HomologicalComplex C (ComplexShape.up ℤ)) (i : ℤ),
  ((F.mapCochainComplexShiftIso n).hom.app X).f i = CategoryTheory.CategoryStruct.id (F.obj (X.X (i + n)))
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_neg : ∀ {w : ℕ} {x : BitVec w} {y : ℕ}, (-x) <<< y = -x <<< y
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l}, Lean.Order.meet P Q = Lean.Order.meet Q P
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {val : PresheafOfModules R.obj}
  {isSheaf : CategoryTheory.Presheaf.IsSheaf J val.presheaf} {val_1 : PresheafOfModules R.obj}
  {isSheaf_1 : CategoryTheory.Presheaf.IsSheaf J val_1.presheaf},
  { val := val, isSheaf := isSheaf } = { val := val_1, isSheaf := isSheaf_1 } → val = val_1
-- Mathlib.Data.List.Map2
List.zipLeft'_nil_left : ∀ {α : Type u} {β : Type v} (bs : List β), [].zipLeft' bs = ([], bs)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_eq_single : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → M} (a : ι),
  (∀ b ∈ s, b ≠ a → f b = 0) → (a ∉ s → f a = 0) → ∑ x ∈ s, f x = f a
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.natIso_hom_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁}
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i)
  (X : CategoryTheory.Discrete I), (CategoryTheory.Discrete.natIso f).hom.app X = (f X).hom
-- Mathlib.Order.UpperLower.Hom
LowerSet.coe_iicsInfHom : ∀ {α : Type u_1} [inst : CompleteLattice α], ⇑LowerSet.iicsInfHom = LowerSet.Iic
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_embDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] (f : α ↪ β) (v : α →₀ M),
  (Finsupp.embDomain f v).support = Finset.map f v.support
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- The interval integral `∫ x in a..b, f x ∂μ` is defined
as `∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ`. If `a ≤ b`, then it equals
`∫ x in Ioc a b, f x ∂μ`, otherwise it equals `-∫ x in Ioc b a, f x ∂μ`.  -/
«term∫_In_.._,_∂_» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.eq_id_of_finrank_le_one : ∀ {R : Type u_3} {V : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  [Module.Free R V] [Module.Finite R V] [StrongRankCondition R] {f : Module.Dual R V} {v : V},
  f v = 0 → Module.finrank R V ≤ 1 → LinearMap.transvection f v = LinearMap.id
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0_k_var : ∀ (x : Lean.Grind.AC.Var), (Lean.Grind.AC.Seq.var x).erase0_k = Lean.Grind.AC.Seq.var x
-- Mathlib.Logic.Equiv.Functor
Bifunctor.mapEquiv.congr_simp : ∀ {α β : Type u} {α' β' : Type v} (F : Type u → Type v → Type w) [inst : Bifunctor F] [inst_1 : LawfulBifunctor F]
  (h h_1 : α ≃ β),
  h = h_1 → ∀ (h' h'_1 : α' ≃ β'), h' = h'_1 → Bifunctor.mapEquiv F h h' = Bifunctor.mapEquiv F h_1 h'_1
-- Mathlib.Order.Bounds.Basic
isGLB_Ioi : ∀ {γ : Type u_3} [inst : LinearOrder γ] [DenselyOrdered γ] {a : γ}, IsGLB (Set.Ioi a) a
-- Mathlib.GroupTheory.FreeGroup.GeneratorEquiv
/-- Isomorphic free groups have equivalent bases (`IsFreeGroup` variant).  -/
Equiv.ofIsFreeGroupEquiv : {G : Type u_3} →
  {H : Type u_4} →
    [inst : Group G] →
      [inst_1 : Group H] →
        [inst_2 : IsFreeGroup G] →
          [inst_3 : IsFreeGroup H] → G ≃* H → IsFreeGroup.Generators G ≃ IsFreeGroup.Generators H
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- **Alias** of `FourierTransform.fourierCLM`. -/
TemperedDistribution.fourierTransformCLM : (R : Type u_2) →
  (E : Type u_3) →
    {F : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransform E F] →
                  [FourierAdd E F] →
                    [FourierSMul R E F] →
                      [inst_8 : TopologicalSpace E] →
                        [inst_9 : TopologicalSpace F] → [ContinuousFourier E F] → E →L[R] F
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.hom_ext : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f₁ f₂ : X ⟶ Y),
  (∀ (x : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f x) f₁ = CategoryTheory.CategoryStruct.comp (𝒰.f x) f₂) →
    f₁ = f₂
-- Mathlib.Algebra.Azumaya.Basic
/-- The "canonical" isomorphism between `R ⊗ Rᵒᵖ` and `End R R` which is equal
to `AlgHom.mulLeftRight R R`.  -/
IsAzumaya.tensorEquivEnd : (R : Type u_1) → [inst : CommSemiring R] → TensorProduct R R Rᵐᵒᵖ ≃ₐ[R] Module.End R R
-- Mathlib.NumberTheory.Real.Irrational
irrational_sqrt_ratCast_iff : ∀ {q : ℚ}, Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
Path.instSubsingletonPUnitUnit : Subsingleton (Path PUnit.unit PUnit.unit)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C),
  (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone F).cone.pt =
    CategoryTheory.Limits.limit (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂'_term.eq_1 : ∀ (n : ℤ) (z τ : ℂ), jacobiTheta₂'_term n z τ = 2 * ↑Real.pi * Complex.I * ↑n * jacobiTheta₂_term n z τ
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- The naive pre-submersive presentation of a quotient `R[Xᵢ] ⧸ (vⱼ)`.
If the definitional equality of the section matters, it can be explicitly provided.

To construct the associated submersive presentation, use
`PreSubmersivePresentation.jacobiMatrix_naive`.
 -/
Algebra.PreSubmersivePresentation.naive : {R : Type u} →
  {ι : Type w} →
    {σ : Type t} →
      [inst : CommRing R] →
        {v : ι → MvPolynomial σ R} →
          (a : ι → σ) →
            Function.Injective a →
              (s : optParam (MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R) (Function.surjInv ⋯)) →
                autoParam
                    (∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)),
                      (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
                    Algebra.PreSubmersivePresentation.naive._auto_1 →
                  Algebra.PreSubmersivePresentation R (MvPolynomial σ R ⧸ Ideal.span (Set.range v)) σ ι
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.constMulHom_apply : ∀ (α : Type u_5) (β : Type u_6) [inst : Mul β] (a : β) (a_1 : α), (Pi.constMulHom α β) a a_1 = Function.const α a a_1
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.Extension.H1Cotangent.equivOfFormallySmooth.congr_simp : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (P₁ : Algebra.Extension R A) (P₂ : Algebra.Extension R A) [inst_3 : Algebra.FormallySmooth R P₁.Ring]
  [inst_4 : Algebra.FormallySmooth R P₂.Ring],
  Algebra.Extension.H1Cotangent.equivOfFormallySmooth P₁ P₂ = Algebra.Extension.H1Cotangent.equivOfFormallySmooth P₁ P₂
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.mk'_num_den : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K),
  IsLocalization.mk' K (IsFractionRing.num A x) (IsFractionRing.den A x) = x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t.WF → ∀ {v : β}, (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.toSetoid_injective : ∀ {X : Type u_2} [inst : TopologicalSpace X], Function.Injective DiscreteQuotient.toSetoid
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.instFromJsonMakeEditLinkProps.fromJson : Lean.Json → Except String ProofWidgets.MakeEditLinkProps
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.sigmaFinite_restrict : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f : α → β} [inst_1 : Zero β] [inst_2 : T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ),
  MeasureTheory.SigmaFinite (μ.restrict hf.sigmaFiniteSet)
-- Lean.Elab.PreDefinition.Main
Lean.Elab.shouldUseWF : Array Lean.Elab.PreDefinition → Bool
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  {x : HahnSeries Γ V},
  0 < x.orderTop →
    ∀ (f : PowerSeries R) (n : ℕ), (HahnSeries.SummableFamily.powerSeriesFamily x f) n = (PowerSeries.coeff n) f • x ^ n
-- Mathlib.Analysis.Matrix.Hermitian
Matrix.IsHermitian.im_star_dotProduct_mulVec_self : ∀ {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [inst : RCLike 𝕜] [inst_1 : Fintype n],
  A.IsHermitian → ∀ (x : n → 𝕜), RCLike.im (star x ⬝ᵥ A.mulVec x) = 0
-- Mathlib.Data.Fintype.Prod
/-- **Alias** of `Set.toFinset_offDiag`. -/
Set.toFinset_off_diag : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑s.offDiag], s.offDiag.toFinset = s.toFinset.offDiag
-- Mathlib.Data.FunLike.Group
FunLike.negZeroClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Neg F]
  [inst_3 : NegZeroClass β] [inst_4 : IsZeroApply F α β] [inst_5 : IsNegApply F α β],
  FunLike.negZeroClass = Function.Injective.negZeroClass (fun f => ⇑f) ⋯ ⋯ ⋯
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} {μ' : MeasureTheory.Measure α} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C'),
  μ.AbsolutelyContinuous μ' →
    ∀ (f : ↥(α →₁ₛ[μ] E)) (f' : ↥(α →₁ₛ[μ'] E)),
      ↑↑↑f =ᵐ[μ] ↑↑↑f' →
        (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ' hT') f'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).minKey ⋯ = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Order.Interval.Set.Defs
/-- We say that a set `s : Set α` is `OrdConnected` if for all `x y ∈ s` it includes the
interval `[[x, y]]`. If `α` is a `DenselyOrdered` `ConditionallyCompleteLinearOrder` with
the `OrderTopology`, then this condition is equivalent to `IsPreconnected s`. If `α` is a
linearly ordered field, then this condition is also equivalent to `Convex α s`.  -/
Set.OrdConnected : {α : Type u_1} → [Preorder α] → Set α → Prop
-- Mathlib.Logic.Equiv.Prod
Equiv.prodPUnit_apply : ∀ (α : Type u_9) (p : α × PUnit.{u_10 + 1}), (Equiv.prodPUnit α) p = p.1
-- Batteries.Lean.Except
Except.map_ok : ∀ {α β : Type u_1} {ε : Type u} (f : α → β) (x : α), f <$> Except.ok x = Except.ok (f x)
-- Init.Data.String.Iterator
/-- The number of UTF-8 bytes remaining in the iterator.
 -/
String.Legacy.Iterator.remainingBytes : String.Legacy.Iterator → ℕ
-- Mathlib.Analysis.Convex.Between
/-- A point lies in the interior of a 1-dimensional face of a simplex if and only if it lies
strictly between its vertices.  -/
Affine.Simplex.mem_interior_face_iff_sbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {n : ℕ}
  (s : Affine.Simplex R P n) {p : P} {i j : Fin (n + 1)} (h : i ≠ j),
  p ∈ (s.face ⋯).interior ↔ Sbtw R (s.points i) p (s.points j)
-- Std.Data.DTreeMap.Internal.Balancing
/-- Rebalances a tree after at most one element was added or removed from either subtree.  -/
Std.DTreeMap.Internal.Impl.balance : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced →
            r.Balanced →
              Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
                  Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size →
                Std.DTreeMap.Internal.Impl α β
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_assoc_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
  (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).hom.app X)
      ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).hom.app X)
      ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X))
-- Mathlib.Algebra.Lie.Ideal
/-- An ideal of `L` is a Lie subalgebra of `L`, so it is a Lie ring.  -/
LieIdeal.lieRing : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (I : LieIdeal R L) → LieRing ↥I
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIco_filter : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G],
  (SummationFilter.symmetricIco G).filter = Filter.map (fun N => Finset.Ico (-N) N) Filter.atTop
-- Mathlib.CategoryTheory.Core
/-- `ofEquivFunctor m` lifts a type-level `EquivFunctor`
to a categorical functor `Core (Type u₁) ⥤ Core (Type u₂)`.
 -/
CategoryTheory.ofEquivFunctor : (m : Type u₁ → Type u₂) →
  [EquivFunctor m] → CategoryTheory.Functor (CategoryTheory.Core (Type u₁)) (CategoryTheory.Core (Type u₂))
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_set_normalizer_iff : ∀ {G : Type u_1} [inst : Group G] {S : Set G} {g : G}, g ∈ Subgroup.normalizer S ↔ ∀ (h : G), h ∈ S ↔ g * h * g⁻¹ ∈ S
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_add_right : ∀ {α : Type u_2} [inst : Add α] [IsRightCancelAdd α] [inst_2 : DecidableEq α] {s t : Finset α},
  t.Nonempty → s.card ≤ (s + t).card
-- Mathlib.Order.Monotone.Monovary
MonotoneOn.monovaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι} [inst_2 : LinearOrder ι], MonotoneOn f s → MonotoneOn g s → MonovaryOn f g s
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_unionFuel : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (fuel : ℕ) (s₁ s₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx (Lean.Grind.AC.Seq.unionFuel fuel s₁ s₂) =
    ctx.op (Lean.Grind.AC.Seq.denote ctx s₁) (Lean.Grind.AC.Seq.denote ctx s₂)
-- Mathlib.Topology.Sets.Compacts
/-- The type of compact sets of a topological space.  -/
TopologicalSpace.Compacts : (α : Type u_4) → [TopologicalSpace α] → Type u_4
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Given an isomorphism `S₁ ≅ S₂` of short complexes and homology data `h₁` and `h₂`
for `S₁` and `S₂` respectively, this is the induced homology isomorphism `h₁.left.H ≅ h₁.left.H`.  -/
CategoryTheory.ShortComplex.homologyMapIso' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) → (h₁ : S₁.HomologyData) → (h₂ : S₂.HomologyData) → h₁.left.H ≅ h₂.left.H
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The forgetful functor from additive group objects to the ambient category.  -/
CategoryTheory.AddGrp.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.Functor (CategoryTheory.AddGrp C) C
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.addSubmonoidWithOneClass : ∀ (S : Type u_1) (R : Type u) {x : NonAssocSemiring R} [inst : SetLike S R] [h : SubsemiringClass S R],
  AddSubmonoidWithOneClass S R
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.biprod.mapBiprod_hom_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] (X Y : C)
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_6 : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] {W : C} (f : X ⟶ W) (g : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp (F.mapBiprod X Y).hom (CategoryTheory.Limits.biprod.desc (F.map f) (F.map g)) =
    F.map (CategoryTheory.Limits.biprod.desc f g)
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.conesIsoComponentHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J D} (X : Cᵒᵖ)
  (t : (F.op.comp ((CategoryTheory.cones J D).obj K)).obj X),
  adj.conesIsoComponentHom X t =
    { app := fun j => (adj.homEquiv (Opposite.unop X) (K.obj j)) (t.app j), naturality := ⋯ }
-- Mathlib.Algebra.Quaternion
/-- The cardinality of a quaternion algebra, as a set.  -/
Cardinal.mk_univ_quaternionAlgebra : ∀ {R : Type u_1} (c₁ c₂ c₃ : R), Cardinal.mk ↑Set.univ = Cardinal.mk R ^ 4
-- Mathlib.Order.Types.Defs
/-- The order type of the linear order on `α`.  -/
OrderType.type : (α : Type u) → [LinearOrder α] → OrderType.{u}
-- Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
_private.Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity.0.«termℤ[i]» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.cancel_left : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : One M] [inst_1 : One N] [inst_2 : One P] {g : OneHom N P}
  {f₁ f₂ : OneHom M N}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Algebra.Pointwise.Stabilizer
_private.Mathlib.Algebra.Pointwise.Stabilizer.0.MulAction.termQ : Lean.ParserDescr
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- If a star subalgebra of `C(X, 𝕜)` separates points, then the real subalgebra
of its purely real-valued elements also separates points.  -/
Subalgebra.SeparatesPoints.rclike_to_real : ∀ {𝕜 : Type u_1} {X : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] {A : StarSubalgebra 𝕜 C(X, 𝕜)},
  A.SeparatesPoints →
    (Subalgebra.comap (AlgHom.compLeftContinuous ℝ RCLike.ofRealAm ⋯)
        (Subalgebra.restrictScalars ℝ A.toSubalgebra)).SeparatesPoints
-- Mathlib.Data.EReal.Operations
EReal.add_ne_top_iff_ne_top_left : ∀ {x y : EReal}, y ≠ ⊥ → y ≠ ⊤ → (x + y ≠ ⊤ ↔ x ≠ ⊤)
-- Mathlib.Algebra.Order.Monoid.TypeTags
Multiplicative.isOrderedCancelMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α],
  IsOrderedCancelMonoid (Multiplicative α)
-- Mathlib.AlgebraicGeometry.Stalk
/-- The canonical map `Spec 𝒪_{X, x} ⟶ U` given `x ∈ U ⊆ X`.  -/
AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → (x : ↥X) → x ∈ U → (AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ ↑U)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.prodMap : ∀ {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [inst : CommMonoid α₁] [inst_1 : CommMonoid α₂]
  [inst_2 : CommMonoid β₁] [inst_3 : CommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂}
  {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ},
  IsMulFreimanHom n A₁ B₁ f₁ → IsMulFreimanHom n A₂ B₂ f₂ → IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousAt_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Type u_4} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f : ι → α → γ} {a : Finset ι},
  (∀ i ∈ a, UpperSemicontinuousAt (f i) x) → UpperSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x