mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseFlexibleNum : ℕ → Std.Internal.Parsec.String.Parser ℕ
-- Lean.Server.ServerTask
Lean.Server.ServerTask.BaseIO.asTask : {α : Type} → BaseIO α → BaseIO (Lean.Server.ServerTask α)
-- Mathlib.Data.List.DropRight
/-- Drop elements from the tail end of a list that satisfy `p : α → Bool`.
Implemented naively via `List.reverse`  -/
List.rdropWhile : {α : Type u_1} → (α → Bool) → List α → List α
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If orders are finite, the divisor of the scalar product of two meromorphic functions is the sum of
the divisors.
 -/
MeromorphicOn.divisor_fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      (∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) →
        (∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) →
          MeromorphicOn.divisor (fun z => f₁ z • f₂ z) U = MeromorphicOn.divisor f₁ U + MeromorphicOn.divisor f₂ U
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_addZ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).addZ (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addZ P Q)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.instFintypeElemVectorVectorsProdEqOne : (G : Type u_2) → [inst : Group G] → (n : ℕ) → [Fintype G] → Fintype ↑(Equiv.Perm.vectorsProdEqOne G n)
-- Init.Grind.ToInt
/-- The embedding into the integers takes multiplication to multiplication, wrapped into the range interval.
 -/
Lean.Grind.ToInt.Mul : (α : Type u) → [Mul α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injectiveDimension.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.injectiveDimension X = sInf {n | ∀ (i : ℕ), n < ↑i → CategoryTheory.HasInjectiveDimensionLT X i}
-- Mathlib.Topology.Constructions
Quotient.preimage_mem_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] [s : Setoid X] {V : Set (Quotient s)} {x : X},
  V ∈ nhds (Quotient.mk' x) → Quotient.mk' ⁻¹' V ∈ nhds x
-- Mathlib.Topology.Inseparable
/-- A set is stable under specialization iff it is a union of closed sets.  -/
stableUnderSpecialization_iff_exists_sUnion_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  StableUnderSpecialization s ↔ ∃ S, (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s
-- Mathlib.Order.Category.Semilat
SemilatInfCat.coe_of : ∀ (α : Type u_1) [inst : SemilatticeInf α] [inst_1 : OrderTop α],
  { X := α, isSemilatticeInf := inst, isOrderTop := inst_1 }.X = α
-- Lean.Parser.Basic
Lean.Parser.checkTailLinebreak : Lean.Syntax → Bool
-- Init.Data.SInt.Basic
/-- Constructs an `Int32` from an `Int`, clamping if the value is too small or too large.  -/
Int32.ofIntClamp : ℤ → Int32
-- Mathlib.Data.Set.Prod
Set.image_fst_graphOn : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Prod.fst '' Set.graphOn f s = s
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.shift_app_comm_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D}
  (h : (CategoryTheory.shiftFunctor D a).obj (F₂.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) h) =
    CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₂ a).hom.app X) h)
-- Mathlib.Data.Finset.Sups
Finset.singleton_sups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {t : Finset α} {a : α},
  {a} ⊻ t = Finset.image (fun x => a ⊔ x) t
-- Std.Http.Server
/-- Active HTTP connections
 -/
Std.Http.Server.activeConnections : Std.Http.Server → Std.Mutex ℕ
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.relabel : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n m : ℕ} {φ : L.BoundedFormula α m},
  φ.IsQF → ∀ (f : α → β ⊕ Fin n), (FirstOrder.Language.BoundedFormula.relabel f φ).IsQF
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j : 𝒰.I₀),
  AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullbackSymmetry
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullbackAssoc (𝒰.f j) (𝒰.f i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f j) (𝒰.f i))
              (CategoryTheory.CategoryStruct.comp (𝒰.f i) f))
            g
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j))
              (CategoryTheory.CategoryStruct.comp (𝒰.f j) f))
            g (CategoryTheory.Limits.pullbackSymmetry (𝒰.f j) (𝒰.f i)).hom (CategoryTheory.CategoryStruct.id Y)
            (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullbackAssoc (𝒰.f i) (𝒰.f j) (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g).hom
            (CategoryTheory.Limits.pullbackSymmetry (𝒰.f i)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))).hom)))
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.instEquivLike : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : Add A] →
        [inst_1 : Add B] →
          [inst_2 : Mul A] →
            [inst_3 : Mul B] →
              [inst_4 : SMul R A] →
                [inst_5 : SMul R B] → [inst_6 : Star A] → [inst_7 : Star B] → EquivLike (A ≃⋆ₐ[R] B) A B
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.continuousOn_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ContinuousOn (ProbabilityTheory.mgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ))
-- Init.Data.Array.Lemmas
Array.map_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α}, Array.map f xs = #[] ↔ xs = #[]
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_image2_eq_csInf_csSup : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) →
    (∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)) →
      s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sInf s) (sSup t)
