mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.normalizer_inf_normalizer_le_normalizer_sup : ∀ {G : Type u_2} [inst : AddGroup G] (H K : AddSubgroup G),
  AddSubgroup.normalizer ↑H ⊓ AddSubgroup.normalizer ↑K ≤ AddSubgroup.normalizer ↑(H ⊔ K)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_succ : ∀ {n d : ℕ} (a : Fin (n + 1) → ℕ), (Behrend.map d) a = a 0 + (∑ x, a x.succ * d ^ ↑x) * d
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H2Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupCohomology.cocycles A 2)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2Iso A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.π A 2)) x) =
    (groupCohomology.shortComplexH2 A).moduleCatToCycles.range.mkQ
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₂ A).hom) x)
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of `x + y` is at most `totalWeight K * log 2`
plus the sum of the logarithmic heights of `x` and `y`.  -/
Height.logHeight₁_add_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.logHeight₁ (x + y) ≤ ↑(Height.totalWeight K) * Real.log 2 + Height.logHeight₁ x + Height.logHeight₁ y
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instMax : {α : Type u_1} → [inst : Lattice α] → Max (NonemptyInterval α)
-- Mathlib.Algebra.Order.Group.Action.End
RelEmbedding.apply_faithfulSMul : ∀ {α : Type u_1} {r : α → α → Prop}, FaithfulSMul (r ↪r r) α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.inter_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.inter m₂ = m₁ ∩ m₂
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.findEntry?_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} [Std.TransCmp cmp] (t : RBTree.RBMap α β cmp) (k : α) (v : β)
  (k' : α), (t.insert k v).findEntry? k' = if cmp k' k = Ordering.eq then some (k, v) else t.findEntry? k'
-- Mathlib.Util.CountHeartbeats
/-- Run a tactic, optionally restoring the original state, and report just the number of heartbeats.
 -/
Mathlib.CountHeartbeats.runTacForHeartbeats : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → optParam Bool true → Lean.Elab.Tactic.TacticM ℕ
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectIsomorphisms.jointlyFaithful : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [∀ (i : I), CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (F i)]
      [CategoryTheory.Limits.HasEqualizers C], CategoryTheory.JointlyFaithful F
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.instWellFoundedRelationWithBot : WellFoundedRelation (WithBot ℕ)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)} {a : ι} {S : Finset ι},
  ProbabilityTheory.Kernel.iIndepSets π κ μ → a ∉ S → ProbabilityTheory.Kernel.IndepSets (piiUnionInter π ↑S) (π a) κ μ
-- Init.Data.Vector.Count
Vector.countP_mono_left : ∀ {α : Type u_1} {p q : α → Bool} {n : ℕ} {xs : Vector α n},
  (∀ x ∈ xs, p x = true → q x = true) → Vector.countP p xs ≤ Vector.countP q xs
