mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.forget_createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat),
  AddMonCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c t =>
      have this := ⋯;
      {
        liftedCone :=
          {
            pt :=
              AddMonCat.of (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt,
            π := { app := fun j => AddMonCat.ofHom (AddMonCat.limitπAddMonoidHom F j), naturality := ⋯ } },
        validLift :=
          CategoryTheory.Limits.Cone.ext
            ((CategoryTheory.Limits.Types.isLimitEquivSections t).trans
                  (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections)).symm.toIso
            ⋯,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget AddMonCat)
            (CategoryTheory.Limits.Types.Small.limitConeIsLimit (F.comp (CategoryTheory.forget AddMonCat)))
            (fun s =>
              AddMonCat.ofHom
                {
                  toFun :=
                    ⇑(CategoryTheory.ConcreteCategory.hom
                        ((CategoryTheory.Limits.Types.Small.limitConeIsLimit
                              (F.comp (CategoryTheory.forget AddMonCat))).lift
                          ((CategoryTheory.forget AddMonCat).mapCone s))),
                  map_zero' := ⋯, map_add' := ⋯ })
            ⋯ }
-- Lean.Util.NumObjs
Lean.Expr.NumObjs.M : Type → Type
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : CategoryTheory.Grp C), (CategoryTheory.Grp.forget C).obj X = X.X
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.toZModPow : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] {n : ℕ}
  [inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L),
  (PadicInt.toZModPow n) ↑((cyclotomicCharacter L p) g) = ↑((modularCyclotomicCharacter L ⋯) g)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.

More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
`L` if it exists, and `0` otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum
over the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. Similar remarks
apply to more general summation filters.)
 -/
tsum : {α : Type u_4} →
  {β : Type u_5} →
    [AddCommMonoid α] →
      [TopologicalSpace α] → (β → α) → optParam (SummationFilter β) (SummationFilter.unconditional β) → α
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_trans_to_affineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : AddCommGroup V₃]
  [inst_4 : Module k V₁] [inst_5 : Module k V₂] [inst_6 : Module k V₃] [inst_7 : AddTorsor V₁ P₁]
  [inst_8 : AddTorsor V₂ P₂] [inst_9 : AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃),
  ↑(e.trans e') = (↑e').comp ↑e
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instReprRange.repr : Lean.Lsp.Range → ℕ → Std.Format
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_uniq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
  (H :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))
  (l : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp l f = g → l = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Right multiplication by a unit of a semiring as a linear equivalence.  -/
Units.mulRightLinearEquiv : (R : Type u_9) →
  {A : Type u_10} →
    [inst : Semiring R] → [inst_1 : Semiring A] → [inst_2 : Module R A] → [IsScalarTower R A A] → Aˣ → A ≃ₗ[R] A
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.natCast : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (n : ℕ), WittVector.mapFun ⇑f ↑n = ↑n
-- Init.Data.Array.Basic
Array.size_pop : ∀ {α : Type u} {xs : Array α}, xs.pop.size = xs.size - 1
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.add_smul : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] [inst_4 : AddCommMonoid V] [inst_5 : AddCommMonoid R]
  [inst_6 : SMulWithZero R V] {x y : HahnSeries Γ R} {z : HahnModule Γ' R V},
  (∀ (r s : R) (u : V), (r + s) • u = r • u + s • u) → (x + y) • z = x • z + y • z
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.abs_abs : ∀ {R : Type u} [inst : CommRing R] [inst_1 : LinearOrder R] [AddLeftMono R] {x y : R}, IsCoprime x y → IsCoprime |x| |y|
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_coe_finset : ∀ {α : Type u} {s : Finset α}, Cardinal.mk ↥s = ↑s.card
-- Mathlib.Probability.Process.Predictable
/-- A process is said to be predictable if it is measurable with respect to the predictable
σ-algebra.  -/
MeasureTheory.IsStronglyPredictable : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      {E : Type u_3} →
        [TopologicalSpace E] → [inst : Preorder ι] → [OrderBot ι] → MeasureTheory.Filtration ι m → (ι → Ω → E) → Prop
-- Mathlib.GroupTheory.Exponent
AddMonoid.exp_eq_one_of_subsingleton : ∀ {G : Type u} [inst : AddMonoid G] [hs : Subsingleton G], AddMonoid.exponent G = 1
-- Init.Data.Order.Classes
Std.IsLinearOrder.toIsPartialOrder : ∀ {α : Type u} {inst : LE α} [self : Std.IsLinearOrder α], Std.IsPartialOrder α
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.hasCompileError : Lean.Environment → Lean.Name → Bool
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.isIdRestFast : Char → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (iso : E ≃L[𝕜] F), fderiv 𝕜 (⇑iso) x = ↑iso
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂_functor : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF).functor = F.comp eB.inverse
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The monoidal functor from a monoidal category `C` to
its localization `LocalizedMonoidal L W ε`.  -/
CategoryTheory.Localization.Monoidal.toMonoidalCategory : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      CategoryTheory.Functor C (CategoryTheory.LocalizedMonoidal L W ε)
-- Lean.Expr
Lean.Expr.bvar.inj : ∀ {deBruijnIndex deBruijnIndex_1 : ℕ},
  Lean.Expr.bvar deBruijnIndex = Lean.Expr.bvar deBruijnIndex_1 → deBruijnIndex = deBruijnIndex_1
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.mem_unop : ∀ {M : Type u_2} [inst : Mul M] {x : M} {S : Subsemigroup Mᵐᵒᵖ}, x ∈ S.unop ↔ MulOpposite.op x ∈ S
-- Mathlib.Tactic.WLOG
/-- The result of running `wlog` on a goal.  -/
Mathlib.Tactic.WLOGResult : Type
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- The right adjoint of a triangulated functor is triangulated.
 -/