-- Mathlib.Algebra.Algebra.Prod
AlgHom.prod_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  {C' : Type u_5} [inst_7 : Semiring C'] [inst_8 : Algebra R C'] (f : A →ₐ[R] B) (g : B →ₐ[R] C) (g' : B →ₐ[R] C'),
  (g.prod g').comp f = (g.comp f).prod (g'.comp f)
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.cell_def : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ), Topology.RelCWComplex.cell (↑E) n = ↑(E.I n)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_mk : ∀ {α : Type u_1} {L₁ : List (α × Bool)} [inst : DecidableEq α], (FreeAddGroup.mk L₁).toWord = FreeAddGroup.reduce L₁
-- Mathlib.Order.Partition.Basic
Partition.rep.congr_simp : ∀ {α : Type u_1} {u t t_1 : Set α} (e_t : t = t_1) (P P_1 : Partition u) (e_P : P = P_1) (ht : t ∈ P),
  P.rep ht = P_1.rep ⋯
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_eq_sum_compProd_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ), κ.compProd η = ProbabilityTheory.Kernel.sum fun n => (κ.seq n).compProd η
-- Init.Data.SInt.Lemmas
Int8.not_maxValue_lt : ∀ {a : Int8}, ¬Int8.maxValue < a
-- Mathlib.Order.CompleteBooleanAlgebra
codisjoint_sInf_iff : ∀ {α : Type u} [inst : Order.Coframe α] {a : α} {s : Set α}, Codisjoint a (sInf s) ↔ ∀ b ∈ s, Codisjoint a b
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite'' : ∀ (c0 c1 : Bool) {a b : Bool}, (bif c0 then a else !bif c1 then b else !a) = bif !c0 && c1 then !b else a
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.D'.eq_1 : ∀ (r : ℕ+), ADEInequality.D' r = {2, 2, r}
-- Mathlib.Data.Finset.Preimage
Finset.image_subset_iff_subset_preimage : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β}
  (hf : Set.InjOn f (f ⁻¹' ↑t)), Finset.image f s ⊆ t ↔ s ⊆ t.preimage f hf
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- Equivalences form a group.  -/
RootPairing.Equiv.instGroup : {ι : 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] → (P : RootPairing ι R M N) → Group (P.Equiv P)
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- The head type  -/
MvPFunctor.A : {n : ℕ} → MvPFunctor.{u} n → Type u
-- Mathlib.Data.FunLike.IsApply
/-- `IsOneApplyEqSelf F α α` states for all `x : α`, `(1 : F) x = x`.  -/
IsOneApplyEqSelf : (F : Type u_1) → (α : outParam (Type u_2)) → [FunLike F α α] → [One F] → Prop
-- Mathlib.Data.QPF.Univariate.Basic
/-- Quotients of polynomial functors.

Roughly speaking, saying that `F` is a quotient of a polynomial functor means that for each `α`,
elements of `F α` are represented by pairs `⟨a, f⟩`, where `a` is the shape of the object and
`f` indexes the relevant elements of `α`, in a suitably natural manner.
 -/
QPF : (Type u → Type v) → Type (max (max (u + 1) (u' + 1)) v)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule'_add : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (x y : LocalizedModule S M),
  IsLocalizedModule.fromLocalizedModule' S f (x + y) =
    IsLocalizedModule.fromLocalizedModule' S f x + IsLocalizedModule.fromLocalizedModule' S f y
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.map.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → γ a),
  Std.DTreeMap.Internal.Impl.map f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.isoLimitCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.LimitCone F),
  CategoryTheory.Limits.limit.isoLimitCone t = (CategoryTheory.Limits.limit.isLimit F).conePointUniqueUpToIso t.isLimit
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_const_smul_apply' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {R : Type u_3} [inst_5 : DistribSMul R F] [inst_6 : SMulCommClass 𝕜 R F] [inst_7 : ContinuousConstSMul R F]
  {i : ℕ} {a : R}, ContDiffAt 𝕜 (↑i) f x → iteratedFDeriv 𝕜 i (fun x => a • f x) x = a • iteratedFDeriv 𝕜 i f x
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_add_tsum_ite : ∀ {β : Type u_2} {f : β → ENNReal} (b : β), ∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod_addSubgroupOf_prod_normal : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H₁ K₁ : AddSubgroup G}
  {H₂ K₂ : AddSubgroup N} [h₁ : (H₁.addSubgroupOf K₁).Normal] [h₂ : (H₂.addSubgroupOf K₂).Normal],
  ((H₁.prod H₂).addSubgroupOf (K₁.prod K₂)).Normal
-- Mathlib.Data.Finset.Card
Finset.card_eq_one_iff_existsUnique : ∀ {α : Type u_1} {s : Finset α}, s.card = 1 ↔ ∃! a, a ∈ s
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- Special case of the grid-lines lemma `lintegral_mul_prod_lintegral_pow_le`, taking the extremal
exponent `p = (#ι - 1)⁻¹`.  -/
MeasureTheory.lintegral_prod_lintegral_pow_le : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {p : ℝ},
  (↑(Fintype.card ι)).HolderConjugate p →
    ∀ {f : ((a : ι) → A a) → ENNReal},
      Measurable f →
        ∫⁻ (x : (i : ι) → A i),
            ∏ i,
              (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^
                (1 / (↑(Fintype.card ι) - 1)) ∂MeasureTheory.Measure.pi μ ≤
          (∫⁻ (x : (i : ι) → A i), f x ∂MeasureTheory.Measure.pi μ) ^ p
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_inf : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] (a : α)
  (S T : Subgroup G), a • (S ⊓ T) = a • S ⊓ a • T
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.HasEval.X : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R], PowerSeries.HasEval PowerSeries.X
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedCounters : Inhabited Lean.Meta.Grind.Counters
-- Lean.Meta.LazyDiscrTree
/-- A discriminator tree for the current module's declarations only.

Note. We use different discriminator trees for imported and current module
declarations since imported declarations are typically much more numerous but
not changed after the environment is created.
 -/
Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef : Type → Type
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_injective : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.Injective PolynomialModule.coeff
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_sub_self : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a : R), Int.fract a - a = -↑⌊a⌋
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndependent_subsingleton_index_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] [Subsingleton ι] (f : ι → M),
  LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
