mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- For any two-sided ideal $I ≤ R$, we have $J(Mₙ(I)) = Mₙ(J(I))$.  -/
TwoSidedIdeal.jacobson_matrix : ∀ {R : Type u_1} [inst : Ring R] {n : Type u_2} [inst_1 : Fintype n] [inst_2 : DecidableEq n] (I : TwoSidedIdeal R),
  (TwoSidedIdeal.matrix n I).jacobson = TwoSidedIdeal.matrix n I.jacobson
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.natCast_eq_map_iff : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : β → α} {n : ℕ} {a : WithTop β},
  ↑n = WithTop.map f a ↔ ∃ x, a = ↑x ∧ f x = ↑n
-- Mathlib.Data.Finset.Interval
/-- A function `f` from `Finset α` is strictly antitone if and only if `f (insert a s) < f s` for
all `s` and `a ∉ s`.  -/
Finset.strictAnti_iff_forall_lt_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β} [inst_1 : DecidableEq α],
  StrictAnti f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f (insert a s) < f s
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.encard_left : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} [H.FiniteIndex],
  Subgroup.IsComplement S ↑H → S.encard = ↑H.index
-- Mathlib.Tactic.Translate.Core
/-- Find the target name of `src`, which is assumed to have been selected by `findAuxDecls`.  -/
Mathlib.Tactic.Translate.findTargetName : Lean.Environment → Mathlib.Tactic.Translate.TranslateData → Lean.Name → Lean.Name → Lean.Name → Lean.CoreM Lean.Name
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m)
  (x :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f))
      (AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun f_deg hm x) =
    x
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instPartialOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β],
  InfTopHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.operator : Lean.Lsp.SymbolKind
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
/-- When `C` is monoidal closed and has suitable limits,
then for any `F : J ⥤ C`, `tensorLeft F` has a right adjoint.  -/
CategoryTheory.MonoidalClosed.FunctorCategory.adj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.MonoidalClosed C] →
        {J : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
            [inst_4 :
                ∀ (F₁ F₂ : CategoryTheory.Functor J C),
                  CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] →
              [inst_5 :
                  ∀ (F₁ F₂ : CategoryTheory.Functor J C),
                    CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂] →
                (F : CategoryTheory.Functor J C) →
                  CategoryTheory.MonoidalCategory.tensorLeft F ⊣
                    (CategoryTheory.eHomFunctor (CategoryTheory.Functor J C) (CategoryTheory.Functor J C)).obj
                      (Opposite.op F)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.tendsto_atTop_of_linearGrowthInf_pos : ∀ {u : ℕ → EReal}, 0 < LinearGrowth.linearGrowthInf u → Filter.Tendsto u Filter.atTop (nhds ⊤)
-- Mathlib.Order.Minimal
MinimalFor.not_prop_of_lt : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {Q : ι → Prop} {f : ι → α} {i j : ι},
  MinimalFor Q f i → f j < f i → ¬Q j
-- Mathlib.Data.Analysis.Filter
CFilter.ofEquiv_val : ∀ {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [inst : PartialOrder α] (E : σ ≃ τ) (F : CFilter α σ) (a : τ),
  (CFilter.ofEquiv E F).f a = F.f (E.symm a)
-- Mathlib.Topology.Sets.VietorisTopology
Continuous.nonemptyCompacts_map' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → TopologicalSpace.NonemptyCompacts β} {g : α → β → γ},
  Continuous f →
    ∀ (hg : Continuous (Function.uncurry g)), Continuous fun x => TopologicalSpace.NonemptyCompacts.map (g x) ⋯ (f x)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (G : Type u) →
                                    [inst_9 : TopologicalSpace G] →
                                      [inst_10 : ChartedSpace H G] →
                                        [inst_11 : AddGroup G] →
                                          [LieAddGroup I (↑⊤) G] →
                                            (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                                              AddGroup ((smoothSheaf IM I M G).presheaf.obj U)
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_trace_of_basis : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {ι : Type u_4}
  {κ : Type u_5} [Finite ι] [Finite κ] (b : Module.Basis ι R S) (c : Module.Basis κ S T) (x : T),
  (Algebra.trace R S) ((Algebra.trace S T) x) = (Algebra.trace R T) x
-- Init.Data.Vector.Lemmas
Vector.instDecidableForallVectorSucc : {α : Type u_1} →
  {n : ℕ} →
    (P : Vector α (n + 1) → Prop) →
      [Decidable (∀ (x : α) (xs : Vector α n), P (xs.push x))] → Decidable (∀ (xs : Vector α (n + 1)), P xs)
-- Mathlib.CategoryTheory.Sites.Over
/-- The equivalence `Sieve Y ≃ Sieve Y.left` for all `Y : Over X`.  -/
CategoryTheory.Sieve.overEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → (Y : CategoryTheory.Over X) → CategoryTheory.Sieve Y ≃o CategoryTheory.Sieve Y.left
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_of_le_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], a ≤ 1 → |a|ₘ = a⁻¹
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.comp_antitoneOn_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : LinearOrder β]
  [inst_2 : Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι},
  MonovaryOn f g s → AntitoneOn g' (g '' s) → AntivaryOn f (g' ∘ g) s
