mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasSeparator.wellPowered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Balanced C] [CategoryTheory.HasSeparator C], CategoryTheory.WellPowered.{v₁, v₁, u₁} C
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- Given a monomorphism `i : X ⟶ Y` of simplicial sets and a nondegenerate `d`-simplex
of `Y` not in the range of `i`, this is the inclusion of the corresponding summand
of the coproduct `sigmaBoundary i d`.  -/
SSet.relativeCellComplexOfMono.Cell.ιSigmaBoundary : {X Y : SSet} →
  {i : X ⟶ Y} →
    {d : ℕ} →
      SSet.relativeCellComplexOfMono.Cell i d →
        ((SSet.boundary d).toSSet ⟶ SSet.relativeCellComplexOfMono.sigmaBoundary i d)
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X Y : C) (f g : X ⟶ Y),
  CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g)
      (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y))
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.dvd_count_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] [Nontrivial α]
  {a : Associates α}, a ≠ 0 → ∀ {p : Associates α}, Irreducible p → ∀ (k : ℕ), k ∣ p.count (a ^ k).factors
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- An affine combination of covariant derivatives is a covariant derivative.  -/
IsCovariantDerivativeOn.affine_combination : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] {s : Set M}
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x},
  IsCovariantDerivativeOn F cov s →
    ∀ {cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x},
      IsCovariantDerivativeOn F cov' s →
        ∀ (g : M → 𝕜), IsCovariantDerivativeOn F (fun σ => g • cov σ + (1 - g) • cov' σ) s
-- Mathlib.GroupTheory.OrderOfElement
/-- See also `orderOf_eq_card_powers`.  -/
Nat.card_submonoidPowers : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] {a : G}, Nat.card ↥(Submonoid.powers a) = orderOf a
-- Mathlib.Topology.Algebra.Star.Real
instContinuousStarReal : ContinuousStar ℝ
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivComm_comp_quotQuotMk : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R),
  (↑(DoubleQuot.quotQuotEquivComm I J)).comp (DoubleQuot.quotQuotMk I J) = DoubleQuot.quotQuotMk J I
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.brecOn_1.go : {motive_1 : Lean.Meta.Match.Example → Sort u} →
  {motive_2 : List Lean.Meta.Match.Example → Sort u} →
    (t : List Lean.Meta.Match.Example) →
      ((t : Lean.Meta.Match.Example) → t.below → motive_1 t) →
        ((t : List Lean.Meta.Match.Example) → Lean.Meta.Match.Example.below_1 t → motive_2 t) →
          motive_2 t ×' Lean.Meta.Match.Example.below_1 t
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
Pi.mabs_eq_one : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Group (α i)] (f : (i : ι) → α i)
  [inst_1 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), MulLeftMono (α i)] [∀ (i : ι), MulRightMono (α i)],
  |f|ₘ = 1 ↔ f = 1
-- Init.Data.Option.Attach
Option.attachWith_map_val : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ (a : α), o = some a → p a),
  Option.map (fun i => f ↑i) (o.attachWith p H) = Option.map f o
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryGTD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : α × β},
  t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryGTD t₁ k fallback = Std.DTreeMap.Const.getEntryGTD t₂ k fallback
-- Mathlib.Order.UpperLower.Closure
/-- The biggest upper subset of an upper set `s` not containing an element `a`.  -/
UpperSet.erase : {α : Type u_1} → [inst : Preorder α] → UpperSet α → α → UpperSet α
-- Init.Data.UInt.Lemmas
USize.mul_zero : ∀ {a : USize}, a * 0 = 0
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuous_coe_ennreal_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ENNReal}, (Continuous fun a => ↑(f a)) ↔ Continuous f
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.whiskerLeft_out_app : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {E : Type u₂} [inst_4 : CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D)
  {G H : CategoryTheory.EnrichedFunctor V D E} (α : G ⟶ H) (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.whiskerLeft F α).out.app X =
    α.out.app (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α}
  {k : α}, Std.DHashMap.Internal.Raw₀.Const.get! (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)) k = ()