CategoryTheory.Adjunction.isTriangulated_rightAdjoint : ∀ {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.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [inst_12 : F.CommShift ℤ] [inst_13 : G.CommShift ℤ] [adj.CommShift ℤ] [F.IsTriangulated],
  G.IsTriangulated
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.UniversallyInjective.universally_injective : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.UniversallyInjective f],
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x =>
        Function.Injective x).universally
    f
-- Mathlib.Data.List.Shortlex
/-- Given a relation `r` on `α`, the shortlex order on `List α`, for which
`[a0, ..., an] < [b0, ..., b_k]` if `n < k` or `n = k` and `[a0, ..., an] < [b0, ..., bk]`
under the lexicographic order induced by `r`.  -/
List.Shortlex : {α : Type u_1} → (α → α → Prop) → List α → List α → Prop
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.liftWith_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  (f : ({β : Type u} → ExceptT ε m β → m (Except ε β)) → m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred),
  ⦃ Std.Internal.Do.wp (f fun {β} x => x.run) post epost.tail ⦄ MonadControl.liftWith f ⦃ post; epost ⦄
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVAdd_zero : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁], AffineEquiv.constVAdd k P₁ 0 = AffineEquiv.refl k P₁
-- Mathlib.Algebra.Star.StarRingHom
/-- Helper instance for cases where the inference via `EquivLike` is too hard.  -/
StarRingEquiv.instFunLike : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Add A] →
      [inst_1 : Add B] →
        [inst_2 : Mul A] → [inst_3 : Mul B] → [inst_4 : Star A] → [inst_5 : Star B] → FunLike (A ≃⋆+* B) A B
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.addHaarMeasure_apply : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} {s : Set G},
  MeasurableSet s →
    (MeasureTheory.Measure.addHaarMeasure K₀) s =
      (MeasureTheory.Measure.haar.addHaarContent K₀).outerMeasure s /
        (MeasureTheory.Measure.haar.addHaarContent K₀).measure ↑K₀
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_subset_Icc_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico b a ⊆ Set.Icc b a
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.sub_one_pos : ∀ {p q : NNReal}, p.HolderConjugate q → 0 < p - 1
-- Std.Async.ContextAsync
/-- Runs all computations concurrently and returns the first result. Each computation runs in its own child context;
when the first completes successfully, all others are cancelled immediately.
 -/
Std.Async.ContextAsync.raceAll : {c : Type u_1} →
  {α : Type} →
    [ForM Std.Async.ContextAsync c (Std.Async.ContextAsync α)] →
      c → optParam Task.Priority Task.Priority.default → Std.Async.ContextAsync α
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.rename.sizeOf_spec : ∀ (a : Lean.Lsp.RenameFile), sizeOf (Lean.Lsp.DocumentChange.rename a) = 1 + sizeOf a
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorems.mk.injEq : ∀
  (theorems theorems_1 :
    Std.TreeMap Lean.Name (Std.TreeMap Lean.Name (Array Mathlib.Meta.FunProp.FunctionTheorem) Lean.Name.quickCmp)
      Lean.Name.quickCmp),
  ({ theorems := theorems } = { theorems := theorems_1 }) = (theorems = theorems_1)
