mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_hom_comp_biproduct_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom
      (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.algebraMap_eq_inl : ∀ (R' : Type u) (M : Type v) [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M], ⇑(algebraMap R' (TrivSqZeroExt R' M)) = TrivSqZeroExt.inl
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along row `i`.  -/
Matrix.det_succ_row : ∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ),
  A.det = ∑ j, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.coe_inv : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)), ↑x⁻¹ = (↑x)⁻¹
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrable_of_intervalIntegral_norm_bounded : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] {a b : ι → ℝ} {f : ℝ → E} (I : ℝ),
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ) →
    Filter.Tendsto a l Filter.atBot →
      Filter.Tendsto b l Filter.atTop →
        (∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I) → MeasureTheory.Integrable f μ
-- Lean.Elab.ConfigEval.DeriveEvalTerm
_private.Lean.Elab.ConfigEval.DeriveEvalTerm.0.Lean.Elab.ConfigEval.ensureEvalTerm.getIndType : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.InductiveVal
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_le_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X)
  (S : CategoryTheory.Sieve X), CategoryTheory.Sieve.generate R ≤ S ↔ R ≤ S.arrows
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesComp : ∀ {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] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesEffectiveEpiFamilies]
  [G.PreservesEffectiveEpiFamilies], (F.comp G).PreservesEffectiveEpiFamilies
-- Mathlib.Algebra.Homology.TotalComplex
/-- The isomorphism `K.total c₁₂ ≅ L.total c₁₂` of homological complexes induced
by an isomorphism of bicomplexes `K ≅ L`.  -/
HomologicalComplex₂.total.mapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                {K L : HomologicalComplex₂ C c₁ c₂} →
                  (K ≅ L) →
                    (c₁₂ : ComplexShape I₁₂) →
                      [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                        [inst_3 : DecidableEq I₁₂] →
                          [inst_4 : K.HasTotal c₁₂] → [inst_5 : L.HasTotal c₁₂] → K.total c₁₂ ≅ L.total c₁₂
-- Mathlib.Data.List.Basic
List.choose_spec : ∀ {α : Type u} (p : α → Prop) [inst : DecidablePred p] (l : List α) (hp : ∃ a ∈ l, p a),
  List.choose p l hp ∈ l ∧ p (List.choose p l hp)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.isUnit_of_dvd : ∀ {R : Type u} [inst : CommSemiring R] {x y : R}, IsCoprime x y → x ∣ y → IsUnit x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_le_neg_pi_div_two : ∀ {x : ℝ}, Real.arcsin x ≤ -(Real.pi / 2) ↔ x ≤ -1
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.symm_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} (h : P.RightHomotopy f g), h.symm.h = h.h
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.Augmented.δ₀Iter_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (Y : CategoryTheory.SimplicialObject.Augmented C)
  {n m : ℕ} (i : ℕ) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.Augmented.δ₀Iter_hom_app._auto_1),
  CategoryTheory.CategoryStruct.comp (Y.left.δ₀Iter i hi) (Y.hom.app (Opposite.op { len := n })) =
    Y.hom.app (Opposite.op { len := m })
-- Mathlib.SetTheory.Ordinal.Principal
/-- An ordinal `o` is said to be principal (or indecomposable) under an operation when `Iio o` is
closed under that operation.

