mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
/-- The image of the proposed limit cone for `F : J ⥤ Mon C` under the forgetful functor
`forget C : Mon C ⥤ C` is isomorphic to the limit cone of `F ⋙ forget C`.
 -/
CategoryTheory.Mon.forgetMapConeLimitConeIso : {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.forget C).mapCone (CategoryTheory.Mon.limitCone F c hc) ≅ c
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConstC.eq_1 : ∀ (k : ℤ) (p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Poly.mulConstC k p c =
    bif k % ↑c == 0 then Lean.Grind.CommRing.Poly.num 0
    else bif k % ↑c == 1 then p else Lean.Grind.CommRing.Poly.mulConstC.go k c p
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintLabelPart.fromJson : Lean.Json → Except String Lean.Lsp.InlayHintLabelPart
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Call.mk : Lean.Expr → Lean.Expr → Lean.Meta.FunInd.Call
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coordChange_coordChange : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e₁ e₂ e₃ : Bundle.Trivialization F proj) {b : B},
  b ∈ e₁.baseSet → b ∈ e₂.baseSet → ∀ (x : F), e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x
-- Mathlib.Combinatorics.Matroid.Basic
/-- create a copy of `M : Matroid α` with a base predicate and ground set defeq
to supplied arguments that are provably equal to those of `M`.  -/
Matroid.copyBase : {α : Type u_1} →
  (M : Matroid α) → (E : Set α) → (IsBase : Set α → Prop) → E = M.E → (∀ (B : Set α), IsBase B ↔ M.IsBase B) → Matroid α
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_union_le_size_add_size : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Mathlib.CategoryTheory.Sites.InducedTopology
/-- The coarsest topology containing all sieves whose image under `F` generates a covering sieve
of `K`.  -/
CategoryTheory.Functor.restrictedTopology : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.GrothendieckTopology D → CategoryTheory.GrothendieckTopology C
-- Mathlib.Algebra.Algebra.Tower
Algebra.lsmul_coe : ∀ (R : Type u) {A : Type w} (B : Type u₁) (M : Type v₁) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M] [inst_6 : Module R M]
  [inst_7 : Module A M] [inst_8 : Module B M] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (a : A), ⇑((Algebra.lsmul R B M) a) = fun x => a • x
-- Lean.Meta.Basic
Lean.Meta.Cache.mk.injEq : ∀ (inferType : Lean.Meta.InferTypeCache) (funInfo : Lean.Meta.FunInfoCache)
  (synthInstance : Lean.Meta.SynthInstanceCache) (whnf : Lean.Meta.WhnfCache)
  (defEqTrans defEqPerm : Lean.Meta.DefEqCache) (inferType_1 : Lean.Meta.InferTypeCache)
  (funInfo_1 : Lean.Meta.FunInfoCache) (synthInstance_1 : Lean.Meta.SynthInstanceCache) (whnf_1 : Lean.Meta.WhnfCache)
  (defEqTrans_1 defEqPerm_1 : Lean.Meta.DefEqCache),
  ({ inferType := inferType, funInfo := funInfo, synthInstance := synthInstance, whnf := whnf, defEqTrans := defEqTrans,
        defEqPerm := defEqPerm } =
      { inferType := inferType_1, funInfo := funInfo_1, synthInstance := synthInstance_1, whnf := whnf_1,
        defEqTrans := defEqTrans_1, defEqPerm := defEqPerm_1 }) =
    (inferType = inferType_1 ∧
      funInfo = funInfo_1 ∧
        synthInstance = synthInstance_1 ∧ whnf = whnf_1 ∧ defEqTrans = defEqTrans_1 ∧ defEqPerm = defEqPerm_1)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_eq_presieve₀_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S},
  E.presieve₀ = F.presieve₀ ↔ E.shrink = F.shrink
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
          k ∈ List.map Sigma.fst l → (↑(m.insertMany l)).getKey? k' = some k
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.scomp_hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F}
  {g₁' : F}, HasDerivAt g₁ g₁' (h x) → HasDerivWithinAt h h' s x → HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_sub_int' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddGroupWithOne G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℤ), f (x - ↑n) = f x - n • b