-- Mathlib.Data.Num.ZNum
Num.toZNum.eq_1 : Num.zero.toZNum = 0
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- A noncomputable way to get a monotone collection of sets that span `univ` and have finite
measure using `Classical.choose`. This definition satisfies monotonicity in addition to all other
properties in `SigmaFinite`.  -/
MeasureTheory.spanningSets : {α : Type u_1} → {m0 : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [MeasureTheory.SigmaFinite μ] → ℕ → Set α
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.frequently_iff_eventually : ∀ {α : Type u} {f : Ultrafilter α} {p : α → Prop}, (∃ᶠ (x : α) in ↑f, p x) ↔ ∀ᶠ (x : α) in ↑f, p x
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_add_im : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : AddGroup R], ↑a.re + a.im = a
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- The option `linter.style.induction` of the deprecated syntax linter flags usages of
the `induction'` tactic, which is a backward-compatible version of Lean 3's `induction` tactic.
Unlike Lean 4's `induction`, variables introduced by `induction'` are not
required to be separated by case, which hinders readability.
 -/
Mathlib.Linter.Style.linter.style.induction : Lean.Option Bool
-- Mathlib.RingTheory.Jacobson.Semiprimary
isSemiprimaryRing_iff : ∀ (R : Type u_1) [inst : Ring R],
  IsSemiprimaryRing R ↔ IsSemisimpleRing (R ⧸ Ring.jacobson R) ∧ IsNilpotent (Ring.jacobson R)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.eval₂_C_mul_T : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] (f : R →+* S) (x : Sˣ) (r : R)
  (n : ℤ), (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.C r * LaurentPolynomial.T n) = f r * ↑(x ^ n)
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.rectVandermonde.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {α : Type u_3} (v w : α → R) (n : ℕ),
  Matrix.rectVandermonde v w n = Matrix.of fun i j => v i ^ ↑j * w i ^ ↑j.rev
-- Mathlib.GroupTheory.Commutator.Basic
commutator_eq_bot_iff : ∀ (G : Type u_1) [inst : Group G], commutator G = ⊥ ↔ IsMulCommutative G
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is cofiltered, then every functor `F : C ⥤ Discrete PUnit` is initial.  -/
CategoryTheory.Functor.initial_of_isCofiltered_pUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofiltered C]
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{u_1 + 1})), F.Initial
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toArray_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.map f t).toArray = Array.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toArray
-- Mathlib.Algebra.Algebra.Operations
/-- The action on a submodule corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.

This is a stronger version of `Submodule.pointwiseDistribMulAction`.  -/
Submodule.pointwiseMulSemiringAction : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {α : Type u_1} →
            [inst_3 : Monoid α] →
              [inst_4 : MulSemiringAction α A] → [SMulCommClass α R A] → MulSemiringAction α (Submodule R A)
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivAt.iteratedFDeriv_cons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x v w : E}
  {hf : IsSymmSndFDerivAt 𝕜 f x}, (iteratedFDeriv 𝕜 2 f x) ![v, w] = (iteratedFDeriv 𝕜 2 f x) ![w, v]
-- Mathlib.Algebra.Regular.Opposite
isAddRightRegular_unop : ∀ {R : Type u_1} [inst : Add R] {a : Rᵃᵒᵖ}, IsAddRightRegular (AddOpposite.unop a) ↔ IsAddLeftRegular a
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.mk_prod : ∀ {G : Type u_1} {ι : Type u_2} [inst : CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G},
  ↑(s.prod f) = ∏ i ∈ s, ↑(f i)
-- Init.Data.List.Lemmas
List.isEmpty_iff : ∀ {α : Type u_1} {l : List α}, l.isEmpty = true ↔ l = []
-- Mathlib.RingTheory.PowerBasis
/-- `pb.equivOfRoot pb' h₁ h₂` is an equivalence of algebras with the same power basis,
where "the same" means that `pb` is a root of `pb'`s minimal polynomial and vice versa.

See also `PowerBasis.equivOfMinpoly` which takes the hypothesis that the
minimal polynomials are identical.
 -/
