mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Given an `A`-module `M`, a term in this type is a presentation by `M` by
generators and relations.  -/
Module.Presentation : (A : Type u) →
  [inst : Ring A] →
    (M : Type v) → [inst_1 : AddCommGroup M] → [Module A M] → Type (max (max (max u v) (w₀ + 1)) (w₁ + 1))
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_X : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  Polynomial.map f Polynomial.X = Polynomial.X
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_eq_iff : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {z : ↥X} (hz : Order.coheight z = 1) {f : ↑X.functionField},
  f ≠ 0 →
    ∀ {n : ℤ},
      AlgebraicGeometry.Scheme.ord f z = n ↔ (AlgebraicGeometry.Scheme.ordHom z hz) f = ↑(Multiplicative.ofAdd n)
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.asiegel_ne_0 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)), a ≠ 0 → NumberField.house.asiegel✝ K a ≠ 0
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rTensor_comp : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {P' : Type uP'} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] [inst_13 : AddCommMonoid P']
  [inst_14 : Module R P'] [inst_15 : Module A P'] [inst_16 : IsScalarTower R A P'] (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P),
  (TensorProduct.AlgebraTensorModule.rTensor R N) (f₂ ∘ₗ f₁) =
    (TensorProduct.AlgebraTensorModule.rTensor R N) f₂ ∘ₗ (TensorProduct.AlgebraTensorModule.rTensor R N) f₁
-- Lean.Setup
Lean.ModuleArtifacts.irParts : Lean.ModuleArtifacts → Array System.FilePath
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_le_iff_le_mul : ∀ {a b : ENNReal}, (b = ⊤ → a ≠ 0) → (a = ⊤ → b ≠ 0) → (a⁻¹ ≤ b ↔ 1 ≤ a * b)
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
/-- [Stacks Tag 01W6](https://stacks.math.columbia.edu/tag/01W6) ((2)) -/
AlgebraicGeometry.IsProper.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.IsProper (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.IsProper f
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.isLocallyNoetherian : ∀ {X : AlgebraicGeometry.Scheme} [h : AlgebraicGeometry.IsLocallyArtinian X], AlgebraicGeometry.IsLocallyNoetherian X
-- Mathlib.Topology.MetricSpace.Holder
/-- A function `f : X → Y` between two `PseudoEMetricSpace`s is Hölder continuous with constant
`C : ℝ≥0` and exponent `r : ℝ≥0` on a set `s : Set X`, if `edist (f x) (f y) ≤ C * edist x y ^ r`
for all `x y ∈ s`.  -/
HolderOnWith : {X : Type u_1} →
  {Y : Type u_2} → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → NNReal → NNReal → (X → Y) → Set X → Prop
-- Mathlib.Analysis.Fourier.Notation
ContinuousFourier.continuous_fourier : ∀ {E : Type u_5} {F : outParam (Type u_6)} {inst : TopologicalSpace E} {inst_1 : TopologicalSpace F}
  {inst_2 : FourierTransform E F} [self : ContinuousFourier E F], Continuous FourierTransform.fourier
-- Mathlib.MeasureTheory.PiSystem
/-- The least Dynkin system containing a collection of basic sets.  -/
MeasurableSpace.DynkinSystem.generate : {α : Type u_3} → Set (Set α) → MeasurableSpace.DynkinSystem α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.eq_empty_iff_forall_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  m = ∅ ↔ ∀ (a : α), a ∉ m
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.maxKey?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxKey? = t₂.maxKey?
-- Mathlib.RingTheory.Artinian.Module
/-- If `M` is an Artinian `R` module, and `S` is an `R`-algebra with a surjective
algebra map, then `M` is an Artinian `S` module.
 -/
isArtinian_of_surjective_algebraMap : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_5}
  [inst_3 : CommSemiring S] [inst_4 : Algebra S R] [inst_5 : Module S M] [IsArtinian R M] [IsScalarTower S R M],
  Function.Surjective ⇑(algebraMap S R) → IsArtinian S M
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point.  -/
ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t (f x₀) →
    ContMDiffWithinAt I I' n f s x₀ →
      (mfderiv[s] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            m + 1 ≤ n →
              f ⁻¹' t ∈ nhdsWithin x₀ s →
                ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) s x₀
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Compositional version of `Finset.measurable_prod` for use by `fun_prop`.  -/
Finset.measurable_prod_apply : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} {β : Type u_5} [inst : CommMonoid M] [inst_1 : MeasurableSpace M]
  [MeasurableMul₂ M] {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : ι → α → β → M} {g : α → β} {s : Finset ι},
  (∀ i ∈ s, Measurable ↿(f i)) → Measurable g → Measurable fun a => (∏ i ∈ s, f i a) (g a)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.unsat_of_verifyBVExpr_eq_true : ∀ (bv : Std.Tactic.BVDecide.BVLogicalExpr) (c : String), Std.Tactic.BVDecide.Reflect.verifyBVExpr bv c = true → bv.Unsat
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.restrict_lt_orderMonoidIso : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible] (γ : ValuativeRel.ValueGroupWithZero R) (x : R),
  v.restrict x < (ValuativeRel.ValueGroupWithZero.orderMonoidIso v) γ ↔ (ValuativeRel.valuation R) x < γ
-- Mathlib.NumberTheory.Modular
/-- The two numbers `c`, `d` in the "bottom row" of `g=[[*,*],[c,d]]` in `SL(2, ℤ)` are coprime.  -/
ModularGroup.bottom_row_coprime : ∀ {R : Type u_1} [inst : CommRing R] (g : Matrix.SpecialLinearGroup (Fin 2) R), IsCoprime (↑g 1 0) (↑g 1 1)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.nonneg_iff_eq_mul_star_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [StarOrderedRing A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A]
  [T2Space A] {a : A}, 0 ≤ a ↔ ∃ b, a = b * star b
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.sum_antidiagonal_swap : ∀ {M : Type u_1} [inst : AddCommMonoid M] {n : ℕ} {f : ℕ × ℕ → M},
  ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p.swap = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.prod_antidiagonal_succ : ∀ {M : Type u_1} [inst : CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M},
  ∏ p ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), f p =
    f (0, n + 1) * ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f (p.1 + 1, p.2)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
