mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.Disjoint.extendDomain : ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) {σ τ : Equiv.Perm α},
  σ.Disjoint τ → (σ.extendDomain f).Disjoint (τ.extendDomain f)
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.quotientQuotientEquivQuotient.congr_simp : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M),
  QuotientGroup.quotientQuotientEquivQuotient N M h = QuotientGroup.quotientQuotientEquivQuotient N M h
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.hasIterationOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C
-- Mathlib.Topology.UniformSpace.Cauchy
isComplete_iff_clusterPt : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  IsComplete s ↔ ∀ (l : Filter α), Cauchy l → l ≤ Filter.principal s → ∃ x ∈ s, ClusterPt x l
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl : ∀ {m : Type u_1} {n : Type u_2} [Finite m] [Finite n] {σ : Equiv.Perm (m ⊕ n)},
  Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) → σ ∈ (Equiv.Perm.sumCongrHom m n).range
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_iso_inv_eq'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : (CategoryTheory.CatCenter C)ˣ) {X Y : C} (f : X ≅ Y)
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (z • f).inv h =
    CategoryTheory.CategoryStruct.comp ((↑z⁻¹).app Y) (CategoryTheory.CategoryStruct.comp f.inv h)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.constInsertManyIfNewUnit! : ∀ {α : Type u} {x : Ord α} [Std.TransOrd α] {ρ : Type u_1} [inst : ForIn Id ρ α] {l : ρ}
  {t : Std.DTreeMap.Internal.Impl α fun x => Unit},
  t.WF → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).WF
-- Init.Data.UInt.Bitwise
USize.toFin_shiftLeft : ∀ (a b : USize), b.toNat < System.Platform.numBits → (a <<< b).toFin = a.toFin <<< b.toFin
-- Mathlib.RingTheory.Polynomial.Ideal
Algebra.mem_ideal_map_adjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (x : S)
  (I : Ideal R) {y : ↥R[x]},
  y ∈ Ideal.map (algebraMap R ↥R[x]) I ↔ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (Polynomial.aeval x) p = ↑y
-- Mathlib.Algebra.GroupWithZero.Regular
/-- The element `0` is left-regular if and only if `R` is trivial.  -/
isLeftRegular_zero_iff_subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsLeftRegular 0 ↔ Subsingleton R
-- Mathlib.Topology.Sheaves.Presheaf
/-- If `H : X ≅ Y` is a homeomorphism,
then given an `H _* ℱ ⟶ 𝒢`, we may obtain an `ℱ ⟶ H ⁻¹ _* 𝒢`.
 -/
TopCat.Presheaf.pushforwardToOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : TopCat} →
      (H₁ : X ≅ Y) →
        {ℱ : TopCat.Presheaf C Y} →
          {𝒢 : TopCat.Presheaf C X} →
            (ℱ ⟶ (TopCat.Presheaf.pushforward C H₁.hom).obj 𝒢) → ((TopCat.Presheaf.pushforward C H₁.inv).obj ℱ ⟶ 𝒢)
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.IsCocontinuous.cover_lift : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {G : CategoryTheory.Functor C D}
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [self : G.IsCocontinuous J K]
  {U : C} {S : CategoryTheory.Sieve (G.obj U)}, S ∈ K (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J U
-- Mathlib.Data.Nat.Digits.Lemmas
/-- Explicit computation of the `i`-th digit of `n` in base `b`.  -/
Nat.getD_digits : ∀ (n i : ℕ) {b : ℕ}, 2 ≤ b → (b.digits n).getD i 0 = n / b ^ i % b
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiagonal_four : Int.divisorsAntidiag 4 = {(1, 4), (2, 2), (4, 1), (-1, -4), (-2, -2), (-4, -1)}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inl_fst_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inl (CategoryTheory.CategoryStruct.comp self.fst h) = h
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) (i₁ i₂ : M₁ →ₗ[R] M₁) (j₁ j₂ : M₂ →ₗ[R] M₂),
  hf.map hf (i₁ * i₂) (j₁ * j₂) = hf.map hf i₁ j₁ * hf.map hf i₂ j₂
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.pow_right_strictMono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommSemiring α] [inst_2 : PartialOrder α] [OrderBot α]
  [inst_4 : CanonicallyOrderedAdd α] [PosMulStrictMono α] [inst_6 : NoZeroDivisors α] [inst_7 : Nontrivial α] {n : ℕ},
  n ≠ 0 → StrictMono fun a => a ^ n
