mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.CoverPreserving
CategoryTheory.CompatiblePreserving.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D},
  (∀ (ℱ : CategoryTheory.Sheaf K (Type w)) {Z : C} {T : CategoryTheory.Presieve Z}
      {x : CategoryTheory.Presieve.FamilyOfElements (G.op.comp ℱ.obj) T},
      x.Compatible →
        ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
          (hg₂ : T g₂),
          CategoryTheory.CategoryStruct.comp f₁ (G.map g₁) = CategoryTheory.CategoryStruct.comp f₂ (G.map g₂) →
            (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) =
              (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)) →
    CategoryTheory.CompatiblePreserving K G
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0),
  CochainComplex.HomComplex.Cocycle.toSingleMk (-f) h p' hp' ⋯ =
    -CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf
-- Init.Data.Nat.Coprime
Nat.Coprime.pow_left : ∀ {m k : ℕ} (n : ℕ), m.Coprime k → (m ^ n).Coprime k
-- Mathlib.Order.Interval.Set.Image
Set.preimage_subtype_val_Ico : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a b : { x // p x }), Subtype.val ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Given two morphisms of sheaves of `R`-modules `f : free ι ⟶ free σ` and `g : free σ ⟶ M`
satisfying `H : f ≫ g = 0` and `IsColimit (CokernelCofork.ofπ g H)`, we obtain
relations of `Presentation M`.  -/
SheafOfModules.relationsOfIsCokernelFree : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {ι σ : Type u} →
              {M : SheafOfModules R} →
                (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) →
                  (g : SheafOfModules.free σ ⟶ M) →
                    (H : CategoryTheory.CategoryStruct.comp f g = 0) →
                      (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) →
                        (CategoryTheory.Limits.kernel
                            (SheafOfModules.generatorsOfIsCokernelFree f g H H').π).GeneratingSections
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.Raw.iter.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β), m.iter = Std.Iter.flatMap (fun b => b.iter) m.buckets.iter
-- Mathlib.Logic.Equiv.Sum
Equiv.sumAssoc_apply_inl_inr : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β),
  (Equiv.sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.inv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {f : E → 𝕜},
  DiffContOnCl 𝕜 f s → (∀ x ∈ closure s, f x ≠ 0) → DiffContOnCl 𝕜 f⁻¹ s
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS : {α : Type u_1} → [Lean.Grind.Semiring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Expr → α
-- Mathlib.Algebra.GroupWithZero.ProdHom
/-- Given groups with zero `G₀`, `H₀`, the natural projection homomorphism from
`WithZero (G₀ˣ × H₀ˣ)` to `H₀`, which is the group with zero that can be identified
as their product.  -/
MonoidWithZeroHom.snd : (G₀ : Type u_1) →
  (H₀ : Type u_2) → [inst : GroupWithZero G₀] → [inst_1 : GroupWithZero H₀] → WithZero (G₀ˣ × H₀ˣ) →*₀ H₀
-- Mathlib.Algebra.Module.FinitePresentation
Module.finitePresentation_of_finite : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  [h : Module.Finite R M], Module.FinitePresentation R M
-- Mathlib.Algebra.CharZero.Defs
OfNat.ofNat_ne_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo], OfNat.ofNat n ≠ 0
-- Lean.Parser.Module
Lean.Parser.Module.updateTokens : Lean.Parser.TokenTable → Lean.Parser.TokenTable
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app : ∀ {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 : CategoryTheory.PreGaloisCategory.AutGalois F) (A : C) [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois A]
  (a : (F.obj A).obj),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F).symm { unop' := x }).hom.app A))
      a =
    (CategoryTheory.ConcreteCategory.hom
        (F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom))
      a
-- Mathlib.Algebra.Homology.Opposite
/-- Sends a complex `X` with objects in `Vᵒᵖ` to the corresponding complex with objects in `V`.  -/
HomologicalComplex.unop : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → HomologicalComplex Vᵒᵖ c → HomologicalComplex V c.symm
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
instContMDiffVectorBundleOfSomeENatTopOfLEInfty : ∀ {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] [inst_8 : NormedAddCommGroup F]
  [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  {a : WithTop ℕ∞} [ContMDiffVectorBundle (↑⊤) F E IB] [h : ENat.LEInfty a], ContMDiffVectorBundle a F E IB
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_f_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q n : ℕ)
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) ((AlgebraicTopology.DoldKan.P q).f n) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) (f.app (Opposite.op { len := n }))
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.inner_quotient_eq : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (x y : E ⧸ K),
  inner 𝕜 x y = inner 𝕜 (K.quotientEquivOrthogonal x) (K.quotientEquivOrthogonal y)
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.uliftFunctor_map : ∀ {x x_1 : GrpCat} (f : x ⟶ x_1),
  GrpCat.uliftFunctor.map f =
    GrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((GrpCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom))
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.op_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.op.inverse = e.inverse.op
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_nonneg_of_neg_one_lt : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, -1 < a → 0 ≤ ⌈a⌉
-- Batteries.Data.Fin.OfBits
/-- Construct an element of `Fin (2 ^ n)` from a sequence of bits (little endian).
 -/
