mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : β → β},
  Std.DHashMap.Const.get? (Std.DHashMap.Const.modify m k f) k = Option.map f (Std.DHashMap.Const.get? m k)
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext : Type
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a + x) ⁻¹' Set.Ico b c = Set.Ico (b - a) (c - a)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.mulMon_NonnegCoeffs : ∀ {p : Lean.Grind.CommRing.Poly} {k : ℤ} (m : Lean.Grind.CommRing.Mon),
  k ≥ 0 → p.NonnegCoeffs → (Lean.Grind.CommRing.Poly.mulMon k m p).NonnegCoeffs
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- `meromorphicTrailingCoefficientAt` is invariant under translation.  -/
meromorphicTrailingCoeffAt_comp_sub_const_eq_meromorphicTrailingCoeffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x c : 𝕜},
  meromorphicTrailingCoeffAt (f ∘ fun x => x - c) x = meromorphicTrailingCoeffAt f (x - c)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.instSetoidConsForallReal : (basis_hd : ℝ → ℝ) →
  (basis_tl : Tactic.ComputeAsymptotics.Basis) →
    Setoid (Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl))
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.mk.injEq : ∀ (keys : Array Lean.Meta.SimpTheoremKey) (levelParams : Array Lean.Name) (proof : Lean.Expr) (priority : ℕ)
  (post perm : Bool) (origin : Lean.Meta.Origin) (rfl backwardRfl : Bool) (keys_1 : Array Lean.Meta.SimpTheoremKey)
  (levelParams_1 : Array Lean.Name) (proof_1 : Lean.Expr) (priority_1 : ℕ) (post_1 perm_1 : Bool)
  (origin_1 : Lean.Meta.Origin) (rfl_1 backwardRfl_1 : Bool),
  ({ keys := keys, levelParams := levelParams, proof := proof, priority := priority, post := post, perm := perm,
        origin := origin, rfl := rfl, backwardRfl := backwardRfl } =
      { keys := keys_1, levelParams := levelParams_1, proof := proof_1, priority := priority_1, post := post_1,
        perm := perm_1, origin := origin_1, rfl := rfl_1, backwardRfl := backwardRfl_1 }) =
    (keys = keys_1 ∧
      levelParams = levelParams_1 ∧
        proof = proof_1 ∧
          priority = priority_1 ∧
            post = post_1 ∧ perm = perm_1 ∧ origin = origin_1 ∧ rfl = rfl_1 ∧ backwardRfl = backwardRfl_1)
-- Mathlib.Data.Sym.Basic
/-- Inserts an element into the term of `Sym α n`, increasing the length by one.
 -/
Sym.«term_::ₛ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.max.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] (j j_1 : C),
  j = j_1 → ∀ (j' j'_1 : C), j' = j'_1 → CategoryTheory.IsFiltered.max j j' = CategoryTheory.IsFiltered.max j_1 j'_1
-- Init.Data.String.Defs
/-- A `Pos s` is a byte offset in `s` together with a proof that this position is at a UTF-8
character boundary.
 -/
String.Pos : String → Type
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.mapsTo_Iio : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  StrictAntiOn f (Set.Iic b) → Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_not_contains_map_fst_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getKeyD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        fallback
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.dontCare : Lean.Expr
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractLeftAux_apply_apply : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (d : Module.Dual R M) (a : M) (a_1 : CliffordAlgebra Q × CliffordAlgebra Q),
  ((CliffordAlgebra.contractLeftAux Q d) a) a_1 = d a • a_1.1 - (CliffordAlgebra.ι Q) a * a_1.2
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trCont.eq_5 : ∀ (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.trCont (Turing.ToPartrec.Cont.fix c k) =
    Turing.PartrecToTM2.Cont'.fix c (Turing.PartrecToTM2.trCont k)
-- Mathlib.CategoryTheory.Galois.Equivalence
CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToContAction F).EssSurj
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.one_apply : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (x : F), 1 x = x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
/-- Assuming we have a sequence of subsets `X n : Set (Cochain K L d)` for all `n : ℕ`,
a sequence of maps `φ n : X n → X (n + 1)` for `n : ℕ`, and an element `x₀ : X 0`,
and under the assumption that for any `x : X n` the cochain `φ n x` coincides
with `x` up to the degree `p₀ + n`, this is a cochain in `Cochain K L d` which
can be understood as the "limit" of the sequence of cochains obtained by
evaluating iterations of `φ` on `x₀`.  -/
CochainComplex.HomComplex.Cochain.InductionUp.limitSequence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {d : ℤ} →
          {X : ℕ → Set (CochainComplex.HomComplex.Cochain K L d)} →
            (φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))) →
              {p₀ : ℤ} →
                (∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)) →
                  ↑(X 0) → CochainComplex.HomComplex.Cochain K L d
