mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.forIn'_eq_foldlM.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.yield b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_1 b
-- Mathlib.SetTheory.Cardinal.ToNat
/-- This function sends finite cardinals to the corresponding natural, and infinite cardinals
to 0.  -/
Cardinal.toNat : Cardinal.{u_1} →*₀ ℕ
-- Mathlib.Order.Interval.Multiset
Multiset.nodup_Ico : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, (Multiset.Ico a b).Nodup
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.adj_unit : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  ContinuousGeneratedByCat.adj.unit = ContinuousGeneratedByCat.adjUnitIso.hom
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the counit of an adjunction is an isomorphism, then one has an isomorphism
`(R ⋙ L ⋙ R) ≅ R`.  -/
CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (h : L ⊣ R) → [CategoryTheory.IsIso h.counit] → R.comp (L.comp R) ≅ R
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.cbmApplyMeasure_apply : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (s : Set X) (x : E),
  (MeasureTheory.cbmApplyMeasure μ B s) x = (B x) (μ s)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_comap : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s : Subring S) (f : R →+* S),
  ↑(Subring.comap f s) = ⇑f ⁻¹' ↑s
-- Mathlib.Logic.Equiv.List
Encodable.encode_list_nil : ∀ {α : Type u_1} [inst : Encodable α], Encodable.encode [] = 0
-- Mathlib.Algebra.CharP.Defs
ExpChar.prime : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] {q : ℕ}, Nat.Prime q → ∀ [hchar : CharP R q], ExpChar R q
-- Aesop.Forward.PremiseIndex
Aesop.PremiseIndex : Type
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.ofDescentData_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData f)
  (i : ι), (CategoryTheory.Pseudofunctor.DescentData'.ofDescentData sq sq₃ D).obj i = D.obj i
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.mem_overGrothendieckTopology : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [P.IsMultiplicative] [P.RespectsIso] (X : CategoryTheory.Over S)
  (R : CategoryTheory.Sieve X),
  R ∈ (AlgebraicGeometry.Scheme.overGrothendieckTopology P S) X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- Let `F` be a functor from the category of sheaves of `R`-modules to sheaves of `S`-modules.
Then a morphism `η : unit S ⟶ F.obj (unit R)` induces a morphism from `free (R := S) I` to
`F.obj (free I)`. See also `mapFreeIso` for the iso version.  -/
SheafOfModules.mapFree : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {C' : Type u₂} →
              [inst_3 : CategoryTheory.Category.{v₂, u₂} C'] →
                {J' : CategoryTheory.GrothendieckTopology C'} →
                  {S : CategoryTheory.Sheaf J' RingCat} →
                    [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] →
                      [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat] →
                        (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) →
                          (I : Type u) →
                            (SheafOfModules.unit S ⟶ F.obj (SheafOfModules.unit R)) →
                              (SheafOfModules.free I ⟶ F.obj (SheafOfModules.free I))
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.seq.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] {g g_1 : PowerSeries A} (e_g : g = g_1) {I I_1 : Ideal A} (e_I : I = I_1)
  (H : g.IsWeierstrassDivisorAt I) (f f_1 : PowerSeries A),
  f = f_1 → ∀ (a a_1 : ℕ), a = a_1 → ∀ (a_2 a_3 : Unit →₀ ℕ), a_2 = a_3 → H.seq f a a_2 = ⋯.seq f_1 a_1 a_3
-- Batteries.Data.Array.Match
Array.Matcher.instIteratorIteratorOfMonad : {n : Type u_1 → Type u_2} →
  {α σ : Type u_1} →
    [Monad n] →
      [inst : BEq α] →
        (m : Array.Matcher α) → [inst_1 : Std.Iterator σ n α] → Std.Iterator (Array.Matcher.Iterator σ n α m) n σ
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Pythagorean theorem, vector inner product form.  -/
norm_add_sq_eq_norm_sq_add_norm_sq_real : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  inner ℝ x y = 0 → ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] [inst_1 : AlgebraicGeometry.IsAffine Y]
  (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (Y.presheaf.obj (Opposite.op ⊤)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.isoSpec.hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Y.isoSpec.hom h)
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.assoc_symm_tmul : ∀ {R : Type u_9} {S : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {M₁₂ : Type u_14} {M₂₃ : Type u_15} [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid M₁₂] [inst_7 : AddCommMonoid M₂₃]
  [inst_8 : Module R M₁] [inst_9 : Module R M₂] [inst_10 : Module S M₂] [inst_11 : IsScalarTower R S M₂]
  [inst_12 : Module R M₃] [inst_13 : Module S M₃] [inst_14 : IsScalarTower R S M₃] [inst_15 : Module R M₁₂]
  [inst_16 : Module S M₁₂] [inst_17 : IsScalarTower R S M₁₂] [inst_18 : Module R M₂₃] [inst_19 : Module S M₂₃]
  [inst_20 : IsScalarTower R S M₂₃] {T : Type u_16} [inst_21 : CommSemiring T] [inst_22 : Algebra R T]
  [inst_23 : Module T M₁] [inst_24 : IsScalarTower R T M₁] [inst_25 : Module T M₁₂] [inst_26 : SMulCommClass S T M₁₂]
  [inst_27 : IsScalarTower R T M₁₂] (f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂)
  (hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)) (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) (hg : IsTensorProduct g)
  (x₁ : M₁) (x₂ : M₂) (x₃ : M₃), (IsTensorProduct.assoc f hf g hg).symm (x₁ ⊗ₜ[R] (g x₂) x₃) = (f x₁) x₂ ⊗ₜ[S] x₃
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- The homotopy equivalence from `X.chainComplex R` to `X.normalizedChainComplex R`.  -/
SSet.homotopyEquivNormalizedChainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) → (R : C) → HomotopyEquiv (X.chainComplex R) (X.normalizedChainComplex R)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_length : ∀ {α : Type u} {L₁ : List (α × Bool)}, (FreeAddGroup.negRev L₁).length = L₁.length
-- Mathlib.Analysis.Normed.Operator.Basic
Submodule.norm_subtypeL_le : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (K : Submodule 𝕜 E), ‖K.subtypeL‖ ≤ 1
-- Init.Data.List.Lemmas
List.foldr_add_const : ∀ {α : Type u_1} {l : List α} {a b : ℕ}, List.foldr (fun x x_1 => x_1 + a) b l = b + a * l.length
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.coeff_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (f : MvPowerSeries σ R) (e : τ →₀ ℕ),
      (MvPowerSeries.coeff e) (MvPowerSeries.subst a f) =
        ∑ᶠ (d : σ →₀ ℕ), (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (d.prod fun s e => a s ^ e)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β} {h₁ : a ∈ t.insertIfNew k v}, (t.insertIfNew k v)[a] = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then v else t[a]
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
CategoryTheory.Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf : ∀ {C : Type u} {A : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Category.{v₁, u₁} A] [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (J : CategoryTheory.GrothendieckTopology C) [inst_3 : CategoryTheory.HasWeakSheafify J A]
  [CategoryTheory.Limits.HasFiniteLimits A] [inst_5 : CategoryTheory.Limits.HasColimitsOfShape K A]
  [CategoryTheory.HasExactColimitsOfShape K A]
  [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.sheafToPresheaf J A)],
  CategoryTheory.HasExactColimitsOfShape K (CategoryTheory.Sheaf J A)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_null_of_ne_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  n ≠ 0 → DividedPowerAlgebra.dp R n 0 = 0
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instMonad.eq_1 : FreeAddGroup.instMonad =
  { map := fun {_α _β} {f} => ⇑(FreeAddGroup.map f), pure := fun {_α} => FreeAddGroup.of,
    seq := fun {α β} f x {_α _β} {x} {f} => (FreeAddGroup.lift f) x,
    seqLeft := fun {α β} x y {_α _β} {x} {f} => (FreeAddGroup.lift f) x,
    seqRight := fun {α β} x y {_α _β} {x} {f} => (FreeAddGroup.lift f) x,
    bind := fun {_α _β} {x} {f} => (FreeAddGroup.lift f) x }
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.cauchy₃ : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α},
  0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑f j) < ε
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.distribMulAction : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (P : Submodule R M) → DistribMulAction R (M ⧸ P)
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.instQuiver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → {f : X ⟶ Y} → Quiver (CategoryTheory.Factorisation f)
-- Batteries.Data.List.Basic
List.takeD_eq_takeDTR : @List.takeD = @List.takeDTR
-- Mathlib.Algebra.DirectSum.Module
DirectSum.instIsCentralScalar : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : (i : ι) → Module Rᵐᵒᵖ (M i)] [∀ (i : ι), IsCentralScalar R (M i)],
  IsCentralScalar R (DirectSum ι fun i => M i)
