mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- The skeleton of a braided monoidal category can be viewed as a commutative monoid, where the
multiplication is given by the tensor product, and satisfies the monoid axioms since it is a
skeleton.
 -/
CategoryTheory.Skeleton.instCommMonoid : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CommMonoid (CategoryTheory.Skeleton C)
-- Mathlib.Algebra.Group.Defs
add_neg_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), a + b + -b = a
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.range_polarizationIn_le_span_coroot : ∀ {ι : 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) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : Module S N] [inst_11 : P.IsValuedIn S] [inst_12 : Fintype ι],
  (P.PolarizationIn S).range ≤ P.corootSpan S
-- Mathlib.Data.Quot
/-- Given a class of functions `q : @Quotient (∀ i, α i) _`, returns the class of `i`-th projection
`Quotient (S i)`.  -/
Quotient.eval : {ι : Type u_3} → {α : ι → Sort u_4} → {S : (i : ι) → Setoid (α i)} → Quotient inferInstance → (i : ι) → Quotient (S i)
-- Init.Sym.Lemmas
Lean.Sym.Int64.eq_eq_true : ∀ (a b : Int64), decide (a = b) = true → (a = b) = True
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsStrictRestriction.ssubset : ∀ {α : Type u_1} {M N : Matroid α}, N.IsStrictRestriction M → N.E ⊂ M.E
-- Mathlib.Algebra.Order.Floor.Defs
/-- A version of `Int.cast_strictMono` for floor rings, whose addition is not necessarily
monotone.  -/
FloorRing.intCast_strictMono : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [FloorRing α], StrictMono Int.cast
-- Init.Data.SInt.Basic
/-- Bitwise and for 16-bit signed integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set,
according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.land : Int16 → Int16 → Int16
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instReprTheoremForm.repr : Mathlib.Meta.FunProp.TheoremForm → ℕ → Std.Format
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.trans_symm : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃}, (e₁₂.trans e₂₃).symm = e₂₃.symm.trans e₁₂.symm
-- Mathlib.Topology.EMetricSpace.Diam
/-- If two sets have nonempty intersection, then the extended diameter of their union
is estimated from above by the sum of their union.  -/
Metric.ediam_union_le : ∀ {X : Type u_2} {s t : Set X} [inst : PseudoEMetricSpace X],
  (s ∩ t).Nonempty → Metric.ediam (s ∪ t) ≤ Metric.ediam s + Metric.ediam t
-- Mathlib.Combinatorics.Matroid.Circuit
/-- In a finitary matroid, each finite set `X` spanned by a set `Y` is in fact
spanned by a finite independent subset of `Y`.  -/
Matroid.exists_subset_finite_closure_of_subset_closure : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.Finitary],
  X.Finite → X ⊆ M.closure Y → ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] (X : C),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X))))
      ((CategoryTheory.ConcreteCategory.hom
          ((F.op.lanUnit.app (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj X)).app (Opposite.op X)))
        { down := CategoryTheory.CategoryStruct.id X }) =
    { down := CategoryTheory.CategoryStruct.id (F.obj X) }
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Version of `aeval` for defining algebra homs out of `R[X]` over a smaller base ring
than `R`.  -/
Polynomial.aevalTower : {R : Type u} →
  {S : Type v} →
    {A' : Type u_1} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A'] →
          [inst_2 : CommSemiring S] →
            [inst_3 : Algebra S R] → [inst_4 : Algebra S A'] → (R →ₐ[S] A') → A' → Polynomial R →ₐ[S] A'
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.zero_apply : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Zero β], (UniformOnFun.ofFun 𝔖) 0 = 0
-- Mathlib.Analysis.Normed.Group.Defs
ENormedAddMonoid.toESeminormedAddMonoid : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ENormedAddMonoid E] → ESeminormedAddMonoid E
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (ζ : ↥(NumberField.Units.torsion K)), (NumberField.IsCMField.unitsMulComplexConjInv K) ↑ζ = ζ ^ 2
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.optionPelim'.match_1.splitter : {α : Type u_1} →
  {β : Sort u_3} →
    (motive : (t : Option α) → (t = none → β) → ((val : α) → t = some val → β) → Sort u_2) →
      (t : Option α) →
        (n : t = none → β) →
          (s : (val : α) → t = some val → β) →
            ((a : α) → (n : some a = none → β) → (s : (val : α) → some a = some val → β) → motive (some a) n s) →
              ((n : none = none → β) → (s : (val : α) → none = some val → β) → motive none n s) → motive t n s
