mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_injective_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty Cᵒᵖ},
  P.unop = Q.unop ↔ P = Q
-- Mathlib.Order.WellQuasiOrder
wellQuasiOrdered_of_isEmpty : ∀ {α : Type u_1} [IsEmpty α] (r : α → α → Prop), WellQuasiOrdered r
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F],
  CategoryTheory.Functor.IsRightKanExtension ((CategoryTheory.SimplicialObject.cosk n).obj X)
    ((CategoryTheory.SimplicialObject.coskAdj n).counit.app ((CategoryTheory.SimplicialObject.truncation n).obj X))
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.equiv : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R} {J : Type u_4} (i : J ≃ I),
  OrthogonalIdempotents (e ∘ ⇑i) ↔ OrthogonalIdempotents e
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme.congr_simp : ∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f f_1 : X ⟶ Y.toPresheafedSpace)
  (e_f : f = f_1) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f_1
-- Init.Meta.Defs
/-- Replaces the trailing whitespace in `stx`, if any, with an empty substring.

The trailing substring's `startPos` and `str` are preserved in order to ensure that the result could
have been produced by the parser, in case any syntax consumers rely on such an assumption.
 -/
Lean.Syntax.unsetTrailing : Lean.Syntax → Lean.Syntax
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
_private.Mathlib.Analysis.CStarAlgebra.CStarMatrix.0.CStarMatrix.cobounded_eq_aux : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalCStarAlgebra A] [inst_3 : PartialOrder A] [inst_4 : StarOrderedRing A],
  Bornology.cobounded (CStarMatrix m n A) = Bornology.cobounded (m → n → A)
-- Mathlib.RingTheory.Bialgebra.Convolution
_private.Mathlib.RingTheory.Bialgebra.Convolution.0.BialgHom.convPow_succ : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C] [inst_5 : Coalgebra.IsCocomm R C] (f : WithConv (C →ₐc[R] A))
  (n : ℕ), f ^ (n + 1) = f ^ n * f
-- Mathlib.Order.WithBotTop
WithBotTop.coe_injective : ∀ {ι : Type u_1}, Function.Injective WithBotTop.coe
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.eq_top_iff' : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (A : NonUnitalSubring R), A = ⊤ ↔ ∀ (x : R), x ∈ A
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.alterKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f : Option (β k) → Option (β k))
  (l : List ((a : α) × β a)),
  Std.Internal.List.alterKey k f l =
    match f (Std.Internal.List.getValueCast? k l) with
    | none => Std.Internal.List.eraseKey k l
    | some v => Std.Internal.List.insertEntry k v l
-- Mathlib.Topology.Partial
rtendsto_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {r : SetRel Y X} {l : Filter Y} {x : X},
  Filter.RTendsto r l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.core s ∈ l