-- Mathlib.ModelTheory.Syntax
/-- Maps a term's symbols along a language equivalence.  -/
FirstOrder.Language.LEquiv.onTerm : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → {α : Type u'} → (L ≃ᴸ L') → L.Term α ≃ L'.Term α
-- Init.System.ST
ST.Prim.mkRef : {σ α : Type} → α → ST σ (ST.Ref σ α)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.hFunctor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (i : ι) (HP : TopPair.HomologyPretheory C c),
  (TopPair.HomologyPretheory.hFunctor i).obj HP = HP.H i
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.tensorH1CotangentOfIsLocalization.congr_simp : ∀ (R : Type u_1) {S : Type u_2} (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  (M M_1 : Submonoid S) (e_M : M = M_1) [inst_7 : IsLocalization M T],
  Algebra.tensorH1CotangentOfIsLocalization R T M = Algebra.tensorH1CotangentOfIsLocalization R T M_1
-- Mathlib.Data.Set.Basic
Set.mem_surjective : ∀ {α : Type u}, Function.Surjective Membership.mem
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Specialization of `Finset.sum_bij` that automatically fills in most arguments.

See `Fintype.sum_bijective` for the version where `s` and `t` are `univ`.  -/
Finset.sum_bijective : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (e : ι → κ),
  Function.Bijective e → (∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → ∑ i ∈ s, f i = ∑ i ∈ t, g i
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instFieldNonZeroDivisors : {R : Type u_1} →
  [inst : CommRing R] →
    [Nontrivial R] →
      [NoZeroDivisors R] →
        [inst_3 : OreLocalization.OreSet (nonZeroDivisors R)] → Field (OreLocalization (nonZeroDivisors R) R)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_smulLeftCLM_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] {g₁ g₂ : E → ℂ},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      ∀ (f : TemperedDistribution E F),
        (TemperedDistribution.smulLeftCLM F g₂) ((TemperedDistribution.smulLeftCLM F g₁) f) =
          (TemperedDistribution.smulLeftCLM F (g₁ * g₂)) f
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- In a functor category, `coconePointwiseProduct` commutes with evaluation.  -/
CategoryTheory.Limits.evaluationCoconePointwiseProductIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {α : Type u_3} →
          {I : α → Type u_4} →
            [inst_2 : (i : α) → CategoryTheory.Category.{u_5, u_4} (I i)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] →
                (F : (i : α) → CategoryTheory.Functor (I i) (CategoryTheory.Functor D C)) →
                  (X : D) →
                    (c : (i : α) → CategoryTheory.Limits.Cocone (F i)) →
                      ((CategoryTheory.evaluation D C).obj X).mapCocone
                          (CategoryTheory.Limits.coconePointwiseProduct c) ≅
                        (CategoryTheory.Limits.Cocone.precompose
                              (CategoryTheory.Limits.pointwiseProductCompEvaluation F X).hom).obj
                          (CategoryTheory.Limits.coconePointwiseProduct fun i =>
                            ((CategoryTheory.evaluation D C).obj X).mapCocone (c i))
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_iff_le_map : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β},
  Measurable f ↔ m₂ ≤ MeasurableSpace.map f m₁
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.coeffList_monomial : ∀ {R : Type u_1} [inst : Semiring R] {x : R},
  x ≠ 0 → ∀ (n : ℕ), ((Polynomial.monomial n) x).coeffList = x :: List.replicate n 0