_private.Mathlib.Probability.Kernel.IonescuTulcea.Traj.0.cast_pi : ∀ {X : ℕ → Type u_1} {s t : Set ℕ} (h : s = t) (x : (i : ↑s) → X ↑i) (i : ↑t), cast ⋯ x i = x ⟨↑i, ⋯⟩
-- Mathlib.Topology.Sequences
/-- A sequentially compact set in a uniform space is totally bounded.  -/
IsSeqCompact.totallyBounded : ∀ {X : Type u_1} [inst : UniformSpace X] {s : Set X}, IsSeqCompact s → TotallyBounded s
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.eventually_filterAt_subset_of_nhds : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {x : X} {o : Set X}, o ∈ nhds x → ∀ᶠ (t : Set X) in v.filterAt x, t ⊆ o
-- Mathlib.Order.SuccPred.Tree
RootedTree.subtreeOf_mem_subtrees : ∀ {t : RootedTree} [inst : DecidableEq ↑t] {v : ↑t}, v ≠ ⊥ → t.subtreeOf v ∈ t.subtrees
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.inf : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → β}
  [inst : TopologicalSpace β] [inst_1 : Zero β] [inst_2 : SemilatticeInf β] [ContinuousInf β],
  MeasureTheory.FinStronglyMeasurable f μ →
    MeasureTheory.FinStronglyMeasurable g μ → MeasureTheory.FinStronglyMeasurable (f ⊓ g) μ
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDeriv_two_apply : ∀ {𝕜 : Type u} [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)
  (z : E) (m : Fin 2 → E), (iteratedFDeriv 𝕜 2 f z) m = ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)