-- Init.Grind.AC
Lean.Grind.AC.eq_erase0 : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (lhs rhs lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_erase0_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' = Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.Order.Interval.Set.Image
StrictAnti.mapsTo_Iio : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  StrictAnti f → Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
-- Mathlib.GroupTheory.Generators
Group.Generators.lift_val_surjective : ∀ {G : Type u_1} {ι : Type u_3} [inst : Group G] (P : Group.Generators G ι), Function.Surjective ⇑(FreeGroup.lift P.val)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformEmbedding_iff' : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.nonneg : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) {x : M} [inst_5 : FiniteDimensional ℝ E], 0 ≤ ↑f x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPushout.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square Cᵒᵖ},
  sq.IsPushout → sq.unop.IsPullback
-- Mathlib.RingTheory.PowerSeries.Catalan
PowerSeries.catalanSeries_sq_mul_X_add_one : PowerSeries.catalanSeries ^ 2 * PowerSeries.X + 1 = PowerSeries.catalanSeries
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.id_apply : ∀ (M : Type u_1) [inst : Monoid M] {R : Type u_10} [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (x : R),
  (MulSemiringActionHom.id M) x = x
-- Mathlib.GroupTheory.OrderOfElement
IsConj.isOfFinOrder : ∀ {G : Type u_1} [inst : Monoid G] {x y : G}, IsConj x y → IsOfFinOrder x → IsOfFinOrder y
-- Mathlib.Logic.Nonempty
/-- Using `Classical.choice`, extracts a term from a `Nonempty` type.  -/
Classical.arbitrary : (α : Sort u_3) → [h : Nonempty α] → α
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- If the product `X ⨯ Y` and the weak equalizer of `π₁ ≫ f` and `π₂ ≫ g` exist, then the
weak pullback of `f` and `g` exists: it is given by composing the equalizer with the projections.  -/
CategoryTheory.Limits.hasWeakLimit_cospan_of_hasLimit_pair_of_hasWeakLimit_parallelPair : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)]
  [CategoryTheory.Limits.HasWeakLimit
      (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g))],
  CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.cospan f g)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_of_degree_eq_one : ∀ {p : Polynomial ℂ}, p.degree = 1 → p.logMahlerMeasure = Real.log ‖p.coeff 1‖ + ‖(p.coeff 1)⁻¹ * p.coeff 0‖.posLog
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- A cocone is colimit iff it becomes limit after the
application of `yoneda.obj X` for all `X : C`.  -/
CategoryTheory.Limits.Cocone.isColimitYonedaEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            CategoryTheory.Limits.IsColimit c ≃
              ((X : C) → CategoryTheory.Limits.IsLimit ((CategoryTheory.yoneda.obj X).mapCone c.op))
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.congr_app : ∀ {X Y : AlgebraicGeometry.Scheme} {f g : X ⟶ Y} (e : f = g) (U : Y.Opens),
  AlgebraicGeometry.Scheme.Hom.app f U =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U)
      (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- The congruence relation induced by `c` on `single i j`.  -/
RingCon.ofMatrix : {R : Type u_1} →
  {n : Type u_2} →
    [inst : NonUnitalNonAssocSemiring R] → [inst_1 : Fintype n] → [DecidableEq n] → RingCon (Matrix n n R) → RingCon R
-- Mathlib.Topology.Algebra.MulAction
Submonoid.continuousSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : Monoid M]
  [inst_3 : MulAction M X] [ContinuousSMul M X] {S : Submonoid M}, ContinuousSMul (↥S) X
-- Init.Data.BitVec.Lemmas
BitVec.twoPow_zero : ∀ {w : ℕ}, BitVec.twoPow w 0 = 1#w
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.toList_cons : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Internal.AssocList α β} {a : α} {b : β a},
  (Std.DHashMap.Internal.AssocList.cons a b l).toList = ⟨a, b⟩ :: l.toList
-- Mathlib.RingTheory.Regular.RegularSequence
_private.Mathlib.RingTheory.Regular.RegularSequence.0.RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing.match_1.eq_1 : ∀ (α : Type u_1) (x : CommRing α) (M : Type u_2) (x_1 : AddCommGroup M) (x_2 : Module α M) (r : α) (rs : List α)
  (motive :
    IsSMulRegular M r ∧
        RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) →
      Sort u_3)
  (h1 : IsSMulRegular M r)
  (h2 : RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs))
  (h_1 :
    (h1 : IsSMulRegular M r) →
      (h2 :
          RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) →
        motive ⋯),
  (match ⋯ with
    | ⋯ => h_1 h1 h2) =
    h_1 h1 h2
-- Mathlib.Order.SupClosed
infClosed_range : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  [inst_2 : FunLike F α β] [InfHomClass F α β] (f : F), InfClosed (Set.range ⇑f)
-- Mathlib.LinearAlgebra.Trace
/-- **Alias** of the forward direction of `LinearMap.IsIdempotentElem.trace_eq_zero_iff`.

---