-- Mathlib.Tactic.GrindAttrs
/-- The `closedness` attribute is a custom grind-set specialized to prove that sets are closed.
It is called by the `closedness` tactic.  -/
Lean.Parser.Attr.closedness? : Lean.ParserDescr
-- Batteries.Classes.RatCast
instRatCastRat : RatCast ℚ
-- Mathlib.Logic.Encodable.Basic
ULower.up.eq_1 : ∀ {α : Type u_1} [inst : Encodable α] (a : ULower α), a.up = (ULower.equiv α).symm a
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.Spec_obj_left : ∀ (S : AlgebraicGeometry.Scheme)
  (A : CategoryTheory.MorphismProperty.CostructuredArrow @AlgebraicGeometry.Etale ⊤ AlgebraicGeometry.Scheme.Spec S),
  ((AlgebraicGeometry.Scheme.AffineEtale.Spec S).obj A).left = AlgebraicGeometry.Spec (Opposite.unop A.left)
-- Mathlib.Data.Set.Finite.Lattice
/-- Example: `Finite (⋃ (i < n), f i)` where `f : ℕ → Set α` and `[∀ i, Finite (f i)]`
(when given instances from `Order.Interval.Finset.Nat`).
 -/
Finite.Set.finite_biUnion'' : ∀ {α : Type u} {ι : Type u_1} (p : ι → Prop) [h : Finite ↑{x | p x}] (t : ι → Set α) [∀ (i : ι), Finite ↑(t i)],
  Finite ↑(⋃ x, ⋃ (_ : p x), t x)
-- Mathlib.Order.RelIso.Set
Subrel.instSymmSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Symm r] (p : α → Prop), Std.Symm (Subrel r p)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipPrefix?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.toSlice.skipPrefix? pat = Option.map String.Pos.toSlice (s.skipPrefix? pat)
-- Lean.Declaration
Lean.ConstructorVal : Type
-- Lean.Data.KVMap
Lean.KVMap.mk.sizeOf_spec : ∀ (entries : List (Lean.Name × Lean.DataValue)), sizeOf { entries := entries } = 1 + sizeOf entries
-- Mathlib.CategoryTheory.Subfunctor.Basic
/-- A subfunctor of a functor consists of a subset of `F.obj U` for every `U`,
compatible with the restriction maps `F.map i`.  -/
CategoryTheory.Subfunctor : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (Type w) → Type (max u w)
-- Init.Data.String.Termination
String.Pos.next?.eq_1 : ∀ {s : String} (pos : s.Pos), pos.next? = Option.map String.Pos.ofToSlice pos.toSlice.next?
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.ComputableSmall.inflate : {α : Type v} → [self : Std.Internal.ComputableSmall α] → Std.Internal.ComputableSmall.Target α → α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertMany_list_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)}, Std.ExtDHashMap.Const.insertMany m l = ∅ ↔ m = ∅ ∧ l = []
-- Init.Data.Int.Gcd
Int.lcm_dvd_lcm_mul_right_left : ∀ (a b c : ℤ), a.lcm b ∣ (a * c).lcm b
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bifunctor `(F -) ⊗ -`.  -/
CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₁ : {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] →
        [CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor C (CategoryTheory.Functor D D)
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- If `(a,b)` is the kernel pair of `f`, and `f` is a coequalizer morphism for some parallel pair, then
`f` is a coequalizer morphism of `a` and `b`.
 -/
CategoryTheory.IsKernelPair.toCoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R X Y : C} →
      {f : X ⟶ Y} →
        {a b : R ⟶ X} →
          (k : CategoryTheory.IsKernelPair f a b) →
            CategoryTheory.RegularEpi f → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)
-- Std.Http.Data.Body.Stream
/-- Creates a selector that resolves when consumer interest is present.
Returns `true` when a consumer is waiting, `false` when the channel closes first.
 -/