-- Lean.Server.References
Lean.Server.RefInfo.mk.sizeOf_spec : ∀ (definition : Option Lean.Server.Reference) (usages : Array Lean.Server.Reference),
  sizeOf { definition := definition, usages := usages } = 1 + sizeOf definition + sizeOf usages
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The expression for the left whiskering `f ▷ η`.  -/
Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft.whiskerLeftM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft m] →
    Mathlib.Tactic.BicategoryLike.Atom₁ →
      Mathlib.Tactic.BicategoryLike.WhiskerLeft → m Mathlib.Tactic.BicategoryLike.WhiskerLeft
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂_eq_pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] (g : β → γ → δ)
  (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ),
  MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqFun.comp (Function.uncurry g) hg (f₁.pair f₂)
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.ae_map_iff_ae_trim : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β} (hf : Measurable f) {p : β → Prop},
  MeasurableSet {x | p x} → ((∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x))
-- Mathlib.Data.Rel
SetRel.mem_core : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} {a : α}, a ∈ R.core t ↔ ∀ ⦃b : β⦄, (a, b) ∈ R → b ∈ t
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Adj.mono : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β}, H ≤ G → H.Adj x y → G.Adj x y
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_biUnion : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} {T : Set ι},
  Countable ↑T →
    T.Pairwise (Function.onFun Disjoint s) →
      (∀ (i : ι), MeasurableSet (s i)) →
        μ.restrict (⋃ i ∈ T, s i) = MeasureTheory.Measure.sum fun i => μ.restrict (s ↑i)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
PolynormableSpace.induced : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [RingHomIsometric σ₁₂] [inst_7 : TopologicalSpace F] [PolynormableSpace 𝕜₂ F] (f : E →ₛₗ[σ₁₂] F),
  PolynormableSpace 𝕜 E
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_top : ∀ {α : Type u_1} [inst : MeasurableSpace α], ↑⊤ = ⊤
-- Mathlib.Data.Set.Card
Set.Finite.exists_encard_eq_coe : ∀ {α : Type u_1} {s : Set α}, s.Finite → ∃ n, s.encard = ↑n
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.exists_eccent_eq_radius : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], ∃ u, G.eccent u = G.radius
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- Being integrally closed is preserved under algebra isomorphisms.  -/
AlgEquiv.isIntegrallyClosedIn : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} {B : Type u_3} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B), IsIntegrallyClosedIn R A ↔ IsIntegrallyClosedIn R B
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.prod_left_ae : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] ⦃f : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) → ∀ᵐ (y : β) ∂ν, MeasureTheory.Integrable (fun x => f (x, y)) μ
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.IsFullyInvariant.eq_1 : ∀ {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N : Submodule R M), N.IsFullyInvariant = ∀ (f : Module.End R M), N ≤ Submodule.comap f N
-- Mathlib.Algebra.Group.Finsupp
/-- Note the general `SMul` instance for `Finsupp` doesn't apply as `ℕ` is not distributive
unless `F i`'s addition is commutative.  -/
Finsupp.instNatSMul : {ι : Type u_1} → {M : Type u_3} → [inst : AddMonoid M] → SMul ℕ (ι →₀ M)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddAction.IsPretransitive.of_embedding : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5},
  Function.Surjective ⇑f → ∀ [AddAction.IsPretransitive G (n ↪ α)], AddAction.IsPretransitive H (n ↪ β)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.lt_natDegree_of_mem_eraseLead_support : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} {a : ℕ}, a ∈ f.eraseLead.support → a < f.natDegree
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsLittleO.right_isTheta_add' : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'},
  f₁ =o[l] f₂ → f₂ =Θ[l] (f₂ + f₁)
-- Std.Do.SPred.Laws
Std.Do.SPred.and_elim_r : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ∧ Q ⊢ₛ Q
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.dvd_bmod_dot_sub_dot_bmod : ∀ (m : ℕ) (xs ys : Lean.Omega.Coeffs), ↑m ∣ Lean.Omega.Coeffs.bmod_dot_sub_dot_bmod m xs ys
-- Mathlib.Util.AtomM.Recurse
/-- Runs a tactic in the `AtomM.RecurseM` monad, given initial data:

* `s`: a reference to the mutable `AtomM` state, for persisting across calls.
  This ensures that atom ordering is used consistently.
* `cfg`: the configuration options
* `wellBehavedDischarge` : MUST be set to `false` IF `eval` accesses local declarations with
  index >= `Context.lctxInitIndices`.
  Reason: it would cause `simp` to cache results too aggressively.
* `eval`: a normalization operation which will be run recursively, potentially dependent on a known
  atom ordering
* `simp`: a cleanup operation which will be used to post-process expressions
* `x`: the tactic to run
 -/