Fin.ofBits : {n : ℕ} → (Fin n → Bool) → Fin (2 ^ n)
-- Mathlib.Algebra.Group.Prod
MulEquiv.coe_prodAssoc : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P],
  ⇑MulEquiv.prodAssoc = ⇑(Equiv.prodAssoc M N P)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_congr : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k k' : α}, (k == k') = true → m.getKey? k = m.getKey? k'
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_le_count_of_factors_le : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)]
  {a b p : Associates α}, b ≠ 0 → Irreducible p → a.factors ≤ b.factors → p.count a.factors ≤ p.count b.factors
-- Mathlib.Topology.Separation.Basic
/-- In an R₀ space, the `Specializes` relation is symmetric.  -/
R0Space.specializes_symm : ∀ {X : Type u} {inst : TopologicalSpace X} [self : R0Space X], Std.Symm Specializes
-- Mathlib.Order.Filter.Tendsto
/-- **Alias** of the forward direction of `Filter.tendsto_iff_comap`. -/
Filter.Tendsto.le_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
  Filter.Tendsto f l₁ l₂ → l₁ ≤ Filter.comap f l₂
-- Mathlib.Data.DFinsupp.Module
/-- Dependent functions with finite support inherit a `DistribMulAction` structure from such a
structure on each coordinate.  -/
DFinsupp.distribMulAction : {ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [inst : Monoid γ] →
        [inst_1 : (i : ι) → AddMonoid (β i)] →
          [(i : ι) → DistribMulAction γ (β i)] → DistribMulAction γ (Π₀ (i : ι), β i)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult.mk.injEq : ∀ (uvars : Array Lean.Elab.Term.Do.Var) (term : Lean.Syntax) (uvars_1 : Array Lean.Elab.Term.Do.Var)
  (term_1 : Lean.Syntax),
  ({ uvars := uvars, term := term } = { uvars := uvars_1, term := term_1 }) = (uvars = uvars_1 ∧ term = term_1)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M),
  f.ker = { toAddSubmonoid := AddMonoidHom.mker f, neg_mem' := ⋯ }
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of `Finset.apply_sup_eq_sup_comp_of_nonempty`. -/
Finset.comp_sup_eq_sup_comp_of_nonempty : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} {f : ι → α} [inst_1 : OrderBot α]
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] {g : α → β}, Monotone g → s.Nonempty → g (s.sup f) = s.sup (g ∘ f)
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.changed : Lean.MVarId → Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep)) → Aesop.NormSeqResult
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.image_uIcc : ∀ {k : Type u_10} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k] (f : k →ᵃ[k] k) (a b : k),
  ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.tendsto_iff_forall_eval_tendsto : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {l : Filter α} {f : α → WeakBilin B} {x : WeakBilin B},
  Function.Injective ⇑B →
    (Filter.Tendsto f l (nhds x) ↔ ∀ (y : F), Filter.Tendsto (fun i => (B (f i)) y) l (nhds ((B x) y)))