For simplicity, we break usual convention and regard `0` as principal.  -/
Ordinal.IsPrincipal : (Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) → Ordinal.{u_1} → Prop
-- Mathlib.Topology.Connected.TotallyDisconnected
totallySeparatedSpace_iff : ∀ (α : Type u) [inst : TopologicalSpace α], TotallySeparatedSpace α ↔ IsTotallySeparated Set.univ
-- Mathlib.Algebra.Module.PUnit
PUnit.vadd : {R : Type u_1} → VAdd R PUnit.{u_3 + 1}
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.comp_right : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : Ring K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] [IsNoetherianRing K] {v : V₂ →ₗ[K] V₃},
  v.HasFiniteRange → ∀ (u : V →ₗ[K] V₂), (v ∘ₗ u).HasFiniteRange
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.ofTensorProductInvOfPiFintype_comp_ofTensorProduct : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (ι : Type u_4) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  ↑(AdicCompletion.ofTensorProductInvOfPiFintype I ι) ∘ₗ AdicCompletion.ofTensorProduct I (ι → R) = LinearMap.id
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.sectionsEquivHom_naturality_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C (Type u₂)} (f : F ⟶ G)
  (X : Type u₂) [inst_1 : Unique X] (τ : (CategoryTheory.Functor.const C).obj X ⟶ F),
  (G.sectionsEquivHom X).symm (CategoryTheory.CategoryStruct.comp τ f) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor C).map f))
      ((F.sectionsEquivHom X).symm τ)
-- Aesop.Forward.RuleInfo
Aesop.instInhabitedSlot.default : Aesop.Slot
-- Init.Data.Int.Lemmas
Int.eq_of_sub_eq_zero : ∀ {a b : ℤ}, a - b = 0 → a = b
-- Lean.Meta.Tactic.Simp.Arith.Util
_private.Lean.Meta.Tactic.Simp.Arith.Util.0.Lean.Meta.Simp.Arith.isSupportedCommRingType : Lean.Expr → Bool
-- Init.Data.String.Basic
String.singleton_eq : ∀ {c : Char}, String.singleton c = String.ofList [c]
-- Init.Data.SInt.Lemmas
ISize.toInt_le_int64MaxValue : ∀ (x : ISize), x.toInt ≤ Int64.maxValue.toInt
-- Batteries.Tactic.HelpCmd
_private.Batteries.Tactic.HelpCmd.0.Batteries.Tactic.elabHelpCats : Option Lean.Ident → Lean.Elab.Command.CommandElabM Unit
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go_eq.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_mk_shrink' : ∀ (α : Type u) [inst : Small.{v, u} α],
  Cardinal.lift.{u, v} (Cardinal.mk (Shrink.{v, u} α)) = Cardinal.lift.{v, u} (Cardinal.mk α)
-- Mathlib.CategoryTheory.Sites.EpiMono
CategoryTheory.Sheaf.instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [inst_4 : J.WEqualsLocallyBijective A]
  (data : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A)
  [inst_5 : CategoryTheory.HasWeakSheafify J A] (f : CategoryTheory.Arrow (CategoryTheory.Sheaf J A))
  [J.HasSheafCompose (CategoryTheory.forget A)],
  CategoryTheory.Mono ((CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization J data).p.app f)
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.ιSigmaStdSimplex_jointly_surjective : ∀ {X Y : SSet} {i : X ⟶ Y} {d n : ℕ}
  (a : (SSet.relativeCellComplexOfMono.sigmaStdSimplex i d).obj (Opposite.op { len := n })),
  ∃ c x, (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := n }))) x = a
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.functorH_obj_coe : ∀ {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)] (n : ℕ)
  (F : CategoryTheory.Sheaf J AddCommGrpCat), ↑((CategoryTheory.Sheaf.functorH J n).obj F) = F.H n
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ioo_of_strictAntiOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → ContinuousOn f (Set.Icc a b) → StrictAntiOn f (Set.Icc a b) → f '' Set.Ioo a b = Set.Ioo (f b) (f a)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.leftOp_left_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ)
  (X_1 : SimplexCategoryᵒᵖ), X.leftOp.left.obj X_1 = Opposite.unop (X.right.obj (Opposite.unop X_1))
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instIsVerdierLeftLocalizingOppositeOpOfIsVerdierRightLocalizing : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C)
  [A.IsVerdierRightLocalizing B], A.op.IsVerdierLeftLocalizing B.op
