mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → (p = Polynomial.X ^ p.natDegree ↔ p.natTrailingDegree = p.natDegree)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression of a 2-morphism into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.eval : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          [Mathlib.Tactic.BicategoryLike.MonadMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
            Lean.Name →
              Mathlib.Tactic.BicategoryLike.Mor₂ →
                Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Mathlib.Logic.Function.Basic
Function.eq_update_self_iff : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a},
  f = Function.update f a b ↔ f a = b
-- Mathlib.CategoryTheory.NatIso
/-- A natural transformation is an isomorphism if all its components are isomorphisms.
 -/
CategoryTheory.NatIso.isIso_of_isIso_app : ∀ {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) [∀ (X : C), CategoryTheory.IsIso (α.app X)], CategoryTheory.IsIso α
-- Mathlib.Data.List.Cycle
Cycle.toMultiset_eq_nil : ∀ {α : Type u_1} {s : Cycle α}, s.toMultiset = 0 ↔ s = Cycle.nil
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.val_apply : ∀ {X : TopCat} {U V : TopologicalSpace.Opens ↑X} (f : U ⟶ V) (x : ↥U), ↑(f x) = ↑x
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsIntegralHom
-- Mathlib.NumberTheory.Primorial
_private.Mathlib.NumberTheory.Primorial.0.«term_#» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mkIso_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.Grp C} (e : G.X ≅ H.X)
  (one_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
      CategoryTheory.Grp.mkIso._auto_1)
  (mul_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
          CategoryTheory.MonObj.mul)
      CategoryTheory.Grp.mkIso._auto_3),
  (CategoryTheory.Grp.mkIso e one_f mul_f).hom.hom.hom = e.hom
-- Init.Data.String.Defs
String.Slice.offset_startInclusive_add_self : ∀ {s : String.Slice}, s.startInclusive.offset + s = s.endExclusive.offset
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePiNat.eq_1 : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)],
  MeasureTheory.Measure.infinitePiNat μ =
    (MeasureTheory.Measure.pi fun i => μ ↑i).bind
      ⇑(ProbabilityTheory.Kernel.traj
          (fun n => ProbabilityTheory.Kernel.const ((i : ↥(Finset.Iic n)) → X ↑i) (μ (n + 1))) 0)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instHasInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], CategoryTheory.Limits.HasInitial (CategoryTheory.CommGrp C)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter_eq_alterₘ : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α fun x => β}
  {a : α} {f : Option β → Option β} (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.Const.alter a f t htb).impl = Std.DTreeMap.Internal.Impl.Const.alterₘ a f t htb
-- Mathlib.Topology.MetricSpace.MetricSeparated
/-- **Alias** of the reverse direction of `Metric.AreSeparated.finset_iUnion_left_iff`. -/
Metric.AreSeparated.finset_iUnion_left : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ι : Type u_3} {I : Finset ι} {s : ι → Set X} {t : Set X},
  (∀ i ∈ I, Metric.AreSeparated (s i) t) → Metric.AreSeparated (⋃ i ∈ I, s i) t
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
_private.Mathlib.Algebra.BigOperators.Group.List.Lemmas.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parsePos : Std.Internal.Parsec.ByteArray.Parser ℕ
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Given a term `e`, add casts to it to unfold constants appearing in it.  -/
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.unfoldConsts : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Init.Data.ByteArray.Lemmas
ByteArray.size_eq_zero_iff : ∀ {a : ByteArray}, a.size = 0 ↔ a = ByteArray.empty
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblU_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F}, P 2 = 0 → W.dblU P = 0
-- Batteries.Recycling.MonadSatisfying.Basic
SatisfiesM_ReaderT_eq : ∀ {m : Type u_1 → Type u_2} {ρ α : Type u_1} {p : α → Prop} {x : ReaderT ρ m α} [inst : Monad m],
  SatisfiesM p x ↔ ∀ (s : ρ), SatisfiesM p (x.run s)