-- Mathlib.Data.Finset.Defs
Finset.subset_of_eq : ∀ {α : Type u_1} {s t : Finset α}, s = t → s ⊆ t
-- Mathlib.Order.Interval.Set.Basic
Set.notMem_Ico_of_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ c → c ∉ Set.Ico b a
-- Init.Data.SInt.Lemmas
Int8.toInt64_mod : ∀ (a b : Int8), (a % b).toInt64 = a.toInt64 % b.toInt64
-- Init.Data.SInt.Lemmas
Int16.mod_self : ∀ {a : Int16}, a % a = 0
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (I X : Set α), M.IsBasis' I X = Maximal (fun A => M.Indep A ∧ A ⊆ X) I
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- A restatement of `Types.Limit.map_π_apply` that uses `Pi.π` and `Pi.map`.  -/
CategoryTheory.Limits.Types.pi_map_π_apply : ∀ {β : Type v} [inst : Small.{u, v} β] {f g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : (fun X => X) (∏ᶜ f)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map α)) x) =
    (CategoryTheory.ConcreteCategory.hom (α b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E],
  Topology.IsQuotientMap f →
    ∀ [ContinuousConstSMul G E],
      (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) →
        ∀ [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E],
          IsCoveringMapOn f (f '' {e | MulAction.stabilizer G e = ⊥})
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- A binary predicate on `BVExpr`.
 -/
Std.Tactic.BVDecide.BVPred.bin : {w : ℕ} →
  Std.Tactic.BVDecide.BVExpr w →
    Std.Tactic.BVDecide.BVBinPred → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVPred
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqBindingS.checkDomains : Array Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContinuousLinearMap.contDiffPointwiseHolderAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {a : E} (f : E →L[ℝ] F), ContDiffPointwiseHolderAt k α (⇑f) a
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A bilinear map is called non-degenerate if it is left-separating and right-separating.  -/
LinearMap.Nondegenerate : {R : Type u_1} →
  {R₁ : Type u_2} →
    {R₂ : Type u_3} →
      {M : Type u_5} →
        {M₁ : Type u_6} →
          {M₂ : Type u_7} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module R M] →
                  [inst_3 : CommSemiring R₁] →
                    [inst_4 : AddCommMonoid M₁] →
                      [inst_5 : Module R₁ M₁] →
                        [inst_6 : CommSemiring R₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₂ M₂] →
                              {I₁ : R₁ →+* R} → {I₂ : R₂ →+* R} → (M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) → Prop
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- The adjoint quadruple `R.op ⊣ G.op ⊣ F.op ⊣ L.op` dual to an
adjoint quadruple `L ⊣ F ⊣ G ⊣ R`.  -/
CategoryTheory.Adjunction.Quadruple.op : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {G : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor D C} →
                CategoryTheory.Adjunction.Quadruple L F G R → CategoryTheory.Adjunction.Quadruple R.op G.op F.op L.op
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_inr_sumElim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α →₀ γ) (g : β →₀ γ),
  Finsupp.comapDomain Sum.inr (f.sumElim g) ⋯ = g
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRiiSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRiiSlice._auto_1) →
    Std.Rii.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RiiSlice α)
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the weights in the centroid
indexed by a `Fintype` sum to 1 if the set is nonempty.  -/
Finset.sum_centroidWeightsIndicator_eq_one_of_nonempty : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] [inst_2 : Fintype ι],
  s.Nonempty → ∑ i, Finset.centroidWeightsIndicator k s i = 1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSliceData.mk.injEq : ∀ {α : Type u} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Rcc α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Rcc α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Algebra.Group.Defs
/-- Zero is a left neutral element for addition  -/
AddMonoid.zero_add : ∀ {M : Type u} [self : AddMonoid M] (a : M), 0 + a = a
-- Mathlib.Algebra.Group.Hom.Defs
/-- Makes an additive group homomorphism from a proof that the map preserves addition.  -/
AddMonoidHom.mk' : {M : Type u_4} →
  {G : Type u_7} →
    [inst : AddGroup G] → [inst_1 : AddZeroClass M] → (f : M → G) → (∀ (a b : M), f (a + b) = f a + f b) → M →+ G
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C}
  (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) h) =
    CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.d₁ c₁₂ i₁ i₂ i₁₂) h)
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.category : Lean.Name → Lean.Name → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserExtension.Entry
-- Mathlib.Order.Interval.Basic
NonemptyInterval.dual_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : BoundedOrder α], NonemptyInterval.dual ⊤ = ⊤
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The projection from a subalgebra of `A` to an additive submonoid of `A`.  -/
Subalgebra.toAddSubmonoid : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A → AddSubmonoid A
-- Init.Data.Rat.Lemmas
Rat.intCast_eq_zero_iff : ∀ {a : ℤ}, ↑a = 0 ↔ a = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.inter_vsub_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s₁ s₂ t : Set β}, s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.setOfFloorNeg : {ι : Type u_3} → {s : Set (ι → ℕ)} → IsProperLinearSet s → [Finite ι] → Set (ι → ℕ)
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The global sections of an affine group scheme over `Spec R` are a `R`-Hopf algebra.  -/
AlgebraicGeometry.instHopfAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfGrpObjOverSchemeSpecAsOverOfIsAffine : {R : CommRingCat} →
  {G : AlgebraicGeometry.Scheme} →
    [inst : G.Over (AlgebraicGeometry.Spec R)] →
      [CategoryTheory.GrpObj (G.asOver (AlgebraicGeometry.Spec R))] →
        [AlgebraicGeometry.IsAffine G] → HopfAlgebra ↑R ↑(G.presheaf.obj (Opposite.op ⊤))