PowerBasis.equivOfRoot : {S : Type u_2} →
  [inst : Ring S] →
    {A : Type u_4} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra A S] →
          {S' : Type u_7} →
            [inst_3 : Ring S'] →
              [inst_4 : Algebra A S'] →
                (pb : PowerBasis A S) →
                  (pb' : PowerBasis A S') →
                    (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0 →
                      (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0 → S ≃ₐ[A] S'
-- Mathlib.Algebra.Group.Semiconj.Basic
SemiconjBy.inv_right_iff : ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toListRev_iter : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β}, m.iter.toListRev = m.toList.reverse
-- Std.Data.TreeSet.Basic
/-- Given a proof that the tree set is not empty, retrieves the smallest element.
 -/
Std.TreeSet.min : {α : Type u} → {cmp : α → α → Ordering} → (t : Std.TreeSet α cmp) → t.isEmpty = false → α
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.smulLeft.congr_simp : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] {G : Type u_9} [inst_4 : Group G] [inst_5 : DistribMulAction G M₁]
  [inst_6 : ContinuousConstSMul G M₁] [inst_7 : SMulCommClass G R₁ M₁],
  ContinuousLinearEquiv.smulLeft = ContinuousLinearEquiv.smulLeft
-- Mathlib.SetTheory.Cardinal.NatCard
/-- There is (noncomputably) an equivalence between a finite type `α` and `Fin (Nat.card α)`.  -/
Finite.equivFin : (α : Type u_4) → [Finite α] → α ≃ Fin (Nat.card α)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafifyLift_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : J.sheafify P ⟶ Q),
  CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ = η → γ = J.sheafifyLift η hQ
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.EdgeDisjointTriangles.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α),
  G.EdgeDisjointTriangles = (G.cliqueSet 3).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.Nondegenerate.toMatrix' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {B : LinearMap.BilinForm R₂ (ι → R₂)}, B.Nondegenerate → (LinearMap.BilinForm.toMatrix' B).Nondegenerate
-- Lean.Meta.Transform
Lean.TransformStep.visit.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.TransformStep.visit e) = 1 + sizeOf e
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_le : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Multiset α} {a : α}, s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a
-- Mathlib.Tactic.Simps.Basic
/-- A variant of `Substring.dropPrefix?` that does not consider `toFoo` to be a prefix to `toFoo_1`.
This is checked by inspecting whether the first character of the remaining part is a digit.

We use this variant because the latter is often a different field with an auto-generated name.
 -/
_private.Mathlib.Tactic.Simps.Basic.0.Simps.dropPrefixIfNotNumber? : String → String → Option String.Slice
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.subtype_injective : ∀ {α : Type u_1} [inst : CompleteLattice α] (L : CompleteSublattice α), Function.Injective ⇑L.subtype
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Pullback `PosMulStrictMono`.  -/
Function.Injective.posMulStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [PosMulStrictMono α] {β : Type u_2}
  [inst_4 : Zero β] [inst_5 : Mul β] [inst_6 : Preorder β] (f : β → α),
  f 0 = 0 → (∀ (x y : β), f (x * y) = f x * f y) → (∀ {x y : β}, f x < f y ↔ x < y) → PosMulStrictMono β
-- Mathlib.CategoryTheory.Limits.Final
/-- A pointfree version of `limitIso`, stating that whiskering by `F` followed by taking the
limit is isomorphic to taking the limit on the codomain of `F`.  -/
CategoryTheory.Functor.Initial.limIso : {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] →
                [inst_4 : CategoryTheory.Limits.HasLimitsOfShape D E] →
                  [inst_5 : CategoryTheory.Limits.HasLimitsOfShape C E] →
                    ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).comp CategoryTheory.Limits.lim ≅
                      CategoryTheory.Limits.lim
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitAnchorRefInfo.mk.inj : ∀ {numDigits : ℕ} {anchor : UInt64} {ordinal numDigits_1 : ℕ} {anchor_1 : UInt64} {ordinal_1 : ℕ},
  { numDigits := numDigits, anchor := anchor, ordinal := ordinal } =
      { numDigits := numDigits_1, anchor := anchor_1, ordinal := ordinal_1 } →
    numDigits = numDigits_1 ∧ anchor = anchor_1 ∧ ordinal = ordinal_1
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_neg : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommGroup M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubgroupClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] (x : M),
  (DirectSum.decompose ℳ) (-x) = -(DirectSum.decompose ℳ) x
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.mk : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {l : α → β} →
          {u : β → α} →
            (choice : (x : β) → x ≤ l (u x) → α) →
              GaloisConnection l u →
                (∀ (x : α), u (l x) ≤ x) → (∀ (a : β) (h : a ≤ l (u a)), choice a h = u a) → GaloisCoinsertion l u
-- Init.Data.BitVec.Lemmas
BitVec.toInt_eq_toNat_of_msb : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → x.toInt = ↑x.toNat
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.congr_arg : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) {x y : ↑unitInterval × X}, x = y → F x = F y
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.instIsScalarTower : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : CommSemiring A] [inst_4 : SMul R S] [inst_5 : Algebra R A] [inst_6 : Algebra S A]
  [inst_7 : Module A M] [IsScalarTower R S A], IsScalarTower R S (TensorAlgebra A M)