mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.Hom.hom_comp_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) {Z' : C}
  (P' : CategoryTheory.ProjectiveResolution Z') {f : Z ⟶ Z'} (φ : P.Hom P' f),
  CategoryTheory.CategoryStruct.comp φ.hom P'.π =
    CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)
-- Mathlib.Util.Notation3
/-- Matches applications.  -/
Mathlib.Notation3.matchApp : Mathlib.Notation3.Matcher → Mathlib.Notation3.Matcher → Mathlib.Notation3.Matcher
-- Mathlib.Computability.EpsilonNFA
εNFA.IsPath.nil : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} (s : σ), M.IsPath s s []
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g))
  {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).SpecTensorTo h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback f g).fromSpecResidueField t) h
-- Std.Time.Format
/-- Formats a `PlainTime` using a specific format.
 -/
Std.Time.PlainTime.format : Std.Time.PlainTime → String → String
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.coe_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubmonoid M), ↑s.topologicalClosure = closure ↑s
-- Mathlib.RingTheory.Etale.StandardEtale
/-- `R[X][Y]/⟨f, Yg-1⟩ ≃ R[X][1/g]/f`  -/
StandardEtalePair.equivAwayQuotient : {R : Type u_1} →
  [inst : CommRing R] →
    (P : StandardEtalePair R) →
      P.Ring ≃ₐ[R] Localization.Away P.g ⧸ Ideal.span {(algebraMap (Polynomial R) (Localization.Away P.g)) P.f}
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α), (t₁.erase k).Equiv (t₂.erase k)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.instIsContinuousCompId_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K],
  ((CategoryTheory.Functor.id C).comp F).IsContinuous J K
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- For any object `J : CardinalDirectedPoset κ`, this is a colimit
cocone exhibiting `J` as the colimit of its subsets
that are of cardinality `< κ` and have a terminal object.  -/
CategoryTheory.CardinalDirectedPoset.cocone : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) →
      CategoryTheory.Limits.Cocone (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet J.PropSet)
-- Mathlib.Tactic.CategoryTheory.Elementwise
_private.Mathlib.Tactic.CategoryTheory.Elementwise.0.Mathlib.Tactic.Elementwise.elementwiseExpr.mkHomElementwise : {α : Type} →
  [Inhabited α] →
    Lean.Expr →
      Lean.Expr → (Lean.Expr → Option (Lean.Level × Lean.Level × Array Lean.Expr) → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.mem_vanishingIdeal_iff : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  {V : Set (σ → K)} {p : MvPolynomial σ k}, p ∈ MvPolynomial.vanishingIdeal k V ↔ ∀ x ∈ V, (MvPolynomial.aeval x) p = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput.cin : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig → aig.Ref
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The action by a subfield is the action by the underlying field.  -/
Subfield.instMulSemiringActionSubtypeMem : {K : Type u} →
  [inst : DivisionRing K] →
    {X : Type u_1} → [inst_1 : Semiring X] → [MulSemiringAction K X] → (F : Subfield K) → MulSemiringAction (↥F) X
-- Mathlib.Probability.Independence.Process.Basic
/-- A random variable $X$ is independent from a stochastic process $(Y_s)_{s \in S}$  if
for all $s_1, ..., s_p \in S$ the variable $Y$ is independent from the family
$(X_{s_1}, ..., X_{s_p})$.  -/
ProbabilityTheory.Kernel.IndepFun.indepFun_process : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : Type u_5} {𝓨 : S → Type u_6}
  [inst : MeasurableSpace 𝓧] [inst_1 : (i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i},
  Measurable X →
    (∀ (i : S), Measurable (Y i)) →
      (∀ (I : Finset S), ProbabilityTheory.Kernel.IndepFun X (fun ω i => Y (↑i) ω) κ P) →
        ∀ [ProbabilityTheory.IsZeroOrMarkovKernel κ], ProbabilityTheory.Kernel.IndepFun X (fun ω i => Y i ω) κ P
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.natTransExtension_app : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] {F₁ F₂ : CategoryTheory.Functor W.Localization D}
  (τ : W.Q.comp F₁ ⟶ W.Q.comp F₂) (X : W.Localization),
  (CategoryTheory.Localization.Construction.natTransExtension τ).app X =
    CategoryTheory.Localization.Construction.NatTransExtension.app τ X
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : SizeOf M] (toSubmonoid : Submonoid M)
  (mulSaturated : toSubmonoid.MulSaturated),
  sizeOf { toSubmonoid := toSubmonoid, mulSaturated := mulSaturated } = 1 + sizeOf toSubmonoid