-- Mathlib.CategoryTheory.Sites.LeftExact
/-- An auxiliary definition to be used in the proof that `J.plusFunctor D` commutes
with finite limits.  -/
CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{t, w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {FD : D → D → Type u_1} →
                {CD : D → Type t} →
                  [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                    [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                      [∀ (X : C),
                            CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] →
                        [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] →
                          {K : Type s} →
                            [inst_8 : CategoryTheory.SmallCategory K] →
                              [CategoryTheory.FinCategory K] →
                                [inst_10 : CategoryTheory.Limits.HasLimitsOfShape K D] →
                                  [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)] →
                                    [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)] →
                                      (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) →
                                        (X : C) →
                                          (S :
                                              CategoryTheory.Limits.Cone
                                                (F.comp
                                                  ((J.plusFunctor D).comp
                                                    ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))) →
                                            S.pt ⟶ (J.plusObj (CategoryTheory.Limits.limit F)).obj (Opposite.op X)
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Eta-expanded form of `ContinuousOn.const_smul` -/
ContinuousOn.fun_const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {s : Set β}, ContinuousOn g s → ∀ (c : M), ContinuousOn (fun i => c • g i) s
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- If `f` is integrable on intervals `Ioc a (b i)`,
where `b i` tends to ∞, and
`∫ x in a .. b i, ‖f x‖ ∂μ` converges to `I : ℝ` along a filter `l`,
then `f` is integrable on the interval (a, ∞)  -/
MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] {b : ι → ℝ} {f : ℝ → E} (I a : ℝ),
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ) →
    Filter.Tendsto b l Filter.atTop →
      Filter.Tendsto (fun i => ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) l (nhds I) → MeasureTheory.IntegrableOn f (Set.Ioi a) μ
-- Std.Data.HashMap.Basic
/-- Returns an array of all values present in the hash map in some order.  -/
Std.HashMap.valuesArray : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Array β
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_neg : ∀ {R : Type u_1} {a b : R} [inst : Neg R] (z : QuadraticAlgebra R a b), (-z).im = -z.im
-- Std.Net.Addr
Std.Net.instInhabitedSocketAddressV6.default : Std.Net.SocketAddressV6
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
MeasureTheory.MemLp.finStronglyMeasurable_of_stronglyMeasurable : ∀ {α : Type u_1} {G : Type u_2} {p : ENNReal} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup G] {f : α → G},
  MeasureTheory.MemLp f p μ →
    MeasureTheory.StronglyMeasurable f → p ≠ 0 → p ≠ ⊤ → MeasureTheory.FinStronglyMeasurable f μ
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- The partition of `I : Box ι` into the boxes `I ∩ {y | y ≤ x i}` and `I ∩ {y | x i < y}`.
One of these boxes can be empty, then this partition is just the single-box partition `⊤`.  -/
BoxIntegral.Prepartition.split : {ι : Type u_1} → (I : BoxIntegral.Box ι) → ι → ℝ → BoxIntegral.Prepartition I
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.exists_ne_odd_degree_of_exists_odd_degree : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v : V),
  Odd (G.degree v) → ∃ w, w ≠ v ∧ Odd (G.degree w)
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.covMatrix_apply : ∀ {I : Finset NNReal} (s t : ↥I), ProbabilityTheory.BrownianReal.covMatrix I s t = ↑(min ↑s ↑t)
-- Std.Time.Format.Modifier
Std.Time.Modifier.N.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.N presentation) = 1 + sizeOf presentation
-- Mathlib.Data.Set.Insert
Set.insert_eq_self : ∀ {α : Type u_1} {s : Set α} {a : α}, insert a s = s ↔ a ∈ s
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coeff_coe : ∀ {R : Type u_1} [inst : Semiring R] (f : PowerSeries R) (i : ℤ),
  ((HahnSeries.ofPowerSeries ℤ R) f).coeff i = if i < 0 then 0 else (PowerSeries.coeff i.natAbs) f
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) {X Y : SimplexCategoryᵒᵖ} (θ : X ⟶ Y),
  (AlgebraicTopology.DoldKan.Γ₀.obj K).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ
