mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.NatIso
/-- The components of a natural isomorphism are isomorphisms.  -/
CategoryTheory.NatIso.isIso_app_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) [CategoryTheory.IsIso α] (X : C), CategoryTheory.IsIso (α.app X)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.pow : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  [StarOrderedRing R] [inst_5 : DecidableEq n] {M : Matrix n n R}, M.PosSemidef → ∀ (k : ℕ), (M ^ k).PosSemidef
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α}, k ∈ Std.ExtHashMap.filterMap f m → k ∈ m
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView!.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.maxView! k v l r =
    match r with
    | Std.DTreeMap.Internal.Impl.leaf => { k := k, v := v, tree := l }
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' =>
      have d := Std.DTreeMap.Internal.Impl.maxView! k' v' l' r';
      { k := d.k, v := d.v, tree := Std.DTreeMap.Internal.Impl.balanceL! k v l d.tree }
-- Mathlib.Algebra.RingQuot
RingQuot.instZero : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → Zero (RingQuot r)
-- Mathlib.Data.Semiquot
Semiquot.isPure_iff : ∀ {α : Type u_1} {s : Semiquot α}, s.IsPure ↔ ∃ a, s = pure a
-- Mathlib.Probability.Independence.Kernel.Indep
/-- A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a
kernel `κ` and a measure `μ` if the family of sets of measurable sets they define is independent.  -/
ProbabilityTheory.Kernel.iIndep : {α : Type u_1} →
  {Ω : Type u_2} →
    {ι : Type u_3} →
      {_mα : MeasurableSpace α} →
        (ι → MeasurableSpace Ω) →
          {_mΩ : MeasurableSpace Ω} →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.iIndep._auto_1 → Prop
-- Mathlib.Algebra.RingQuot
RingQuot.instNeg : {R : Type uR} → [inst : Ring R] → (r : R → R → Prop) → Neg (RingQuot r)
-- Init.Data.UInt.Lemmas
instLawfulCommIdentityUInt32HMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.CandidateKind.noConfusionType : Sort v✝ →
  Lean.Server.FileWorker.SignatureHelp.CandidateKind → Lean.Server.FileWorker.SignatureHelp.CandidateKind → Sort v✝
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.root_indexEquiv_eq_smul : ∀ {ι : 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) (i : ι) (g : P.Aut),
  P.root ((↑g).indexEquiv i) = g • P.root i
-- Mathlib.Topology.Instances.CantorSet
quarters_mem_preCantorSet : ∀ (n : ℕ), 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
-- Init.MetaTypes
/-- The configuration for `dsimp`.
Passed to `dsimp` using, for example, the `dsimp (config := {zeta := false})` syntax.

Implementation note: this structure is only used for processing the `(config := ...)` syntax, and it is not used internally.
It is immediately converted to `Lean.Meta.Simp.Config` by `Lean.Elab.Tactic.elabSimpConfig`.
 -/
Lean.Meta.DSimp.Config : Type
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.order_prod : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_4}
  (f : ι → MvPowerSeries σ R) (s : Finset ι), (∏ i ∈ s, f i).order = ∑ i ∈ s, (f i).order
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.r.isEquiv : ∀ {R : Type u} [inst : CommSemiring R] (S : Submonoid R) (M : Type v) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsEquiv (M × ↥S) (LocalizedModule.r S M)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isNone_min?_eq_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.min?.isNone = t.isEmpty
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.vanishingIdeal_anti_mono : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  {A B : Set (σ → K)}, A ⊆ B → MvPolynomial.vanishingIdeal k B ≤ MvPolynomial.vanishingIdeal k A
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_insert_left : ∀ {α : Type u_2} [inst : DecidableEq α] {s t : Finset α} {a : α}, Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.map_fst_toArray_eq_keysArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → Array.map Prod.fst (Std.DHashMap.Raw.Const.toArray m) = m.keysArray
-- Mathlib.GroupTheory.Index
MonoidHom.card_fiber_eq_of_mem_range : ∀ {G : Type u_1} {M : Type u_2} {F : Type u_3} [inst : Group G] [inst_1 : Fintype G] [inst_2 : Monoid M]
  [inst_3 : DecidableEq M] [inst_4 : FunLike F G M] [MonoidHomClass F G M] (f : F) {x y : M},
  x ∈ Set.range ⇑f → y ∈ Set.range ⇑f → {g | f g = x}.card = {g | f g = y}.card
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.instSubtypeMemSubalgebraMin : {R : Type u} →
  [inst : CommSemiring R] →
    {C : Type u_1} →
      [inst_1 : CommSemiring C] → [inst_2 : Algebra R C] → (S₁ S₂ : Subalgebra R C) → Algebra ↥(S₁ ⊓ S₂) ↥S₁
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_leftUnitor_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor F).hom.app X =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)) F).obj
        X)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.instSubsingletonOfIsEmpty : ∀ {X : Type u_1} [IsEmpty X], Subsingleton (OnePoint X)