-- Init.Data.Array.Erase
Array.eraseP_eq_iff : ∀ {α : Type u_1} {ys : Array α} {p : α → Bool} {xs : Array α},
  xs.eraseP p = ys ↔
    (∀ a ∈ xs, ¬p a = true) ∧ xs = ys ∨
      ∃ a as bs, (∀ b ∈ as, ¬p b = true) ∧ p a = true ∧ xs = as.push a ++ bs ∧ ys = as ++ bs
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instAddCommMonoid : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → AddCommMonoid (MeasureTheory.FiniteMeasure Ω)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α},
  Std.ExtDHashMap.Const.get! (m₁ ∩ m₂) k = if k ∈ m₂ then Std.ExtDHashMap.Const.get! m₁ k else default
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t.isEmpty = true → (t.insertIfNew k v).minKey? = some k
-- Mathlib.MeasureTheory.Measure.LevyConvergence
/-- The **Lévy convergence theorem**: the weak convergence of probability measures is equivalent
to the pointwise convergence of their characteristic functions.  -/
MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ₀ : MeasureTheory.ProbabilityMeasure E}
  {μ : ℕ → MeasureTheory.ProbabilityMeasure E},
  Filter.Tendsto μ Filter.atTop (nhds μ₀) ↔
    ∀ (t : E),
      Filter.Tendsto (fun n => MeasureTheory.charFun (↑(μ n)) t) Filter.atTop (nhds (MeasureTheory.charFun (↑μ₀) t))
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAux.h1 : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {N : Type u} [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  {P : Type u} [inst_3 : AddCommGroup P] [inst_4 : Module R P] {g : N →ₗ[R] P},
  Function.Surjective ⇑g →
    ∀ {k : ℕ} (x : AdicCompletion.AdicCauchySequence I N),
      (∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤) → ∀ (n : ℕ), g (↑x (k + n)) ∈ Submodule.map g (I ^ (k + n) • ⊤)
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.instProductivenessRelation : {α α₂ β : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : Std.Iterator α m (Std.IterM m β)] →
        [inst_2 : Std.Iterator α₂ m β] →
          [Std.Iterators.Finite α m] →
            [Std.Iterators.Productive α₂ m] →
              Std.Iterators.ProductivenessRelation (Std.Iterators.Types.Flatten α α₂ β m) m
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast.inj : ∀ {declName unfold refold unfold' refold' declName_1 unfold_1 refold_1 unfold'_1 refold'_1 : Lean.Name},
  Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast declName unfold refold unfold' refold' =
      Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast declName_1 unfold_1 refold_1 unfold'_1 refold'_1 →
    declName = declName_1 ∧ unfold = unfold_1 ∧ refold = refold_1 ∧ unfold' = unfold'_1 ∧ refold' = refold'_1
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_prod_nonempty_of_submultiplicative_on_pred : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] [inst_2 : Preorder β] [IsOrderedMonoid β]
  (f : α → β) (p : α → Prop),
  (∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b) →
    (∀ (a b : α), p a → p b → p (a * b)) →
      ∀ (s : Multiset α), s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (Multiset.map f s).prod
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- The circleMap for a fixed center is continuous as a function on `ℝ × ℝ`.
 -/
Real.circleMap.continuous : ∀ {c : ℂ}, Continuous fun x => circleMap c x.1 x.2
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The counit axiom associated to a coalgebra.  -/
CategoryTheory.Comonad.Coalgebra.counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra),
  CategoryTheory.CategoryStruct.comp self.a (G.ε.app self.A) = CategoryTheory.CategoryStruct.id self.A
-- Mathlib.Algebra.Group.Basic
div_eq_iff_eq_mul' : ∀ {G : Type u_3} [inst : CommGroup G] {a b c : G}, a / b = c ↔ a = b * c
-- Mathlib.Data.PNat.Prime
PNat.Prime.ne_one : ∀ {p : ℕ+}, p.Prime → p ≠ 1
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanClientCapabilities.mk.sizeOf_spec : ∀ (incrementalDiagnosticSupport? silentDiagnosticSupport? : Option Bool)
  (rpcWireFormat? : Option Lean.Lsp.RpcWireFormat),
  sizeOf
      { incrementalDiagnosticSupport? := incrementalDiagnosticSupport?,
        silentDiagnosticSupport? := silentDiagnosticSupport?, rpcWireFormat? := rpcWireFormat? } =
    1 + sizeOf incrementalDiagnosticSupport? + sizeOf silentDiagnosticSupport? + sizeOf rpcWireFormat?
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.tensorHom_neg_neg_add_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.AddGrpObj A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (β_ A A).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h))
-- Lean.Server.References
/-- Converts a list of LSP module imports to the module imports of the references data structure.
Removes all imports for which we cannot resolve the corresponding `DocumentUri`.
 -/
Lean.Server.DirectImports.convertImportInfos : Array Lean.Lsp.ImportInfo → IO Lean.Server.DirectImports
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.notMem_bot : ∀ (x : ℕ × ℕ), x ∉ ⊥
-- Mathlib.RingTheory.Ideal.Prod
Ideal.map_snd_prod : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal R) (J : Ideal S),
  Ideal.map (RingHom.snd R S) (I.prod J) = J
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The homotopy between `π K ≫ ι₀ K` and `𝟙 K.cylinder`.  -/
HomologicalComplex.cylinder.πCompι₀Homotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] →
                  (∀ (j : ι), ∃ i, c.Rel i j) →
                    Homotopy
                      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K)
                        (HomologicalComplex.cylinder.ι₀ K))
                      (CategoryTheory.CategoryStruct.id K.cylinder)