-- Mathlib.Order.ULift
ULift.instLawfulLTOrd_mathlib : ∀ {α : Type u} [inst : LT α] [inst_1 : Ord α] [inst_2 : Std.LawfulLTOrd α], Std.LawfulLTOrd (ULift.{v, u} α)
-- Mathlib.CategoryTheory.Yoneda
/-- Any representing object for a representable functor `F` is isomorphic to `reprX F`.  -/
CategoryTheory.Functor.RepresentableBy.isoReprX : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v)) → [hF : F.IsRepresentable] → {Y : C} → F.RepresentableBy Y → (Y ≅ F.reprX)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.ext_iff : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  {f g : A →ₑ+[φ] B}, f = g ↔ ∀ (x : A), f x = g x
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCohomologyRelation.trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} {γ₁ γ₂ γ₃ : CategoryTheory.PresheafOfGroups.OneCochain G U}
  {α β : CategoryTheory.PresheafOfGroups.ZeroCochain G U},
  CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁ γ₂ α →
    CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₂ γ₃ β →
      CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁ γ₃ (β * α)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.triangle_obj₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  (X.triangle f g).obj₂ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.CategoryStruct.comp f g))
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence_functor : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) {G : CategoryTheory.Functor B A}
  (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence hF hG).functor = F.comp eB.inverse
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instSMulOfSMulCommClassRealOfContinuousConstSMul : {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 : ℕ∞} →
                {R : Type u_6} →
                  [inst_4 : Semiring R] →
                    [inst_5 : Module R F] →
                      [SMulCommClass ℝ R F] → [ContinuousConstSMul R F] → SMul R (TestFunction Ω F n)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.analyticOnNhd_weierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ), AnalyticOnNhd ℂ (L.weierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_stalkPushforward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y),
  CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯)
      (TopCat.Presheaf.stalkPushforward C f F x) =
    CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F y) (F.stalkSpecializes h)