-- Lean.Util.Trace
_private.Lean.Util.Trace.0.Lean.isTracingEnabledForExport : Lean.Options → Lean.Name → BaseIO Bool
-- Mathlib.Data.Set.Sigma
Set.univ_sigma_preimage_mk : ∀ {ι : Type u_1} {α : ι → Type u_3} (s : Set ((i : ι) × α i)), (Set.univ.sigma fun i => Sigma.mk i ⁻¹' s) = s
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.lintegral_preCDF_fst : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) [MeasureTheory.IsFiniteMeasure ρ],
  ∫⁻ (x : α), ProbabilityTheory.preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) Set.univ
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
/-- This is Lemma 2.5 (a) from [Geck](Geck2017).  -/
RootPairing.Base.root_sub_root_mem_of_mem_of_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [CharZero R] [IsDomain R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [Finite ι] [P.IsCrystallographic] {b : P.Base} (i j k : ι),
  i ≠ j →
    i ∈ b.support →
      j ∈ b.support →
        P.root k + P.root i - P.root j ∈ Set.range ⇑P.root →
          k ≠ j → P.root k + P.root i ∈ Set.range ⇑P.root → P.root k - P.root j ∈ Set.range ⇑P.root
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedENodeMap : Inhabited Lean.Meta.Grind.ENodeMap
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.HasCoequalizerOfIsSplitPair.out : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  (G : CategoryTheory.Functor D C) [self : CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] {A B : D} (f g : A ⟶ B)
  [G.IsSplitPair f g], CategoryTheory.Limits.HasCoequalizer f g
-- Mathlib.Topology.Algebra.InfiniteSum.Order
le_hasProd' : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [CanonicallyOrderedMul α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α},
  HasProd f a → ∀ (i : ι), f i ≤ a
-- Mathlib.Algebra.CharP.Defs
ringExpChar.of_eq : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R] {q : ℕ}, ringExpChar R = q → ExpChar R q
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.step_takeWhile.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : false = true → motive true) (h_2 : false = false → motive false),
  (match hP : false with
    | true => h_1 hP
    | false => h_2 hP) =
    h_2 ⋯