-- Mathlib.MeasureTheory.Function.UnifTight
/-- A finite sequence of Lp functions is uniformly tight.  -/
MeasureTheory.unifTight_finite : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} [Finite ι],
  p ≠ ⊤ → ∀ {f : ι → α → β}, (∀ (i : ι), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UnifTight f p μ
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
/-- If `A` is a left `B`-localizing triangulated subcategory in the sense of Verdier,
then the induced functor between the localizations with respect to `(B.inverseImage A.ι).trW`
and `B.trW` is fully faithful.  -/
CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fullyFaithful : {C : Type u_1} →
  {D₁ : Type u_3} →
    {D₂ : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} D₁] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂] →
            (A B : CategoryTheory.ObjectProperty C) →
              [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
                [inst_4 : CategoryTheory.HasShift C ℤ] →
                  [inst_5 : CategoryTheory.Preadditive C] →
                    [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                      [inst_7 : CategoryTheory.Pretriangulated C] →
                        [CategoryTheory.IsTriangulated C] →
                          [inst_9 : A.IsTriangulated] →
                            [B.IsTriangulated] →
                              [B.IsClosedUnderIsomorphisms] →
                                [A.IsVerdierLeftLocalizing B] →
                                  {L₁ : CategoryTheory.Functor A.FullSubcategory D₁} →
                                    {L₂ : CategoryTheory.Functor C D₂} →
                                      {F : CategoryTheory.Functor D₁ D₂} →
                                        [L₁.IsLocalization (B.inverseImage A.ι).trW] →
                                          [L₂.IsLocalization B.trW] → (L₁.comp F ≅ A.ι.comp L₂) → F.FullyFaithful
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- A set is linear if it is a coset of a finitely generated additive submonoid.  -/
IsLinearSet : {M : Type u_1} → [AddCommMonoid M] → Set M → Prop
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
/-- A left Kan extension `t` of the identity along `f` that commutes with `f`, in the sense that
`t.whisker f` is a left Kan extension, is a right adjoint to `f`. The unit of this adjoint is
given by the unit of the Kan extension.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan.adjunction : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.id a)} →
          t.IsKan → (t.whisker f).IsKan → CategoryTheory.Bicategory.Adjunction f t.extension
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (X : Cᵒᵖ),
  (CategoryTheory.CategoryStruct.id M).app X = CategoryTheory.CategoryStruct.id (M.obj X)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.Nondegenerate.congr : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {B : LinearMap.BilinForm R M} (e : M ≃ₗ[R] M'),
  B.Nondegenerate → ((LinearMap.BilinForm.congr e) B).Nondegenerate
-- Lean.Server.Requests
Lean.Server.RequestHandlerCompleteness.complete.sizeOf_spec : sizeOf Lean.Server.RequestHandlerCompleteness.complete = 1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_unitIso_hom_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁),
  ((CategoryTheory.Comma.mapRightIso L i).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.Analytic.Linear
/-- `fst` is entire  -/
analyticOnNhd_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {t : Set (E × F)}, AnalyticOnNhd 𝕜 (fun p => p.1) t
-- Mathlib.Order.Ideal
Order.Ideal.exists_maximal : ∀ {P : Type u_1} [inst : PartialOrder P] [OrderTop P] [Nontrivial P], ∃ I, I.IsMaximal
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- The left part of the Dyck word decomposition,
inside the `U, D` pair that `firstReturn` refers to. `insidePart 0 = 0`.  -/
DyckWord.insidePart : DyckWord → DyckWord
-- Init.Notation
/-- `a >> b` executes `a`, ignores the result, and then executes `b`.
If `a` fails then `b` is not executed. Because `b` is not always executed, it
is passed as a thunk so it can be forced only when needed.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `>>` in identifiers is `andThen`. -/
«term_>>_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X},
  CategoryTheory.Limits.pullbackConeEquivBinaryFan.unitIso = CategoryTheory.NatIso.ofComponents (fun c => c.eta) ⋯
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierInvCLM_apply : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransformInv E F] [inst_6 : FourierInvAdd E F]
  [inst_7 : FourierInvSMul R E F] [inst_8 : TopologicalSpace E] [inst_9 : TopologicalSpace F]
  [inst_10 : ContinuousFourierInv E F] (f : E),
  (FourierTransform.fourierInvCLM R E) f = FourierTransformInv.fourierInv f
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.functor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] (X : Cᵒᵖ),
  (CategoryTheory.Subobject.functor C).obj X = CategoryTheory.Subobject (Opposite.unop X)
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.PatternMatchState : Type
-- Mathlib.NumberTheory.SmoothNumbers
/-- The cardinality of the set of `k`-rough numbers `≤ N` is bounded by the sum of `⌊N/p⌋`
over the primes `k ≤ p ≤ N`.  -/
Nat.roughNumbersUpTo_card_le : ∀ (N k : ℕ), (N.roughNumbersUpTo k).card ≤ ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p