-- Mathlib.Topology.LocallyFinite
/-- Let `f : ℕ → α → β` be a sequence of functions on a topological space. Suppose
that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
function `F :  α → β` such that for any `x`, for sufficiently large values of `n`, we have
`f n =ᶠ[𝓝 x] F`.  -/
LocallyFinite.exists_forall_eventually_atTop_eventuallyEq : ∀ {α : Type u_3} {X : Type u_4} [inst : TopologicalSpace X] {f : ℕ → X → α},
  (LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) → ∃ F, ∀ (x : X), ∀ᶠ (n : ℕ) in Filter.atTop, f n =ᶠ[nhds x] F
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.coe_toSubsemigroup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), ↑s.toSubsemigroup = ↑s
-- Mathlib.Order.Category.BddOrd
BddOrd.ofHom_id : ∀ {X : Type u} [inst : PartialOrder X] [inst_1 : BoundedOrder X],
  BddOrd.ofHom (BoundedOrderHom.id X) = CategoryTheory.CategoryStruct.id (BddOrd.of X)
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- An equivalence of domains induces a linear equivalence of finitely supported functions.

This is `domCongr` as a `LinearEquiv`.  -/
SkewMonoidAlgebra.domLCongr : {k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      {A : Type u_4} →
        [inst : Semiring k] →
          [inst_1 : AddCommMonoid A] → [inst_2 : Module k A] → G ≃ H → SkewMonoidAlgebra A G ≃ₗ[k] SkewMonoidAlgebra A H
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.node.injEq : ∀ {α : Type u} (a : α) (child sibling : Batteries.BinomialHeap.Imp.HeapNode α) (a_1 : α)
  (child_1 sibling_1 : Batteries.BinomialHeap.Imp.HeapNode α),
  (Batteries.BinomialHeap.Imp.HeapNode.node a child sibling =
      Batteries.BinomialHeap.Imp.HeapNode.node a_1 child_1 sibling_1) =
    (a = a_1 ∧ child = child_1 ∧ sibling = sibling_1)
-- Init.Data.Array.Lemmas
Array.toList_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Option α → Option β → γ} {xs : Array α} {ys : Array β},
  (Array.zipWithAll f xs ys).toList = List.zipWithAll f xs.toList ys.toList
-- Mathlib.Order.Hom.CompleteLattice
instCoeTCSInfHomOfSInfHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : InfSet α] [inst_2 : InfSet β]
  [inst_3 : sInfHomClass F α β], instCoeTCSInfHomOfSInfHomClass = { coe := fun f => { toFun := ⇑f, map_sInf' := ⋯ } }
-- Batteries.Recycling.RBTree.Basic
/-- True if the specified `cut` matches at least one element of of `t`.  -/
RBTree.RBNode.MemP : {α : Type u_1} → (α → Ordering) → RBTree.RBNode α → Prop
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instDivCoeOfSubgroupClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → DivInvMonoid (R i)] [inst_2 : ∀ (i : ι), SubgroupClass (S i) (R i)],
  RestrictedProduct.instDivCoeOfSubgroupClass R = { div := fun x y => ⟨fun i => x i / y i, ⋯⟩ }
-- Init.Data.String.Lemmas.Splits
String.copy_slice_eq_append_of_lt : ∀ {s : String} {p q : s.Pos} (h : p < q),
  (s.slice p q ⋯).copy = String.singleton (p.get ⋯) ++ (s.slice (p.next ⋯) q ⋯).copy
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The assignment of each relation to a polynomial in the generators.  -/
Algebra.Presentation.relation : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (self : Algebra.Presentation R S ι σ) → σ → self.Ring
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.models_sentence_of_mem : ∀ {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence}, φ ∈ T → T ⊨ᵇ φ
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- The range of a strongly measurable function is separable.  -/
MeasureTheory.StronglyMeasurable.isSeparable_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [inst : TopologicalSpace β],
  MeasureTheory.StronglyMeasurable f → TopologicalSpace.IsSeparable (Set.range f)
-- Mathlib.Order.Bounds.Basic
upperBounds_Iio : ∀ {γ : Type u_3} [inst : LinearOrder γ] [DenselyOrdered γ] {a : γ}, upperBounds (Set.Iio a) = Set.Ici a
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂Obj_obj_map : ∀ {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₄)) (X₁ : C₁) (X₂ : C₂) {x x_1 : C₃} (φ : x ⟶ x_1),
  ((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).map φ = (G.obj ((F₁₂.obj X₁).obj X₂)).map φ
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_div_dvd : ∀ {K : Type u} [inst : Field K] (p : Polynomial K) {q : Polynomial K},
  q ≠ 0 → ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).num ∣ p
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The second part of the third cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_σ_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 1)},
  CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.σ i) = CategoryTheory.CategoryStruct.id (X.obj { len := n })
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.exactFunctor_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.exactFunctor C D F ↔
    CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