-- Lean.Meta.Basic
/-- `dependsOnHigherOrderOutParam` is true if the type of this parameter depends on
the higher-order output parameter of a previous local instance.
Example:
```
getElem :
  {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
  {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
  (xs : cont) → (i : idx) → dom xs i → elem
```
This flag is true for the parameter with type `dom xs i` since `dom` is an output parameter
of the instance `[self : GetElem cont idx elem dom]`
 -/
Lean.Meta.ParamInfo.dependsOnHigherOrderOutParam : Lean.Meta.ParamInfo → Bool
-- Mathlib.SetTheory.ZFC.Class
Class.ext_iff : ∀ {x y : Class.{u}}, x = y ↔ ∀ (z : ZFSet.{u}), x z ↔ y z
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.range.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N),
  f.range = (Subgroup.map f ⊤).copy (Set.range ⇑f) ⋯
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume_eq_det : ∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] (L : Submodule ℤ (ι → ℝ)) [inst_2 : DiscreteTopology ↥L]
  [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L),
  ZLattice.covolume L MeasureTheory.volume = |(Matrix.of (Subtype.val ∘ ⇑b)).det|
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An equivalence between `MonoOver A` and `MonoOver B` gives an equivalence
between `Subobject A` and `Subobject B`.  -/
CategoryTheory.Subobject.lowerEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {A : C} →
          {B : D} →
            (CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B) →
              (CategoryTheory.Subobject A ≌ CategoryTheory.Subobject B)
-- Init.SizeOf
BitVec.ofFin.sizeOf_spec : ∀ {w : ℕ} (toFin : Fin (2 ^ w)), sizeOf { toFin := toFin } = 1 + sizeOf toFin
-- Mathlib.Algebra.DirectSum.Module
/-- Coproducts in the categories of modules and additive monoids commute with the forgetful functor
from modules to additive monoids.  -/
DirectSum.coe_toModule_eq_coe_toAddMonoid : ∀ (R : Type u) [inst : Semiring R] (ι : Type v) {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (N : Type u₁) [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] (φ : (i : ι) → M i →ₗ[R] N),
  ⇑(DirectSum.toModule R ι N φ) = ⇑(DirectSum.toAddMonoid fun i => (φ i).toAddMonoidHom)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a : α}, (t.getKey? a).isSome = t.contains a
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.representableByUliftFunctorEquiv_apply_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {X : C}
  (R : (F.comp CategoryTheory.uliftFunctor.{w, v}).RepresentableBy X) {Y : C},
  (CategoryTheory.Functor.representableByUliftFunctorEquiv R).homEquiv = R.homEquiv.trans Equiv.ulift
-- Init.WFExtrinsicFix
/-- A fixpoint combinator that allows for deferred proofs of termination.

`extrinsicFix₃ R F` is function implemented as the loop
`extrinsicFix₃ R F a b c = F a b c (fun a b c _ => extrinsicFix₃ R F a b c)`.

If the loop can be shown to be well-founded, `extrinsicFix₃_eq_apply` proves that it satisfies the
fixpoint equation. Otherwise, `extrinsicFix₃ R F` is opaque, i.e., it is impossible to prove
nontrivial properties about it.
 -/
WellFounded.extrinsicFix₃ : {α : Sort u_1} →
  {β : α → Sort u_2} →
    {γ : (a : α) → β a → Sort u_3} →
      {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4} →
        [∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)] →
          (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop) →
            ((a : α) →
                (b : β a) →
                  (c : γ a b) →
                    ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c) →
              (a : α) → (b : β a) → (c : γ a b) → C₃ a b c
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.rootSpan_map_toPerfPair : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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),
  Submodule.map (↑P.toPerfPair) (P.rootSpan R) = Submodule.span R (Set.range P.root')
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  Function.Injective f →
    Measurable f → (∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)) → MeasurableEmbedding f
-- Init.Notation
/-- "Dependent" if-then-else, normally written via the notation `if h : c then t(h) else e(h)`,
is sugar for `dite c (fun h => t(h)) (fun h => e(h))`, and it is the same as
`if c then t else e` except that `t` is allowed to depend on a proof `h : c`,
and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypothesis,
even though it has different types in the two cases.)