-- Mathlib.Order.Antisymmetrization
instReflAntisymmRel : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Refl r], Std.Refl (AntisymmRel r)
-- Mathlib.Data.ENat.Basic
ENat.toNat_pos : ∀ {n : ℕ∞}, n ≠ 0 → n ≠ ⊤ → 0 < n.toNat
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- The underlying linear map of an affine isometry is in fact a linear isometry.  -/
AffineIsometry.linearIsometry : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P →ᵃⁱ[𝕜] P₂) → V →ₗᵢ[𝕜] V₂
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.instMin : {ι : 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 𝒜] → Min (HomogeneousIdeal 𝒜)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The negation of a Jacobian point class on a Weierstrass curve `W`.

If `P` is a Jacobian point representative on `W`, then `W.negMap ⟦P⟧` is definitionally equivalent
to `W.neg P`.  -/
WeierstrassCurve.Jacobian.negMap : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Jacobian R → WeierstrassCurve.Jacobian.PointClass R → WeierstrassCurve.Jacobian.PointClass R
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The isomorphism between left lifts induced by a left unitor.  -/
CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (t : CategoryTheory.Bicategory.LeftLift f g) → (t.whisker (CategoryTheory.CategoryStruct.id c)).ofIdComp ≅ t
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.toBasis_orthonormalBasisOneI : Complex.orthonormalBasisOneI.toBasis = Complex.basisOneI
-- Mathlib.Data.Sym.Sym2
/-- The symmetric square is equivalent to the second symmetric power.  -/
Sym2.equivSym : (α : Type u_4) → Sym2 α ≃ Sym α 2
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split'.eq_def : ∀ (x : ONote),
  x.split' =
    match x with
    | ONote.zero => (0, 0)
    | e.oadd n a =>
      if e = 0 then (0, ↑n)
      else
        match a.split' with
        | (a', m) => ((e - 1).oadd n a', m)
-- Mathlib.Analysis.Analytic.Order
/-- If an analytic function `f` vanishes at `z₀`, then the analytic order of its derivative
at `z₀` is at least `n` if and only if the analytic order of `f` at `z₀` is at least `n + 1`.  -/
analyticOrderAt_deriv_ge_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {z₀ : 𝕜} {f : 𝕜 → E},
  AnalyticAt 𝕜 f z₀ → f z₀ = 0 → ∀ {n : ℕ}, ↑n ≤ analyticOrderAt (deriv f) z₀ ↔ ↑n + 1 ≤ analyticOrderAt f z₀
-- Init.Data.Array.Lemmas
Array.foldl_toList_eq_flatMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {acc : Array β} {F : Array β → α → Array β} {G : α → List β},
  (∀ (acc : Array β) (a : α), (F acc a).toList = acc.toList ++ G a) →
    (List.foldl F acc l).toList = acc.toList ++ List.flatMap G l