Mathlib.Tactic.AtomM.RecurseM.run : {α : Type} →
  IO.Ref Mathlib.Tactic.AtomM.State →
    Mathlib.Tactic.AtomM.Recurse.Config →
      Bool →
        (Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result) →
          (Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result) → Mathlib.Tactic.AtomM.RecurseM α → Lean.MetaM α
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_iff_le : ∀ {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} [hl : l.NeBot], Cauchy l ↔ l ×ˢ l ≤ uniformity α
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.ext_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (zero : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
  (one : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
  (left :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom =
        CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
      CategoryTheory.Limits.parallelPair.ext._auto_1)
  (right :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom =
        CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
      CategoryTheory.Limits.parallelPair.ext._auto_3)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.parallelPair.ext zero one left right).hom.app X =
    (CategoryTheory.Limits.WalkingParallelPair.rec zero one X).hom
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.toLp_compMeasurePreserving : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β}
  {g : β → E} (hg : MeasureTheory.MemLp g p μb) (hf : MeasureTheory.MeasurePreserving f μ μb),
  (MeasureTheory.Lp.compMeasurePreserving f hf) (MeasureTheory.MemLp.toLp g hg) = MeasureTheory.MemLp.toLp (g ∘ f) ⋯
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termN : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_consₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ (a : α) (b : β a), Std.DHashMap.Internal.IsHashSelf (↑(m.consₘ a b)).buckets
-- Init.Data.List.MapIdx
List.exists_of_mem_mapFinIdx : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : (i : ℕ) → α → i < l.length → β},
  b ∈ l.mapFinIdx f → ∃ i, ∃ (h : i < l.length), f i l[i] h = b
-- Mathlib.Analysis.Normed.Module.Span
/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural continuous
linear map from the span of `x` to `𝕜`.  -/
ContinuousLinearEquiv.coord : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → (x : E) → x ≠ 0 → StrongDual 𝕜 ↥(𝕜 ∙ x)
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value_Iii : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot],
      l₁ ≤ Filter.principal s →
        l₂ ≤ Filter.principal s →
          ∀ {f : X → α},
            ContinuousOn f s → Filter.Tendsto f l₁ Filter.atBot → Filter.Tendsto f l₂ Filter.atTop → Set.univ ⊆ f '' s
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a monoid inherits a 1.  -/
OneMemClass.one : {A : Type u_3} →
  {M₁ : Type u_4} → [inst : SetLike A M₁] → [inst_1 : One M₁] → [hA : OneMemClass A M₁] → (S' : A) → One ↥S'
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TrySuggestionEntry.mk : Lean.Name → ℕ → Lean.Elab.Tactic.Try.TrySuggestionEntry
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionIdentifier : Lean.ToJson Lean.Lsp.CompletionIdentifier
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- If `P` is local at the source and the target, then restriction on both source and target
preserves `P`.  -/
AlgebraicGeometry.IsZariskiLocalAtSource.resLE : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsZariskiLocalAtTarget P] {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), P f → P (AlgebraicGeometry.Scheme.Hom.resLE f U V e)
-- Mathlib.RingTheory.Ideal.Pointwise
/-- The action on an ideal corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
Ideal.pointwiseDistribMulAction : {M : Type u_1} →
  {R : Type u_3} → [inst : Monoid M] → [inst_1 : Semiring R] → [MulSemiringAction M R] → DistribMulAction M (Ideal R)
-- Std.Time.DateTime.WallTime
/-- Converts a `WallTime` to a `Minute.Offset`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.toMinutes : Std.Time.WallTime → Std.Time.Minute.Offset
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_zero_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : PadicSeq p), f.norm = 0 ↔ f ≈ 0
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.minimalPeriod_eq_one_iff_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : α} {g : G},
  Function.minimalPeriod (fun x => g +ᵥ x) a = 1 ↔ a ∈ AddAction.fixedBy α g
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- If two functions `f` and `g` admit Taylor series `p` and `q` in a set `s`, then the Cartesian
product of `f` and `g` admits the Cartesian product of `p` and `q` as a Taylor series.  -/
HasFTaylorSeriesUpToOn.prodMk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F}
  {p : E → FormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞},
  HasFTaylorSeriesUpToOn n f p s →
    ∀ {g : E → G} {q : E → FormalMultilinearSeries 𝕜 E G},
      HasFTaylorSeriesUpToOn n g q s →
        HasFTaylorSeriesUpToOn n (fun y => (f y, g y)) (fun y k => (p y k).prod (q y k)) s