mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Basic
Std.LawfulDeterministicIterator.mk : ∀ {β α : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β],
  (∀ (it : Std.IterM m β), ∃ step, it.IsPlausibleStep = fun x => x = step) → Std.LawfulDeterministicIterator α m
-- Mathlib.Condensed.Explicit
/-- A `CondensedSet` version of `Condensed.ofSheafStonean`.  -/
CondensedSet.ofSheafStonean : (F : CategoryTheory.Functor Stoneanᵒᵖ (Type (u + 1))) → [CategoryTheory.Limits.PreservesFiniteProducts F] → CondensedSet
-- Std.Data.DHashMap.RawLemmas
_private.Std.Data.DHashMap.RawLemmas.0.Std.DHashMap.Raw.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.insert a b = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.insert ⟨m, h⟩ a b) else m
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.instIteratorLoop : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {n : Type x → Type x'} →
        [inst : Monad m] →
          [Monad n] → [inst_2 : Std.Iterator α m β] → Std.IteratorLoop (Std.Iterators.Types.Take α m) m n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : t₁.WF)
  (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew k v t₁ ⋯).impl.Equiv
        (Std.DTreeMap.Internal.Impl.insertIfNew k v t₂ ⋯).impl
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a congruence relation `c` on a semiring and a homomorphism
`f` constant on the equivalence classes of `c`, `f` has the same image
as the homomorphism that `f` induces on the quotient.  -/
RingCon.rangeS_lift : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  (H : c ≤ RingCon.ker f), (c.lift f H).rangeS = f.rangeS
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.affineSpan_pair_comm : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ : P}, line[k, p₁, p₂] = line[k, p₂, p₁]
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The unit isomorphism of the equivalence `equivalence₂` between `A` and `B`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso : {A : Type u_1} →
  {A' : Type u_2} →
    {B : Type u_3} →
      {B' : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] →
                {eA : A ≌ A'} →
                  (eB : B ≌ B') →
                    {e' : A' ≌ B'} →
                      {F : CategoryTheory.Functor A B'} →
                        (eA.functor.comp e'.functor ≅ F) →
                          (CategoryTheory.Functor.id A ≅
                            (F.comp eB.inverse).comp (eB.functor.comp (e'.inverse.comp eA.inverse)))
-- Mathlib.Order.SuccPred.LinearLocallyFinite
iterate_succ_toZ : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι} (i : ι), i0 ≤ i → Order.succ^[(toZ i0 i).toNat] i0 = i
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instAddMemClass : ∀ {M : Type u_1} [inst : Add M], AddMemClass (AddSubsemigroup M) M
-- Mathlib.Topology.MetricSpace.Basic
MetricSpace.instT0Space : ∀ {γ : Type w} [inst : MetricSpace γ], T0Space γ
-- Mathlib.Order.Heyting.Basic
Pi.instGeneralizedHeytingAlgebra : {ι : Type u_1} →
  {α : ι → Type u_4} → [(i : ι) → GeneralizedHeytingAlgebra (α i)] → GeneralizedHeytingAlgebra ((i : ι) → α i)
-- Mathlib.Data.Stream.Defs
/-- Drop first `n` elements of a stream.  -/
Stream'.drop : {α : Type u} → ℕ → Stream' α → Stream' α
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.hom_id : ∀ {M : MagmaCat}, MagmaCat.Hom.hom (CategoryTheory.CategoryStruct.id M) = MulHom.id ↑M
-- Mathlib.Tactic.Linter.Style
/-- The `lambdaSyntax` linter flags uses of the symbol `λ` to define anonymous functions.
This is syntactically equivalent to the `fun` keyword; mathlib style prefers using the latter.
 -/
Mathlib.Linter.linter.style.lambdaSyntax : Lean.Option Bool
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_neg : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.T R (-n) = Polynomial.Chebyshev.T R n
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- Finite wide pushouts are finite colimits, so if `C` has all finite colimits,
it also has finite wide pushouts
 -/
CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.HasFiniteWidePushouts C
-- Mathlib.Data.NNReal.Defs
NNReal.coe_ofScientific : ∀ (m : ℕ) (s : Bool) (e : ℕ), ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.directedAffineCover_I₀ : ∀ (X : AlgebraicGeometry.Scheme), X.directedAffineCover.I₀ = ↑X.affineOpens
-- Lean.Meta.Constructions.BRecOn
_private.Lean.Meta.Constructions.BRecOn.0.Lean.buildBRecOnMinorPremise.go : Lean.Level →
  Array Lean.Expr →
    Array Lean.Expr → Array Lean.Expr → Lean.Expr → Array Lean.Expr → List Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.contDiffOn_extendCoordChange_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} [inst_5 : ChartedSpace H M],
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I n M →
      ContDiffOn 𝕜 n (↑(ModelWithCorners.extendCoordChange e e').symm) (ModelWithCorners.extendCoordChange e e').target
-- Mathlib.LinearAlgebra.Charpoly.ToMatrix
Matrix.charpoly_toLin : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] {n : Type u_5} [inst_5 : Fintype n] [inst_6 : DecidableEq n]
  (A : Matrix n n R) (b : Module.Basis n R M), ((Matrix.toLin b b) A).charpoly = A.charpoly
-- Init.Internal.Order.Basic
Lean.Order.admissible_pprod_snd : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.CCPO α] [inst_1 : Lean.Order.CCPO β] (P : β → Prop),
  Lean.Order.admissible P → Lean.Order.admissible fun x => P x.snd
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biInter_biUnion : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → Set β),
  ⋂ y ∈ s.biUnion t, f y = ⋂ x ∈ s, ⋂ y ∈ t x, f y
-- Lean.Meta.InferType
/-- Returns `.true` if `e` is `Prop`, `.false` if it is `Type _`, and `.undef` otherwise.  -/
_private.Lean.Meta.InferType.0.Lean.Meta.isArrowProposition'.checkProp : Lean.Expr → Lean.Meta.ArrowPropResult✝
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.symm : ∀ {x : PSet.{u_1}} {y : PSet.{u_2}}, x.Equiv y → y.Equiv x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Catch.x : Lean.Elab.Term.Do.ToCodeBlock.Catch → Lean.Syntax
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {F : CategoryTheory.PreZeroHypercover S} →
          (s₀ : E.I₀ → F.I₀) →
            (h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i)) →
              autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i) (F.f (s₀ i)) = E.f i)
                  CategoryTheory.PreZeroHypercover.Hom.w₀._autoParam →
                E.Hom F
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.hom_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C}
  (m : t.pt ⟶ W),
  m = h.desc { pt := W, ι := CategoryTheory.NatTrans.mk' (fun b => CategoryTheory.CategoryStruct.comp (t.ι.app b) m) ⋯ }
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.le_size : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [self : Std.Sat.AIG.LawfulOperator α β f]
  (aig : Std.Sat.AIG α) (input : β aig), aig.decls.size ≤ (f aig input).aig.decls.size
-- Init.WFTactics
/-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
reasoning after applying lexicographic order lemmas.
It can be extended by adding more macro definitions, e.g.
```
macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
```
 -/
tacticDecreasing_trivial : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.mk : {R : Type u} →
  [inst : Ring R] →
    {Γ₀ : outParam (Type v)} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        [toUniformSpace : UniformSpace R] →
          [toIsUniformAddGroup : IsUniformAddGroup R] →
            (v : Valuation R Γ₀) → (∀ (s : Set R), s ∈ nhds 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s) → Valued R Γ₀
-- Mathlib.Data.Multiset.Bind
/-- `s.bind f` is the monad bind operation, defined as `(s.map f).join`. It is the union of `f a` as
`a` ranges over `s`.  -/
Multiset.bind : {α : Type u_1} → {β : Type v} → Multiset α → (α → Multiset β) → Multiset β
-- Mathlib.Order.Category.BoolAlg
BoolAlg.ext : ∀ {X Y : BoolAlg} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.mem_eqLocus : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [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₂}
  {x : M} {f g : M →ₛₗ[τ₁₂] M₂}, x ∈ f.eqLocus g ↔ f x = g x
-- Std.Data.HashMap.Basic
/-- Carries out a monadic action on each mapping in the hash map in some order.  -/
Std.HashMap.forM : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        {m : Type w → Type w'} → [Monad m] → (α → β → m PUnit.{w + 1}) → Std.HashMap α β → m PUnit.{w + 1}
-- Mathlib.Logic.Basic
/-- **Alias** of `and_congr`. -/
Iff.and : ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∧ b ↔ c ∧ d)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMul : ∀ {M : Type u_1} [inst : MulOneClass M],
  CanLift (Set M) (Submonoid M) SetLike.coe fun s => 1 ∈ s ∧ ∀ {x y : M}, x ∈ s → y ∈ s → x * y ∈ s
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The bottom right map in the forward hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip) →
        (CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' C)
-- Std.Data.TreeSet.Basic
Std.TreeSet.instForMOfMonad : {α : Type u} → {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForM m (Std.TreeSet α cmp) α
-- Mathlib.RingTheory.Depth.Rees
/-- The implication `(3) → (4)` of `exists_isRegular_tfae`: for `M N` finitely generated
module over Noetherian ring `R` and ideal `I` satisfying `IM < M` and `Supp N = V(I)`,
if `Ext N M i = 0` for all `i < n`,
then there exists an `M`-regular sequence of length `n` contained in `I`.  -/
ModuleCat.exists_isRegular_of_exists_subsingleton_ext : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (n : ℕ)
  (M : ModuleCat R) [Module.Finite R ↑M],
  I • ⊤ < ⊤ →
    ∀ (N : ModuleCat R) [Module.Finite R ↑N],
      Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I →
        (∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i)) →
          ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.uniqueHom_default : ∀ {A : Type u} (x y : CategoryTheory.Codiscrete A), default = (x.iso y).hom
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasFDerivAt_finsetProd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} [inst_3 : DecidableEq ι] [Finite ι] {x : ι → 𝔸'},
  HasFDerivAt (fun x => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • ContinuousLinearMap.proj i) x
-- Init.Data.UInt.Basic
instOrOpUInt16 : OrOp UInt16
-- Mathlib.Control.Bifunctor
Bifunctor.lawfulFunctor : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α : Type u₀}, LawfulFunctor (F α)
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.map_eq_zero_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → (Polynomial.map f p = 0 ↔ p = 0)
-- Mathlib.Algebra.Group.ForwardDiff
/-- The `n`-th forward difference of a polynomial of degree `< n` is zero (formulated using explicit
sums over `range n`).
 -/
fwdDiff_iter_sum_mul_pow_eq_zero : ∀ {R : Type u_3} [inst : CommRing R] {n : ℕ} (P : ℕ → R),
  ((fwdDiff 1)^[n] fun r => ∑ k ∈ Finset.range n, P k * r ^ k) = 0
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.brecOn_1.eq : ∀ {motive_1 : Lean.IR.Alt → Sort u} {motive_2 : Lean.IR.FnBody → Sort u} {motive_3 : Array Lean.IR.Alt → Sort u}
  {motive_4 : List Lean.IR.Alt → Sort u} (t : Array Lean.IR.Alt) (F_1 : (t : Lean.IR.Alt) → t.below → motive_1 t)
  (F_2 : (t : Lean.IR.FnBody) → t.below → motive_2 t)
  (F_3 : (t : Array Lean.IR.Alt) → Lean.IR.Alt.below_1 t → motive_3 t)
  (F_4 : (t : List Lean.IR.Alt) → Lean.IR.Alt.below_2 t → motive_4 t),
  Lean.IR.Alt.brecOn_1 t F_1 F_2 F_3 F_4 = F_3 t (Lean.IR.Alt.brecOn_1.go t F_1 F_2 F_3 F_4).2
-- Lean.Data.Options
Lean.instInhabitedOptionDecls : Inhabited Lean.OptionDecls
-- Mathlib.Algebra.Category.Grp.Images
/-- the factorisation of any morphism in `AddCommGrpCat` through a mono has
the universal property of the image.  -/
AddCommGrpCat.isImage : {G H : AddCommGrpCat} → (f : G ⟶ H) → CategoryTheory.Limits.IsImage (AddCommGrpCat.monoFactorisation f)
-- Lean.Meta.Basic
/-- Inserts `fvarId` into the `zetaDeltaFVarIds` set.
 -/
Lean.Meta.addZetaDeltaFVarId : Lean.FVarId → Lean.MetaM Unit
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.coresNatTrans_app : ∀ (k : Type u) {G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (f : G →* H) (n : ℕ)
  (X : Rep.{u, u, u} k H),
  (groupHomology.coresNatTrans k f n).app X = groupHomology.map f (CategoryTheory.CategoryStruct.id (Rep.res f X)) n
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Functor.instFullQuotientHomRelLift : ∀ {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] (L : CategoryTheory.Functor C D) [L.Full],
  (CategoryTheory.Quotient.lift L.homRel L ⋯).Full
-- Mathlib.Order.Bounds.OrderIso
OrderIso.isLUB_preimage' : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : β},
  IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x
-- Mathlib.Analysis.Normed.Order.UpperLower
IsClosed.upperClosure_pi : ∀ {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)}, IsClosed s → BddBelow s → IsClosed ↑(upperClosure s)
-- Mathlib.Order.LiminfLimsup
Filter.limsup_congr : ∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β},
  (∀ᶠ (a : α) in f, u a = v a) → Filter.limsup u f = Filter.limsup v f
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_inter_eq_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α), K ⊆ M.coloops → M.closure X ∩ K = X ∩ K
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cast : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig1 aig2 : Std.Sat.AIG α} →
        Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1 →
          aig1.decls.size ≤ aig2.decls.size → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig2
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- If a simple module is contained in a sum of semisimple modules, it must be isomorphic
to a submodule of one of the summands.  -/
Submodule.le_linearEquiv_of_le_sSup : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [IsSimpleModule R ↥N] (s : Set (Submodule R M)) [hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m],
  N ≤ sSup s → ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)
