mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F` is initial, and `F ⋙ G` has a limit, then `G` has a limit also.

We can't make this an instance, because `F` is not determined by the goal.
(Even if this weren't a problem, it would cause a loop with `comp_hasLimit`.)
 -/
CategoryTheory.Functor.Initial.hasLimit_of_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} [CategoryTheory.Limits.HasLimit (F.comp G)], CategoryTheory.Limits.HasLimit G
-- Mathlib.RingTheory.Ideal.Operations
/-- **Alias** of the reverse direction of `Ideal.radical_eq_iff`.

---

An ideal is radical iff it is equal to its radical.  -/
Ideal.IsRadical.radical : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I.IsRadical → I.radical = I
-- Mathlib.Algebra.Homology.BifunctorShift
HomologicalComplex₂.shiftFunctor₁XXIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a x a' : ℤ) (h : a' = a + x) (b : ℤ),
  K.shiftFunctor₁XXIso a x a' h b = CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An induction principle for `ArchimedeanClass`  -/
ArchimedeanClass.ind : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  {motive : ArchimedeanClass M → Prop},
  (∀ (a : M), motive (ArchimedeanClass.mk a)) → ∀ (x : ArchimedeanClass M), motive x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constMinEntry?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.minEntry? t₁ = Std.DTreeMap.Raw.Const.minEntry? t₂
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `InvMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under inverses.  -/
InvMemClass : (S : Type u_3) → (G : outParam (Type u_4)) → [Inv G] → [SetLike S G] → Prop
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.mkImpCongr : Lean.Expr → Lean.Meta.Simp.Result → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Std.Data.TreeMap.Raw.Basic
/-- Well-formedness predicate for tree maps. Users of `TreeMap` will not need to interact with
this. Users of `TreeMap.Raw` will need to provide proofs of `WF` to lemmas and should use lemmas
like `WF.empty` and `WF.insert` (which are always named exactly like the operations they are about)
to show that map operations preserve well-formedness. The constructors of this type are internal
implementation details and should not be accessed by users.
 -/
Std.TreeMap.Raw.WF : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Prop
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_unitIso_hom_app_hom_app : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (X_1 : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A)
  (X_2 : (CategoryTheory.Over U)ᵒᵖ),
  (U.sheafEquivOver.unitIso.hom.app X_1).hom.app X_2 =
    X_1.obj.map (U.overEquivalence.unitIso.inv.app (Opposite.unop X_2)).op
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.mk_mem_interedges_iff : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s t : Finset α} {a b : α},
  (a, b) ∈ G.interedges s t ↔ a ∈ s ∧ b ∈ t ∧ G.Adj a b
-- Aesop.Stats.Basic
Aesop.enableStatsTracing : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → m Bool
-- Mathlib.Data.Matrix.Basic
Matrix.diagonalLinearMap_apply : ∀ (n : Type u_3) (R : Type u_7) (α : Type u_11) [inst : DecidableEq n] [inst_1 : Semiring R] [inst_2 : AddCommMonoid α]
  [inst_3 : Module R α] (a : n → α), (Matrix.diagonalLinearMap n R α) a = (↑(Matrix.diagonalAddMonoidHom n α)).toFun a
-- Init.Data.UInt.Bitwise
UInt64.xor_left_inj : ∀ {a b : UInt64} (c : UInt64), a ^^^ c = b ^^^ c ↔ a = b
-- Mathlib.RepresentationTheory.Maschke
LinearMap.conjugate_i : ∀ {k : Type u_1} [inst : CommRing k] {G : Type u_2} [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) (i : V →ₗ[MonoidAlgebra k G] W),
  (∀ (v : V), π (i v) = v) → ∀ (g : G) (v : V), (π.conjugate g) (i v) = v