-- Lean.Elab.Match
/-- Remark: if the discriminant is `Syntax.missing`, we abort the elaboration of the `match`-expression.
This can happen due to error recovery. Example
```
example : (p ∨ p) → p := fun h => match
```
If we don't abort, the elaborator loops because we will keep trying to expand
```
match
```
into
```
let d := <Syntax.missing>; match
```
Recall that `Syntax.setArg stx i arg` is a no-op when `i` is out-of-bounds.  -/
Lean.Elab.Term.isAtomicDiscr : Lean.Syntax → Lean.Elab.TermElabM Bool
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Noether's second isomorphism theorem**: given a subgroup `N` of `G` and a
subgroup `H` of the normalizer of `N` in `G`,
defines an isomorphism between `H/(H ∩ N)` and `(HN)/N`.  -/
QuotientGroup.quotientInfEquivProdNormalizerQuotient : {G : Type u} →
  [inst : Group G] →
    (H N : Subgroup G) → (hLE : H ≤ Subgroup.normalizer ↑N) → ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
-- Mathlib.Algebra.Algebra.Operations
/-- `Submodule.pointwiseNeg` distributes over multiplication.

This is available as an instance in the `Pointwise` locale.  -/
Submodule.hasDistribPointwiseNeg : {R : Type u} →
  [inst : CommSemiring R] → {A : Type u_1} → [inst_1 : Ring A] → [inst_2 : Algebra R A] → HasDistribNeg (Submodule R A)
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize : ∀ (φ : FirstOrder.Language.ring.Sentence),
  FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ → {p | ¬FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}.Finite
-- Mathlib.Data.LawfulXor.Basic
xor_cancel_right : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a b : α), a ^^^ b ^^^ b = a
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
inv_lt_of_mabs_lt : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α],
  |a|ₘ < b → b⁻¹ < a
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instInhabited : Inhabited AddCommMonCat
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_inter_le_size_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.isOrderedRing : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedRing α], IsOrderedRing { x // 0 ≤ x }
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mkCommaObject_right_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (X : C),
  (CategoryTheory.WithInitial.mkCommaObject F).right.obj X = F.obj (CategoryTheory.WithInitial.incl.obj X)
-- Mathlib.Topology.Closure
/-- The complement of a set has the same frontier as the original set.  -/
frontier_compl : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), frontier sᶜ = frontier s
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
Complex.val_UnitI : ↑Complex.UnitI = Complex.I
-- Std.Sat.AIG.CachedLemmas
/-- The central equality theorem between `mkConstCached` and `mkConst`.
 -/
Std.Sat.AIG.denote_mkConstCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {val : Bool} {aig : Std.Sat.AIG α},
  ⟦assign, { aig := aig, ref := aig.mkConstCached val }⟧ = val
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_iInf : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {ι : Sort u_1} [Nonempty ι] (f : F),
  Function.Injective ⇑f →
    ∀ (s : ι → NonUnitalSubring R), NonUnitalSubring.map f (iInf s) = ⨅ i, NonUnitalSubring.map f (s i)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- In a 2-truncated quasicategory, left homotopy implies right homotopy.
 -/