-- Batteries.Data.AssocList
Batteries.AssocList.instEmptyCollection : {α : Type u_1} → {β : Type u_2} → EmptyCollection (Batteries.AssocList α β)
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_pred_left_eq_insert_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  b < a → ¬IsMin b → Set.Ioo (Order.pred b) a = insert b (Set.Ioo b a)
-- Mathlib.Algebra.Lie.Subalgebra
LieHom.coe_range : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂), ↑f.range = Set.range ⇑f
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.adjoin_of_forall_isAlgebraic : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [NoZeroDivisors S] {s t : Set S},
  (∀ x ∈ s \ t, IsAlgebraic (↥(Algebra.adjoin R t)) x) →
    ∀ {a : A}, IsAlgebraic (↥(Algebra.adjoin R s)) a → IsAlgebraic (↥(Algebra.adjoin R t)) a
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.tsupport_lineDerivOp_subset : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E] (m : E) (f : SchwartzMap E F), tsupport ⇑(LineDeriv.lineDerivOp m f) ⊆ tsupport ⇑f
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.comp_ker_subtype : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [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₂}
  (f : M →ₛₗ[τ₁₂] M₂), f ∘ₛₗ f.ker.subtype = 0
-- Lean.Parser.Command
Lean.Parser.Command.derivingClass.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Parser.Basic
Lean.Parser.mkIdResult : String.Pos.Raw → Option Lean.Parser.Token → Lean.Name → optParam Bool true → Lean.Parser.ParserFn
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- the underlying continuous map of underlying spaces from the source to an open subset of the
target.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y}
  [self : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)
-- Mathlib.Topology.Instances.Rat
Rat.instMetricSpace : MetricSpace ℚ
-- Mathlib.Topology.Algebra.MulAction
ContinuousWithinAt.smul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {b : Y} {s : Set Y},
  ContinuousWithinAt f s b → ContinuousWithinAt g s b → ContinuousWithinAt (f • g) s b
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.extractMonadInfo.mkUnknownMonadResult : Lean.Elab.TermElabM (Lean.Elab.Do.MonadInfo × Lean.Expr)
-- Mathlib.FieldTheory.Perfect
injective_frobenius : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [PerfectRing R p],
  Function.Injective ⇑(frobenius R p)
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isIso_iff_isHomeomorph : ∀ {X Y : TopCat} (f : X ⟶ Y), CategoryTheory.IsIso f ↔ IsHomeomorph ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sum_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [inst : Fintype ι],
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance Y (∑ i, X i) μ = ∑ i, ProbabilityTheory.covariance Y (X i) μ
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_iUnion_toPlots : ∀ {X : Type u_1} {ι : Type u_2} (D : ι → DiffeologicalSpace X),
  DiffeologicalSpace.generateFrom (⋃ i, (D i).toPlots) = ⨆ i, D i