An idempotent endomorphism of a module over a characteristic-zero commutative ring
with vanishing trace is the zero map, provided its range and kernel are finite and free.

The `Module.Free` and `Module.Finite` instance arguments on `range e` and `ker e` are
automatic over a field, and more generally over any principal ideal domain `R` for which
`M` itself is finite and free (submodules of finite free modules over a PID are finite
and free).  -/
LinearMap.IsIdempotentElem.eq_zero_of_trace_eq_zero : ∀ {R : Type u_6} [inst : CommRing R] [CharZero R] {M : Type u_7} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  {e : M →ₗ[R] M},
  IsIdempotentElem e →
    ∀ [Module.Free R ↥e.range] [Module.Finite R ↥e.range] [Module.Free R ↥e.ker] [Module.Finite R ↥e.ker],
      (LinearMap.trace R M) e = 0 → e = 0
-- Mathlib.Algebra.CubicDiscriminant
Cubic.of_a_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R],
  P.a = 0 → P.toPoly = Polynomial.C P.b * Polynomial.X ^ 2 + Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
-- Mathlib.Order.Category.Preord
Preord.comp_apply : ∀ {X Y Z : Preord} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic.eval_apply : ∀ {R : Type u_1} {S : Type u_2} (q : R) (n : ℕ) [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  Polynomial.eval (f q) (Polynomial.cyclotomic n S) = f (Polynomial.eval q (Polynomial.cyclotomic n R))
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.SheafedSpace.colimit_exists_rep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  [inst_2 : Small.{v, w} J] (F : CategoryTheory.Functor J (AlgebraicGeometry.SheafedSpace C))
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] (x : ↑↑(CategoryTheory.Limits.colimit F).toPresheafedSpace),
  ∃ i y, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i).hom.base) y = x
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyMap_exact₃_of_distTriang : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
  (hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ)
  (h : autoParam (n₀ + 1 = n₁) CochainComplex.homologyMap_exact₃_of_distTriang._auto_1),
  { X₁ := HomologicalComplex.homology T.obj₂ n₀, X₂ := HomologicalComplex.homology T.obj₃ n₀,
      X₃ := HomologicalComplex.homology T.obj₁ n₁, f := HomologicalComplex.homologyMap T.mor₂ n₀,
      g := CochainComplex.homologyδOfTriangle T n₀ n₁ h, zero := ⋯ }.Exact
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSigma_ground_eq : ∀ {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {h : Pairwise (Function.onFun Disjoint fun i => (M i).E)},
  (Matroid.disjointSigma M h).E = ⋃ i, (M i).E
-- Mathlib.RingTheory.Valuation.Basic
Valuation.instCommGroupWithZeroSubtypeMemSubmonoidMrangeMonoidWithZeroHomOfClass : {K : Type u_4} →
  {Γ₀ : Type u_6} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : DivisionRing K] →
        (v : Valuation K Γ₀) → CommGroupWithZero ↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v))
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- The structure for `apply` lemmas stored in the `RefinedDiscrTree`.  -/
Mathlib.Tactic.ClickSuggestions.ApplyLemma : Type
-- Mathlib.Data.Num.Basic
/-- Ordering on `ZNum`s.  -/
ZNum.cmp : ZNum → ZNum → Ordering
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
the base is nonnegative and positive when the base is positive.
This is the `NNReal` analogue of `evalRpow` for `Real`.  -/
Mathlib.Meta.Positivity.evalNNRealRpow : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.isInducing : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} {T : Set (Set β)},
  Topology.IsInducing f →
    TopologicalSpace.IsTopologicalBasis T → TopologicalSpace.IsTopologicalBasis (Set.preimage f '' T)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Connected.dist_triangle : ∀ {V : Type u_1} {G : SimpleGraph V} {u v w : V}, G.Connected → G.dist u w ≤ G.dist u v + G.dist v w