Std.Http.Body.Stream.interestSelector : Std.Http.Body.Stream → Std.Async.Selector Bool
-- Init.Data.String.Basic
/-- Given a position in `s.slice! p₀ p₁`, obtain the corresponding position in `s`, or panic if
taking `s.slice! p₀ p₁` already panicked.  -/
String.Pos.ofSlice! : {s : String} → {p₀ p₁ : s.Pos} → (s.slice! p₀ p₁).Pos → s.Pos
-- Mathlib.CategoryTheory.Center.Basic
/-- The action of the center of a category on an object. (This is necessary as
`NatTrans.app x X` is syntactically an endomorphism of `(𝟭 C).obj X`
rather than of `X`.)  -/
CategoryTheory.CatCenter.app : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.CatCenter C → (X : C) → X ⟶ X
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
/-- Pull a subgroup back to an opposite subgroup along `MulOpposite.unop`  -/
Subgroup.op : {G : Type u_2} → [inst : Group G] → Subgroup G → Subgroup Gᵐᵒᵖ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Given a structured arrow `X ⟶ T(Y)`, and an arrow `Y ⟶ Y'`, we can construct a morphism of
structured arrows given by `(X ⟶ T(Y)) ⟶ (X ⟶ T(Y) ⟶ T(Y'))`.  -/
CategoryTheory.StructuredArrow.homMk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {Y' : C} →
            {T : CategoryTheory.Functor C D} →
              (f : CategoryTheory.StructuredArrow S T) →
                (g : f.right ⟶ Y') →
                  f ⟶ CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map g))
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.isKProjective_of_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K : CochainComplex C ℤ},
  ((CochainComplex.opEquivalence C).functor.obj (Opposite.op K)).IsKInjective → K.IsKProjective
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.instAddCommMonoidPointOfIsComm : {R : Type u_1} → [inst : CommRing R] → {σ : Type u_3} → (F : FormalGroup R) → [F.IsComm] → AddCommMonoid (F.Point σ)
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.ciSup_eq_max'_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι},
  (∃ x ∈ s, sSup ∅ ≤ f x) →
    ∀ (h' : autoParam (Finset.image f s).Nonempty Finset.ciSup_eq_max'_image._auto_1),
      ⨆ i ∈ s, f i = (Finset.image f s).max' h'
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mk_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} (x : (i : ι) → R i)
  (hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ A i) (i : ι), (RestrictedProduct.mk x hx) i = x i
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
cmp_mul_neg_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightReflectLT R]
  [AddRightStrictMono R] {a : R}, a < 0 → ∀ (b c : R), cmp (a * b) (a * c) = cmp c b
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- An equivalence of root pairings is a morphism where the maps of weight and coweight spaces are
bijective.

See also `RootPairing.Equiv.toEndUnit`.  -/
RootPairing.Equiv : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                RootPairing ι R M N →
                                  RootPairing ι₂ R M₂ N₂ → Type (max (max (max (max (max u_1 u_3) u_4) u_5) u_6) u_7)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.set_finite : ∀ {α : Type u_1} (M : Matroid α) [M.Finite] (X : Set α), autoParam (X ⊆ M.E) Matroid.set_finite._auto_1 → X.Finite
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso X i).inv.right =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.right W)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_one : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : One Y], ⇑1 = 1
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_X_sub_C_mul_iff : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [IsDomain R] {a : R},
  ((Polynomial.X - Polynomial.C a) * f).Splits ↔ f.Splits
-- Mathlib.Order.Shrink
equivShrink_lt_equivShrink : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] {x y : α},
  (equivShrink α) x < (equivShrink α) y ↔ x < y
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonWaitForILeans.toJson : Lean.Lsp.WaitForILeans → Lean.Json
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integralAgainstBilinLM.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) (μ : MeasureTheory.Measure E)
  (φ : E → F₂),
  ContDiffMapSupportedIn.integralAgainstBilinLM B μ φ =
    { toFun := fun f => if MeasureTheory.IntegrableOn φ (↑K) μ then ∫ (x : E), (B (f x)) (φ x) ∂μ else 0, map_add' := ⋯,
      map_smul' := ⋯ }
-- Mathlib.GroupTheory.Congruence.BigOperators
Con.coe_finsuppProd : ∀ {ι : Type u_1} {β : Type u_2} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Zero β] (c : Con M) (h : ι → β → M)
  (f : ι →₀ β), ↑(f.prod h) = f.prod fun i b => ↑(h i b)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintParams.fromJson : Lean.Json → Except String Lean.Lsp.InlayHintParams
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto' : ∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [inst_2 : OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω}
  {μs : ι → MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs L (nhds μ) →
    ∀ {E : Set Ω}, ↑μ (frontier E) = 0 → Filter.Tendsto (fun i => ↑(μs i) E) L (nhds (↑μ E))
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.MinimalAxioms.inf_sSup_le_iSup_inf : ∀ {α : Type u} [inst : CompleteLattice α],
  Order.Frame.MinimalAxioms α → ∀ (a : α) (s : Set α), a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
-- Mathlib.Algebra.Group.Subgroup.Actions
/-- Note that this provides `IsScalarTower S G G` which is needed by `smul_mul_assoc`.  -/
Subgroup.instIsScalarTowerSubtypeMem : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst_1 : SMul α β] [inst_2 : MulAction G α]
  [inst_3 : MulAction G β] [IsScalarTower G α β] (S : Subgroup G), IsScalarTower (↥S) α β
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.LeanDiagnosticTag.unsolvedGoals.sizeOf_spec : sizeOf Lean.Lsp.LeanDiagnosticTag.unsolvedGoals = 1
-- Mathlib.RingTheory.Frobenius
/-- Let `G` be a finite group acting on `S`, `R` be the fixed subring, and `Q` be a prime of `S`
with finite residue field. This is an arbitrary choice of a Frobenius over `Q`. It is chosen so that
the Frobenius elements of `Q₁` and `Q₂` are conjugate if they lie over the same prime.  -/
arithFrobAt : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (G : Type u_3) →
            [inst_3 : Group G] →
              [inst_4 : MulSemiringAction G S] →
                [SMulCommClass G R S] →
                  (Q : Ideal S) → [Finite G] → [Algebra.IsInvariant R S G] → [Q.IsPrime] → [Finite (S ⧸ Q)] → G