-- Init.Prelude
/-- The `pure` function is overloaded via `Pure` instances.

`Pure` is typically accessed via `Monad` or `Applicative` instances.
 -/
Pure : (Type u → Type v) → Type (max (u + 1) v)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.le_of_testBit : ∀ {n m : ℕ}, (∀ (i : ℕ), n.testBit i = true → m.testBit i = true) → n ≤ m
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.monoModSerre_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] (X Y : C), P.monoModSerre 0 ↔ P X
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.map_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] ⦃X : D⦄,
  ∀ R ∈ K X,
    ∀ ⦃u : Φ.fiber.Elements⦄ (f : ((CategoryTheory.CategoryOfElements.π Φ.fiber).comp F).obj u ⟶ X),
      ∃ Y g,
        ∃ (_ : R.arrows g),
          ∃ v q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (F.map ↑q) f
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Equivalence.trans_toAdjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (e' : D ≌ E),
  (e.trans e').toAdjunction = e.toAdjunction.comp e'.toAdjunction
-- Mathlib.Computability.Language
Language.reverse_mul : ∀ {α : Type u_1} (l m : Language α), (l * m).reverse = m.reverse * l.reverse
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.indiscreteTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [IndiscreteTopology X]
  (h : X ≃ₜ Y), IndiscreteTopology Y
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₁ : (w : UInt8) → ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done → Option Char
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_finset_inf : ∀ {ι : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] (f : ι → TopologicalSpace.Opens α) (s : Finset ι),
  ↑(s.inf f) = s.inf (SetLike.coe ∘ f)
-- Lean.LocalContext
Lean.LocalContext.findDeclRev? : {β : Type u_1} → Lean.LocalContext → (Lean.LocalDecl → Option β) → Option β
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCancelMonoid α],
  OrderDual.instAddCancelMonoid =
    { toAddLeftCancelMonoid := OrderDual.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.subset_smul_finset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s t : Finset β}
  {a : α}, s ⊆ a • t ↔ a⁻¹ • s ⊆ t
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.mk.inj : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} {inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀}
  {inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰}
  {functor : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme}
  {natTrans : functor ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰}
  {equifibered : CategoryTheory.NatTrans.Equifibered natTrans}
  {functor_1 : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme}
  {natTrans_1 : functor_1 ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰}
  {equifibered_1 : CategoryTheory.NatTrans.Equifibered natTrans_1},
  { functor := functor, natTrans := natTrans, equifibered := equifibered } =
      { functor := functor_1, natTrans := natTrans_1, equifibered := equifibered_1 } →
    functor = functor_1 ∧ natTrans ≍ natTrans_1
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.opHom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : C)
  (f : X ⟶ Y), (CategoryTheory.opHom X Y) f = f.op
-- Mathlib.Data.Fintype.Card
Fintype.card_unit : Fintype.card Unit = 1
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- Fixed points of sup of subgroups is intersection  -/
fixedPoints_subgroup_sup : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {P Q : Subgroup M},
  MulAction.fixedPoints (↥(P ⊔ Q)) α = MulAction.fixedPoints (↥P) α ∩ MulAction.fixedPoints (↥Q) α
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_spec : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f.mk' x y * f ↑y = f x
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.subset_interior_succ : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (n : ℕ), K n ⊆ interior (K (n + 1))
-- Mathlib.CategoryTheory.Functor.Currying
/-- Natural isomorphism witnessing `comp_flip_curry_eq`.  -/
CategoryTheory.Functor.curryObjCompIso : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} D] →
            {E : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E] →
                (F : CategoryTheory.Functor (C × B) D) →
                  (G : CategoryTheory.Functor D E) →
                    (CategoryTheory.Functor.curry.obj (F.comp G)).flip ≅
                      (CategoryTheory.Functor.curry.obj F).flip.comp
                        ((CategoryTheory.Functor.whiskeringRight C D E).obj G)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasFDerivAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {f' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x → f₁ =ᶠ[nhds x] f → HasFDerivAt f₁ f' x