-- Init.Data.Option.Lemmas
Option.get!_some : ∀ {α : Type u_1} [inst : Inhabited α] {a : α}, (some a).get! = a
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_StateT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε : Type u_1} {ρ α : Type u} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ sh)} [inst : Std.Do.WP m sh] [inst_1 : Monad m]
  [inst_2 : MonadExceptOf ε m],
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q = (Std.Do.wp (MonadLift.monadLift (MonadExceptOf.throw e))).apply Q
-- Mathlib.Algebra.Homology.Single
CochainComplex.fromSingle₀Equiv_apply_coe : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V)
  (φ : (CochainComplex.single₀ V).obj X ⟶ C), ↑((C.fromSingle₀Equiv X) φ) = φ.f 0
-- Mathlib.Data.Sum.Order
Sum.not_inl_le_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a : α} {b : β}, ¬Sum.inl b ≤ Sum.inr a
-- Init.Data.List.Find
List.head_filter : ∀ {α : Type u_1} {p : α → Bool} {l : List α} (h : List.filter p l ≠ []),
  (List.filter p l).head h = (List.find? p l).get ⋯
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.isPrimitive_iff : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Fintype n] [inst_3 : DecidableEq n]
  (A : Matrix n n R), A.IsPrimitive ↔ (∀ (i j : n), 0 ≤ A i j) ∧ ∃ k > 0, ∀ (i j : n), 0 < (A ^ k) i j
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- There exists an automorphism `f` of `A` that maps `b` to `a`.
`f` is obtained by considering `u` and `selfProdPermIncl h b`.
Both are inclusions of `A` into `selfProd F X` mapping `b` respectively `a` to the same element
in the fiber of `selfProd F X`. Applying `connected_component_unique` yields the result.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.subobj_selfProd_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A : C}
  {u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X} {a : (F.obj A).obj},
  (CategoryTheory.ConcreteCategory.hom (F.map u)) a = CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X →
    ∀ [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.Mono u] (b : (F.obj A).obj),
      ∃ f, (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) b = a
-- Mathlib.Data.Multiset.FinsetOps
/-- `ndinter s t` is the lift of the list `∩` operation. This operation
does not respect multiplicities, unlike `s ∩ t`, but it is suitable as
an intersection operation on `Finset`. (`s ∩ t` would also work as an intersection operation
on finset, but this is more efficient.)  -/
Multiset.ndinter : {α : Type u_1} → [DecidableEq α] → Multiset α → Multiset α → Multiset α
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotientInfEquivSupQuotient_apply_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M)
  (x : ↥p),
  have map := Submodule.inclusion ⋯;
  (LinearMap.quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk x) = Submodule.Quotient.mk (map x)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Auxiliary function to constructing a linear map `M ⊗ N → P` given a bilinear map `M → N → P`
with the property that its composition with the canonical bilinear map `M → N → M ⊗ N` is
the given bilinear map `M → N → P`.  -/
TensorProduct.liftAux : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {M : Type u_7} →
            {N : Type u_8} →
              {P₂ : Type u_17} →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid N] →
                    [inst_4 : AddCommMonoid P₂] →
                      [inst_5 : Module R M] →
                        [inst_6 : Module R N] →
                          [inst_7 : Module R₂ P₂] → (M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) → TensorProduct R M N →+ P₂
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.eq_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) {x : N} {y : M}, y = e.symm x ↔ e y = x
-- Init.Data.Array.Attach
Array.attachWith_reverse : ∀ {α : Type u_1} {P : α → Prop} {xs : Array α} {H : ∀ a ∈ xs.reverse, P a},
  xs.reverse.attachWith P H = (xs.attachWith P ⋯).reverse