-- Mathlib.Topology.Connected.Clopen
/-- A continuous map from a connected space to a disjoint union `Σ i, X i` can be lifted to one of
the components `X i`. See also `ContinuousMap.exists_lift_sigma` for a version with bundled
`ContinuousMap`s.  -/
Continuous.exists_lift_sigma : ∀ {α : Type u} {ι : Type u_1} {X : ι → Type u_2} [inst : TopologicalSpace α] [ConnectedSpace α]
  [inst_2 : (i : ι) → TopologicalSpace (X i)] {f : α → (i : ι) × X i},
  Continuous f → ∃ i g, Continuous g ∧ f = Sigma.mk i ∘ g
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.hasFiniteProducts : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.ContainsIdentities]
  [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts], CategoryTheory.Limits.HasFiniteProducts D
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.isPrimitive_of_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] {p q : Polynomial R}, p.IsPrimitive → q ∣ p → q.IsPrimitive
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.finalizeImport : {α σ : Type} → Lean.SimpleScopedEnvExtension.Descr α σ → σ → σ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [Inhabited α],
  t.WF → ∀ {k : α} {f : Option β → Option β} {hc : k ∈ t.alter k f}, (t.alter k f).getKey k hc = k
-- Init.Data.List.Impl
List.eraseP.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α),
  List.eraseP p (a :: as) = bif p a then as else a :: List.eraseP p as
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A fraction is equal to its expansion by a factor from `S`.  -/
OreLocalization.expand' : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (r : X) (s s' : ↥S), r /ₒ s = s' • r /ₒ (s' * s)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.map_single : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A) (r : relations.R),
  (relations.map fun₀ | r => 1) = relations.relation r