-- Mathlib.Algebra.Algebra.Basic
smul_algebra_smul_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [IsScalarTower R A M] (r : R) (a : A) (m : M),
  a • r • m = r • a • m
-- Mathlib.Topology.Irreducible
Function.Involutive.toPerm.congr_simp : ∀ {α : Sort u_1} (f f_1 : α → α) (e_f : f = f_1) (h : Function.Involutive f),
  Function.Involutive.toPerm f h = Function.Involutive.toPerm f_1 ⋯
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The trivial zeroes of the odd Hurwitz zeta function.  -/
HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat_sub_one : ∀ (a : UnitAddCircle) (n : ℕ), HurwitzZeta.hurwitzZetaOdd a (-2 * ↑n - 1) = 0
-- Mathlib.Algebra.Prime.Defs
Irreducible.ne_zero : ∀ {M : Type u_1} [inst : MonoidWithZero M] {p : M}, Irreducible p → p ≠ 0
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.Option.instDecidableEq.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (val : α) → motive (some val)),
  (match none with
    | none => h_1 ()
    | some val => h_2 val) =
    h_1 ()
-- Mathlib.Topology.MetricSpace.Defs
Metric.subsingleton_sphere : ∀ {γ : Type w} [inst : MetricSpace γ] (x : γ) {r : ℝ}, r ≤ 0 → (Metric.sphere x r).Subsingleton
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.currySum_apply : ∀ {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [inst : Fintype ι] [inst_1 : Fintype ι']
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  [inst_5 : NormedAddCommGroup G'] [inst_6 : NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 (fun x => G) G')
  (m : ι → G) (m' : ι' → G), (f.currySum m) m' = f (Sum.elim m m')
-- Mathlib.CategoryTheory.Monoidal.Preadditive
/-- The isomorphism showing how tensor product on the right distributes over direct sums.  -/
CategoryTheory.rightDistributor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [CategoryTheory.MonoidalPreadditive C] →
          [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            {J : Type} →
              [inst_5 : Finite J] →
                (f : J → C) →
                  (X : C) →
                    CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ≅
                      ⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X
-- Mathlib.Order.Filter.EventuallyConst
/-- The proposition that a function is eventually constant along a filter on the domain.  -/
Filter.EventuallyConst : {α : Type u_1} → {β : Type u_2} → (α → β) → Filter α → Prop
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
/-- Implementation: This is a construction which will be used in the proof that
the sieve generated by a single arrow is effective epimorphic if and only if
the arrow is an effective epi.
 -/
CategoryTheory.effectiveEpiStructOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : Y ⟶ X) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Sieve.generateSingleton f).arrows.cocone →
          CategoryTheory.EffectiveEpiStruct f
