mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.antipode_right : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) [self : CategoryTheory.HopfObj X],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.HopfObj.antipode)
        CategoryTheory.MonObj.mul) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
/-- Let `M, N` be `R`-modules, `m ≤ M` be an `R`-submodule. Then we have a linear isomorphism between
tensor products of the quotient and the quotient of the tensor product:
`(M ⧸ m) ⊗[R] N ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N)`.
 -/
TensorProduct.quotientTensorEquiv : {R : Type u_1} →
  {M : Type u_2} →
    (N : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                (m : Submodule R M) →
                  TensorProduct R (M ⧸ m) N ≃ₗ[R] TensorProduct R M N ⧸ (TensorProduct.map m.subtype LinearMap.id).range
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- Part of an `sl₂` triple used in Geck's construction of a Lie algebra from a root system.  -/
RootPairing.GeckConstruction.e : {ι : 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] →
                  {P : RootPairing ι R M N} →
                    [P.IsCrystallographic] →
                      {b : P.Base} →
                        [Finite ι] →
                          [IsDomain R] → [CharZero R] → ↥b.support → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
-- Mathlib.Algebra.Module.LocalizedModule.Away
IsLocalizedModule.Away.mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N} {r : R},
  IsUnit ((algebraMap R (Module.End R N)) r) →
    (∀ (x : N), ∃ n y, r ^ n • x = f y) →
      (∀ (x y : M), f x = f y → ∃ n, r ^ n • x = r ^ n • y) → IsLocalizedModule.Away r f
-- Mathlib.Order.KrullDimension
Order.krullDim_of_isSimpleOrder : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], Order.krullDim α = 1
-- Mathlib.Logic.Equiv.Set
Equiv.Set.insert_symm_apply_inr : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a : α} (H : a ∉ s) (b : PUnit.{u + 1}),
  (Equiv.Set.insert H).symm (Sum.inr b) = ⟨a, ⋯⟩
-- Mathlib.Topology.Algebra.Star
ContinuousOn.star : ∀ {α : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R]
  [inst_3 : TopologicalSpace α] {f : α → R} {s : Set α}, ContinuousOn f s → ContinuousOn (fun x => star (f x)) s
-- Std.Http.Internal.LowerCase
/-- Proof that applying `toLower` to any string results in a string that satisfies the `IsLowerCase`
predicate.
 -/