/-- The connecting homomorphism `Q.obj (S.X₃) ⟶ (Q.obj S.X₁)⟦(1 : ℤ)⟧`
in the derived category when `S` is a short exact short complex of
cochain complexes in an abelian category.  -/
DerivedCategory.triangleOfSESδ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} →
          S.ShortExact →
            (DerivedCategory.Q.obj S.X₃ ⟶
              (CategoryTheory.shiftFunctor (DerivedCategory C) 1).obj (DerivedCategory.Q.obj S.X₁))
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isSuccLimit_of_isPrincipal_mul : ∀ {o : Ordinal.{u}}, 2 < o → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o → Order.IsSuccLimit o
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.compl_top : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι], ⊤.compl = ⊥
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.runInBase : Lean.Elab.Do.ControlStack → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getCommRingInst? : Option ℕ → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.IterM.step_take.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Init.Data.List.Lex
List.le_iff_lt_or_eq : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  [Std.Asymm fun x1 x2 => x1 < x2] {l₁ l₂ : List α}, l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassDistinguished_smul : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {a : A} {g : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) (a • g) ≠ 0),
  (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.tensorTensorTensorComm_symm : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P],
  (TensorProduct.tensorTensorTensorComm R M N P Q).symm = TensorProduct.tensorTensorTensorComm R M P N Q
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.Blunt.anti : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C₁ C₂ : ConvexCone R M}, C₂ ≤ C₁ → C₁.Blunt → C₂.Blunt
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.instNontrivialOfNonempty : ∀ {V : Type u_2} [Nonempty V], Nontrivial (Digraph V)
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.GoTo.noConfusionType : Sort v✝ → ExistsAndEq.GoTo → ExistsAndEq.GoTo → Sort v✝
-- Mathlib.LinearAlgebra.Matrix.WithConv
instOneWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [One α] → One (WithConv (Matrix m n α))
-- Mathlib.Topology.Bornology.BoundedOperation
/-- A typeclass saying that `(p : R × R) ↦ p.1 + p.2` maps any product of bounded sets to a bounded
set. This property follows from `LipschitzAdd`, and thus automatically holds, e.g., for seminormed
additive groups.  -/
BoundedAdd : (R : Type u_1) → [Bornology R] → [Add R] → Prop
-- Mathlib.Algebra.Order.Monoid.WithTop
WithBot.isOrderedAddMonoid : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α], IsOrderedAddMonoid (WithBot α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.data? : Lean.Lsp.InlayHint → Option Lean.Json
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.top_closure_add_self_subset : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [SeparatelyContinuousAdd M] (s : AddSubmonoid M),
  closure ↑s + closure ↑s ⊆ closure ↑s
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.add_comm : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddCommMonoid X] [inst_3 : DistribMulAction R X] (x y : OreLocalization S X), x + y = y + x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- `rpowIntegrand₀₁ p t` is operator monotone for all `p ∈ Ioo 0 1` and all `t ∈ Ioi 0`.  -/
CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁ : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p t : ℝ},
  p ∈ Set.Ioo 0 1 → 0 < t → MonotoneOn (cfcₙ (p.rpowIntegrand₀₁ t)) (Set.Ici 0)
-- Mathlib.CategoryTheory.ComposableArrows.Two
CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg),
  (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h).app 1 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₁ fg).obj 1)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_add : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι), ∀ U ∈ p.basisSets, ∃ V ∈ p.basisSets, V + V ⊆ U
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul`.  -/
Right.one_lt_mul : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightStrictMono α] {a b : α},
  1 < a → 1 < b → 1 < a * b
-- Mathlib.Order.Disjointed
biUnion_range_succ_disjointed : ∀ {α : Type u_3} (f : ℕ → Set α) (n : ℕ), ⋃ i ∈ Finset.range (n + 1), disjointed f i = (partialSups f) n
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, ContinuousWithinAt f t x → s ⊆ t → ContinuousWithinAt f s x
-- Mathlib.Tactic.NormNum.BigOperators
/-- `n` unifies with `0`  -/
Mathlib.Meta.Nat.UnifyZeroOrSuccResult.zero : {n : Q(ℕ)} → «$n» =Q 0 → Mathlib.Meta.Nat.UnifyZeroOrSuccResult n