-- Mathlib.Tactic.Simps.NotationClass
/-- Find arguments by prepending `ℤ` and duplicating the first argument. Used for `zsmul`.  -/
Simps.zsmulArgs : Simps.findArgType
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.evalCLM_apply : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_7}
  (F : Type u_8) [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] (a : E) (m : E →SLₚₜ[σ] F), (PointwiseConvergenceCLM.evalCLM σ F a) m = m a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageAddMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] [inst_4 : FunLike F α β] [inst_5 : AddMonoidHomClass F α β] (f : F) (a : Finset α),
  (Finset.imageAddMonoidHom f) a = (Finset.imageAddHom f).toFun a
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- The one point compactification of a `T1Space` space is a `T1Space`.  -/
OnePoint.instT1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], T1Space (OnePoint X)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDiv_eq_iff : ∀ {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₁ r₂ : X} {s₁ s₂ : ↥S}, r₁ /ₒ s₁ = r₂ /ₒ s₂ ↔ ∃ u v, u • r₂ = v • r₁ ∧ ↑u * ↑s₂ = v * ↑s₁
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_signedInfDist_incenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  SignType.sign ((s.signedInfDist i) s.incenter) = 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH1_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.shortComplexH1 A).g = groupHomology.d₁₀ A
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_intCast_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoMod hp a (↑m * p + b) = toIcoMod hp a b
-- Aesop.BuiltinRules.Rfl
Aesop.BuiltinRules.rfl : Aesop.RuleTac
-- Mathlib.Topology.Inseparable
Specializes.clusterPt : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {f : Filter X}, x ⤳ y → ClusterPt x f → ClusterPt y f
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.orthogonal.eq_1 : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (Φ : LinearMap.BilinForm R M)
  (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N : LieSubmodule R L M),
  LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N = { toSubmodule := Φ.orthogonal ↑N, lie_mem := ⋯ }
-- Mathlib.Logic.Small.Set
small_insert : ∀ {α : Type u1} (x : α) (s : Set α) [Small.{u, u1} ↑s], Small.{u, u1} ↑(insert x s)
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.succ?_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (f : Std.PRange.UpwardEnumerable.Map α β) {a b : α},
  Std.PRange.succ? a = some b ↔ Std.PRange.succ? (f.toFun a) = some (f.toFun b)
-- Init.Grind.Lemmas
Lean.Grind.eq_true_of_imp_eq_false : ∀ {a b : Prop}, (a → b) = False → a = True
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.fixedBy_mul : ∀ (α : Type u_1) {M : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] (m₁ m₂ : M),
  MulAction.fixedBy α m₁ ∩ MulAction.fixedBy α m₂ ⊆ MulAction.fixedBy α (m₁ * m₂)
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.BuiltinParserAttribute.add : Lean.Name → Lean.Name → Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.instSigmaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type v} (g : β → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct g] [∀ (b : β), CategoryTheory.Projective (g b)],
  CategoryTheory.Projective (∐ g)
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat_2 : {α : Type u} → Std.Rci.Sliceable (Subarray α) ℕ (Subarray α)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {f : β → α}, ∅.inf f = ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_eq_fallback : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} {fallback : β a}, m.contains a = false → m.getD a fallback = fallback
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Condition on `w : TwoSquare T L R B` expressing that it is a Guitart exact square.
It is equivalent to saying that for any `X₃ : C₃`, the induced functor
`CostructuredArrow L X₃ ⥤ CostructuredArrow R (B.obj X₃)` is final (see `guitartExact_iff_final`)
or equivalently that for any `X₂ : C₂`, the induced functor
`StructuredArrow X₂ T ⥤ StructuredArrow (R.obj X₂) B` is initial (see `guitartExact_iff_initial`).
See also  `guitartExact_iff_isConnected_rightwards`, `guitartExact_iff_isConnected_downwards`
for characterizations in terms of the connectedness of auxiliary categories.  -/
CategoryTheory.TwoSquare.GuitartExact : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} → CategoryTheory.TwoSquare T L R B → Prop
-- Mathlib.NumberTheory.Rayleigh
compl_beattySeq' : ∀ {r s : ℝ}, r.HolderConjugate s → {x | ∃ k, beattySeq' r k = x}ᶜ = {x | ∃ k, beattySeq s k = x}
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
/-- Lower bound on the edge densities between non-uniform parts of `SzemerediRegularity.increment`.
 -/
