mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.homCongr_symm_apply : ∀ (k : Type u_1) {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] [inst_1 : Semiring k]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z)
  (f : Y ⟶ Z),
  (CategoryTheory.Linear.homCongr k f₁ f₂).symm f =
    CategoryTheory.CategoryStruct.comp f₁.hom (CategoryTheory.CategoryStruct.comp f f₂.inv)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_maxKey?_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {km kmm : α} (hkm : t.maxKey? = some km), (t.modify k f).maxKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.mk : ∀ {o : ONote}, Exists o.NFBelow → o.NF
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
MultilinearMap.domCoprod_apply : ∀ {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [inst : CommSemiring R] {N₁ : Type u_6} [inst_1 : AddCommMonoid N₁]
  [inst_2 : Module R N₁] {N₂ : Type u_7} [inst_3 : AddCommMonoid N₂] [inst_4 : Module R N₂] {N : Type u_8}
  [inst_5 : AddCommMonoid N] [inst_6 : Module R N] (a : MultilinearMap R (fun x => N) N₁)
  (b : MultilinearMap R (fun x => N) N₂) (v : (i : ι₁ ⊕ ι₂) → (fun x => N) i),
  (a.domCoprod b) v = (a fun i₁ => v (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ => v (Sum.inr i₂)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X))
      (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) ((t.truncLTι b).app ((t.truncGE a).obj X))) =
    CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X)
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_of_two_le_of_pos : ∀ {n b : ℕ}, 2 ≤ b → 0 < n → b.digits n = n % b :: b.digits (n / b)
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.isLE_Q_obj_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ), (DerivedCategory.Q.obj K).IsLE n ↔ K.IsLE n
-- Lean.ExtraModUses
Lean.instBEqExtraModUse.beq : Lean.ExtraModUse → Lean.ExtraModUse → Bool
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.inr_apply : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B] (x : B),
  (NonUnitalAlgHom.inr R A B) x = (0, x)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_le_comap_iff_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S], Function.Surjective ⇑f → ∀ (I J : Ideal S), Ideal.comap f I ≤ Ideal.comap f J ↔ I ≤ J
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
deriv_riemannZeta_eq_neg_inv_sub_sq_add : ∀ {s : ℂ}, s ≠ 1 → deriv riemannZeta s = -(s - 1)⁻¹ ^ 2 + deriv riemannZeta₀ s
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_symm : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f), ↑(e.lift_openEmbedding hf).symm = f ∘ ↑e.symm
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_roo : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_roo._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
    List.filter (fun e => decide ((cmp e lowerBound).isGT = true ∧ (cmp e upperBound).isLT = true)) t.toList
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
AEMeasurable.iInf : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Sort u_5} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α},
  (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (fun b => ⨅ i, f i b) μ
-- Mathlib.Probability.Moments.Variance
/-- The `ℝ≥0∞`-valued variance of the real-valued random variable `X` according to the volume
measure.

This is defined as the Lebesgue integral of `(X - 𝔼[X])^2`.  -/
ProbabilityTheory.«termEVar[_]» : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.all_filterMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} {p : β → Bool},
  (Array.filterMap f xs).all p =
    xs.all fun a =>
      match f a with
      | some b => p b
      | none => true
-- Batteries.Data.List.Lemmas
List.findIdx_add_mem_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} (s : ℕ),
  List.findIdx p xs < xs.length → List.findIdx p xs + s ∈ List.findIdxs p xs s
-- Init.Data.String.PosRaw
/-- Accesses the indicated byte in the UTF-8 encoding of a string.

At runtime, this function is implemented by efficient, constant-time code.
 -/