-- Mathlib.NumberTheory.RatFunc.Ostrowski
/-- The maximal ideal of `K[X]` generated by the `uniformizingPolynomial` for `v`.  -/
_private.Mathlib.NumberTheory.RatFunc.Ostrowski.0.RatFunc.termPᵥ : Lean.ParserDescr
-- Init.Data.ByteArray.Lemmas
ByteArray.append_assoc : ∀ {a b c : ByteArray}, a ++ b ++ c = a ++ (b ++ c)
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The image of a finitely presented group under a surjective homomorphism whose kernel is
finitely generated as a normal subgroup is finitely presented.  -/
Group.IsFinitelyPresented.of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] [hG : Group.IsFinitelyPresented G] (f : G →* H),
  Function.Surjective ⇑f → f.ker.IsFinitelyNormallyGenerated → Group.IsFinitelyPresented H
-- Mathlib.RingTheory.Polynomial.DegreeLT
/-- The map `taylor r` induces an automorphism of the module `R[X]_n` of polynomials of
degree `< n`.  -/
Polynomial.taylorLinearEquiv : {R : Type u_1} → [inst : CommRing R] → R → (n : ℕ) → ↥(Polynomial.degreeLT R n) ≃ₗ[R] ↥(Polynomial.degreeLT R n)
-- Mathlib.Data.List.Lattice
List.erase_bagInter_of_not_mem : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α} [inst : DecidableEq α], a ∉ l₂ → (l₁.erase a).bagInter l₂ = l₁.bagInter l₂
-- Mathlib.Order.OrderIsoNat
WellFoundedGT.monotone_chain_condition : ∀ {α : Type u_1} [inst : PartialOrder α] [h : WellFoundedGT α] (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m
-- Lean.Parser.Types
Lean.Parser.ParserModuleContext.openDecls : Lean.Parser.ParserModuleContext → List Lean.OpenDecl
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.map_toCoalgHom : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Bialgebra S A]
  [inst_5 : Bialgebra R B] [inst_6 : Algebra R A] [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S A]
  [inst_9 : Semiring C] [inst_10 : Semiring D] [inst_11 : Bialgebra S C] [inst_12 : Bialgebra R D]
  [inst_13 : Algebra R C] [inst_14 : IsScalarTower R S C] (f : A →ₐc[S] C) (g : B →ₐc[R] D),
  ↑(Bialgebra.TensorProduct.map f g) = Coalgebra.TensorProduct.map ↑f ↑g
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- Up to an equivalence, the type `SmallShiftedHom.{w} W X Y m` does
not depend on the universe `w`.  -/
CategoryTheory.Localization.SmallShiftedHom.chgUniv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            {X Y : C} →
              {m : M} →
                [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                    CategoryTheory.Localization.SmallShiftedHom W X Y m ≃
                      CategoryTheory.Localization.SmallShiftedHom W X Y m
-- Mathlib.Lean.Elab.InfoTree
/-- Accumulates contexts and visits nodes if `ctx?` is not `none`.  -/
Lean.Elab.InfoTree.findSomeM?.go : {m : Type → Type} →
  [Monad m] →
    {α : Type} →
      (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m (Option α)) →
        Option Lean.Elab.ContextInfo → Lean.Elab.InfoTree → m (Option α)
-- Mathlib.Topology.Order.OrderClosed
PredOrder.nhdsLT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a : α} [PredOrder α],
  nhdsWithin a (Set.Iio a) = ⊥
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A sieve induces a presheaf.  -/
CategoryTheory.Sieve.functor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Sieve X → CategoryTheory.Functor Cᵒᵖ (Type v₁)
-- Mathlib.Topology.Algebra.Group.Basic
continuousOn_neg_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G]
  [inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn (-f) s ↔ ContinuousOn f s
-- Mathlib.Probability.Decision.Risk.Basic
/-- See `avgRisk_const_left'` for a similar result with integrals swapped.  -/
ProbabilityTheory.avgRisk_const_left : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (μ : MeasureTheory.Measure 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
  (π : MeasureTheory.Measure Θ),
  ProbabilityTheory.avgRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) κ π = ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂μ.bind ⇑κ ∂π
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.opOp_apply : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A),
  (AlgEquiv.opOp R A) a = MulOpposite.op (MulOpposite.op a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {fallback : β} {f : β → β}, (m.modify k f).getD k fallback = (Option.map f m[k]?).getD fallback
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_add_self_of_mem_nhds_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {U : Set G},
  U ∈ nhds 0 → closure U ⊆ U + U
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `lowerHemicontinuousAt_singleton_iff`. -/
ContinuousAt.lowerHemicontinuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α},
  ContinuousAt f x → LowerHemicontinuousAt (fun x => {f x}) x
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coordChange_apply_snd : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e₁ e₂ : Bundle.Trivialization F proj) {p : Z},
  proj p ∈ e₁.baseSet → e₁.coordChange e₂ (proj p) (↑e₁ p).2 = (↑e₂ p).2
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDifferentiableAt_smul_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E}
  {c : 𝕜}, c ≠ 0 → (LineDifferentiableAt 𝕜 f x (c • v) ↔ LineDifferentiableAt 𝕜 f x v)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Copy of a lax braided structure on a functor `F` with new `ε` and `μ` fields equal to the old