Std.Http.Internal.IsLowerCase.isLowerCase_toLower : ∀ {s : String}, Std.Http.Internal.IsLowerCase s.toLower
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.mkOffsetPattern : Lean.Expr → ℕ → Lean.Expr
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map_id : ∀ {α : Type u} (s : Stream'.WSeq α), Stream'.WSeq.map id s = s
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.IsIntegral.component_integral : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty ↥↑U],
  IsDomain ↑(X.presheaf.obj (Opposite.op U))
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom) →
    (Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom) →
      (Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom) →
        (Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom) →
          (Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.Mor₁ → Lean.Expr → m Mathlib.Tactic.BicategoryLike.CoherenceHom) →
            (Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
              (Mathlib.Tactic.BicategoryLike.Mor₁ →
                  Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                (Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                    Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                  (Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                      Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                    (Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                      (Mathlib.Tactic.BicategoryLike.CoherenceHom →
                          Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                            Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
                        Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.comp : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} {t : ι → Ω → ι},
  MeasureTheory.IsProgressive f u →
    MeasureTheory.IsProgressive f t →
      (∀ (i : ι) (ω : Ω), t i ω ≤ i) → MeasureTheory.IsProgressive f fun i ω => u (t i ω) ω
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int8.intCast_neg : ∀ (i : ℤ), ↑(-i) = -↑i
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.instNoZeroDivisors : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R], NoZeroDivisors (MvPolynomial σ R)
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformly_congr_inseparable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {F' : ι → α → β},
  (∀ᶠ (x : ι) in p, ∀ (y : α), Inseparable (F x y) (F' x y)) → (TendstoUniformly F f p ↔ TendstoUniformly F' f p)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.coe_mem_principalUnitGroup_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) {x : ↥A.unitGroup},
  ↑x ∈ A.principalUnitGroup ↔ A.unitGroupMulEquiv x ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.mk : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    {S : AlgebraicGeometry.Scheme} →
      {J : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
            {𝒰 : S.OpenCover} →
              [inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀] →
                [inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                  (cocone :
                      (i : 𝒰.I₀) →
                        CategoryTheory.Limits.Cocone
                          (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))) →
                    ((i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (cocone i)) →
                      (∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)) →
                        AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNormEssSup_eq_essSup_enorm : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] (f : α → ε) (μ : MeasureTheory.Measure α),
  MeasureTheory.eLpNormEssSup f μ = essSup (fun x => ‖f x‖ₑ) μ
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.ae_withDensity_iff_ae_restrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {f : α → ENNReal},
  Measurable f → ((∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, p x)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.kernelSequence_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.kernelSequence f).X₁ = CategoryTheory.Limits.kernel f
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- A reflexive quiver generates a free category, defined as a quotient of the free category
on its underlying quiver (called the "path category") by the hom relation that uses the specified
reflexivity arrows as the identity arrows.  -/
CategoryTheory.Cat.FreeRefl : (V : Type u_1) → [CategoryTheory.ReflQuiver V] → Type u_1
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux_one : ∀ (n : ℕ), Equiv.Perm.signAux 1 = 1
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] {A : Type u'}
  [inst_3 : CategoryTheory.Category.{v', u'} A] [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P =
    (CategoryTheory.Limits.colimit.isColimit
          (((CategoryTheory.Functor.whiskeringLeft
                    (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).fiber.Elementsᵒᵖ Cᵒᵖ A).obj
                (CategoryTheory.CategoryOfElements.π
                    (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).fiber).op).obj
            P)).coconePointUniqueUpToIso
      (CategoryTheory.Limits.colimitOfDiagramTerminal
        (CategoryTheory.Limits.IsInitial.op (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj (Opposite.op (⊤_ C))).Elements
          (CategoryTheory.Functor.Elements.isInitialOfCorepresentableBy
            (CategoryTheory.shrinkCoyonedaCorepresentableBy (Opposite.op (⊤_ C)))))
        (((CategoryTheory.Functor.whiskeringLeft
                  (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).fiber.Elementsᵒᵖ Cᵒᵖ A).obj
              (CategoryTheory.CategoryOfElements.π
                  (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).fiber).op).obj
          P))
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.eqToIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n m : ℕ} (h : n = m),
  X.eqToIso h = CategoryTheory.Functor.mapIso X (CategoryTheory.eqToIso ⋯)
-- Std.Time.Format.Modifier
/-- Ante meridiem (before noon)
 -/
Std.Time.DayPeriod.am : Std.Time.DayPeriod
-- Mathlib.Algebra.Group.Commute.Basic
SemiconjBy.function_semiconj_mul_right_swap : ∀ {G : Type u_1} [inst : Semigroup G] {a b c : G},
  SemiconjBy a b c → Function.Semiconj (fun x => x * a) (fun x => x * c) fun x => x * b
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.nonempty : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω), Nonempty Ω
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk'_mem_incidenceSet_right_iff : ∀ {V : Type u} (G : SimpleGraph V) {a b : V}, s(a, b) ∈ G.incidenceSet b ↔ G.Adj a b
-- Lean.Environment
Lean.ImportM.Context.mk.injEq : ∀ (env : Lean.Environment) (opts : Lean.Options) (env_1 : Lean.Environment) (opts_1 : Lean.Options),
  ({ env := env, opts := opts } = { env := env_1, opts := opts_1 }) = (env = env_1 ∧ opts = opts_1)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_nat_lt : ∀ {n : ℕ} {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ k < n, p k), Nat.find ⋯ = ↑(Fin.find (fun x => p ↑x) ⋯)
-- Mathlib.RingTheory.Algebraic.Basic
/-- An element of `R` is algebraic, when viewed as an element of the `R`-algebra `A`.  -/
isAlgebraic_algebraMap : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R] (x : R),
  IsAlgebraic R ((algebraMap R A) x)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat.sizeOf_spec : ∀ (e thm : Lean.Expr) (d : ℕ) (a : Int.Internal.Linear.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat e thm d a) =
    1 + sizeOf e + sizeOf thm + sizeOf d + sizeOf a
-- Mathlib.Data.Multiset.Sort
Multiset.sort_zero : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r]
  [inst_3 : Std.Total r], Multiset.sort 0 r = []
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} {g : G → E} {t : Set G},
  DiffContOnCl 𝕜 f s → DiffContOnCl 𝕜 g t → Set.MapsTo g t s → DiffContOnCl 𝕜 (f ∘ g) t
-- Mathlib.Topology.Compactness.Compact
compactSpace_generateFrom' : ∀ {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)},
  T = TopologicalSpace.generateFrom S →
    (∀ (ι : Type u) (U : ι → ↑S), ⋃ i, ↑(U i) = Set.univ → ∃ J, J.Finite ∧ ⋃ i ∈ J, ↑(U i) = Set.univ) → CompactSpace X
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.eventually_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [ClosedIicTopology β],
  Asymptotics.IsEquivalent l u v → (∀ᶠ (t : α) in l, 0 < v t) → ∀ᶠ (x : α) in l, 0 < u x
-- Init.Data.Vector.Range
Vector.mem_range'_1 : ∀ {s n m : ℕ}, m ∈ Vector.range' s n ↔ s ≤ m ∧ m < s + n
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMul.of_le : ∀ {𝕜 : 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 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {m n : WithTop ℕ∞},
  m ≤ n → ∀ [h : ContMDiffMul I n G], ContMDiffMul I m G
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : N ≃+ P} (x : M), (f.ofAddEquivOfLocalizations k) x = k (f x)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_top : ∀ {V : Type u_1} {W : Type u_2} {f : V → W},
  Function.Injective f → SimpleGraph.comap f (SimpleGraph.completeGraph W) = SimpleGraph.completeGraph V
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_le_of_sum_range_le : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : TopologicalSpace α] {c : α}
  [ClosedIicTopology α] {f : ℕ → α}, Summable f → (∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) → ∑' (n : ℕ), f n ≤ c
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_uIoc : ∀ (x y : NNReal), NNReal.toReal '' Set.uIoc x y = Set.uIoc ↑x ↑y
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_string_add : ∀ {s : String} {p : String.Pos.Raw}, (s + p).byteIdx = s.utf8ByteSize + p.byteIdx
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.addUnit_of_mem_ofAddUnits_spec_val_eq_of_mem : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ S.ofAddUnits),
  ↑(S.addUnit_of_mem_ofAddUnits h) = x