-- Mathlib.NumberTheory.MahlerMeasure
/-- If an integer polynomial has Mahler measure equal to 1, then all its complex roots are integral
over ℤ.  -/
Polynomial.isIntegral_of_mahlerMeasure_eq_one : ∀ {p : Polynomial ℤ},
  (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 → ∀ {z : ℂ}, z ∈ p.aroots ℂ → IsIntegral ℤ z
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A trivial block is a `Set X` which is either a subsingleton or `univ`.

Note: It is not necessarily a block when the action is not by a group.  -/
MulAction.IsTrivialBlock : {X : Type u_2} → Set X → Prop
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- Maps the sources  -/
CategoryTheory.Dial.Hom.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] → {X Y : CategoryTheory.Dial C} → X.Hom Y → (X.src ⟶ Y.src)
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'_id : ∀ {n : ℕ} (x : Fin (n + 2)), SimplexCategory.II.map' OrderHom.id x = x
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F =
    CategoryTheory.coyoneda.mapIso (CategoryTheory.Limits.limitOpIsoOpColimit F).symm ≪≫
      CategoryTheory.preservesLimitIso CategoryTheory.coyoneda F.op
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.ext.inj : ∀ {ext₁? : Option Lean.Meta.SimpExtension} {ext₂? : Option Lean.Meta.Simp.SimprocExtension}
  {h : (ext₁?.isSome || ext₂?.isSome) = true} {ext₁?_1 : Option Lean.Meta.SimpExtension}
  {ext₂?_1 : Option Lean.Meta.Simp.SimprocExtension} {h_1 : (ext₁?_1.isSome || ext₂?_1.isSome) = true},
  Lean.Elab.Tactic.ResolveSimpIdResult.ext ext₁? ext₂? h =
      Lean.Elab.Tactic.ResolveSimpIdResult.ext ext₁?_1 ext₂?_1 h_1 →
    ext₁? = ext₁?_1 ∧ ext₂? = ext₂?_1
-- Mathlib.Data.Sign.Defs
SignType.le_neg_one_iff : ∀ {a : SignType}, a ≤ -1 ↔ a = -1
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : WithTop α),
  (a * b).untop₀ = a.untop₀ * b.untop₀
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.enorm_map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H)
  (x : TensorProduct 𝕜 E F), ‖(TensorProduct.map f.toLinearMap g.toLinearMap) x‖ₑ = ‖x‖ₑ
-- Mathlib.Algebra.Group.Action.Defs
/-- Let `Q / P / N / M` be a tower. If `P / N / M`, `Q / N / M` and `Q / P / N` are
scalar towers, then `Q / P / M` is also a scalar tower.
 -/
IsScalarTower.to₁₃₄ : ∀ (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [inst : SMul M N] [inst_1 : SMul M P]
  [inst_2 : SMul M Q] [inst_3 : SMul P Q] [inst_4 : Monoid N] [inst_5 : MulAction N P] [inst_6 : MulAction N Q]
  [IsScalarTower M N P] [IsScalarTower M N Q] [IsScalarTower N P Q], IsScalarTower M P Q
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurable_cylinderEvents_lambda : ∀ {α : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {mα : MeasurableSpace α} [m : (i : ι) → MeasurableSpace (X i)]
  (f : α → (i : ι) → X i), (∀ (i : ι), Measurable fun a => f a i) → Measurable f
-- Mathlib.Algebra.Group.Prod
/-- Given additive monoids `A`, `B`, the natural inclusion homomorphism
from `A` to `A × B`.  -/
AddMonoidHom.inl : (M : Type u_3) → (N : Type u_4) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M →+ M × N
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.Equiv.liftInner_stepAsHetT_bind_congr : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α₁ β α₂ : Type u_1} {γ : Type u_4} [inst : Monad m]
  [inst_1 : LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_6 : Std.Iterator α₁ m β] [inst_7 : Std.Iterator α₂ m β] {ita : Std.IterM m β} {itb : Std.IterM m β}
  {f : Std.IterStep (Std.IterM m β) β → Std.Iterators.HetT n γ}
  {g : Std.IterStep (Std.IterM m β) β → Std.Iterators.HetT n γ},
  ita.Equiv itb →
    (∀ (sa : Std.IterStep (Std.IterM m β) β),
        ita.stepAsHetT.Property sa →
          ∀ (sb : Std.IterStep (Std.IterM m β) β),
            itb.stepAsHetT.Property sb → sa.bundledQuotient = sb.bundledQuotient → f sa = g sb) →
      (Std.Iterators.HetT.liftInner n ita.stepAsHetT).bind f = (Std.Iterators.HetT.liftInner n itb.stepAsHetT).bind g
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_le : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
  {S : Subalgebra R A}, s ⊆ ↑S → Algebra.adjoin R s ≤ S
-- Init.Control.StateRef
StateRefT'.instMonadExceptOf : {ω σ : Type} → {m : Type → Type} → (ε : Type u_1) → [MonadExceptOf ε m] → MonadExceptOf ε (StateRefT' ω σ m)
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from rings to types preserves all limits. (That is, the underlying
types could have been computed instead as limits in the category of types.)
 -/
