mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Similarity
Similar.refl : ∀ {ι : Type u_1} {P₁ : Type u_3} [inst : PseudoEMetricSpace P₁] (v₁ : ι → P₁), Similar v₁ v₁
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instHasRingHomPropertyFlat : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.Flat fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Mathlib.Algebra.Group.Defs
mul_left_cancel_iff : ∀ {G : Type u_1} [inst : Mul G] [IsLeftCancelMul G] {a b c : G}, a * b = a * c ↔ b = c
-- Init.Grind.AC
Lean.Grind.AC.Expr.denote_toSeq' : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} (e : Lean.Grind.AC.Expr)
  (s : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx (e.toSeq' s) = ctx.op (Lean.Grind.AC.Expr.denote ctx e) (Lean.Grind.AC.Seq.denote ctx s)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The remainder `r` in the proof of Weierstrass division.  -/
PowerSeries.IsWeierstrassDivisorAt.mod : {A : Type u_1} →
  [inst : CommRing A] →
    {g : PowerSeries A} →
      {I : Ideal A} → g.IsWeierstrassDivisorAt I → PowerSeries A → [IsPrecomplete I A] → Polynomial A
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n) (s : Set M), n ≠ 0 → MDiff[s] ⇑h
-- Mathlib.Analysis.Convex.PartitionOfUnity
/-- Let `X` be a normal paracompact topological space (e.g., any extended metric space). Let `E` be
a topological real vector space. Let `t : X → Set E` be a family of convex sets. Suppose that for
each point `x : X`, there exists a vector `c : E` that belongs to `t y` for all `y` in a
neighborhood of `x`. Then there exists a continuous map `g : C(X, E)` such that `g x ∈ t x` for all
`x`. See also `exists_continuous_forall_mem_convex_of_local`.  -/
exists_continuous_forall_mem_convex_of_local_const : ∀ {X : Type u_2} {E : Type u_3} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [NormalSpace X] [ParacompactSpace X] [inst_5 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E]
  {t : X → Set E},
  (∀ (x : X), Convex ℝ (t x)) → (∀ (x : X), ∃ c, ∀ᶠ (y : X) in nhds x, c ∈ t y) → ∃ g, ∀ (x : X), g x ∈ t x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey?.isSome = true
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
MonoidHom.uniformContinuous_of_continuousAt_one : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  [inst_4 : Group β] [IsUniformGroup β] (f : α →* β), ContinuousAt (⇑f) 1 → UniformContinuous ⇑f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_erase!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase! k t).get? k = none
-- Mathlib.Combinatorics.Quiver.Arborescence
Quiver.Arborescence.mk : {V : Type u} → [inst : Quiver V] → (root : V) → ((b : V) → Unique (Quiver.Path root b)) → Quiver.Arborescence V
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.withChangePos : Lean.SubExpr.Pos →
  Lean.SubExpr.Pos → optParam Lean.Widget.ExprDiffTag✝ Lean.Widget.ExprDiffTag.change✝ → Lean.Widget.ExprDiff✝
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- The pushout of `(𝟙 Y, f)` and `(𝟙 Y, g)`.  -/
_private.Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers.0.CategoryTheory.NormalEpiCategory.Q : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        [CategoryTheory.Limits.HasCokernels C] →
          [CategoryTheory.IsNormalEpiCategory C] →
            {X Y : C} →
              (f g : X ⟶ Y) →
                [CategoryTheory.Epi (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id Y) f)] →
                  [CategoryTheory.Epi (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id Y) g)] → C
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep.eq_1 : ∀ {α : Type u_1} [inst : EDist α] (s : Set α), s.einfsep = ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Let `E` be a real, finite-dimensional, inner product space and `s` be a subset of `E`. A function
`f` on `E` is harmonic in a neighborhood of `s` if it is harmonic at every point of `s`.
 -/
InnerProductSpace.HarmonicOnNhd : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [FiniteDimensional ℝ E] →
        {F : Type u_2} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (E → F) → Set E → Prop
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift_mk_compr₂ : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : TensorProduct R M N →ₗ[R] P), TensorProduct.lift ((TensorProduct.mk R M N).compr₂ f) = f
-- Init.Data.List.Lemmas
List.foldr.eq_2 : ∀ {α : Type u} {β : Type v} (f : α → β → β) (init : β) (a : α) (as : List α),
  List.foldr f init (a :: as) = f a (List.foldr f init as)
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.fiberEquivGroup.congr_simp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e e_1 : ↑(f ⁻¹' {x})),
  e = e_1 → hf.fiberEquivGroup e = hf.fiberEquivGroup e_1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_adj_penultimate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v), ¬w.Nil → w.toSubgraph.Adj w.penultimate v