-- Lean.Util.MonadCache
Lean.MonadStateCacheT.instMonadControl : {α β : Type} →
  {m : Type → Type} → [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → MonadControl m (Lean.MonadStateCacheT α β m)
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_exp_mul_Ioi : ∀ {a : ℝ}, a < 0 → ∀ (c : ℝ), MeasureTheory.IntegrableOn (fun x => Real.exp (a * x)) (Set.Ioi c) MeasureTheory.volume
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ici_zero_eq_univ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : Zero α] [IsBotZeroClass α]
  [inst_4 : Fintype α], Finset.Ici 0 = Finset.univ
-- Mathlib.Algebra.WithConv
WithConv.toConv_zero : ∀ {A : Type u_2} [inst : AddMonoid A], WithConv.toConv 0 = 0
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.GetElem?.match_1.eq_1 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (e : elem) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match some e with
    | some e => h_1 e
    | none => h_2 ()) =
    h_1 e
-- Mathlib.NumberTheory.MulChar.Basic
/-- The sum over all values of the trivial multiplicative character on a finite ring is
the cardinality of its unit group.  -/
MulChar.sum_one_eq_card_units : ∀ {R : Type u_1} [inst : CommMonoid R] [inst_1 : Fintype R] {R' : Type u_2} [inst_2 : CommRing R']
  [inst_3 : DecidableEq R], ∑ a, 1 a = ↑(Fintype.card Rˣ)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.restrictFunctor_obj_left : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), (X.restrictFunctor.obj U).left = ↑U