SSet.Truncated.HomotopicL.homotopicR : ∀ {X : SSet.Truncated 2} [X.Quasicategory₂]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicL f g → SSet.Truncated.HomotopicR f g
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.sub_liftCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {A : C} (k k' : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) (hk' : CategoryTheory.CategoryStruct.comp k' S.g = 0),
  S.liftCycles k hk - S.liftCycles k' hk' = S.liftCycles (k - k') ⋯
-- Mathlib.Algebra.Free
FreeMagma.pure_bind : ∀ {α β : Type u} (f : α → FreeMagma β) (x : α), pure x >>= f = f x
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.toSeminormedGroup.eq_1 : ∀ {E : Type u_5} [inst : NormedGroup E],
  NormedGroup.toSeminormedGroup =
    { toNorm := inst.toNorm, toGroup := inst.toGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.prime_of_irreducible_absNorm_span : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] {a : S},
  a ≠ 0 → Irreducible (Ideal.absNorm (Ideal.span {a})) → Prime a
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete, runs the `IO` action `f` on its result, and then
continues as the resulting task. This new task has priority `prio`.

Running the resulting `BaseIO` action causes this new task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped.
 -/
BaseIO.bindTask : {α : Type u_1} →
  {β : Type} →
    Task α →
      (α → BaseIO (Task β)) → optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task β)
-- Init.Data.String.TakeDrop
/-- Returns a `String.Slice` obtained by removing the specified number of characters \(Unicode code
points\) from the start of the string.

If `n` is greater than `s.toList.length`, returns an empty slice.

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

Examples:

* `"red green blue".drop 4 == "green blue".toSlice`

* `"red green blue".drop 10 == "blue".toSlice`

* `"red green blue".drop 50 == "".toSlice`

* `"مرحبا بالعالم".drop 3 == "با بالعالم".toSlice`
 -/
String.drop : String → ℕ → String.Slice
-- Lean.Meta.Tactic.Grind.Theorems
/-- A global declaration in the environment.  -/
Lean.Meta.Grind.Origin.decl : Lean.Name → Lean.Meta.Grind.Origin
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_inter_support_eq : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (s t : Set α),
  s ∩ Function.support f = t ∩ Function.support f → ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The cone associated to a pullback is a limit cone.  -/
CategoryTheory.Limits.pullback.isLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasPullback f g] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.pullback.cone f g)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Chord
SimpleGraph.Walk.isChord_sym2Mk : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {u' v' : V},
  p.IsChord s(u', v') ↔ G.Adj u' v' ∧ s(u', v') ∉ p.edges ∧ u' ∈ p.support ∧ v' ∈ p.support
-- Init.System.IO
/-- Returns metadata for the indicated file, following symlinks. Throws an exception if the file does
not exist or the metadata cannot be accessed.
 -/
System.FilePath.metadata : System.FilePath → IO IO.FS.Metadata
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.Decidable.instLawfulBackwardPatternForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.LawfulBackwardPattern p
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_zero : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {c : ℝ} (g' : α → F') (l : Filter α), 0 ≤ c → Asymptotics.IsBigOWith c l (fun _x => 0) g'
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- The absolute convex hull of a set `s` is the minimal absolute convex set that includes `s`.  -/
absConvexHull : (𝕜 : Type u_1) →
  {E : Type u_2} → [SeminormedRing 𝕜] → [SMul 𝕜 E] → [AddCommMonoid E] → [PartialOrder 𝕜] → ClosureOperator (Set E)
-- Mathlib.Tactic.Widget.SelectInsertParamsClass
_private.Mathlib.Tactic.Widget.SelectInsertParamsClass.0.Lean.Elab.mkSelectInsertParamsInstance : Lean.Name → Lean.Elab.TermElabM Lean.Command
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioi_of_Ici : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a : ι → α}
  {A : α}, Filter.Tendsto a l (nhds A) → MeasureTheory.AECover (μ.restrict (Set.Ioi A)) l fun i => Set.Ici (a i)
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.isPrime_of_irreducible_absNorm : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] {I : Ideal S},
  Irreducible (Ideal.absNorm I) → I.IsPrime
-- Init.Data.String.Lemmas.Basic
String.singleton_inj : ∀ {c d : Char}, String.singleton c = String.singleton d ↔ c = d
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat],
  ((SheafOfModules.forget R).comp (PresheafOfModules.restrictScalars α)).Faithful
-- Mathlib.Algebra.Star.StarAlgHom
/-- The `Function.prod` of two morphisms is a morphism.  -/
NonUnitalStarAlgHom.prod : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : DistribMulAction R B] →
                    [inst_6 : Star B] →
                      [inst_7 : NonUnitalNonAssocSemiring C] →
                        [inst_8 : DistribMulAction R C] →
                          [inst_9 : Star C] → (A →⋆ₙₐ[R] B) → (A →⋆ₙₐ[R] C) → A →⋆ₙₐ[R] B × C