-- Mathlib.Algebra.Star.Basic
MulOpposite.instInvolutiveStar : {R : Type u} → [InvolutiveStar R] → InvolutiveStar Rᵐᵒᵖ
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceReferenceParams : Lean.Lsp.FileSource Lean.Lsp.ReferenceParams
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The Lie bracket of two vectors `v` and `w` in the Lie algebra of a Lie group is obtained by
taking the Lie bracket of the associated invariant vector fields, at the identity.  -/
instBracketGroupLieAlgebra : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Group G] → Bracket (GroupLieAlgebra I G) (GroupLieAlgebra I G)
-- Init.Data.List.Attach
List.length_attach : ∀ {α : Type u_1} {l : List α}, l.attach.length = l.length
-- Mathlib.Combinatorics.SimpleGraph.Cayley
/-- The Cayley graph induced by an operation `[Mul M]` with generators `s`  -/
SimpleGraph.mulCayley : {M : Type u_1} → Set M → [Mul M] → SimpleGraph M
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_update : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ) (a : R),
  (p.update n a).coeff = Function.update p.coeff n a
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.leftCosetEquivSubgroup.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} (g : α),
  Subgroup.leftCosetEquivSubgroup g =
    { toFun := fun x => ⟨g⁻¹ * ↑x, ⋯⟩, invFun := fun x => ⟨g * ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.InformationTheory.Hamming
Hamming.instAddMonoid : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → AddMonoid (β i)] → AddMonoid (Hamming β)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- If a function `g` is a left and right inverse of a linear map `f`, then `g` is linear itself.  -/
LinearMap.inverse : {R : Type u_1} →
  {S : Type u_5} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module S M₂] →
                    {σ : R →+* S} →
                      {σ' : S →+* R} →
                        [RingHomInvPair σ σ'] →
                          (f : M →ₛₗ[σ] M₂) →
                            (g : M₂ → M) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → M₂ →ₛₗ[σ'] M
-- Std.Data.ExtDHashMap.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulBEq` is available.  -/
Std.ExtDHashMap.Const.getD_filterMap' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : LawfulBEq α] {f : α → β → Option γ} {k : α} {fallback : γ},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.filterMap f m) k fallback =
    ((Std.ExtDHashMap.Const.get? m k).bind (f k)).getD fallback
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.disjUnion_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₂ : BoxIntegral.Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion),
  (π₁.disjUnion π₂ h).boxes = π₁.boxes ∪ π₂.boxes
-- Mathlib.Order.Max
IsBot.lt_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsBot a → a ≠ b → a < b
-- Lean.Elab.DeclModifiers
Lean.Elab.instBEqComputeKind.beq : Lean.Elab.ComputeKind → Lean.Elab.ComputeKind → Bool
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral.congr_simp : ∀ {α : Type u_5} {E : Type u_6} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (a a_1 : ↥(MeasureTheory.Lp E 1 μ)),
  a = a_1 → MeasureTheory.L1.integral a = MeasureTheory.L1.integral a_1
-- Mathlib.Algebra.Group.Action.Defs
SMul.comp.smul.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : SMul M α] (g : N → M) (n : N) (a : α),
  SMul.comp.smul g n a = g n • a
-- Init.Data.SInt.Bitwise
ISize.neg_one_xor : ∀ {a : ISize}, -1 ^^^ a = ~~~a
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.instMonoidWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → MonoidWithZero ↑(Set.Icc 0 1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {outWidth w len : ℕ}
  {oldLayer : aig.RefVec (len * w)} {h : outWidth = (len + 1) / 2 * w} {hlen : 0 < len} {w_1 len_1 : ℕ}
  {oldLayer_1 : aig.RefVec (len_1 * w_1)} {h_1 : outWidth = (len_1 + 1) / 2 * w_1} {hlen_1 : 0 < len_1},
  { w := w, len := len, oldLayer := oldLayer, h := h, hlen := hlen } =
      { w := w_1, len := len_1, oldLayer := oldLayer_1, h := h_1, hlen := hlen_1 } →
    w = w_1 ∧ len = len_1 ∧ oldLayer ≍ oldLayer_1
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
contMDiffOn_iff_contDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {s : Set E},
  ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s ↔ ContDiffOn 𝕜 n f s
-- Mathlib.Algebra.BigOperators.Finsupp.Fin
finTwoArrowEquiv'_sum_eq : ∀ {M : Type u_1} {d : M × M} [inst : AddCommMonoid M], (((finTwoArrowEquiv' M).symm d).sum fun x n => n) = d.1 + d.2
-- Mathlib.Topology.Order.LeftRightNhds
/-- **Alias** of `countable_setOfPred_isolated_left`.

---

The set of points which are isolated on the left is countable when the space is
second-countable.  -/
countable_setOf_isolated_left : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | nhdsWithin x (Set.Iio x) = ⊥}.Countable
-- Mathlib.GroupTheory.OrderOfElement
orderOf.eq_1 : ∀ {G : Type u_1} [inst : Monoid G] (x : G), orderOf x = Function.minimalPeriod (fun x_1 => x * x_1) 1
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.uniqueFromInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasInitial C] → (P : C) → Unique (⊥_ C ⟶ P)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `∏' i, f i` is the unconditional product of `f`, if it exists, or 1 otherwise.

More generally, if `L` is a `SummationFilter`, `∏'[L] i, f i` is the product of `f` with respect to
`L` if it exists, and `1` otherwise.

(Note that even if the unconditional product exists, it might not be unique if the topology is not
separated. When the multiplicative support of `f` is finite, we make the most reasonable choice,
to use the product over the multiplicative support. Otherwise, we choose arbitrarily an `a`
satisfying `HasProd f a`. Similar remarks apply to more general summation filters.)  -/
tprod : {α : Type u_4} →
  {β : Type u_5} →
    [CommMonoid α] → [TopologicalSpace α] → (β → α) → optParam (SummationFilter β) (SummationFilter.unconditional β) → α
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.nfp_le_of_isPrincipal : ∀ {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  a < o → Ordinal.IsPrincipal op o → Ordinal.nfp (op a) a ≤ o
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.diagonal_vec1 : ∀ {α : Type u} [inst : Zero α] (a : α), Matrix.diagonal ![a] = !![a]
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_smul : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) [inst_4 : SMul R' R] [inst_5 : SMul R' A]
  [inst_6 : IsScalarTower R' R A] (r : R') (x : ↥S), ↑(r • x) = r • ↑x
-- Mathlib.RingTheory.NoetherNormalization
/-- There exists some `s ≤ n` and an integral injective algebra homomorphism
from `k[X_0,...,X_(s-1)]` to `k[X_0,...,X_(n-1)]/I` if `I ≠ ⊤`.  -/
exists_integral_inj_algHom_of_quotient : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) k)),
  I ≠ ⊤ → ∃ s ≤ n, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.getD (Std.DTreeMap.filterMap f t) k fallback =
      ((Std.DTreeMap.Const.get? t k).bind (f k')).getD fallback
-- Mathlib.Data.Nat.Init
Nat.decidableLoHi : (lo hi : ℕ) → (P : ℕ → Prop) → [DecidablePred P] → Decidable (∀ (x : ℕ), lo ≤ x → x < hi → P x)
-- Mathlib.Order.Preorder.Chain
Flag.mk : {α : Type u_4} →
  [inst : LE α] →
    (carrier : Set α) →
      IsChain (fun x1 x2 => x1 ≤ x2) carrier →
        (∀ ⦃s : Set α⦄, IsChain (fun x1 x2 => x1 ≤ x2) s → carrier ⊆ s → carrier = s) → Flag α
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.topologicalSpace_mono : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] {𝔖₁ 𝔖₂ : Set (Set E)} [inst_7 : TopologicalSpace F]
  [inst_8 : IsTopologicalAddGroup F],
  𝔖₂ ⊆ 𝔖₁ → UniformConvergenceCLM.instTopologicalSpace σ F 𝔖₁ ≤ UniformConvergenceCLM.instTopologicalSpace σ F 𝔖₂
-- Mathlib.RingTheory.ZMod.UnitsCyclic
/-- `(ZMod n)ˣ` is cyclic iff `n` is of the form
`0`, `1`, `2`, `4`, `p ^ m`, or `2 * p ^ m`,
where `p` is an odd prime and `1 ≤ m`.  -/
ZMod.isCyclic_units_iff : ∀ (n : ℕ),
  IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
-- Init.Data.Range.Polymorphic.Char
Char.instUpwardEnumerable : Std.PRange.UpwardEnumerable Char
-- Lean.Expr
Lean.Literal.strVal.sizeOf_spec : ∀ (val : String), sizeOf (Lean.Literal.strVal val) = 1 + sizeOf val
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.head.eq_1 : ∀ {F : PFunctor.{uA, uB}} (x : F.M), x.head = PFunctor.Approx.head' (x.approx 1)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.continuous_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α},
  Continuous f ↔ ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in nhds a, dist (f x) (f a) < ε
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.mk.injEq : ∀ {α : Type u_5} {ι : Type u_6} (idxFun : ι → Option α) (proper : ∃ i, idxFun i = none) (idxFun_1 : ι → Option α)
  (proper_1 : ∃ i, idxFun_1 i = none),
  ({ idxFun := idxFun, proper := proper } = { idxFun := idxFun_1, proper := proper_1 }) = (idxFun = idxFun_1)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_cond_eq_left : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a : α}, ∏ᶠ (i : α) (_ : i = a), f i = f a