-- Init.Core
/-- You should not use this function  -/
PNonScalar.mk : ℕ → PNonScalar
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularMono.lift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y W : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.IsRegularMono f] (k k_1 : W ⟶ Y) (e_k : k = k_1)
  (h :
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.left f) =
      CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.right f)),
  CategoryTheory.IsRegularMono.lift f k h = CategoryTheory.IsRegularMono.lift f_1 k_1 ⋯
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
/-- The equalizer of two morphisms of type-valued functors of types of the form
`A.toFunctor ⟶ F₂` with `A : Subfunctor F₁`, as a subcomplex of `F₁`.  -/
CategoryTheory.Subfunctor.equalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₁ F₂ : CategoryTheory.Functor C (Type w)} →
      {A : CategoryTheory.Subfunctor F₁} → (A.toFunctor ⟶ F₂) → (A.toFunctor ⟶ F₂) → CategoryTheory.Subfunctor F₁
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.nth_mul_coeff : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (k : Type u_1) [inst : CommRing k] [CharP k p] (n : ℕ),
  ∃ f,
    ∀ (x y : WittVector p k),
      (x * y).coeff (n + 1) =
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
          f (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (ε : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
  (X : C),
  (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ ε).app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) ε
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairing_castSucc : ∀ {m : ℕ} (k : Fin (m + 1)) (n : ℕ),
  SSet.prodStdSimplex.pairing k.castSucc n = (SSet.prodStdSimplex.pairingCore k n).pairing
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.down_sInf : ∀ {α : Type u_1} [inst : InfSet α] (s : Set (ULift.{v, u_1} α)), (sInf s).down = sInf (ULift.up ⁻¹' s)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Ric.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Ric α}, r.toList = (Std.Ric.Internal.iter r).toList
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.essImage_yonedaGrp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaGrp.essImage = fun F => (F.comp (CategoryTheory.forget GrpCat)).IsRepresentable
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD_of_not_continuous : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : Zero X] {f : X → R} {g : ContinuousMapZero X R}, ¬Continuous f → ContinuousMapZero.mkD f g = g
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.restrictScalars_apply : ∀ {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : Ring S] [inst_3 : Nontrivial S] [inst_4 : AddCommGroup M] [inst_5 : Algebra R S] [inst_6 : Module S M]
  [inst_7 : Module R M] [inst_8 : IsScalarTower R S M] [inst_9 : Module.IsTorsionFree R S] (b : Module.Basis ι S M)
  (i : ι), ↑((Module.Basis.restrictScalars R b) i) = b i
-- Lean.Environment
Lean.ModuleData.imports : Lean.ModuleData → Array Lean.Import
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.toLawson_ofLawson : ∀ {α : Type u_1} (a : Topology.WithLawson α), Topology.WithLawson.toLawson (Topology.WithLawson.ofLawson a) = a
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int16.natCast : NatCast Int16
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_neg_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddGroup (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {g : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ}, (∀ (i : ι), h i 0 = 1) → (-g).prod h = g.prod fun i b => h i (-b)
-- Mathlib.Topology.Connected.PathConnected
isPathConnected_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PathConnectedSpace X]
  {f : X → Y}, Continuous f → IsPathConnected (Set.range f)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.Sheaf.H'.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)]
  (F F_1 : CategoryTheory.Sheaf J AddCommGrpCat),
  F = F_1 → ∀ (n n_1 : ℕ), n = n_1 → ∀ (X X_1 : C), X = X_1 → F.H' n X = F_1.H' n_1 X_1