ones.

This is useful to fix definitional equalities.  -/
CategoryTheory.Functor.LaxBraided.copy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} →
                  (hF : F.LaxBraided) →
                    (ε' :
                        CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                          F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                      (μ' :
                          (X Y : C) →
                            CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶
                              F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
                        autoParam (ε' = CategoryTheory.Functor.LaxMonoidal.ε F)
                            CategoryTheory.Functor.LaxBraided.copy._auto_1 →
                          autoParam (μ' = CategoryTheory.Functor.LaxMonoidal.μ F)
                              CategoryTheory.Functor.LaxBraided.copy._auto_3 →
                            F.LaxBraided
-- Mathlib.Order.Filter.ENNReal
Real.limsInf_of_not_isBounded : ∀ {f : Filter ℝ}, ¬Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f → f.limsInf = 0
-- Aesop.Builder.Basic
Aesop.PhaseSpec.toRule : Aesop.PhaseSpec →
  Lean.Name →
    Aesop.BuilderName →
      Aesop.ScopeName → Aesop.RuleTacDescr → Aesop.IndexingMode → Option Aesop.RulePattern → Aesop.BaseRuleSetMember
-- Mathlib.RingTheory.IntegralClosure.GoingDown
/-- [Stacks Tag 00H8](https://stacks.math.columbia.edu/tag/00H8) -/
instHasGoingDownOfIsDomainOfFaithfulSMulOfIsIntegralOfIsIntegrallyClosed : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain S]
  [FaithfulSMul R S] [Algebra.IsIntegral R S] [IsIntegrallyClosed R], Algebra.HasGoingDown R S
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.le_lexOrder_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  (φ ψ : MvPowerSeries σ R), φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodAssoc.eq_1 : ∀ (M : Type u_1) (N : Type u_2) (P : Type u_3) [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P],
  AddEquiv.coprodAssoc M N P =
    (AddMonoid.Coprod.lift (AddMonoid.Coprod.map (AddMonoidHom.id M) AddMonoid.Coprod.inl)
          (AddMonoid.Coprod.inr.comp AddMonoid.Coprod.inr)).toAddEquiv
      (AddMonoid.Coprod.lift (AddMonoid.Coprod.inl.comp AddMonoid.Coprod.inl)
        (AddMonoid.Coprod.map AddMonoid.Coprod.inr (AddMonoidHom.id P)))
      ⋯ ⋯
-- Init.Data.Array.GetLit
Array.toListLitAux.eq_1 : ∀ {α : Type u_1} (xs : Array α) (n : ℕ) (hsz : xs.size = n) (x : List α) (x_3 : 0 ≤ xs.size),
  xs.toListLitAux n hsz 0 x_3 x = x
-- Init.Data.List.MinMaxIdx
/-- Returns the index of an element of `xs` that maximizes `f`. If `x`, `y`
are such that `f x = f y`, it returns the index of whichever comes first in the list.
Returns `none` if the list is empty.

The correctness of this function assumes `β` to be linearly pre-ordered.
 -/
List.maxIdxOn? : {β : Type u_1} → {α : Type u_2} → [inst : LE β] → [DecidableLE β] → (α → β) → List α → Option ℕ
-- Std.Time.DateTime.Timestamp
Std.Time.instToStringTimestamp : ToString Std.Time.Timestamp
-- Std.Time.DateTime
/-- Represents a date and time with timezone information.
 -/
Std.Time.DateTime : Type
-- Mathlib.FieldTheory.KummerPolynomial
/-- Let `p` be a prime number. Let `K` be a field.
Let `t ∈ K` be an element which does not have a `p`th root in `K`.
Then the polynomial `x ^ p - t` is irreducible over `K`.  -/
X_pow_sub_C_irreducible_of_prime : ∀ {K : Type u} [inst : Field K] {p : ℕ},
  Nat.Prime p → ∀ {a : K}, (∀ (b : K), b ^ p ≠ a) → Irreducible (Polynomial.X ^ p - Polynomial.C a)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_add_mk : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Add γ] [inst_3 : ContinuousAdd γ] (f g : α → γ) (hf : MeasureTheory.AEStronglyMeasurable f μ)
  (hg : MeasureTheory.AEStronglyMeasurable g μ),
  MeasureTheory.AEEqFun.mk f hf + MeasureTheory.AEEqFun.mk g hg = MeasureTheory.AEEqFun.mk (f + g) ⋯
-- Mathlib.Algebra.Category.ModuleCat.Localization
/-- The linear map `M →ₗ[R] (M.localizedModule S)` which
exhibits `M.localizedModule S` as a localized module of `M`.  -/
ModuleCat.localizedModuleMkLinearMap : {R : Type u} →
  [inst : CommRing R] →
    [inst_1 : Small.{v, u} R] → (M : ModuleCat R) → (S : Submonoid R) → ↑M →ₗ[R] ↑(M.localizedModule S)
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.op_le_op : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, AddOpposite.op a ≤ AddOpposite.op b ↔ a ≤ b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.keys_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {f : α → Bool},
  t.WF → (Std.DTreeMap.Raw.filter (fun k x => f k) t).keys = List.filter f t.keys
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.under_map_eq_map : ∀ {S : Type u_6} {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] {Sₚ : Type u_9}
  [inst_2 : CommRing S] [inst_3 : Algebra R S] [inst_4 : CommRing Sₚ] [inst_5 : Algebra S Sₚ] [inst_6 : Algebra R Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [IsScalarTower R S Sₚ],
  Ideal.under S (Ideal.map (algebraMap R Sₚ) p) = Ideal.map (algebraMap R S) p
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.diagonal_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f f g).inv
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal g)
          (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f g)
            (CategoryTheory.CategoryStruct.comp f g) g g f f (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.ker_eval : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {s : S},
  IsIntegral R s → RingHom.ker (Polynomial.aeval s).toRingHom = Ideal.span {minpoly R s}
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If there exists a nonzero `s ∈ S` such that `n ∣ s`, then `IsCyclotomicExtension S A B`
if and only if `IsCyclotomicExtension (S ∪ {n}) A B`.  -/
IsCyclotomicExtension.iff_union_of_dvd : ∀ {n : ℕ} [NeZero n] {S : Set ℕ} (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B], (∃ s ∈ S, s ≠ 0 ∧ n ∣ s) → (IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.lift_mapRingHom_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : CommSemiring S] [inst_5 : Algebra S A] [inst_6 : Algebra R S]
  [IsScalarTower R S A] (f : M →* A) (x : MonoidAlgebra R M),
  ((MonoidAlgebra.lift S A M) f) ((MonoidAlgebra.mapRingHom M (algebraMap R S)) x) = ((MonoidAlgebra.lift R A M) f) x
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- A structure designed to hold the hypotheses for the Mellin-functional-equation argument
(most general version: rapid decay at `∞` up to constant terms)  -/
WeakFEPair : (E : Type u_1) → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → Type u_1