-- Mathlib.GroupTheory.Perm.List
List.mem_or_mem_of_zipWith_swap_prod_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α} {x : α},
  (List.zipWith Equiv.swap l l').prod x ≠ x → x ∈ l ∨ x ∈ l'
-- Mathlib.Order.Category.Lat
Lat.hom_ext : ∀ {X Y : Lat} {f g : X ⟶ Y}, Lat.Hom.hom f = Lat.Hom.hom g → f = g
-- Mathlib.Data.Sum.Order
Sum.Lex.le_def : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α ⊕ₗ β},
  a ≤ b ↔ Sum.Lex (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) (ofLex a) (ofLex b)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_eq_of_not_monic : ∀ {R : Type u} [inst : Ring R] {q : Polynomial R} (p : Polynomial R), ¬q.Monic → p %ₘ q = p
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n'),
  (-γ).leftShift a n' hn' = -γ.leftShift a n' hn'
-- Lean.Elab.Binders
Lean.Elab.Term.checkBinderAnnotations : Lean.Option Bool
-- Mathlib.RingTheory.Flat.Stability
Module.Flat.instLocalizationAlgebraMapSubmonoid : ∀ {R : Type u} [inst : CommSemiring R] {A : Type u_3} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] [Module.Flat R A]
  (S : Submonoid R), Module.Flat (Localization S) (Localization (Algebra.algebraMapSubmonoid A S))
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.mem_polar_iff : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {x' : StrongDual 𝕜 E} (s : Set E),
  x' ∈ StrongDual.polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.prependMap : {α : Type u} →
  {β : α → Type v} →
    Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Zipper α β → Std.DTreeMap.Internal.Zipper α β
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_X : ∀ {R : Type u_1} [inst : Semiring R] (r : R), (Polynomial.taylor r) Polynomial.X = Polynomial.X + Polynomial.C r
-- Lean.ErrorExplanation
Lean.ErrorExplanation.Metadata.summary : Lean.ErrorExplanation.Metadata → String
-- Mathlib.Topology.Algebra.SeparationQuotient.Hom
/-- The lift of a monoid hom from `M` to a monoid hom from `SeparationQuotient M`.  -/
SeparationQuotient.liftContinuousMonoidHom : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] →
        [inst_2 : CommMonoid M] →
          [inst_3 : ContinuousMul M] →
            [inst_4 : CommMonoid N] →
              (f : M →ₜ* N) → (∀ (x y : M), Inseparable x y → f x = f y) → SeparationQuotient M →ₜ* N
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : CategoryTheory.Functor Y.Modules X.Modules}
  (h : AlgebraicGeometry.Scheme.Modules.pullback f ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Modules.pullbackComp (CategoryTheory.CategoryStruct.id X) f).inv
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.Scheme.Modules.pullback f).whiskerLeft (AlgebraicGeometry.Scheme.Modules.pullbackId X).hom)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.pullback f).rightUnitor.hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Mathlib.RingTheory.Idempotents
/-- One can lift a family of complete orthogonal idempotents of `R/e₀` to get one on `R`.