-- Mathlib.Algebra.Module.PUnit
PUnit.distribMulAction : {R : Type u_1} → [inst : Monoid R] → DistribMulAction R PUnit.{u_3 + 1}
-- Mathlib.NumberTheory.Padics.PadicNumbers
Rat.padicValuation_cast : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (x : ℤ), (Rat.padicValuation p) ↑x = (Int.padicValuation p) x
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAt_sub_const_iff : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasFDerivAt (fun x => f x - c) f' x ↔ HasFDerivAt f f' x
-- Init.Data.Iterators.Basic
Std.Iter.toIterM_toIter : ∀ {α β : Type w} (it : Std.IterM Id β), it.toIter.toIterM = it
-- Mathlib.LinearAlgebra.TensorProduct.Defs
_private.Mathlib.LinearAlgebra.TensorProduct.Defs.0.TensorProduct.addMonoidWithWrongNSMul : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → AddMonoid (TensorProduct R M N)
-- Mathlib.Tactic.TermCongr
/-- Monad for `mkCongrOfAux`, for caching `CongrResult`s.  -/
Mathlib.Tactic.TermCongr.M : Type → Type
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_and_wOppSide_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WSameSide x y ∧ s.WOppSide x y ↔ x ∈ s ∨ y ∈ s
-- Mathlib.Logic.Denumerable
Denumerable.ofNat_encode : ∀ {α : Type u_1} [inst : Denumerable α] (a : α), Denumerable.ofNat α (Encodable.encode a) = a
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.one_div_mul : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r : R} {s t : ↥S},
  1 /ₒ t * (r /ₒ s) = r /ₒ (s * t)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintTextEdit.newText : Lean.Elab.InlayHintTextEdit → String
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_le_iff : ∀ {a : ENNReal} {r : NNReal}, ↑r ≤ a ↔ ∀ (p : NNReal), a = ↑p → r ≤ p
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_mul : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A B : Matrix.SpecialLinearGroup n R), ↑(A * B) = ↑A * ↑B
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.mk.injEq : ∀ (declName : Lean.Name) (levelParams : List Lean.Name) (type value : Lean.Expr) (declNames : Array Lean.Name)
  (declNameNonRec : Lean.Name) (fixedParamPerms : Lean.Elab.FixedParamPerms)
  (fixpointType : Array Lean.Elab.PartialFixpointType) (declName_1 : Lean.Name) (levelParams_1 : List Lean.Name)
  (type_1 value_1 : Lean.Expr) (declNames_1 : Array Lean.Name) (declNameNonRec_1 : Lean.Name)
  (fixedParamPerms_1 : Lean.Elab.FixedParamPerms) (fixpointType_1 : Array Lean.Elab.PartialFixpointType),
  ({ declName := declName, levelParams := levelParams, type := type, value := value, declNames := declNames,
        declNameNonRec := declNameNonRec, fixedParamPerms := fixedParamPerms, fixpointType := fixpointType } =
      { declName := declName_1, levelParams := levelParams_1, type := type_1, value := value_1,
        declNames := declNames_1, declNameNonRec := declNameNonRec_1, fixedParamPerms := fixedParamPerms_1,
        fixpointType := fixpointType_1 }) =
    (declName = declName_1 ∧
      levelParams = levelParams_1 ∧
        type = type_1 ∧
          value = value_1 ∧
            declNames = declNames_1 ∧
              declNameNonRec = declNameNonRec_1 ∧ fixedParamPerms = fixedParamPerms_1 ∧ fixpointType = fixpointType_1)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.mk.inj : ∀ {B : Type u₁} {as as_1 : B}, { as := as } = { as := as_1 } → as = as_1
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Ring.polar_pi : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (Mᵢ i)] [inst_2 : AddCommGroup P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (x y : (i : ι) → Mᵢ i),
  QuadraticMap.polar (⇑(QuadraticMap.pi Q)) x y = ∑ i, QuadraticMap.polar (⇑(Q i)) (x i) (y i)
-- Mathlib.Data.List.Rotate
List.Nodup.rotate_congr_iff : ∀ {α : Type u} {l : List α}, l.Nodup → ∀ {i j : ℕ}, l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
-- Mathlib.Order.Category.FinBoolAlg
/-- The category of finite Boolean algebras with bounded lattice morphisms.  -/
FinBoolAlg : Type (u_1 + 1)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeList.match_3.eq_2 : ∀ {α : Type u_1} (motive : List α → List ℕ → Sort u_2) (xs : List α) (n : ℕ) (ns : List ℕ)
  (h_1 : (xs : List α) → motive xs []) (h_2 : (xs : List α) → (n : ℕ) → (ns : List ℕ) → motive xs (n :: ns)),
  (match xs, n :: ns with
    | xs, [] => h_1 xs
    | xs, n :: ns => h_2 xs n ns) =
    h_2 xs n ns
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.WeaklyRegular.smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.WeaklyRegular] {x : ENNReal}, x ≠ ⊤ → (x • μ).WeaklyRegular
-- Lean.Parser.Types
Lean.Parser.ParserCache.tokenCache : Lean.Parser.ParserCache → Lean.Parser.TokenCacheEntry
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.terminal.comp_from_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] {P Q : C}
  (f : P ⟶ Q) {Z : C} (h : ⊤_ C ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.terminal.from Q) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.terminal.from P) h
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1_of_not_measurableSet : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  ¬MeasurableSet s → ∀ (x : G), MeasureTheory.condExpIndL1 hm μ s x = 0
-- Mathlib.AlgebraicGeometry.Scheme
/-- Pretty printer for applying morphisms of schemes to set-theoretic points.  -/
AlgebraicGeometry.Scheme.delabCoeFunAppNotation : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The functor `SimplexCategory ⥤ SSet` which sends `⦋n⦌` to the standard simplex `Δ[n]` is a
cosimplicial object in the category of simplicial sets. (This functor is essentially given by the
Yoneda embedding).  -/
SSet.stdSimplex : CategoryTheory.CosimplicialObject SSet
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernsteinApproximation.apply_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] (n : ℕ) (f : C(↑unitInterval, E)),
  (bernsteinApproximation n f) 0 = f 0
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ),
  Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.num k) = Lean.Grind.CommRing.denoteSInt k