CommSemiRingCat.forget_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommSemiRingCat)
-- Mathlib.Algebra.Category.Ring.Under.Property
RingHom.HasStableEqualizers.preservesLimit_parallelPair_tensorProd : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.HasStableEqualizers fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B),
      P (CommRingCat.Hom.hom A.hom) →
        P (CommRingCat.Hom.hom B.hom) →
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (R.tensorProd S)
-- Lean.Elab.Match
Lean.Elab.Term.PatternVarDecl.mk.inj : ∀ {fvarId fvarId_1 : Lean.FVarId}, { fvarId := fvarId } = { fvarId := fvarId_1 } → fvarId = fvarId_1
-- Mathlib.Algebra.Module.Submodule.Defs
/-- Reinterpret a submodule as an additive subgroup.  -/
Submodule.toAddSubgroup : {R : Type u} →
  {M : Type v} → [inst : Ring R] → [inst_1 : AddCommGroup M] → {module_M : Module R M} → Submodule R M → AddSubgroup M
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsCardinalLocallyPresentable.toHasColimitsOfSize : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} (κ : Cardinal.{w}) {inst_1 : Fact κ.IsRegular}
  [self : CategoryTheory.IsCardinalLocallyPresentable C κ], CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.valuedCompletion_le_one_iff : ∀ {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ₀'] {K : Type u_7} [inst_2 : Field K] {v : Valuation K Γ₀}
  {w : Valuation K Γ₀'} (h : v.IsEquiv w) {x : v.Completion},
  Valued.v x ≤ 1 ↔ Valued.v ((UniformSpace.Completion.mapEquiv h.uniformEquiv) x) ≤ 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.size =
    if Std.DTreeMap.Internal.Impl.contains k t = true then t.size - 1 else t.size
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substInvOfIsUnit.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] (P P_1 : PowerSeries R) (e_P : P = P_1) (hP' : IsUnit ((PowerSeries.coeff 1) P))
  (a a_1 : Unit →₀ ℕ), a = a_1 → P.substInvOfIsUnit hP' a = P_1.substInvOfIsUnit ⋯ a_1
-- Mathlib.SetTheory.Descriptive.Tree
/-- Adjoint of `subAt`, given by pasting x before the root of T. Explicitly,
elements are prefixes of x or x with an element of T appended  -/
Descriptive.Tree.pullSub : {A : Type u_1} → ↥(Descriptive.tree A) → List A → ↥(Descriptive.tree A)
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- For a `V`-category `C`, construct the opposite `V`-category structure on the type `Cᵒᵖ`
using the braiding in `V`.  -/
CategoryTheory.EnrichedCategory.opposite : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      [CategoryTheory.BraidedCategory V] →
        (C : Type u) → [CategoryTheory.EnrichedCategory V C] → CategoryTheory.EnrichedCategory V Cᵒᵖ
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `hasFiniteSupport_of_finsum_ne_zero`. -/
finite_support_of_finsum_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M}, ∑ᶠ (i : α), f i ≠ 0 → Function.HasFiniteSupport f
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.IterM.step_drop.match_3.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Batteries.Data.UnionFind.Basic
Batteries.UFNode.mk.sizeOf_spec : ∀ (parent rank : ℕ), sizeOf { parent := parent, rank := rank } = 1 + sizeOf parent + sizeOf rank
-- Mathlib.GroupTheory.Subgroup.Simple
AddSubgroup.Normal.eq_bot_or_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] [IsSimpleAddGroup G] {H : AddSubgroup G}, H.Normal → H = ⊥ ∨ H = ⊤
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. A version for `ℝ`-valued functions.
For an alternative version, convenient if the infinite sums are already expressed as `p`-th powers,
see `inner_le_Lp_mul_Lq_hasSum_of_nonneg`.  -/
Real.summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p q : ℝ},
  p.HolderConjugate q →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) →
          (Summable fun i => g i ^ q) →
            (Summable fun i => f i * g i) ∧
              ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- If there is an absolute upper bound on the size of a set satisfying `P`, then the