-- Aesop.Forward.State.UpdateGoal
Aesop.GoalRef.updateForwardState : Aesop.PhaseName → Aesop.GoalRef → Aesop.TreeM Unit
-- Mathlib.Data.Finset.Sum
Finset.disjSum_mono_right : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α), Monotone s.disjSum
-- Mathlib.Tactic.PNatToNat
Mathlib.Tactic.PNatToNat.coe_inj : ∀ (m n : ℕ+), m = n ↔ ↑m = ↑n
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
      (CategoryTheory.CategoryStruct.comp
        ((s.cofan (Opposite.op { len := n })).inj
          (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
        (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h
-- Mathlib.Combinatorics.Additive.Corner.Roth
/-- The **corners theorem** for finite abelian groups.

The maximum density of a corner-free set in `G × G` goes to zero as `|G|` tends to infinity.  -/
corners_theorem : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : Fintype G] (ε : ℝ),
  0 < ε →
    cornersTheoremBound ε ≤ Fintype.card G →
      ∀ (A : Finset (G × G)), ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card → ¬IsCornerFree ↑A
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forgetToQuiv_faithful : ∀ {V W : CategoryTheory.ReflQuiv} (F G : ↑V ⥤rq ↑W),
  CategoryTheory.ReflQuiv.forgetToQuiv.map F = CategoryTheory.ReflQuiv.forgetToQuiv.map G → F = G
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atBot_atTop : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {f : α → β}
  [inst_2 : Preorder β], Filter.Tendsto f Filter.atBot Filter.atTop ↔ ∀ (b : β), ∃ i, ∀ a ≤ i, b ≤ f a
-- Mathlib.GroupTheory.ResiduallyFinite
Group.exists_finiteIndexNormalSubgroup_notMem : ∀ {G : Type u_1} [inst : Group G] [Group.ResiduallyFinite G] (g : G), g ≠ 1 → ∃ H, g ∉ H
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult.ctxInfo : Lean.Elab.GoalsAtResult → Lean.Elab.ContextInfo
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.sub_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  MonovaryOn f₁ g s → AntivaryOn f₂ g s → MonovaryOn (f₁ - f₂) g s
-- Mathlib.AlgebraicGeometry.Cover.Over
/-- A variant of `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp` with the arguments in the
fiber products flipped.  -/
AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
                        [Q.HasOfPostcompProperty Q] →
                          [Q.IsStableUnderBaseChange] →
                            [Q.IsStableUnderComposition] →
                              Q (X ↘ S) →
                                Q (W ↘ S) →
                                  (∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) →
                                    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) W
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.instHasNoLoopSymm : ∀ {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop], c.symm.HasNoLoop
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An iso `α ≃* β` can equivalently be viewed as an iso `αᵐᵒᵖ ≃* βᵐᵒᵖ`.  -/
MulEquiv.op : {α : Type u_3} → {β : Type u_4} → [inst : Mul α] → [inst_1 : Mul β] → α ≃* β ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ)
-- Mathlib.Data.Finset.Filter
Finset.filter_false : ∀ {α : Type u_1} {h : DecidablePred fun x => False} (s : Finset α), {x ∈ s | False} = ∅
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` is stable under composition with localization away maps on the left,
then so is `Locally P`.  -/
RingHom.locally_stableUnderCompositionWithLocalizationAwaySource : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesKernel.iso_inv_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesKernel.iso G f).inv
      (G.map (CategoryTheory.Limits.kernel.ι f)) =
    CategoryTheory.Limits.kernel.ι (G.map f)
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_weighted_of_constant : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (x : ℝ),
  (∀ i ∈ s, 0 ≤ w i) → ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 ≤ z i) → (∀ i ∈ s, w i ≠ 0 → z i = x) → ∏ i ∈ s, z i ^ w i = x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.not_nil_iff : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w},
  ¬p.Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, p = SimpleGraph.Walk.cons h q
-- Mathlib.Algebra.Quandle
Rack.toShelf : {α : Type u} → [self : Rack α] → Shelf α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {a k : α} {v : β},
      Std.DTreeMap.Raw.Const.get? (t.insert k v) a =
        if cmp k a = Ordering.eq then some v else Std.DTreeMap.Raw.Const.get? t a
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.liftR_map_last : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] [lawful : LawfulMvFunctor F] {α : TypeVec.{u} n}
  {ι ι' : Type u} (R : ι' → ι' → Prop) (x : F (α ::: ι)) (f g : ι → ι'),
  (∀ (x : ι), R (f x) (g x)) →
    MvFunctor.LiftR' (α.RelLast' R) (MvFunctor.map (TypeVec.id ::: f) x) (MvFunctor.map (TypeVec.id ::: g) x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_of_mem_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m.keysArray → m.contains k = true
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.adjoin_tmul_eq_top : ∀ (R : Type uR) (A : Type uA) (B : Type uB) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B], Algebra.adjoin R {t | ∃ a b, a ⊗ₜ[R] b = t} = ⊤
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instZero : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → Zero (TestFunction Ω F n)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.un.injEq : ∀ {w : ℕ} (op : Std.Tactic.BVDecide.BVUnOp) (operand : Std.Tactic.BVDecide.BVExpr w) (op_1 : Std.Tactic.BVDecide.BVUnOp)
  (operand_1 : Std.Tactic.BVDecide.BVExpr w),
  (Std.Tactic.BVDecide.BVExpr.un op operand = Std.Tactic.BVDecide.BVExpr.un op_1 operand_1) =
    (op = op_1 ∧ operand = operand_1)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns symbol priorities for inferring E-matching patterns.  -/
Lean.Meta.Grind.getSymbolPriorities : Lean.Meta.Grind.GrindM Lean.Meta.Grind.SymbolPriorities
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app._auto_1),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C n).map
          ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app X).unop).op
      ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_mono : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x : E}
  {p : Seminorm 𝕜 E} {r₁ r₂ : ℝ}, r₁ ≤ r₂ → p.closedBall x r₁ ⊆ p.closedBall x r₂
-- Lean.Data.DeclarationRange
Lean.DeclarationLocation.mk : Lean.Name → Lean.DeclarationRange → Lean.DeclarationLocation
-- Init.Data.Sum.Lemmas
Sum.getLeft?.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (val : α), (Sum.inl val).getLeft? = some val
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.oplax_right_unitality : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.OplaxMonoidal] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.η F)))
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
/-- The tensor product of two quadratic maps injects into quadratic maps on tensor products.

Note this is heterobasic; the quadratic map on the left can take values in a module over a larger
ring than the one on the right.  -/
QuadraticMap.tensorDistrib : (R : Type uR) →
  (A : Type uA) →
    {M₁ : Type uM₁} →
      {M₂ : Type uM₂} →
        {N₁ : Type uN₁} →
          {N₂ : Type uN₂} →
            [inst : CommRing R] →
              [inst_1 : CommRing A] →
                [inst_2 : AddCommGroup M₁] →
                  [inst_3 : AddCommGroup M₂] →
                    [inst_4 : AddCommGroup N₁] →
                      [inst_5 : AddCommGroup N₂] →
                        [inst_6 : Algebra R A] →
                          [inst_7 : Module R M₁] →
                            [inst_8 : Module A M₁] →
                              [inst_9 : Module R N₁] →
                                [inst_10 : Module A N₁] →
                                  [inst_11 : SMulCommClass R A M₁] →
                                    [IsScalarTower R A M₁] →
                                      [inst_13 : IsScalarTower R A N₁] →
                                        [inst_14 : Module R M₂] →
                                          [inst_15 : Module R N₂] →
                                            [Invertible 2] →
                                              TensorProduct R (QuadraticMap A M₁ N₁) (QuadraticMap R M₂ N₂) →ₗ[A]
                                                QuadraticMap A (TensorProduct R M₁ M₂) (TensorProduct R N₁ N₂)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.gc_comap_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), GaloisConnection (MeasurableSpace.comap f) (MeasurableSpace.map f)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.MorphismProperty.whiskerRight_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [W.IsMonoidal] {X₁ X₂ : C} (f : X₁ ⟶ X₂),
  W f → ∀ (Y : C), W (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmoothOfRelativeDimension_respectsIso : ∀ {n : ℕ}, RingHom.RespectsIso (@RingHom.IsStandardSmoothOfRelativeDimension n)
-- Mathlib.Topology.Algebra.UniformMulAction
vadd_uniformity : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : AddGroup M] [inst_2 : AddAction M X]
  [UniformContinuousConstVAdd M X] (c : M), c +ᵥ uniformity X = uniformity X
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, k ∉ t → (f (t.get? k)).isNone = true → (t.alter k f).size = t.size
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (x : SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.obj F).hom.app x =
    F.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of x))
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is polynomial on a set `s`, so is its derivative.  -/
CPolynomialOn.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜}, CPolynomialOn 𝕜 f s → CPolynomialOn 𝕜 (deriv f) s
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.one_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (a : TensorPower R n M), (TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul GradedMonoid.GOne.one a) = a
-- Init.Prelude
/-- Abbreviation for `DecidableRel (· ≤ · : α → α → Prop)`.  -/
DecidableLE : (α : Type u) → [LE α] → Type (max 0 u)