-- Batteries.Data.List.Lemmas
List.getElem_filter_eq_getElem_getElem_findIdxs : ∀ {i : ℕ} {α : Type u_1} {xs : List α} {p : α → Bool} (h : i < (List.filter p xs).length),
  (List.filter p xs)[i] = xs[(List.findIdxs p xs)[i]]
-- Mathlib.Order.Hom.Lattice
InfHom.instTop : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → [Top β] → Top (InfHom α β)
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is minimized when
`f` and `g` antivary together on `s`. Stated by permuting the entries of `g`.  -/
AntivaryOn.sum_smul_le_sum_smul_comp_perm : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f i • g (σ i)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.commShiftIso_zero : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} (F : CategoryTheory.Functor C D) (A : Type u_6) {inst_2 : AddMonoid A}
  {inst_3 : CategoryTheory.HasShift C A} {inst_4 : CategoryTheory.HasShift D A} [self : F.CommShift A],
  CategoryTheory.Functor.commShiftIso F 0 = CategoryTheory.Functor.CommShift.isoZero F A
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResultCore.solved : Lean.Meta.InjectionResultCore
-- Mathlib.RingTheory.Localization.Module
IsLocalizedModule.mapEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_4} {N' : Type u_5} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (Rₛ : Type u_6)
  [inst_11 : CommSemiring Rₛ] [inst_12 : Algebra R Rₛ] [inst_13 : Module Rₛ M'] [inst_14 : Module Rₛ N']
  [inst_15 : IsScalarTower R Rₛ M'] [inst_16 : IsScalarTower R Rₛ N'] [inst_17 : IsLocalization S Rₛ] (e : M ≃ₗ[R] N)
  (a : N'), (IsLocalizedModule.mapEquiv S f g Rₛ e).symm a = ((IsLocalizedModule.map S g f) ↑e.symm) a
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.ObjectProperty.of_essentiallySmall_index : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.EssentiallySmall.{w, v_1, u_1} J]
  [CategoryTheory.IsFiltered J] (pres : CategoryTheory.Limits.ColimitPresentation J X),
  (∀ (i : J), P (pres.diag.obj i)) → P.ind X
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Construct a term of `ProfiniteAddGrp` from a type endowed with the structure of a
profinite topological additive group.  -/
ProfiniteAddGrp.ofProfinite : (G : Profinite) → [inst : AddGroup ↑G.toTop] → [IsTopologicalAddGroup ↑G.toTop] → ProfiniteAddGrp.{u_1}
-- Mathlib.RepresentationTheory.Coinvariants
Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (x : V) (g : G) (r : k),
  ρ.ofCoinvariantsTprodLeftRegular
      ((Representation.Coinvariants.mk (ρ.tprod (Representation.leftRegular k G))) (x ⊗ₜ[k] MonoidAlgebra.single g r)) =
    r • (ρ g⁻¹) x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {a : α} {h' : (t.getKey? a).isSome = true}, (t.getKey? a).get h' = t.getKey a ⋯
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instSMulCommClass_circle_closedBall : SMulCommClass Circle Complex.UnitClosedDisc Complex.UnitDisc
-- Mathlib.NumberTheory.Padics.PadicNumbers
_private.Mathlib.NumberTheory.Padics.PadicNumbers.0.Padic.lim' : {p : ℕ} → [inst : Fact (Nat.Prime p)] → CauSeq ℚ_[p] ⇑padicNormE → PadicSeq p
-- Lean.Compiler.ExternAttr
Lean.ExternAttrData.mk.sizeOf_spec : ∀ (entries : List Lean.ExternEntry), sizeOf { entries := entries } = 1 + sizeOf entries
-- Init.Data.BitVec.Bitblast
/-- The unsigned parallel prefix of `x` at `s` is `true` if and only if x interpreted
as a natural number is greater or equal than `2 ^ (w - 1 - (s - 1))`.  -/
BitVec.uppcRec_true_iff : ∀ {w : ℕ} (x : BitVec w) (s : ℕ) (h : s < w), x.uppcRec s h = true ↔ 2 ^ (w - 1 - (s - 1)) ≤ x.toNat
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instMulTorsionFree : ∀ {α : Type u_1} [inst : Monoid α] [IsMulTorsionFree α], IsMulTorsionFree αᵐᵒᵖ
-- Mathlib.GroupTheory.Submonoid.Center
unitsCenterToCenterUnits.eq_1 : ∀ (M : Type u_1) [inst : Monoid M],
  unitsCenterToCenterUnits M = (Units.map (Submonoid.center M).subtype).codRestrict (Submonoid.center Mˣ) ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (mem : k ∈ t₂), (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.mul_inv_mem_range_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (σ σ' : S.Section) (g : G), σ g * (σ' g)⁻¹ ∈ S.inl.range
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h₂ : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S],
  h₂.IsPreservedBy F
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.assoc_toAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Semiring D] [inst_9 : Bialgebra S C]
  [inst_10 : Bialgebra R D] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C],
  (Bialgebra.TensorProduct.assoc R S A C D).toAlgEquiv = Algebra.TensorProduct.assoc R S S A C D