-- Std.Time.Time.PlainTime
Std.Time.instOrdPlainTime : Ord Std.Time.PlainTime
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.addCommMonoid : {α : Type u_1} → AddCommMonoid (MeasureTheory.OuterMeasure α)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symmEquiv_symm_apply_symm_apply : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M₂ ≃ₛₗ[σ'] M) (a : M₂),
  (LinearEquiv.symmEquiv.symm e).symm a = e a
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.sheafToPresheaf_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  (X Y : CategoryTheory.Sheaf J A),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.sheafToPresheaf J A) X Y =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.sheafToPresheaf J A).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_eq_mk_of_archimedean : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M}
  [Archimedean M], a ≠ 0 → b ≠ 0 → ArchimedeanClass.mk a = ArchimedeanClass.mk b
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_two_gt_d9 : 0.6931471803 < Real.log 2
-- Mathlib.Algebra.FiniteSupport.Basic
Function.hasFiniteSupport_fun_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M], Function.HasFiniteSupport 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The first part of the third simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_σ_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 1)},
  CategoryTheory.CategoryStruct.comp (X.σ i) (X.δ i.castSucc) =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n }))
-- Mathlib.Tactic.CrossRefAttribute
/-- Extract the underlying identifier as a string from a `wikidataId` node.  -/
Lean.TSyntax.getWikidataId : Lean.TSyntax Mathlib.CrossRef.wikidataIdKind → Lean.CoreM String
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.nnnorm : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : SeminormedAddCommGroup β]
  {f : α → β}, MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => ‖f x‖₊) μ