-- Mathlib.Analysis.Convex.Exposed
IsExposed.isCompact : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] [OrderClosedTopology 𝕜] [T2Space E]
  {A B : Set E}, IsExposed 𝕜 A B → IsCompact A → IsCompact B
-- Mathlib.Algebra.Group.Hom.Defs
map_ne_zero_iff : ∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : Zero R] [inst_1 : Zero S] [inst_2 : FunLike F R S]
  [ZeroHomClass F R S] (f : F), Function.Injective ⇑f → ∀ {x : R}, f x ≠ 0 ↔ x ≠ 0
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.perpBisector_eq_top : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P}, AffineSubspace.perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂
-- Mathlib.Algebra.Azumaya.Defs
IsAzumaya.toFinite : ∀ {R : Type u_1} {A : Type u_2} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  [self : IsAzumaya R A], Module.Finite R A
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_pow : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  (a : M) {n : ℕ}, n ≠ 0 → UniqueFactorizationMonoid.radical (a ^ n) = UniqueFactorizationMonoid.radical a
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Transfer `CompletelyDistribLattice` across an `Equiv`.  -/
Equiv.completelyDistribLattice : {α : Type u} → {β : Type v} → α ≃ β → [CompletelyDistribLattice β] → CompletelyDistribLattice α
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- An internally-graded `R`-algebra `A` is one that can be decomposed into a collection
of `Submodule R A`s indexed by `ι` such that the canonical map `A → ⨁ i, 𝒜 i` is bijective and
respects multiplication, i.e. the product of an element of degree `i` and an element of degree `j`
is an element of degree `i + j`.

Note that the fact that `A` is internally-graded, `GradedAlgebra 𝒜`, implies an externally-graded
algebra structure `DirectSum.GAlgebra R (fun i ↦ ↥(𝒜 i))`, which in turn makes available an
`Algebra R (⨁ i, 𝒜 i)` instance.
 -/
GradedRing : {ι : Type u_1} →
  {A : Type u_3} →
    {σ : Type u_4} →
      [DecidableEq ι] →
        [AddMonoid ι] →
          [inst : Semiring A] → [inst_1 : SetLike σ A] → [AddSubmonoidClass σ A] → (ι → σ) → Type (max u_1 u_3)
-- Mathlib.Data.Prod.TProd
List.TProd.elim_of_mem : ∀ {ι : Type u} {α : ι → Type v} {i j : ι} {l : List ι} [inst : DecidableEq ι],
  (i :: l).Nodup → ∀ (hj : j ∈ l) (v : List.TProd α (i :: l)), v.elim ⋯ = List.TProd.elim v.2 hj