SzemerediRegularity.edgeDensity_chunk_not_uniform : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ε ≤ 1 →
        ∀ {hU : U ∈ P.parts} {hV : V ∈ P.parts},
          U ≠ V →
            ¬G.IsUniform ε U V →
              ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤
                (∑ ab ∈ (SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts,
                    ↑(G.edgeDensity ab.1 ab.2) ^ 2) /
                  16 ^ P.parts.card
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The forgetful functor from `𝒪_{Spec R}` modules to sheaves of `R`-modules.  -/
AlgebraicGeometry.modulesSpecToSheaf : {R : CommRingCat} →
  CategoryTheory.Functor (AlgebraicGeometry.Spec R).Modules
    (TopCat.Sheaf (ModuleCat ↑R) ↑(AlgebraicGeometry.Spec R).toPresheafedSpace)
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
/-- Compute the target of the composition of two open partial homeomorphisms induced by fiberwise
linear equivalences.  -/
FiberwiseLinear.target_trans_openPartialHomeomorph : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {φ φ' : B → F ≃L[𝕜] F} {U U' : Set B} (hU : IsOpen U)
  (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(φ x).symm) U) (hU' : IsOpen U')
  (hφ' : ContinuousOn (fun x => ↑(φ' x)) U') (h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'),
  ((FiberwiseLinear.openPartialHomeomorph φ hU hφ h2φ).trans
        (FiberwiseLinear.openPartialHomeomorph φ' hU' hφ' h2φ')).target =
    (U ∩ U') ×ˢ Set.univ
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.MonObj A} {X : D} {mod : CategoryTheory.ModObj A X} {X_1 : D}
  {mod_1 : CategoryTheory.ModObj A X_1}, { X := X, mod := mod } = { X := X_1, mod := mod_1 } → X = X_1 ∧ mod ≍ mod_1
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.units_smul_span_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M}, Submodule.span R (Set.range v) = ⊤ → ∀ {w : ι → Rˣ}, Submodule.span R (Set.range (w • v)) = ⊤
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.coeff_scaleRoots : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R) (i : ℕ),
  (p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)
-- Mathlib.Topology.Irreducible
irreducibleComponents_eq_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [IrreducibleSpace X], irreducibleComponents X = {Set.univ}
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (W : (↑V).Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((TopologicalSpace.Opens.map (X.homOfLE e).base).obj W) ≤
    (AlgebraicGeometry.Scheme.Hom.opensFunctor V.ι).obj W
-- Mathlib.Data.Nat.Factorization.Defs
/-- Every nonzero natural number has a unique prime factorization  -/
Nat.factorization_inj : Set.InjOn Nat.factorization {x | x ≠ 0}
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity_le_of_dvd : ∀ {M : Type u_1} [inst : CommMonoid M] {k l : ℕ}, k ∣ l → rootsOfUnity k M ≤ rootsOfUnity l M
-- Mathlib.Data.Finite.Defs
/-- A set is infinite if it is not finite.

This is protected so that it does not conflict with global `Infinite`.  -/
Set.Infinite : {α : Type u} → Set α → Prop
-- Mathlib.Order.Completion
DedekindCut.principalIso_apply : ∀ {α : Type u_1} [inst : CompleteLattice α] (a : α), DedekindCut.principalIso a = DedekindCut.principal a
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.mem_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {x : E}, x ∈ ⊤
-- Lean.Parser.Extension
Lean.Parser.getSyntaxNodeKinds : Lean.Environment → List Lean.SyntaxNodeKind
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOpCLM_apply : ∀ {R : Type u_4} {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] [inst_1 : TopologicalSpace E] [inst_2 : Ring R]
  [inst_3 : AddCommGroup V] [inst_4 : AddCommGroup E] [inst_5 : Module R E] [inst_6 : LineDerivAdd V E E]
  [inst_7 : LineDerivSMul R V E E] [inst_8 : ContinuousLineDeriv V E E] {n : ℕ} (m : Fin n → V) (x : E),
  (LineDeriv.iteratedLineDerivOpCLM R E m) x = LineDeriv.iteratedLineDerivOp m x
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instCategory : CategoryTheory.Category.{u, u + 1} AddCommGrpCat
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.rightAdjointMate_comp_evaluation_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] (f : X ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (fᘁ) X)
      (CategoryTheory.CategoryStruct.comp (ε_ X Xᘁ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ f)
      (CategoryTheory.CategoryStruct.comp (ε_ Y Yᘁ) h)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_antimono : ∀ {X : AlgebraicGeometry.Scheme} {S T : TopologicalSpace.Closeds ↥X},
  S ≤ T →
    AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal T ≤ AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal S
-- Mathlib.Order.CompleteLattice.Defs
CompleteLattice.toCompleteSemilatticeSup : {α : Type u_8} → [self : CompleteLattice α] → CompleteSemilatticeSup α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.diag_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag X) (CategoryTheory.Limits.prod.map f f) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.diag Y)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- **Hölder's inequality for integrable functions**: the scalar multiplication of an integrable
vector-valued function by a scalar function with finite essential supremum is integrable.  -/
MeasureTheory.Integrable.essSup_smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {R : Type u_8} [inst_1 : NormedRing R] [inst_2 : Module R β] [IsBoundedSMul R β] {f : α → β},
  MeasureTheory.Integrable f μ →
    ∀ {g : α → R},
      MeasureTheory.AEStronglyMeasurable g μ →
        essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤ → MeasureTheory.Integrable (fun x => g x • f x) μ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add'_zero : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y),
  CategoryTheory.Localization.Preadditive.add' W f (L.map 0) = f