-- Mathlib.Algebra.DirectSum.Basic
instCoeFunDirectSumForall : (ι : Type u_1) →
  (β : ι → Type u_2) → [inst : (i : ι) → AddCommMonoid (β i)] → CoeFun (DirectSum ι β) fun x => (a : ι) → β a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Functor.toOver_comp_forget : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} S]
  (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X)
  (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y),
  (F.toOver X f ⋯).comp (CategoryTheory.Over.forget X) = F
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_zero_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c x : P), EuclideanGeometry.inversion c 0 x = c
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk_coe : ∀ {α : Type u_2} [inst : TopologicalSpace α] (U : TopologicalSpace.Opens α), { carrier := ↑U, is_open' := ⋯ } = U
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.update_eq_add_sub_coeff : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (n : ℕ) (a : R),
  p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
and `B ⟶ X` is an arrow of `S`. This is the hom `B ⟶ X`, as an arrow.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {X : C} → {S : J.Cover X} → {T : (I : S.Arrow) → J.Cover I.Y} → (S.bind T).Arrow → S.Arrow
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_inv_app : ∀ (X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair),
  CategoryTheory.Limits.walkingSpanOpEquiv.counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.GroupTheory.DivisibleHull
/-- If `f : M → ℕ+ → M → ℕ+ → α` respects the equivalence on
localization, lift it to a function `DivisibleHull M → DivisibleHull M → α`.  -/
DivisibleHull.liftOn₂ : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {α : Type u_2} →
      DivisibleHull M →
        DivisibleHull M →
          (f : M → ℕ+ → M → ℕ+ → α) →
            (∀ (m n m' n' : M) (s t s' t' : ℕ+),
                DivisibleHull.mk m s = DivisibleHull.mk m' s' →
                  DivisibleHull.mk n t = DivisibleHull.mk n' t' → f m s n t = f m' s' n' t') →
              α
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.map_one₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P}
  (f : M →* N →* P) (n : N), (f 1) n = 1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Continuous.borel_measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → Measurable f
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.range_lift : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {K : Type u_3} [inst_2 : Group K] (f : G →* K)
  (g : H →* K), (Monoid.Coprod.lift f g).range = f.range ⊔ g.range
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- If `g` is a collection of subsets of `α` such that the `σ`-algebra generated from `g` contains
the same sets as `g`, then `g` was already a `σ`-algebra.  -/
MeasurableSpace.mkOfClosure : {α : Type u_1} → (g : Set (Set α)) → {t | MeasurableSet t} = g → MeasurableSpace α
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂_compl₁₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₁' : Type u_8} {M₂' : Type u_9} {n : Type u_11} {m : Type u_12}
  {n' : Type u_13} {m' : Type u_14} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m]
  [inst_8 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : AddCommMonoid M₁']
  [inst_10 : Module R M₁'] [inst_11 : AddCommMonoid M₂'] [inst_12 : Module R M₂'] (b₁' : Module.Basis n' R M₁')
  (b₂' : Module.Basis m' R M₂') [inst_13 : Fintype n'] [inst_14 : Fintype m'] [inst_15 : DecidableEq n']
  [inst_16 : DecidableEq m'] (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R),
  ((Matrix.toLinearMap₂ b₁ b₂) M).compl₁₂ ((Matrix.toLin b₁' b₁) P) ((Matrix.toLin b₂' b₂) Q) =
    (Matrix.toLinearMap₂ b₁' b₂') (P.transpose * M * Q)
-- Mathlib.Data.ENat.Basic
ENat.lift_add : ∀ (a b : ℕ∞) (h : a + b < ⊤), (a + b).lift h = a.lift ⋯ + b.lift ⋯
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.mk.inj : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} {inst : Field F} {inst_1 : Field E} {inst_2 : Field K}
  {inst_3 : Algebra F E} {inst_4 : Algebra F K} {carrier : IntermediateField F E} {emb : ↥carrier →ₐ[F] K}
  {carrier_1 : IntermediateField F E} {emb_1 : ↥carrier_1 →ₐ[F] K},
  { carrier := carrier, emb := emb } = { carrier := carrier_1, emb := emb_1 } → carrier = carrier_1 ∧ emb ≍ emb_1
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_zero : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q), LinearMap.ofIsCompl h 0 0 = 0
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplexCompIso_hom_app_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W] [inst_3 : CategoryTheory.Preadditive W] {W' : Type u_5}
  [inst_4 : CategoryTheory.Category.{u_6, u_5} W'] [inst_5 : CategoryTheory.Preadditive W']
  {F : CategoryTheory.Functor V W} {G : CategoryTheory.Functor W W'} {H : CategoryTheory.Functor V W'}
  (e : F.comp G ≅ H) [inst_6 : F.Additive] [inst_7 : G.Additive] [inst_8 : H.Additive] (c : ComplexShape ι)
  (C : HomologicalComplex V c) (x : ι),
  ((CategoryTheory.Functor.mapHomologicalComplexCompIso e c).hom.app C).f x = e.hom.app (C.X x)
-- Mathlib.SetTheory.Lists
Lists'.toList.eq_2 : ∀ {α : Type u_1}, Lists'.nil.toList = []
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SymM.run : {α : Type} → Lean.Meta.Sym.SymM α → Lean.MetaM α
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.prod_neg : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : CommMonoid M] [inst_1 : HasDistribNeg M] (f : ι → M),
  ∏ x ∈ s, -f x = (-1) ^ s.card * ∏ x ∈ s, f x
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_mul_unit_left_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsUnit x → (IsRelPrime (x * y) z ↔ IsRelPrime y z)
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- `MonoidAlgebra.single n m` for `m : M`, `r : R` is the element `rm : PolynomialModule R M`.  -/
PolynomialModule.single : (R : Type u_2) →
  {M : Type u_3} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ℕ → M → PolynomialModule R M
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.distortion_single : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} [inst : Fintype ι] (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I J hJ x h).distortion = J.distortion
-- Mathlib.Tactic.Translate.Reorder
/-- Try to determine the value of the `(reorder := ...)` option that would be needed to translate
type `e₁` to type `e₂`. If there is no good guess, default to `[]`.
The heuristic that we use is to compare the conclusions of `e₁` and `e₂`,
and to observe which variables are swapped.
We also apply this heuristic recursively in hypotheses.  -/
Mathlib.Tactic.Translate.guessReorder : Lean.Expr → Lean.Expr → Lean.MetaM Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.RingTheory.WittVector.WittPolynomial
xInTermsOfW_vars_aux : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ Finset.range (n + 1)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.instIsProbabilityMeasureForallTrajMeasure : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)}
  [MeasureTheory.IsProbabilityMeasure μ₀],
  MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.Kernel.trajMeasure μ₀ κ)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