-- Init.Sym.Lemmas
Lean.Sym.Fin.le_eq_true : ∀ {n : ℕ} (a b : Fin n), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The localization of `R` at the complement of a prime ideal is a local ring.  -/
Localization.AtPrime.isLocalRing : ∀ {R : Type u_1} [inst : CommSemiring R] (P : Ideal R) [hp : P.IsPrime], IsLocalRing (Localization P.primeCompl)
-- Mathlib.RingTheory.MvPolynomial.Localization
IsLocalization.Away.invSelf.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x x_1 : R)
  (e_x : x = x_1) [inst_3 : IsLocalization.Away x S], IsLocalization.Away.invSelf x = IsLocalization.Away.invSelf x_1
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_inf_ne_zero : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, H.relIndex L ≠ 0 → K.relIndex L ≠ 0 → (H ⊓ K).relIndex L ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.inclusionObj.eq_2 : ∀ {C : Type u} (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a : C),
  CategoryTheory.FreeMonoidalCategory.inclusionObj (n.tensor a) =
    (CategoryTheory.FreeMonoidalCategory.inclusionObj n).tensor (CategoryTheory.FreeMonoidalCategory.of a)
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
support_subset_support_matPolyEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (m : Matrix n n (Polynomial R)) (i j : n), (m i j).support ⊆ (matPolyEquiv m).support
-- Mathlib.Order.Hom.Bounded
BotHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Bot α] [inst_1 : Bot β] [inst_2 : SizeOf α] [inst_3 : SizeOf β] (toFun : α → β)
  (map_bot' : toFun ⊥ = ⊥), sizeOf { toFun := toFun, map_bot' := map_bot' } = 1 + sizeOf map_bot'
-- Init.System.Platform
System.Platform.eight_le_numBits : 8 ≤ System.Platform.numBits
-- Mathlib.Data.Quot
/-- Note that this provides `DecidableRel (Quotient.lift₂ f h)` when `α = β`.  -/
Quotient.lift₂.decidablePred : {α : Sort u_1} →
  {β : Sort u_2} →
    {sa : Setoid α} →
      {sb : Setoid β} →
        (f : α → β → Prop) →
          (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) →
            [hf : (a : α) → DecidablePred (f a)] → (q₁ : Quotient sa) → DecidablePred (Quotient.lift₂ f h q₁)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isOrthoᵢ_flip : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [inst : CommSemiring R]
  [inst_1 : CommSemiring R₁] [inst_2 : AddCommMonoid M₁] [inst_3 : Module R₁ M₁] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] {I₁ I₁' : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M) {v : n → M₁},
  B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.map_map_equiv : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  {f : α → β → γ} {g : α → γ → δ},
  (Std.TreeMap.Raw.map g (Std.TreeMap.Raw.map f t)).Equiv (Std.TreeMap.Raw.map (fun k v => g k (f k v)) t)
-- Mathlib.Order.Category.BoolAlg
/-- The category of Boolean algebras.  -/
BoolAlg : Type (u_1 + 1)
-- Mathlib.Algebra.Tropical.Basic
Tropical.instInvOfNeg : {R : Type u} → [Neg R] → Inv (Tropical R)
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A module is semisimple iff it is generated by its simple submodules.  -/
sSup_simples_eq_top_iff_isSemisimpleModule : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  sSup {m | IsSimpleModule R ↥m} = ⊤ ↔ IsSemisimpleModule R M
-- Init.Data.Int.Gcd
Int.dvd_gcd : ∀ {a b : ℤ} {c : ℕ}, ↑c ∣ a → ↑c ∣ b → c ∣ a.gcd b
-- Mathlib.Tactic.Ring.Common
/-- The expression `e` (the sum of monomials) is equal to `0`.  -/
Mathlib.Tactic.Ring.Common.Overlap.zero : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {e : Q(«$α»)} → Q(Mathlib.Meta.NormNum.IsNat «$e» 0) → Mathlib.Tactic.Ring.Common.Overlap bt sα e
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.le_order_subst_right' : ∀ {R : Type u_2} [inst : CommRing R] {f φ : PowerSeries R},
  PowerSeries.constantCoeff f = 0 →
    PowerSeries.constantCoeff φ = 0 → f.order ≤ PowerSeries.order (PowerSeries.subst f φ)
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the forward direction of `SimpleGraph.isUniversal_compl_iff_isIsolated`. -/
SimpleGraph.IsIsolated.of_isUniversal_compl : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, Gᶜ.IsUniversal v → G.IsIsolated v
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.comp_hom_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {X Y Z : CategoryTheory.Triangulated.SpectralObject C ι} (α : X ⟶ Y) (β : Y ⟶ Z)
  {Z_1 : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C} (h : Z.ω₁ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α β).hom h =
    CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp β.hom h)