-- Mathlib.Topology.Instances.Real.Lemmas
Real.subfield_eq_of_closed : ∀ {K : Subfield ℝ}, IsClosed ↑K → K = ⊤
-- Lean.Language.Basic
Lean.Language.SnapshotTask.mk : {α : Type} →
  Option Lean.Syntax →
    Lean.Language.SnapshotTask.ReportingRange → Option IO.CancelToken → Task α → Lean.Language.SnapshotTask α
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.comp_def : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.RationalMap Y)
  [inst_2 : f.IsDominant] (g : Y.PartialMap Z), f.comp g.toRationalMap = (f.representative.comp g).toRationalMap
-- Init.Data.List.Basic
/-- Separates a list of pairs into two lists that contain the respective first and second components.

`O(|l|)`. This is a tail-recursive version of `List.unzip` that's used at runtime.

Examples:
* `[("Monday", 1), ("Tuesday", 2)].unzipTR = (["Monday", "Tuesday"], [1, 2])`
* `[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzipTR = ([x₁, x₂, x₃], [y₁, y₂, y₃])`
* `([] : List (Nat × String)).unzipTR = (([], []) : List Nat × List String)`
 -/
List.unzipTR : {α : Type u} → {β : Type v} → List (α × β) → List α × List β
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.isomorphisms C).HasTwoOutOfThreeProperty
-- Mathlib.Data.Num.Basic
PosNum.decidableLT : DecidableLT PosNum
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_finsetSum : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} (s : Finset ι)
  {f : ι → α → E},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) →
    (MeasureTheory.setToFun μ T hT fun a => ∑ i ∈ s, f i a) = ∑ i ∈ s, MeasureTheory.setToFun μ T hT (f i)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- `parallelPair f g` is the diagram in `C` consisting of the two morphisms `f` and `g` with
common domain and codomain.  -/
CategoryTheory.Limits.parallelPair : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (X ⟶ Y) → (X ⟶ Y) → CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.isPiSystem_Iic_rat : IsPiSystem (⋃ a, {Set.Iic ↑a})
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- The key that's handled. May be anonymous for certain kinds.  -/
Lean.Elab.ConfigEval.EvalConfigItemHandler.key : Lean.Elab.ConfigEval.EvalConfigItemHandler → Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.IsComonHom.hom_counit : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : C}
  {inst_2 : CategoryTheory.ComonObj M} {inst_3 : CategoryTheory.ComonObj N} (f : M ⟶ N)
  [self : CategoryTheory.IsComonHom f],
  CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkHeaders.checkHeader : Lean.Elab.Command.PreElabHeaderResult → ℕ → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_mk : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M}
  (x : M) (hx : x ∈ p), ↑⟨x, hx⟩ = x
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of a constant and a `C^n` function is `C^n`.  -/
ContDiff.const_smul : ∀ {𝕜 : 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] {n : WithTop ℕ∞}
  {R : Type u_3} [inst_5 : DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {f : E → F} (c : R),
  ContDiff 𝕜 n f → ContDiff 𝕜 n fun y => c • f y
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_erase_attach : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} (f : ι → M) (i : ↥s),
  ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j