CategoryTheory.Limits.PreservesInitial.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasInitial C]
  [inst_3 : CategoryTheory.Limits.HasInitial D]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G],
  (CategoryTheory.Limits.PreservesInitial.iso G).inv = CategoryTheory.Limits.initialComparison G
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.apply_iterate : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ},
  Function.IsPeriodicPt f n x → ∀ (m : ℕ), Function.IsPeriodicPt f n (f^[m] x)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyLE! : {α : Type u} → {β : α → Type v} → [Ord α] → [Inhabited α] → α → Std.DTreeMap.Internal.Impl α β → α
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instMinOfLinearOrder : {α : Type u_1} → [inst : AddMonoid α] → [LinearOrder α] → Min (AddUnits α)
-- Std.Time.Date.Unit.Weekday
/-- Monday.  -/
Std.Time.Weekday.monday : Std.Time.Weekday
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- **Alias** of `MeasureTheory.measure_inter_add_sdiff₀`.

---

A null measurable set `t` is Carathéodory measurable: for any `s`, we have
`μ (s ∩ t) + μ (s \ t) = μ s`.  -/
MeasureTheory.measure_inter_add_diff₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasureTheory.NullMeasurableSet t μ → μ (s ∩ t) + μ (s \ t) = μ s
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_5} {H : ι → AddSubgroup G} [∀ (i : ι), (H i).Characteristic],
  (⨅ i, H i).Characteristic
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddEquiv.subsemigroupMap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : ↥S),
  ↑((e.subsemigroupMap S) x) = e ↑x
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.continuousAt_rpow_const : ∀ (x q : ℝ), x ≠ 0 ∨ 0 ≤ q → ContinuousAt (fun x => x ^ q) x
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBase.isBasis_of_isRestriction : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α}, N.IsBase I → N.IsRestriction M → M.IsBasis I N.E
-- Mathlib.RepresentationTheory.Coinvariants
Rep.instIsLeftAdjointModuleCatCoinvariantsFunctor : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G], (Rep.coinvariantsFunctor k G).IsLeftAdjoint
-- Mathlib.Data.ZMod.Basic
ZMod.cast_id' : ∀ {n : ℕ}, ZMod.cast = id
-- Init.Data.List.TakeDrop
List.takeWhile_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {l : List α},
  List.takeWhile p (List.map f l) = List.map f (List.takeWhile (p ∘ f) l)
-- Mathlib.Topology.WithTopology
WithTopology.instMin.eq_1 : ∀ {X : Type u_1} (t : TopologicalSpace X) [inst : Min X],
  WithTopology.instMin t = { min := fun x y => WithTopology.toTopology t (x.ofTopology ⊓ y.ofTopology) }
-- Mathlib.Algebra.DirectSum.Basic
/-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type
`ι₂` together with the fibres of a map `f : ι₁ → ι₂`.  -/
DirectSum.sigmaFiberAddEquiv : {ι₁ ι₂ : Type v} →
  [DecidableEq ι₂] →
    (f : ι₁ → ι₂) →
      {β : ι₁ → Type w} →
        [inst : (i : ι₁) → AddCommMonoid (β i)] →
          (DirectSum ι₁ fun i => β i) ≃+ DirectSum ι₂ fun j => DirectSum { i // f i = j } fun i => β ↑i
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mod2Shift : USize → USize → USize
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        Std.DHashMap.Internal.Raw₀.Const.get? (m₁.inter m₂) k =
          if m₂.contains k = true then Std.DHashMap.Internal.Raw₀.Const.get? m₁ k else none
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.compl_truncatedSup : ∀ {α : Type u_1} [inst : BooleanAlgebra α] [inst_1 : DecidableLE α] (s : Finset α) (a : α),
  (s.truncatedSup a)ᶜ = s.compls.truncatedInf aᶜ
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomAddAct.vadd_aeeqFun_aeeq : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : VAdd M α] [inst_3 : MeasurableConstVAdd M α]
  [inst_4 : MeasureTheory.VAddInvariantMeasure M α μ] (c : Mᵈᵃᵃ) (f : α →ₘ[μ] β),
  ↑(c +ᵥ f) =ᵐ[μ] fun x => ↑f (DomAddAct.mk.symm c +ᵥ x)
-- Mathlib.Data.FunLike.Group
FunLike.involutiveNeg.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : InvolutiveNeg β]
  [inst_3 : IsNegApply F α β], FunLike.involutiveNeg = Function.Injective.involutiveNeg (fun f => ⇑f) ⋯ ⋯