String.getUTF8Byte : (s : String) → (p : String.Pos.Raw) → p < s.rawEndPos → UInt8
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- A facet of a simplicial complex is a maximal face.  -/
Geometry.SimplicialComplex.facets : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] → [inst_3 : Module 𝕜 E] → Geometry.SimplicialComplex 𝕜 E → Set (Finset E)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_comp_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W h) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac._auto_1)
  [h₁ : (hS.sc k ⋯).HasRightHomology] [h₂ : (hS.sc (k + 1) ⋯).HasLeftHomology] {Z : C} (h : S.obj ⟨k + 1 + 1, ⋯⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hS.sc k ⋯).pOpcycles
      (CategoryTheory.CategoryStruct.comp (hS.opcyclesIsoCycles k ⋯).hom
        (CategoryTheory.CategoryStruct.comp (hS.sc (k + 1) ⋯).iCycles h)) =
    CategoryTheory.CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.singleton_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {e : α}, e ∈ M.E → {e} ⊆ M.E
-- Mathlib.CategoryTheory.Sites.Coverage
/-- A presheaf is a sheaf for the Grothendieck topology generated by a union of coverages iff it is a
sheaf for the Grothendieck topology generated by each coverage separately.
 -/
CategoryTheory.Presieve.isSheaf_sup : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] (K L : CategoryTheory.Coverage C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
  CategoryTheory.Presieve.IsSheaf (K ⊔ L).toGrothendieck P ↔
    CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ∧ CategoryTheory.Presieve.IsSheaf L.toGrothendieck P
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.Label.ofNat_ctorIdx : ∀ (x : Lean.Meta.NormCast.Label), Lean.Meta.NormCast.Label.ofNat x.ctorIdx = x
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- If `f` is a continuous multilinear map, then `f.toContinuousLinearMap m i` is the continuous
linear map obtained by fixing all coordinates but `i` equal to those of `m`, and varying the
`i`-th coordinate.  -/
ContinuousMultilinearMap.toContinuousLinearMap : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] →
                      ContinuousMultilinearMap R M₁ M₂ → [DecidableEq ι] → ((i : ι) → M₁ i) → (i : ι) → M₁ i →L[R] M₂
-- Init.Data.Array.Basic
Array.uget.eq_1 : ∀ {α : Type u} (xs : Array α) (i : USize) (h : i.toNat < xs.size), xs.uget i h = xs[i.toNat]
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₂.π c₁ c (i₂, i₁) = j) {Z : C} (h_1 : (K.total c).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.flip.ιTotal c i₂ i₁ j h)
      (CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) h_1) =
    CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) h_1
-- Init.Data.List.Erase
List.eraseP_subset : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.eraseP p l ⊆ l
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
/-- We say `f` HasGaussNorm if the values `v (coeff t f) * ∏ i : t.support, c i` is bounded above,
that is `gaussNorm f` is finite.  -/
MvPowerSeries.HasGaussNorm : {R : Type u_1} → {σ : Type u_2} → (R → ℝ) → (σ → ℝ) → MvPowerSeries σ R → [Semiring R] → Prop
-- Plausible.Shrinkable
Plausible.Nat.shrinkable : Plausible.Shrinkable ℕ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ Std.ExtHashMap.filter f m},
  (Std.ExtHashMap.filter f m)[k] = m[k]
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.StepResult.mk.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {events : Array (Std.Http.Protocol.H1.Event dir)}
  {output : Std.Http.Internal.ChunkedBuffer} {events_1 : Array (Std.Http.Protocol.H1.Event dir)}
  {output_1 : Std.Http.Internal.ChunkedBuffer},
  { events := events, output := output } = { events := events_1, output := output_1 } →
    events = events_1 ∧ output = output_1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.IsFinitePresentation.isFinite_presentation : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R}
  {q : M.QuasicoherentData} [self : q.IsFinitePresentation] (i : q.I), (q.presentation i).IsFinite
-- Mathlib.RingTheory.ClassGroup.Basic
FractionalIdeal.mk0.congr_simp : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] [inst_5 : IsDedekindDomain R],
  FractionalIdeal.mk0 K = FractionalIdeal.mk0 K