-- Mathlib.Data.List.Chain
List.IsChain.imp_of_mem_imp : ∀ {α : Type u_1} {R S : α → α → Prop} {l : List α},
  (∀ (a b : α), a ∈ l → b ∈ l → R a b → S a b) → List.IsChain R l → List.IsChain S l
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.eventually_atTop_curry : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {p : α × β → Prop},
  (∀ᶠ (x : α × β) in Filter.atTop, p x) → ∀ᶠ (k : α) in Filter.atTop, ∀ᶠ (l : β) in Filter.atTop, p (k, l)
-- Init.Data.UInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toUInt8 : Bool → UInt8
-- Mathlib.RingTheory.AdicCompletion.RingHom
/-- `RingHom` variant of `IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq`.
 -/
IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq' : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] {I : Ideal S} {a : ℕ → ℕ}
  (ha : StrictMono a) (f : (n : ℕ) → R →+* S ⧸ I ^ a n),
  (∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) →
    ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I ⋯).comp (f n) = f m
-- Lean.Parser.Basic
Lean.Parser.checkTailWs : Lean.Syntax → Bool
-- Plausible.Gen
/-- `pick default xs n` chooses a weight & a generator `(k, gen)` from the list `xs` such that `n < k`.
If `xs` is empty, the `default` generator with weight 0 is returned.   -/
Plausible.Gen.pick : {α : Type u_1} → Plausible.Gen α → List (ℕ × Plausible.Gen α) → ℕ → ℕ × Plausible.Gen α
-- Mathlib.Data.Vector.Basic
/-- `v.insertIdx a i` inserts `a` into the vector `v` at position `i`
(and shifting later components to the right).  -/
List.Vector.insertIdx : {α : Type u_1} → {n : ℕ} → α → Fin (n + 1) → List.Vector α n → List.Vector α (n + 1)
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- `gcdExt a b` returns the triple `(g, α, β)` such that
- `g = gcd a b` (with `g ≥ 0`), and
- `g = α * a + β * b`.
 -/
Lean.Meta.Grind.Arith.gcdExt : ℤ → ℤ → ℤ × ℤ × ℤ