-- Mathlib.Order.CompleteLattice.Defs
ofDual_sInf : ∀ {α : Type u_1} [inst : SupSet α] (s : Set αᵒᵈ), OrderDual.ofDual (sInf s) = sSup (⇑OrderDual.toDual ⁻¹' s)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- `[]` is `Sorted`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} (f : ℝ → ℝ),
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
      f).Sorted
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_coe_pi : 2 • ↑Real.pi = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_mem_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β} {a : α} {b : β},
  a ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instIntCast.eq_1 : ∀ {R : Type u_1} [inst : IntCast R], MulOpposite.instIntCast = { intCast := fun n => MulOpposite.op ↑n }
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonServerInfo : Lean.FromJson Lean.Lsp.ServerInfo
-- Mathlib.Algebra.Algebra.Basic
nat_algebra_subsingleton : ∀ {R : Type u_1} [inst : Semiring R], Subsingleton (Algebra ℕ R)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Equality of the composition of the unit, associator, and counit with the identity
`F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F`  -/
CategoryTheory.Adjunction.CoreUnitCounit.left_triangle : ∀ {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}
  (self : CategoryTheory.Adjunction.CoreUnitCounit F G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.unit F)
      (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft self.counit)) =
    CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F)
-- Mathlib.RepresentationTheory.Homological.Resolution
classifyingSpaceUniversalCover_obj : ∀ (G : Type u) [inst : Monoid G] (n : SimplexCategoryᵒᵖ),
  (classifyingSpaceUniversalCover G).obj n = Action.ofMulAction G (Fin ((Opposite.unop n).len + 1) → G)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_X_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (i : σ) (m : σ →₀ ℕ) (k : ℕ),
  MvPolynomial.coeff m (MvPolynomial.X i ^ k) = if (fun₀ | i => k) = m then 1 else 0
-- Init.Data.UInt.Lemmas
UInt16.mod_self : ∀ {a : UInt16}, a % a = 0
-- Mathlib.Logic.Unique
Unique.toInhabited : {α : Sort u} → Unique α → Inhabited α
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.IsDPMorphism.comp : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} {C : Type u_3} [inst_2 : CommSemiring C] {K : Ideal C}
  (hK : DividedPowers K) {f : A →+* B} {g : B →+* C},
  hJ.IsDPMorphism hK g → hI.IsDPMorphism hJ f → hI.IsDPMorphism hK (g.comp f)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instSubNegZeroMonoid : (A : Type u_3) → (E : Type u_4) → [SubNegZeroMonoid E] → SubNegZeroMonoid (WithCStarModule A E)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- A modification `Γ` between oplax natural transformations `η` and `θ` (between lax functors)
consists of a family of 2-morphisms `Γ.app a : η.app a ⟶ θ.app a`, which satisfies the equation
`(F.map f ◁ app b) ≫ θ.naturality f = η.naturality f ≫ (app a ▷ G.map f)`
for each 1-morphism `f : a ⟶ b`.
 -/
CategoryTheory.Lax.OplaxTrans.Modification : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A] [T2Space A] (s : Set A),
  (StarAlgebra.adjoin R s).topologicalClosure ≤ StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R s)
-- Mathlib.Data.Real.Basic
Real.instField : Field ℝ
-- Mathlib.Geometry.RingedSpace.OpenImmersion
_private.Mathlib.Geometry.RingedSpace.OpenImmersion.0.AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.termIsOpenImmersion : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendId_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F),
  s.extendId.inv.hom = CategoryTheory.CategoryStruct.id s.pt
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of colimits along an equivalence in the shape.  -/
CategoryTheory.Limits.preservesColimitsOfShape_of_equiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {J' : Type w₂}
  [inst_3 : CategoryTheory.Category.{w₂', w₂} J'] (e : J ≌ J') (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape J F], CategoryTheory.Limits.PreservesColimitsOfShape J' F