maximal subset property always holds.  -/
Matroid.existsMaximalSubsetProperty_of_bdd : ∀ {α : Type u_1} {P : Set α → Prop},
  (∃ n, ∀ (Y : Set α), P Y → Y.encard ≤ ↑n) → ∀ (X : Set α), Matroid.ExistsMaximalSubsetProperty P X
-- Mathlib.Order.Notation
Min.ext_iff : ∀ {α : Type u} {x y : Min α}, x = y ↔ min = min
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.MagmaCat.Hom.mk : {A B : MagmaCat} → (↑A →ₙ* ↑B) → A.Hom B
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- The isomorphism `(ofCocone c).obj ⟨j, _⟩ ≅ c.pt`.  -/
CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIsoPt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} →
          {F : CategoryTheory.Functor (↑(Set.Iio j)) C} →
            (c : CategoryTheory.Limits.Cocone F) → (CategoryTheory.SmallObject.SuccStruct.ofCocone c).obj ⟨j, ⋯⟩ ≅ c.pt
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.slope_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  x₁ = x₂ → y₁ = W.negY x₂ y₂ → W.slope x₁ x₂ y₁ y₂ = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.powerRevlex.eq_1 : ∀ (k₁ k₂ : ℕ),
  Lean.Grind.CommRing.powerRevlex k₁ k₂ =
    bif k₁.blt k₂ then Ordering.gt else bif k₂.blt k₁ then Ordering.lt else Ordering.eq
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.instMulOneClass.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.Coprod.instMulOneClass =
    { one := Monoid.Coprod.instMulOneClass._aux_1, mul := Monoid.Coprod.instMulOneClass._aux_3, one_mul := ⋯,
      mul_one := ⋯ }
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist_le_inv_nat_succ : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  (uniformity α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 ≤ 1 / (↑n + 1)}
-- Batteries.Recycling.RBTree.Basic
/-- The resulting tree is well formed.  -/
RBTree.RBSet.ModifyWF.wf : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp} {cut : α → Ordering} {f : α → α}
  [self : t.ModifyWF cut f], RBTree.RBNode.WF cmp (RBTree.RBNode.modify cut f ↑t)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_inf_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Injective ⇑f →
    ∀ (S T : AddSubsemigroup M), AddSubsemigroup.comap f (AddSubsemigroup.map f S ⊓ AddSubsemigroup.map f T) = S ⊓ T
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.frobeniusMorphism.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {A B : C} (f : A ⟶ B)
  (A' : CategoryTheory.Subobject A) (B' : CategoryTheory.Subobject B),
  CategoryTheory.Regular.frobeniusMorphism f A' B' =
    ⋯.lift
      (CategoryTheory.CategoryStruct.comp
        ((A' ⊓ (CategoryTheory.Subobject.pullback f).obj B').ofLE ((CategoryTheory.Subobject.pullback f).obj B') ⋯)
        (CategoryTheory.Subobject.pullbackπ f B'))
      (CategoryTheory.CategoryStruct.comp ((A' ⊓ (CategoryTheory.Subobject.pullback f).obj B').ofLE A' ⋯)
        (CategoryTheory.Subobject.imageFactorisation f A').F.e)
      ⋯
-- Mathlib.Order.Atoms
/-- A simple `BoundedOrder` is also a `BooleanAlgebra`.  -/
IsSimpleOrder.booleanAlgebra : {α : Type u_4} → [DecidableEq α] → [inst : Lattice α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → BooleanAlgebra α
-- Mathlib.Algebra.CharP.Two
CharTwo.range_natCast : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharP R 2], Set.range Nat.cast = {0, 1}
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- The Lie algebra morphism from Lie derivations into linear endomorphisms.  -/
LieDerivation.toLinearMapLieHom : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieDerivation R L L →ₗ⁅R⁆ L →ₗ[R] L
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getEntry.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (e_a : a = a_1) (l l_1 : Std.DHashMap.Internal.AssocList α β)
  (e_l : l = l_1) (a_2 : Std.DHashMap.Internal.AssocList.contains a l = true),
  Std.DHashMap.Internal.AssocList.getEntry a l a_2 = Std.DHashMap.Internal.AssocList.getEntry a_1 l_1 ⋯
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
continuous_from_compactlyGenerated : ∀ {X : Type w} {Y : Type x} [inst : TopologicalSpace X] [t : TopologicalSpace Y] (f : X → Y),
  (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousHull.gc : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜],
  GaloisConnection (Ideal.homogeneousHull 𝒜) HomogeneousIdeal.toIdeal
-- Mathlib.Analysis.SpecialFunctions.Exponential
differentiable_exp_smul_const : ∀ (𝕂 : Type u_1) {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
  (x : 𝔸), Differentiable 𝕂 fun t => NormedSpace.exp (t • x)
-- Mathlib.Order.SupClosed
compl_image_latticeClosure : ∀ {α : Type u_3} [inst : BooleanAlgebra α] (s : Set α), compl '' latticeClosure s = latticeClosure (compl '' s)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.succ_zero : Order.succ 0 = 1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.monoidalCategoryStruct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
      CategoryTheory.MonoidalCategoryStruct (PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)))
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalGrind : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtension_iff_precomp : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (F' : CategoryTheory.Functor D H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (α : L.comp F' ⟶ F),
  F'.IsRightKanExtension α ↔
    F'.IsRightKanExtension (CategoryTheory.CategoryStruct.comp (G.associator L F').hom (G.whiskerLeft α))
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_conj : ∀ (x : ℂ), Complex.tan ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.tan x)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.subset_normalClosure : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, s ⊆ ↑(AddSubgroup.normalClosure s)
-- Init.Data.List.Basic
/-- Extracts the first `n` elements of `xs`, or the whole list if `n` is greater than `xs.length`.

`O(min n |xs|)`.

Examples:
* `[a, b, c, d, e].take 0 = []`
* `[a, b, c, d, e].take 3 = [a, b, c]`
* `[a, b, c, d, e].take 6 = [a, b, c, d, e]`
 -/
List.take : {α : Type u} → ℕ → List α → List α
-- Batteries.Lean.Except
/-- Map a function over an `Except` value, using a proof that the value is `.ok`.  -/
Except.pmap : {ε : Type u} → {α β : Type v} → (x : Except ε α) → ((a : α) → x = Except.ok a → β) → Except ε β
-- Mathlib.LinearAlgebra.Projection
LinearMap.isProj_range_iff_isIdempotentElem : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] (f : M →ₗ[S] M),
  LinearMap.IsProj f.range f ↔ IsIdempotentElem f
-- Lean.Elab.DeclModifiers
Lean.Elab.instInhabitedRecKind : Inhabited Lean.Elab.RecKind
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_id : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G},
  groupHomology.chainsMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.id A) =
    CategoryTheory.CategoryStruct.id (groupHomology.inhomogeneousChains A)