-- Init.Data.Ord.Basic
Ordering.isGT_iff_eq_gt : ∀ {o : Ordering}, o.isGT = true ↔ o = Ordering.gt
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_subset : ∀ {α : Type u_2} [inst : One α] {s : Finset α}, 1 ⊆ s ↔ 1 ∈ s
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.iso.eq_1 : ∀ {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],
  IsLocalizedModule.iso S f =
    { toLinearMap := IsLocalizedModule.fromLocalizedModule S f,
      invFun := (Equiv.ofBijective ⇑(IsLocalizedModule.fromLocalizedModule S f) ⋯).invFun, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.incl_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : AdicCompletion I M) (n : ℕ), (AdicCompletion.incl I M) x n = ↑x n
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnriched_assoc_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ F₄ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₃ F₄]
  [inst_8 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₃]
  [inst_9 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₄]
  [inst_10 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₄] {Z : CategoryTheory.Functor J V}
  (h : CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₄ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₂ F₃)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₃ F₄)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₃)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₃ F₄))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₃ F₄)
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
        (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₂ F₃ F₄))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₄) h)
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.mem_valueGroup : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B) {b : Bˣ},
  ↑b ∈ Set.range ⇑f → b ∈ f.valueGroup
-- Mathlib.Order.Bounds.Basic
maximal_iff_isGreatest : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {a : α}, Maximal (fun x => x ∈ s) a ↔ IsGreatest s a
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instSeminormedAddCommGroupCarrier : (M : SemiNormedGrp₁) → SeminormedAddCommGroup M.carrier
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_inf : ∀ {M : Type u_1} [inst : AddMonoid M] (S T : AddSubmonoid M), (S ⊓ T).addUnits = S.addUnits ⊓ T.addUnits
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.bvar.injEq : ∀ (deBruijnIndex nargs deBruijnIndex_1 nargs_1 : ℕ),
  (Lean.Meta.RefinedDiscrTree.Key.bvar deBruijnIndex nargs =
      Lean.Meta.RefinedDiscrTree.Key.bvar deBruijnIndex_1 nargs_1) =
    (deBruijnIndex = deBruijnIndex_1 ∧ nargs = nargs_1)
-- Init.Data.Vector.Lemmas
Vector.set_set : ∀ {α : Type u_1} {n i : ℕ} (a : α) {b : α} {xs : Vector α n} (hi : i < n), (xs.set i a hi).set i b hi = xs.set i b hi
-- Init.Data.Array.Lemmas
Array.eq_of_mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ Array.replicate n a → b = a
-- Init.Prelude
/-- Sequences two `EStateM ε σ` actions, passing the returned value from the first into the second.
 -/
EStateM.bind : {ε σ α β : Type u} → EStateM ε σ α → (α → EStateM ε σ β) → EStateM ε σ β
-- Mathlib.RingTheory.DedekindDomain.Basic
/-- A Dedekind ring is a commutative ring that is Noetherian, integrally closed, and
has Krull dimension at most one.

This is exactly `IsDedekindDomain` minus the `IsDomain` hypothesis.

The integral closure condition is independent of the choice of field of fractions:
use `isDedekindRing_iff` to prove `IsDedekindRing` for a given `fraction_map`.
 -/
IsDedekindRing : (A : Type u_2) → [CommRing A] → Prop
-- Mathlib.GroupTheory.OrderOfElement
nsmulCoprime.eq_1 : ∀ {n : ℕ} {G : Type u_6} [inst : AddGroup G] (h : (Nat.card G).Coprime n),
  nsmulCoprime h =
    { toFun := fun g => n • g, invFun := fun g => (Nat.card G).gcdB n • g, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.nonneg : ∀ (x : ℝ), 0 ≤ x.smoothTransition