-- Lean.Expr
Lean.MVarIdSet : Type
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_add_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (m : ℤ),
  Int.fract (a + ↑m) = Int.fract a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.State.mk.sizeOf_spec : ∀ (vars : Lean.PArray Lean.Expr) (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (vars' : Lean.PArray Lean.Expr) (varMap' : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (natToIntMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr))
  (natDef : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var)
  (dvds : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr))
  (lowers uppers : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr))
  (diseqs : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr))
  (elimEqs : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) (elimStack : List Int.Internal.Linear.Var)
  (occurs : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet) (assignment : Lean.PArray ℚ) (nextCnstrId : ℕ)
  (caseSplits : Bool) (steps : ℕ) (conflict? : Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof)
  (diseqSplits : Lean.PHashMap Int.Internal.Linear.Poly Lean.FVarId) (divMod : Lean.PHashSet (Lean.Expr × ℤ))
  (toIntIds : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (toIntInfos : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo)
  (toIntTermMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo)
  (toIntVarMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr) (usedCommRing : Bool)
  (nonlinearOccs : Lean.PHashMap Int.Internal.Linear.Var (List Int.Internal.Linear.Var)),
  sizeOf
      { vars := vars, varMap := varMap, vars' := vars', varMap' := varMap', natToIntMap := natToIntMap,
        natDef := natDef, dvds := dvds, lowers := lowers, uppers := uppers, diseqs := diseqs, elimEqs := elimEqs,
        elimStack := elimStack, occurs := occurs, assignment := assignment, nextCnstrId := nextCnstrId,
        caseSplits := caseSplits, steps := steps, conflict? := conflict?, diseqSplits := diseqSplits, divMod := divMod,
        toIntIds := toIntIds, toIntInfos := toIntInfos, toIntTermMap := toIntTermMap, toIntVarMap := toIntVarMap,
        usedCommRing := usedCommRing, nonlinearOccs := nonlinearOccs } =
    1 + sizeOf vars + sizeOf varMap + sizeOf vars' + sizeOf varMap' + sizeOf natToIntMap + sizeOf natDef + sizeOf dvds +
                                          sizeOf lowers +
                                        sizeOf uppers +
                                      sizeOf diseqs +
                                    sizeOf elimEqs +
                                  sizeOf elimStack +
                                sizeOf occurs +
                              sizeOf assignment +
                            sizeOf nextCnstrId +
                          sizeOf caseSplits +
                        sizeOf steps +
                      sizeOf conflict? +
                    sizeOf diseqSplits +
                  sizeOf divMod +
                sizeOf toIntIds +
              sizeOf toIntInfos +
            sizeOf toIntTermMap +
          sizeOf toIntVarMap +
        sizeOf usedCommRing +
      sizeOf nonlinearOccs
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the reverse direction of `Order.le_pred_iff_isMin`. -/
IsMin.le_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, IsMin a → a ≤ Order.pred a
-- Mathlib.GroupTheory.Congruence.Defs
/-- The supremum of additive congruence relations `c, d` equals the
smallest additive congruence relation containing the binary relation '`x` is related to `y`
by `c` or `d`'.  -/
AddCon.sup_eq_addConGen : ∀ {M : Type u_1} [inst : Add M] (c d : AddCon M), c ⊔ d = addConGen fun x y => c x y ∨ d x y
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) → [CategoryTheory.CreatesLimits F.unop] → CategoryTheory.CreatesColimits F
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The isomorphism `Y ⨿[X] Z ≅ Z ⨿[X] Y`.  -/
CategoryTheory.Limits.pushoutSymmetry : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasPushout f g] →
            CategoryTheory.Limits.pushout f g ≅ CategoryTheory.Limits.pushout g f
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instMonoidHomClass : ∀ (M : Type u_4) [inst : MulOne M], MonoidHomClass (Monoid.End M) M M
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- The basis is currently just a list. If this is a performance bottleneck, we should use
a better data-structure. For examples, we could use a simple indexing for the linear case
where we map variable in the leading monomial to `EqCnstr`.
 -/
Lean.Meta.Grind.Arith.CommRing.CommRing.basis : Lean.Meta.Grind.Arith.CommRing.CommRing → List Lean.Meta.Grind.Arith.CommRing.EqCnstr
-- Init.Data.SInt.Lemmas
Int32.lt_irrefl : ∀ {a : Int32}, ¬a < a