We use this to be able to communicate the if-then-else condition to the branches.
For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to
avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...`
to avoid the bounds check inside the if branch. (Of course in this case we have only
lifted the check into an explicit `if`, but we could also use this proof multiple times
or derive `i < arr.size` from some other proposition that we are checking in the `if`.)
 -/
termDepIfThenElse : Lean.ParserDescr
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedPriority : Inhabited Aesop.Frontend.Priority
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.local_affine : ∀ (self : AlgebraicGeometry.Scheme) (x : ↑self.toTopCat),
  ∃ U R, Nonempty (self.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instCommGroup : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : CommGroup γ] → [IsTopologicalGroup γ] → CommGroup (α →ₘ[μ] γ)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- The non-unital subsemiring `R` of the non-unital semiring `R`.  -/
NonUnitalSubsemiring.instTop : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → Top (NonUnitalSubsemiring R)
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.add : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [inst : Add β] {g : α → β},
  Filter.EventuallyConst f l → Filter.EventuallyConst g l → Filter.EventuallyConst (f + g) l
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_mul_right_self : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [I.IsTwoSided], I ⊔ I * J = I
-- Mathlib.Topology.UniformSpace.Cauchy
UniformSpace.subset_countable_closure_of_almost_dense_set : ∀ {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (s : Set α),
  (∀ U ∈ uniformity α, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U) → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
-- Mathlib.RingTheory.IsAdjoinRoot
/-- The basis on `S` generated by powers of `h.root`.

Auxiliary definition for `IsAdjoinRootMonic.powerBasis`.  -/
IsAdjoinRootMonic.basis : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        {f : Polynomial R} → [inst_2 : Algebra R S] → IsAdjoinRootMonic S f → Module.Basis (Fin f.natDegree) R S
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [inst_2 : Small.{v, u₂} K] [inst_3 : CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))),
  CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimitCone F)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_id : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {g : σ → R} (p : MvPolynomial σ R),
  MvPolynomial.eval₂ (RingHom.id R) g p = (MvPolynomial.eval g) p
-- Mathlib.Data.Finset.Sigma
biInf_finsetSigma' : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset ι)
  (t : (i : ι) → Finset (α i)) (f : (i : ι) → α i → β), ⨅ i ∈ s, ⨅ j ∈ t i, f i j = ⨅ ij ∈ s.sigma t, f ij.fst ij.snd
-- Mathlib.RingTheory.Perfection
PerfectionMap.comp_symm_equiv' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π),
  π.comp ↑m.equiv.symm = Perfection.coeff R p 0
-- Mathlib.Data.ENNReal.Basic
ENNReal.forall_ne_top : ∀ {p : ENNReal → Prop}, (∀ (x : ENNReal), x ≠ ⊤ → p x) ↔ ∀ (x : NNReal), p ↑x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_of_injOn : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (e : ι → κ),
  Set.InjOn e ↑s →
    Set.MapsTo e ↑s ↑t → (∀ i ∈ t, i ∉ e '' ↑s → g i = 1) → (∀ i ∈ s, f i = g (e i)) → ∏ i ∈ s, f i = ∏ j ∈ t, g j
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_FG : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.contentIdeal.FG
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Cat} (F : X ⟶ Y)
  {X_1 Y_1 : CategoryTheory.Join C ↑X} (f : X_1 ⟶ Y_1),
  ((CategoryTheory.Join.pseudofunctorRight C).map F).toFunctor.map f =
    CategoryTheory.Join.homInduction (fun x x_1 f => (CategoryTheory.Join.inclLeft C ↑Y).map f)
      (fun x x_1 g => (CategoryTheory.Join.inclRight C ↑Y).map (F.toFunctor.map g))
      (fun c d => CategoryTheory.Join.edge c (F.toFunctor.obj d)) f
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.Bool.and_congr : ∀ (lhs rhs lhs' rhs' : Bool), lhs' = lhs → rhs' = rhs → (lhs' && rhs') = (lhs && rhs)
-- Mathlib.CategoryTheory.Sites.Canonical
/-- A variant of `yonedaCompSheafToPresheaf` with a raise in the universe level.  -/
CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] →
        (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).comp
            (CategoryTheory.sheafToPresheaf J (Type (max v w))) ≅
          CategoryTheory.uliftYoneda.{w, v, u}
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- The category of nonempty finite linear orders.  -/
NonemptyFinLinOrd : Type (u_1 + 1)
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- Two indexed families of points that are injective on the given
`Finset`s and with the same points in the image of those `Finset`s
have the same centroid.  -/
Finset.centroid_eq_of_inj_on_of_image_eq : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {ι₂ : Type u_5} (s₂ : Finset ι₂) {p : ι → P},
  (∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) →
    ∀ {p₂ : ι₂ → P},
      (∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j) → p '' ↑s = p₂ '' ↑s₂ → Finset.centroid k s p = Finset.centroid k s₂ p₂
-- Mathlib.Probability.HasLaw
ProbabilityTheory.hasLaw_smul_dirac_iff : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {P : MeasureTheory.Measure Ω} [MeasurableSingletonClass 𝓧] {x : 𝓧},
  ProbabilityTheory.HasLaw X (P Set.univ • MeasureTheory.Measure.dirac x) P ↔ X =ᵐ[P] fun x_1 => x
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f g : β → α}, (∀ (b : β), f b = g b) → ∏'[L] (b : β), f b = ∏'[L] (b : β), g b
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula**: if `f : ℂ → ℂ` is continuous on a closed disc of radius `R` and is
complex differentiable at all but countably many points of its interior, then for any `w` in this
interior we have $\oint_{|z-c|=R}\frac{f(z)}{z-w}dz=2\pi i\,f(w)$.
 -/
Complex.circleIntegral_div_sub_of_differentiable_on_off_countable : ∀ {R : ℝ} {c w : ℂ} {s : Set ℂ},
  s.Countable →
    w ∈ Metric.ball c R →
      ∀ {f : ℂ → ℂ},
        ContinuousOn f (Metric.closedBall c R) →
          (∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) →
            ∮ (z : ℂ) in C(c, R), f z / (z - w) = 2 * ↑Real.pi * Complex.I * f w
-- Mathlib.Topology.Homotopy.Path
/-- Suppose `F : Homotopy p q`. Then we have a `Homotopy p.symm q.symm` by reversing the second
argument.
 -/
Path.Homotopy.symm₂ : {X : Type u} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → {p q : Path x₀ x₁} → p.Homotopy q → p.symm.Homotopy q.symm
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_node4R : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α),
  (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_type_le : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.lift.{max v w, u} (Ordinal.type r) ≤ Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (InitialSeg r s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α},
  (a == b) = true →
    ∀ {h₁ : Std.Internal.List.containsKey a l = true} {h₂ : Std.Internal.List.containsKey b l = true},
      Std.Internal.List.getEntry a l h₁ = Std.Internal.List.getEntry b l h₂
-- Lean.Util.NumApps
/-- Returns the number of applications for each declaration used in `e`.

This operation is performed in `IO` because the result depends on the memory representation of the object.

Note: Use this function primarily for diagnosing performance issues.
 -/
Lean.Expr.numApps : Lean.Expr → optParam ℕ 0 → IO (Array (Lean.Name × ℕ))
-- Mathlib.Data.Matrix.DMatrix
DMatrix.subsingleton_of_empty_left : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [IsEmpty m], Subsingleton (DMatrix m n α)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.mk : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategoryStruct C] →
          (actionObj : D → C → D) →
            ((d : D) → {c c' : C} → (c ⟶ c') → (actionObj d c ⟶ actionObj d c')) →
              ({d d' : D} → (d ⟶ d') → (c : C) → actionObj d c ⟶ actionObj d' c) →
                ({c c' : C} → {d d' : D} → (d ⟶ d') → (c ⟶ c') → (actionObj d c ⟶ actionObj d' c')) →
                  ((d : D) →
                      (c c' : C) →
                        actionObj d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') ≅
                          actionObj (actionObj d c) c') →
                    ((d : D) → actionObj d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ d) →
                      CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.single_eq_updateRow_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (r : α), Matrix.single i j r = Matrix.updateRow 0 i (Pi.single j r)
-- Init.Data.Repr
instReprSourceInfo : Repr Lean.SourceInfo
-- Mathlib.Analysis.Fourier.Notation
FourierTransformInv.mk : {E : Type u} → {F : outParam (Type v)} → (E → F) → FourierTransformInv E F
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_baseChange : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) (A : Type u_6) [inst_8 : CommRing A] [inst_9 : Algebra R A],
  LinearMap.toMvPolynomial (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂)
      (LinearMap.baseChange A f) i =
    (MvPolynomial.map (algebraMap R A)) (LinearMap.toMvPolynomial b₁ b₂ f i)
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- Any valuation subring of `K` induces a natural valuation on `K`.  -/
ValuationSubring.valuation : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → Valuation K A.ValueGroup
-- Mathlib.Tactic.GuardHypNums
/-- `guard_hyp_nums n` succeeds if there are exactly `n` hypotheses and fails otherwise.

Note that, depending on what options are set, some hypotheses in the local context might
not be printed in the goal view. This tactic computes the total number of hypotheses,
not the number of visible hypotheses.
 -/
guardHypNums : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.tensorUnit_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {X : C},
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C D)).obj X =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit D