mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `‖r₁‖ < r₂`, then for any natural `k` we have `n ^ k r₁ ^ n = o (r₂ ^ n)` as `n → ∞`.  -/
isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt : ∀ {R : Type u_2} [inst : NormedRing R] (k : ℕ) {r₁ : R} {r₂ : ℝ},
  ‖r₁‖ < r₂ → (fun n => ↑n ^ k * r₁ ^ n) =o[Filter.atTop] fun n => r₂ ^ n
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.invRotate_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C),
  T.invRotate.obj₁ = (CategoryTheory.shiftFunctor C (-1)).obj T.obj₃
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLEMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ A₃ : C} (f : A₁ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g] (h : A₃ ⟶ B)
  [inst_3 : CategoryTheory.Mono h] (h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
  (h₂ : CategoryTheory.Subobject.mk g ≤ CategoryTheory.Subobject.mk h),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₁)
      (CategoryTheory.Subobject.ofMkLEMk g h h₂) =
    CategoryTheory.Subobject.ofMkLEMk f h ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.lift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) (CategoryTheory.Limits.prod.map h k) =
    CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)
-- Mathlib.Algebra.Order.Module.Defs
neg_of_smul_neg_right' : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : LinearOrder α] [inst_4 : LinearOrder β] [PosSMulMono α β], a • b < 0 → 0 ≤ b → a < 0
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_hom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (j : J) {Z : C}
  (h : CategoryTheory.Limits.colimit G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).hom h) =
    CategoryTheory.CategoryStruct.comp (F.map (e.unit.app j))
      (CategoryTheory.CategoryStruct.comp (w.inv.app (e.inverse.obj (e.functor.obj j)))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimit.ι G (e.functor.obj (e.inverse.obj (e.functor.obj j)))) h))
-- Mathlib.Analysis.RCLike.Basic
RCLike.conjCLE_apply : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.conjCLE = ⇑(starRingEnd K)
-- Mathlib.Order.Compare
cmp_ofDual : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] (x y : αᵒᵈ),
  cmp (OrderDual.ofDual x) (OrderDual.ofDual y) = cmp y x
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f]
  [AlgebraicGeometry.IsLocallyNoetherian Y], AlgebraicGeometry.IsLocallyNoetherian X
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_def : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ‖f‖ = (MeasureTheory.eLpNorm (↑↑f) p μ).toReal
-- Mathlib.Data.ZMod.Basic
/-- The identity between `ZMod m` and `ZMod n` when `m = n`, as a ring isomorphism.  -/
ZMod.ringEquivCongr : {m n : ℕ} → m = n → ZMod m ≃+* ZMod n
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toPSet.eq_1 : ∀ (o : Ordinal.{u}), o.toPSet = PSet.mk o.ToType fun a => (↑a.toOrd).toPSet
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.domRestrict_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : ↥p), (f.domRestrict p) x = f ↑x
-- Init.Sym.DSimp.DSimprocDSL
/-- Evaluate ground (fully concrete) terms.  -/
Lean.Parser.Sym.DSimp.ground : Lean.ParserDescr
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X_1 : C₁) (X_2 : C₂)
  (X_3 : C₃),
  ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X_1).obj X_2).obj X_3 =
    ((X.obj (F₁.obj X_1)).obj (F₂.obj X_2)).obj (F₃.obj X_3)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_equiv : ∀ {α β : Type u} (f : α ≃ β) (s : Set β), Cardinal.mk ↑(⇑f ⁻¹' s) = Cardinal.mk ↑s
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q.Monic → (p * q).Monic
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The full and essentially surjective functor
`CochainComplex.Plus C ⥤ HomotopyCategory.Plus C`.  -/
HomotopyCategory.Plus.quotient : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.Functor (CochainComplex.Plus C) (HomotopyCategory.Plus C)
-- Mathlib.Data.Nat.Nth
/-- **Alias** of `Nat.surjective_count_of_infinite_setOfPred`. -/
Nat.surjective_count_of_infinite_setOf : ∀ {p : ℕ → Prop} [inst : DecidablePred p], {n | p n}.Infinite → Function.Surjective (Nat.count p)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[1] ⟶ Λ[2, 2]` which avoids `1`.  -/
SSet.horn₂₂.ι₀₂ : SSet.stdSimplex.obj { len := 1 } ⟶ (SSet.horn 2 2).toSSet
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator.instMkXorCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkXorCached
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.min : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α},
  IsLocalMax f a → IsLocalMax g a → IsLocalMax (fun x => min (f x) (g x)) a
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The Hecke ring `𝕋 Δ H Z` with coefficients in `Z`: the diagonal Hecke coset module
`HeckeCosetModule Δ H H Z`, the finitely-supported `Z`-linear combinations of double cosets
`H\Δ/H`. The convolution product making it a ring is developed in later files.  -/
HeckeRing : {G : Type u_1} → [inst : Group G] → Submonoid G → Subgroup G → (Z : Type u_2) → [Zero Z] → Type (max u_2 u_1)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.tr.match_1.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2to1.Λ' K Γ Λ σ → Sort u_5)
  (q : Turing.TM2.Stmt Γ Λ σ) (h_1 : (q : Λ) → motive (Turing.TM2to1.Λ'.normal q))
  (h_2 : (k : K) → (s : Turing.TM2to1.StAct K Γ σ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2to1.Λ'.go k s q))
  (h_3 : (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2to1.Λ'.ret q)),
  (match Turing.TM2to1.Λ'.ret q with
    | Turing.TM2to1.Λ'.normal q => h_1 q
    | Turing.TM2to1.Λ'.go k s q => h_2 k s q
    | Turing.TM2to1.Λ'.ret q => h_3 q) =
    h_3 q
-- Std.Data.Iterators.Lemmas.Consumers.Set
Std.IterM.toExtTreeSet.congr_simp : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  (it it_1 : Std.IterM m β),
  it = it_1 → ∀ (cmp : β → β → Ordering) [inst_3 : Std.TransCmp cmp], it.toExtTreeSet cmp = it_1.toExtTreeSet cmp
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.coe_one : ∀ {A : Type u_1} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A], ⇑1 = id
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (x : p + n = q),
  CochainComplex.HomComplex.Cochain.fromSingleMk f x =
    CochainComplex.HomComplex.Cochain.single
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom f) n
-- Mathlib.Order.Basic
Pi.himp_def : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → HImp (π i)] (x y : (i : ι) → π i), y ⇨ x = fun i => y i ⇨ x i
-- Aesop.Stats.Basic
Aesop.ForwardRuleStateStats.mk.inj : ∀ {ruleName : Aesop.RuleName} {clusterStateStats : Array Aesop.ForwardClusterStateStats} {ruleName_1 : Aesop.RuleName}
  {clusterStateStats_1 : Array Aesop.ForwardClusterStateStats},
  { ruleName := ruleName, clusterStateStats := clusterStateStats } =
      { ruleName := ruleName_1, clusterStateStats := clusterStateStats_1 } →
    ruleName = ruleName_1 ∧ clusterStateStats = clusterStateStats_1
-- Lean.Meta.Sym.SymM
/-- A registered extension for `SymM`. Each extension gets a unique index into the
extensions array in `Sym.State`. Can only be created via `registerSymExtension`.
 -/
Lean.Meta.Sym.SymExtension : Type → Type
-- Init.Data.Vector.Zip
_private.Init.Data.Vector.Zip.0.Vector.getElem?_zipWith.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a : α) (b : β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_1 : Option β) → motive x x_1),
  (match some a, some b with
    | some a, some b => h_1 a b
    | x, x_1 => h_2 x x_1) =
    h_1 a b
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
isTranscendenceBasis_equiv : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (e : ι ≃ ι') {f : ι' → A}, IsTranscendenceBasis R (f ∘ ⇑e) ↔ IsTranscendenceBasis R f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.add : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Data.Finset.Slice
/-- Everything in the `r`-th slice of `𝒜` has size `r`.  -/
Finset.sized_slice : ∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {r : ℕ}, Set.Sized r ↑(𝒜.slice r)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- A category `HasWidePullbacks` if it has all limits of shape `WidePullbackShape J`, i.e. if it
has a wide pullback for every collection of morphisms with the same codomain.  -/
CategoryTheory.Limits.HasWidePullbacks : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Topology.Algebra.Monoid
tendsto_finsetProd : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : CommMonoid M] [ContinuousMul M]
  {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι),
  (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => ∏ c ∈ s, f c b) x (nhds (∏ c ∈ s, a c))
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_eq_of_inf_eq : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B C : IntermediateField F E},
  A ⊓ C = B ⊓ C → A.relfinrank C = B.relfinrank C
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_obj_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] (U : N),
  ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor p).obj U).snd =
    CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk (CategoryTheory.CategoryStruct.id (p.obj U))
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
lTensor.inverse_of_rightInverse_comp_lTensor : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) {h : P → N} (hgh : Function.RightInverse h ⇑g),
  lTensor.inverse_of_rightInverse Q hfg hgh ∘ₗ LinearMap.lTensor Q g = (LinearMap.lTensor Q f).range.mkQ
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V W : (↑U).Opens}
  (e : (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V = (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj W),
  X.presheaf.map (CategoryTheory.eqToHom e).op = (↑U).presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.self_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Limits.LimitPresentation.self X).π =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.const PUnit.{s + 1}).obj X)
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.toMultiplicativeLeft_symm_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] (f : Multiplicative α →* β) (a : α),
  (AddMonoidHom.toMultiplicativeLeft.symm f) a = Additive.ofMul (f (Multiplicative.ofAdd a))
-- Mathlib.CategoryTheory.Products.Associator
/-- The equivalence of categories expressing associativity of products of categories.
 -/
CategoryTheory.prod.associativity : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) → [inst_2 : CategoryTheory.Category.{v₃, u₃} E] → (C × D) × E ≌ C × D × E
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] {f g : BoundedLatticeHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The lineality space of a cone is a face.  -/
PointedCone.IsFaceOf.lineal : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (C : PointedCone R M), (↑C.lineal).IsFaceOf C
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, (m.insert k).contains a = (k == a || m.contains a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl k =
    (Std.DTreeMap.Internal.Impl.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x
-- Mathlib.Topology.Order.SuccPred
AccPt.isSuccLimit : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α]
  {a : α} {s : Set α}, AccPt a (Filter.principal s) → Order.IsSuccLimit a
-- Mathlib.Data.Set.Basic
Set.compl_ssubset_univ : ∀ {α : Type u} {s : Set α}, sᶜ ⊂ Set.univ ↔ s.Nonempty
-- Mathlib.Order.LiminfLimsup
/-- If `x ≤ Filter.liminf u atTop`, then for all `ε < 0`, eventually we have `x + ε < u b`.  -/
Filter.eventually_add_neg_lt_of_le_liminf : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : Preorder β]
  [inst_2 : AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α},
  Filter.IsBoundedUnder GE.ge Filter.atTop u →
    x ≤ Filter.liminf u Filter.atTop → ε < 0 → ∀ᶠ (b : β) in Filter.atTop, x + ε < u b
-- Lean.Data.Lsp.Internal
Lean.Lsp.instEmptyCollectionDecls : EmptyCollection Lean.Lsp.Decls
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.isPeriodicPt_iff_minimalPeriod_dvd : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x ↔ Function.minimalPeriod f x ∣ n
-- Init.Data.UInt.Lemmas
UInt32.zero_sub : ∀ (a : UInt32), 0 - a = -a
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If G preserves initial objects and pushouts, it preserves all finite colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_of_preservesInitial_and_pushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G],
  CategoryTheory.Limits.PreservesFiniteColimits G
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Example: the **full shift** on alphabet `A` over the additive monoid `G`.

It is the subshift whose underlying set is the set of all configurations
`G → A`.
 -/
SymbolicDynamics.FullShift.fullShift : (A : Type u_1) →
  (G : Type u_2) → [inst : TopologicalSpace A] → [inst_1 : AddMonoid G] → SymbolicDynamics.FullShift.Subshift A G
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- If the quotient by an ideal is a field, then the ideal is maximal.  -/
Ideal.Quotient.maximal_of_isField : ∀ {R : Type u_5} [inst : CommRing R] (I : Ideal R), IsField (R ⧸ I) → I.IsMaximal
-- Batteries.Data.List.Lemmas
List.idxOfNth_countBefore_getElem : ∀ {α : Type u_1} {i : ℕ} [inst : BEq α] [ReflBEq α] {xs : List α} {h : i < xs.length},
  List.idxOfNth xs[i] xs (List.countBefore xs[i] xs i) = i
-- Mathlib.Order.Antichain
/-- If `t` is an antichain shadowed by and including the set of minimal elements of `s`,
then `t` *is* the set of minimal elements of `s`.  -/
IsAntichain.eq_setOfPred_minimal : ∀ {α : Type u_1} {s t : Set α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) t →
    (∀ (x : α), Minimal (fun x => x ∈ s) x → x ∈ t) →
      (∀ a ∈ t, ∃ b, a ≤ b ∧ Minimal (fun x => x ∈ s) b) → {x | Minimal (fun x => x ∈ s) x} = t
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.instIsIsoCokernelComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.cokernelComparison f G)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
IsTranscendenceBasis.of_comp : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'] {x : ι → A} (f : A →ₐ[R] A'),
  Function.Injective ⇑f → IsTranscendenceBasis R (⇑f ∘ x) → IsTranscendenceBasis R x
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.atIdxSlow?_intermediateZip : ∀ {α₁ α₂ β₁ β₂ : Type w} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂]
  [Std.Iterators.Productive α₁ Id] [Std.Iterators.Productive α₂ Id] {it₁ : Std.Iter β₁}
  {memo : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out }} {it₂ : Std.Iter β₂} {n : ℕ},
  Std.Iter.atIdxSlow? n (Std.Iter.Intermediate.zip it₁ memo it₂) =
    match memo with
    | none => do
      let __do_lift ← Std.Iter.atIdxSlow? n it₁
      let __do_lift_1 ← Std.Iter.atIdxSlow? n it₂
      pure (__do_lift, __do_lift_1)
    | some memo =>
      match n with
      | 0 => do
        let __do_lift ← Std.Iter.atIdxSlow? n it₂
        pure (↑memo, __do_lift)
      | n'.succ => do
        let __do_lift ← Std.Iter.atIdxSlow? n' it₁
        let __do_lift_1 ← Std.Iter.atIdxSlow? (n' + 1) it₂
        pure (__do_lift, __do_lift_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_unitOfList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h' : k' ∈ Std.HashMap.Raw.unitOfList l}, (Std.HashMap.Raw.unitOfList l).getKey k' h' = k
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.instEDistOfFiniteElemSet : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [PseudoEMetricSpace β] → [Finite ↑𝔖] → EDist (UniformOnFun α β 𝔖)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.coe_chartAt_symm_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (p : H × E)
  (q : TangentBundle I M), (↑(chartAt (ModelProd H E) q).symm p).proj = ↑(chartAt H q.proj).symm p.1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.finite : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} [M.RankFinite], M.Indep I → I.Finite
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.compl_lattice_sdiff_singleton_mem_nhds : ∀ (L : PeriodPair) (x : ℂ), (↑L.lattice \ {x})ᶜ ∈ nhds x
-- Mathlib.Topology.Category.LightProfinite.Sequence
/-- The continuous map from `ℕ∪{∞}` to `ℝ` sending `n` to `1/(n+1)` and `∞` to `0` is a closed
embedding.
 -/
LightProfinite.isClosedEmbedding_natUnionInftyEmbedding : Topology.IsClosedEmbedding ⇑LightProfinite.natUnionInftyEmbedding
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  {F : CategoryTheory.Functor C V}
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] {G : CategoryTheory.Functor C V}
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution U G] (f : F ⟶ G) {Z : CategoryTheory.Functor C V}
  (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id U) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U G).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F).hom
      (CategoryTheory.CategoryStruct.comp f h)