-- Init.Data.Nat.Basic
Nat.Nat.instAntisymmNotLt : Std.Antisymm fun x1 x2 => ¬x1 < x2
-- Mathlib.Topology.MetricSpace.Completion
UniformSpace.Completion.dist_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : UniformSpace.Completion α), dist x y = dist y x
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.desc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α α_1 : CochainComplex.HomComplex.Cochain F K (-1)) (e_α : α = α_1) (β β_1 : G ⟶ K) (e_β : β = β_1)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)),
  CochainComplex.mappingCone.desc φ α β eq = CochainComplex.mappingCone.desc φ α_1 β_1 ⋯
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.instInhabitedFinsupp : {ι : Type u_1} → {R : Type u_3} → [inst : Semiring R] → Inhabited (Module.Basis ι R (ι →₀ R))
-- Mathlib.Algebra.Opposites
MulOpposite.isCancelAdd_iff : ∀ {α : Type u_1} [inst : Add α], IsCancelAdd αᵐᵒᵖ ↔ IsCancelAdd α
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAt.mul : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [ContMDiffMul I n G] {f g : M → G} {x : M},
  ContMDiffAt I' I n f x → ContMDiffAt I' I n g x → ContMDiffAt I' I n (f * g) x
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.exact₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.exact₃._auto_1), (X.sc₃ f g fg h n₀ n₁ hn₁).Exact
-- Mathlib.GroupTheory.Nilpotent
Group.isNilpotent_of_subsingleton : ∀ {G : Type u_1} [inst : Group G] [Subsingleton G], Group.IsNilpotent G
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- The compact coherentification makes any space into a compactly coherent space.  -/
CompactCoherentification.instCompactlyCoherentSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X], CompactlyCoherentSpace (CompactCoherentification X)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- The image of `SL(n, ℤ)` in `GL(n, ℝ)` is discrete.  -/
Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n],
  DiscreteTopology ↥(Matrix.SpecialLinearGroup.mapGL ℝ).range
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.SplitCandidate.none.sizeOf_spec : sizeOf Lean.Meta.Grind.SplitCandidate.none✝ = 1
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instAddCommMonoid : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddCommMonoid (LowerSet α)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_ofNat : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddMonoidWithOne G]
  [inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo],
  f (OfNat.ofNat n) = f 0 + OfNat.ofNat n
-- Mathlib.Algebra.Group.Action.Units
IsAddUnit.vadd : ∀ {G : Type u_1} {M : Type u_3} [inst : AddGroup G] [inst_1 : AddMonoid M] [inst_2 : AddAction G M]
  [VAddCommClass G M M] [VAddAssocClass G M M] {m : M} (g : G), IsAddUnit m → IsAddUnit (g +ᵥ m)
-- Mathlib.Order.Category.PartOrdEmb
/-- Typecheck a `OrderEmbedding` as a morphism in `PartOrdEmb`.  -/
PartOrdEmb.ofHom : {X Y : Type u} →
  [inst : PartialOrder X] →
    [inst_1 : PartialOrder Y] → X ↪o Y → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.congr_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp}, t₁.Equiv t₂ → (t₁.Equiv t₃ ↔ t₂.Equiv t₃)
-- Mathlib.RingTheory.Bialgebra.Basic
/-- If `R` is a field (or even a commutative semiring) and `A`
is an `R`-algebra with a coalgebra structure, then `Bialgebra.mk'`
consumes proofs that the counit and comultiplication preserve
the identity and multiplication, and produces a bialgebra
structure on `A`.  -/
Bialgebra.mk' : (R : Type u) →
  (A : Type v) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          [C : Coalgebra R A] →
            CoalgebraStruct.counit 1 = 1 →
              (∀ {a b : A}, CoalgebraStruct.counit (a * b) = CoalgebraStruct.counit a * CoalgebraStruct.counit b) →
                CoalgebraStruct.comul 1 = 1 →
                  (∀ {a b : A}, CoalgebraStruct.comul (a * b) = CoalgebraStruct.comul a * CoalgebraStruct.comul b) →
                    Bialgebra R A