-- Mathlib.Algebra.Module.LinearMap.Polynomial
/-- Let `L` and `M` be finite free modules over `R`,
and let `φ : L →ₗ[R] Module.End R M` be a linear family of endomorphisms.
Let `b` be a basis of `L` and `bₘ` a basis of `M`.
Then `LinearMap.polyCharpoly φ b` is the polynomial that evaluates on elements `x` of `L`
to the characteristic polynomial of `φ x` acting on `M`.  -/
LinearMap.polyCharpoly : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      {ι : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup L] →
            [inst_2 : Module R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  (L →ₗ[R] Module.End R M) →
                    [Fintype ι] →
                      [DecidableEq ι] →
                        [Module.Free R M] → [Module.Finite R M] → Module.Basis ι R L → Polynomial (MvPolynomial ι R)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- An internal symmetric relation in the category of types gives rise to a standard symmetric
relation.  -/
TypeCat.symm_of_symmetricRelation : ∀ {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.SymmetricRelation p₁ p₂), Std.Symm (TypeCat.Rel.ofPair p₁ p₂)
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.fiberEquivAddGroup.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hf : IsAddQuotientCoveringMap f G) {x : X} (e : ↑(f ⁻¹' {x})),
  hf.fiberEquivAddGroup e = (Equiv.ofBijective (fun g => ⟨g +ᵥ ↑e, ⋯⟩) ⋯).symm
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- Like `Submodule.map_pow`  -/
CliffordAlgebra.submodule_map_pow_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)) (n : ℕ),
  Submodule.map CliffordAlgebra.reverse (p ^ n) = Submodule.map CliffordAlgebra.reverse p ^ n
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toList_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_8 : Std.PRange.InfinitelyUpwardEnumerable α] [inst_9 : Std.Rxc.IsAlwaysFinite α]
  [inst_10 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)<...=Std.PRange.succ hi).toList = List.map Std.PRange.succ (lo<...=hi).toList
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalStarRing.lift_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : (i : ι) → StarRing (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : StarRing P] (g : (i : ι) → G i →⋆ₙ+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι) (x : G i),
  (DirectLimit.NonUnitalStarRing.lift G f P g Hg) ((DirectLimit.NonUnitalStarRing.of G f i) x) = (g i) x
-- Mathlib.Data.Finset.Image
Finset.filterMap_mono : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) {s t : Finset α}
  {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'}, s ⊆ t → Finset.filterMap f s f_inj ⊆ Finset.filterMap f t f_inj
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.unitsLift_symm_apply_apply_inv' : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : Monoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousMul M] (f : C(X, M)ˣ) (x : X), ↑((ContinuousMap.unitsLift.symm f) x)⁻¹ = ↑f⁻¹ x
-- Lean.Attributes
Lean.AttributeImplCore : Type
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_mul_eq_zero_of_right : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {q : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) (x : S)
  (p : Polynomial R), Polynomial.eval₂ f x q = 0 → Polynomial.eval₂ f x (p * q) = 0