-- Init.Data.Int.Cooper
_private.Init.Data.Int.Cooper.0.Int.Cooper.resolve_left_inv.eq_1 : ∀ (a p k : ℤ), Int.Cooper.resolve_left_inv a p k = (k + p) / a
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- The Cartesian product of two continuous alternating maps, as a continuous alternating map.  -/
ContinuousAlternatingMap.prod : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {N' : Type u_5} →
        {ι : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R N] →
                      [inst_6 : TopologicalSpace N] →
                        [inst_7 : AddCommMonoid N'] →
                          [inst_8 : Module R N'] →
                            [inst_9 : TopologicalSpace N'] → M [⋀^ι]→L[R] N → M [⋀^ι]→L[R] N' → M [⋀^ι]→L[R] (N × N')
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodProdProdComm_toAddEquiv : ∀ (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄],
  ↑(LinearEquiv.prodProdProdComm R M M₂ M₃ M₄) = AddEquiv.prodProdProdComm M M₂ M₃ M₄
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The maximal atlas of `M` for the `C^n` manifold with corners structure corresponding to the
model with corners `I`.  -/
IsManifold.maximalAtlas : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ →
                  (M : Type u_4) → [inst : TopologicalSpace M] → [ChartedSpace H M] → Set (OpenPartialHomeomorph M H)
-- Mathlib.Analysis.Fourier.AddCircle
/-- Express Fourier coefficients of `f` on an interval in terms of those of its derivative.  -/
fourierCoeffOn_of_hasDeriv_right : ∀ {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ},
  n ≠ 0 →
    ContinuousOn f (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
        IntervalIntegrable f' MeasureTheory.volume a b →
          fourierCoeffOn hab f n =
            1 / (-2 * ↑Real.pi * Complex.I * ↑n) *
              ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
-- Mathlib.Order.Bounds.Image
mem_lowerBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → a ∈ lowerBounds s → b ∈ lowerBounds t → f a b ∈ lowerBounds (Set.image2 f s t)
-- Mathlib.Analysis.Convex.Gauge
gauge_neg_set_neg : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} (x : E), gauge (-s) (-x) = gauge s x
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_zero_eq_constantCoeff_apply : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R),
  (MvPowerSeries.coeff 0) φ = MvPowerSeries.constantCoeff φ
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- We say that a set `H : Set (X → α)` of functions is equicontinuous at a point within a subset
if the family `(↑) : ↥H → (X → α)` is equicontinuous at that point within that same subset.  -/
Set.EquicontinuousWithinAt : {X : Type u_3} → {α : Type u_6} → [tX : TopologicalSpace X] → [uα : UniformSpace α] → Set (X → α) → Set X → X → Prop
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  {f : β → C} [inst_2 : CategoryTheory.Limits.HasCoproduct f],
  (CategoryTheory.ObjectProperty.ofObj f).IsSeparating → CategoryTheory.IsSeparator (∐ f)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.coeff_divByMonic_X_sub_C : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (a : R) (n : ℕ),
  (p /ₘ (Polynomial.X - Polynomial.C a)).coeff n = ∑ i ∈ Finset.Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
-- Aesop.Util.Basic
Aesop.instMonadParentDeclStateRefT'_aesop : {m : Type → Type} → {ω σ : Type} → [Lean.Elab.MonadParentDecl m] → Lean.Elab.MonadParentDecl (StateRefT' ω σ m)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε], MeasureTheory.MemLp 0 p μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC_nc.go : ℤ → Lean.Grind.CommRing.Mon → ℕ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Combinatorics.HalesJewett
/-- Change the index types of a subspace.  -/
Combinatorics.Subspace.reindex : {η : Type u_5} →
  {α : Type u_6} →
    {ι : Type u_7} →
      {η' : Type u_9} →
        {α' : Type u_10} →
          {ι' : Type u_11} → Combinatorics.Subspace η α ι → η ≃ η' → α ≃ α' → ι ≃ ι' → Combinatorics.Subspace η' α' ι'
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- Every normal epimorphism is a regular epimorphism.  -/
CategoryTheory.NormalEpi.regularEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : X ⟶ Y) → [I : CategoryTheory.NormalEpi f] → CategoryTheory.RegularEpi f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.GradedAlgebra.ι_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  (CliffordAlgebra.GradedAlgebra.ι Q) m =
    (DirectSum.of (fun i => ↥(CliffordAlgebra.evenOdd Q i)) 1) ⟨(CliffordAlgebra.ι Q) m, ⋯⟩
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that `|v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁)`.  -/
GenContFract.abs_sub_convs_le : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K],
  ¬(GenContFract.of v).TerminatedAt n →
    |v - (GenContFract.of v).convs n| ≤ 1 / ((GenContFract.of v).dens n * (GenContFract.of v).dens (n + 1))
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.one_le_div : ∀ {α : Type u_2} [inst : Group α] {f : Filter α}, f.NeBot → 1 ≤ f / f
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.isHamiltonian_iff_support_get_bijective : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b},
  p.IsHamiltonian ↔ Function.Bijective p.support.get
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yn a1 (n + 1) = Pell.xn a1 n + Pell.yn a1 n * a
-- Aesop.EMap
/-- An index for `rep`. For each expression `e` at index `i` in `rep`,
`idx.getMatch` returns a list of indexes containing `i`. This is used as a
pre-filter during lookups/insertions/modifications to reduce the number of
defeq comparisons.  -/
Aesop.EMap.idx : {α : Type u_1} → Aesop.EMap α → Lean.Meta.DiscrTree ℕ
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.epsilon_zero_eq_nfp`. -/
Ordinal.epsilon0_eq_nfp : Ordinal.epsilon 0 = Ordinal.nfp (fun a => Ordinal.omega0 ^ a) 0
-- Std.Data.HashMap.Raw
/-- Removes the mapping for the given key if it exists.  -/
Std.HashMap.Raw.erase : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → Std.HashMap.Raw α β
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n m : ℕ}
  (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (F : CategoryTheory.ComposableArrows C m) (X : Fin (n + 1)),
  ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).obj F).obj X = F.obj (Φ.obj X)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instMin.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β],
  InfTopHom.instMin =
    {
      min := fun f g =>
        have __src := f.toTopHom ⊓ g.toTopHom;
        let __SupHom := f.toInfHom ⊓ g.toInfHom;
        { toInfHom := __SupHom, map_top' := ⋯ } }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.Equiv.beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : BEq β]
  [EquivBEq α] [LawfulHashable α] [ReflBEq β], m₁.Equiv m₂ → Std.DHashMap.Const.beq m₁ m₂ = true
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.singleton : {ι : Type u_1} →
  {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i : ι} → (x : M i) → x ≠ 1 → Monoid.CoprodI.NeWord M i i
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
/-- **Alias** of `MvPowerSeries.le_lexOrder_mul`. -/
MvPowerSeries.lexOrder_mul_ge : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  (φ ψ : MvPowerSeries σ R), φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- A line through a point on a sphere is tangent if and only if the squared distance
from the external point to the tangent point equals the power of the point.  -/
EuclideanGeometry.Sphere.isTangentAt_iff_dist_sq_eq_power : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t p : P} {s : EuclideanGeometry.Sphere P},
  t ∈ s → (s.IsTangentAt t line[ℝ, p, t] ↔ dist p t ^ 2 = s.power p)
-- Mathlib.Analysis.Calculus.Gradient.Basic
Filter.EventuallyEq.gradient : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {f₁ : F → 𝕜}, f₁ =ᶠ[nhds x] f → gradient f₁ =ᶠ[nhds x] gradient f
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.rotate'.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (x : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (l : List α) → motive l 0) (h_3 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n.succ),
  (match [], x with
    | [], x => h_1 x
    | l, 0 => h_2 l
    | a :: l, n.succ => h_3 a l n) =
    h_1 x
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.essImage_ιHeart : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (H : Type u') [inst_6 : CategoryTheory.Category.{v', u'} H]
  [inst_7 : CategoryTheory.Preadditive H] [inst_8 : t.Heart H], t.ιHeart.essImage = t.heart
-- Init.Data.Format.Syntax
/-- Pretty print the given syntax `stx` as a `Format`.
Nodes deeper than `maxDepth` are omitted.
Setting the `showInfo` flag will also print the `SourceInfo` for each node.  -/
Lean.Syntax.formatStx : Lean.Syntax → optParam (Option ℕ) none → optParam Bool false → Std.Format
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.of_subsingleton : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Subsingleton A] (a : A),
  spectrum R a = ∅