Note that the lemma itself is stated in terms of surjections (where `T = S / I`)
instead for syntactic generality.  -/
CompleteOrthogonalIdempotents.exists_eq_comp_of_ker_eq_span : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] {I : Type u_3} [inst_2 : Fintype I] (f : R →+* S)
  (e₀ : R),
  IsIdempotentElem e₀ →
    RingHom.ker f = Ideal.span {e₀} →
      ∀ (e : I → S),
        CompleteOrthogonalIdempotents e →
          (∀ (i : I), e i ∈ f.range) → ∃ e', (CompleteOrthogonalIdempotents fun t => Option.rec e₀ e' t) ∧ e = ⇑f ∘ e'
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toArray_roc_iff : ∀ {m n i : ℕ}, 0 < (m<...=n).toArray[i]! ↔ i < n - m
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- If a `G ⋙ F` has a limit, and `G` is an equivalence, we can construct a limit of `F`.  -/
CategoryTheory.Enriched.HasConicalLimit.of_equiv_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {J' : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J'] (V : Type u') [inst_2 : CategoryTheory.Category.{v', u'} V]
  [inst_3 : CategoryTheory.MonoidalCategory V] {C : Type u} [inst_4 : CategoryTheory.Category.{v, u} C]
  [inst_5 : CategoryTheory.EnrichedOrdinaryCategory V C] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor J' J) [G.IsEquivalence] [CategoryTheory.Enriched.HasConicalLimit V (G.comp F)],
  CategoryTheory.Enriched.HasConicalLimit V F
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C}
  (h : X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f').arrow h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) h)
-- Mathlib.FieldTheory.IsPerfectClosure
IsPRadical.of_id : ∀ (K : Type u_1) [inst : CommSemiring K] (p : ℕ), IsPRadical (RingHom.id K) p
-- Lean.Environment
/-- Information private to the module.  -/
Lean.Environment.Visibility.private : Lean.Environment.Visibility
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.reindex_inv_π_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) {Z : C}
  (h : (f ∘ ⇑ε) b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (ε b)) h
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.l_hom_inv : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.l_hom X).comp (CategoryTheory.FreeMonoidalCategory.Hom.l_inv X))
    (CategoryTheory.FreeMonoidalCategory.Hom.id (CategoryTheory.FreeMonoidalCategory.unit.tensor X))
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.ext_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂} {inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂}
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {x y : P.Hom Q},
  x = y ↔ x.weightMap = y.weightMap ∧ x.coweightMap = y.coweightMap ∧ x.indexEquiv = y.indexEquiv
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.J.eq_1 : SSet.modelCategoryQuillen.J = ⨆ n, CategoryTheory.MorphismProperty.ofHoms fun i => (SSet.horn (n + 1) i).ι
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.uliftFunctor_map_exact : ∀ (R : Type u) [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.Exact → (S.map (ModuleCat.uliftFunctor.{u_1, v, u} R)).Exact
-- Mathlib.SetTheory.Ordinal.Notation
/-- **Alias** of the forward direction of `ONote.lt_def`. -/
ONote.repr_lt_repr : ∀ {x y : ONote}, x < y → x.repr < y.repr
-- Mathlib.Analysis.InnerProductSpace.LinearMap
_private.Mathlib.Analysis.InnerProductSpace.LinearMap.0.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_right_Ico : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => x * c) '' Set.Ico a b = Set.Ico (a * c) (b * c)
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Scalar multiplication of rational functions.  -/
RatFunc.smul : {K : Type u_2} →
  [inst : CommRing K] → {R : Type u_3} → [SMul R (FractionRing (Polynomial K))] → R → RatFunc K → RatFunc K
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.NatTrans.CommShift₂.mk : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D] {M : Type u_6}
  [inst_3 : AddCommMonoid M] [inst_4 : CategoryTheory.HasShift C₁ M] [inst_5 : CategoryTheory.HasShift C₂ M]
  [inst_6 : CategoryTheory.HasShift D M] {G₁ G₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} {τ : G₁ ⟶ G₂}
  {h : CategoryTheory.CommShift₂Setup D M} [inst_7 : G₁.CommShift₂ h] [inst_8 : G₂.CommShift₂ h],
  autoParam (∀ (X₁ : C₁), CategoryTheory.NatTrans.CommShift (τ.app X₁) M)
      CategoryTheory.NatTrans.CommShift₂.commShift_app._autoParam →
    autoParam (∀ (X₂ : C₂), CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.flipApp τ X₂) M)
        CategoryTheory.NatTrans.CommShift₂.commShift_flipApp._autoParam →
      CategoryTheory.NatTrans.CommShift₂ τ h