-- Aesop.RulePattern.Cache
Aesop.instInhabitedRulePatternCache.default : Aesop.RulePatternCache
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The inclusion of `(G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃)` in
`mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j`
when `r (i₁, i₂, i₃) = j`.  -/
CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) →
                      (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) →
                                    (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                                      (X₂ : CategoryTheory.GradedObject I₂ C₂) →
                                        (X₃ : CategoryTheory.GradedObject I₃ C₃) →
                                          [inst_5 :
                                              (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj
                                                    X₂).HasMap
                                                ρ₁₂.p] →
                                            [inst_6 :
                                                (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
                                                          (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁
                                                            X₂)).obj
                                                      X₃).HasMap
                                                  ρ₁₂.q] →
                                              (i₁ : I₁) →
                                                (i₂ : I₂) →
                                                  (i₃ : I₃) →
                                                    (j : J) →
                                                      r (i₁, i₂, i₃) = j →
                                                        ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
                                                          CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
                                                            (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁
                                                              X₂)
                                                            X₃ j)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNonUnitalNonAssocSemiring : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [NonUnitalNonAssocSemiring R] → NonUnitalNonAssocSemiring (l.Germ R)
-- Mathlib.CategoryTheory.Limits.Final.Connected
CategoryTheory.instInitialDiscreteOfIsConnected : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : Type w} [Unique T]
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) [CategoryTheory.IsConnected C], F.Initial
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_subset_uIcc_iff_le' : ∀ {α : Type u_1} [inst : Lattice α] {a₁ a₂ b₁ b₂ : α},
  Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_unitOfList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  (Std.ExtDHashMap.Const.unitOfList l).size ≤ l.length
-- Mathlib.CategoryTheory.ObjectProperty.Retract
/-- A predicate `C → Prop` on the objects of a category is stable under retracts
if whenever `P Y`, then all the objects `X` that are retracts of `Y` also satisfy `P X`.  -/
CategoryTheory.ObjectProperty.IsStableUnderRetracts : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.restrict.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {K : CategoryTheory.Precoverage C} {ι : C → Type w} {X Y : C}
  {f : X ⟶ Y} {a : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y} {Y_1 : C} {f_1 : X ⟶ Y_1}
  {a_1 : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y_1},
  CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f a =
      CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f_1 a_1 →
    Y = Y_1 ∧ f ≍ f_1 ∧ a ≍ a_1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The function between the basic open set `D(f)` in `Proj` to the corresponding basic open set in
`Spec A⁰_f`. This is bundled into a continuous map in `TopComponent.forward`.
 -/
AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace →
                  ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                          (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.spanFinrank_maximalIdeal_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : IsLocalRing R],
  Submodule.spanFinrank (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R)) =
    Submodule.spanFinrank (IsLocalRing.maximalIdeal R)
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.iso_inv_naturality_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) [h : CategoryTheory.CatCommSq T L R B]
  {x y : C₁} (f : x ⟶ y) {Z : C₄} (h_1 : R.obj (T.obj y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (B.map (L.map f))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T L R B).inv.app y) h_1) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T L R B).inv.app x)
      (CategoryTheory.CategoryStruct.comp (R.map (T.map f)) h_1)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_fst_dvd_orderOf : ∀ {α : Type u_4} {β : Type u_5} [inst : Monoid α] [inst_1 : Monoid β] {x : α × β}, orderOf x.1 ∣ orderOf x
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  (AlgebraicGeometry.Scheme.Hom.appIso f U).hom =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The subgraph of `B` corresponding to a copy of `A` inside `B`.  -/
SimpleGraph.Copy.toSubgraph : {α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → A.Copy B → B.Subgraph
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.isChain_dartAdj_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), List.IsChain G.DartAdj p.darts
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.degreeOf_sub_lt : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] {x : σ} {f g : MvPolynomial σ R} {k : ℕ},
  0 < k →
    (∀ m ∈ f.support, k ≤ m x → MvPolynomial.coeff m f = MvPolynomial.coeff m g) →
      (∀ m ∈ g.support, k ≤ m x → MvPolynomial.coeff m f = MvPolynomial.coeff m g) → MvPolynomial.degreeOf x (f - g) < k
-- Init.Data.List.Nat.TakeDrop
List.findIdx_take : ∀ {α : Type u_1} {xs : List α} {i : ℕ} {p : α → Bool}, List.findIdx p (List.take i xs) = min i (List.findIdx p xs)