mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (U : CategoryTheory.Comonad C) [inst_2 : U.Additive] (F G : U.Coalgebra) (n : ℕ) (α : F ⟶ G), (n • α).f = n • α.f
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.coe_comp : ∀ (P : TopCat → Prop) {X Y Z : CompHausLike P} (f : X ⟶ Y) (g : Y ⟶ Z),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult.discrs : Lean.Elab.Term.GeneralizeResult → Array Lean.Elab.Term.Discr
-- Mathlib.RingTheory.Binomial
/-- The `n`th ascending Pochhammer polynomial evaluated at any element is divisible by `n!`  -/
BinomialRing.factorial_nsmul_multichoose : ∀ {R : Type u_1} {inst : AddCommMonoid R} {inst_1 : Pow R ℕ} [self : BinomialRing R] (r : R) (n : ℕ),
  n.factorial • BinomialRing.multichoose r n = (ascPochhammer ℕ n).smeval r
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_strict_mono_endpoints : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a a' b b' : E}
  {r : k}, a < a' → b < b' → 0 ≤ r → r ≤ 1 → (AffineMap.lineMap a b) r < (AffineMap.lineMap a' b') r
-- Init.Data.SInt.Lemmas
Int16.mul_comm : ∀ (a b : Int16), a * b = b * a
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If a function `f` is continuously polynomial on a set `s` and `g` is a continuous linear map,
then `g ∘ f` is continuously polynomial on `s`.  -/
ContinuousLinearMap.comp_cpolynomialOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} (g : F →L[𝕜] G),
  CPolynomialOn 𝕜 f s → CPolynomialOn 𝕜 (⇑g ∘ f) s
-- Init.Data.SInt.Bitwise
ISize.and_self : ∀ {a : ISize}, a &&& a = a
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.le_length_digits_le : ∀ (b n m : ℕ), n ≤ m → (b.digits n).length ≤ (b.digits m).length
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.domCongr_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N) (m : M) (a : A),
  (MonoidAlgebra.domCongr R A e) (MonoidAlgebra.single m a) = MonoidAlgebra.single (e m) a
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- The identity is a diffeomorphism of any charted space, for any groupoid.  -/
Structomorph.refl : {H : Type u} →
  [inst : TopologicalSpace H] →
    {G : StructureGroupoid H} →
      (M : Type u_5) →
        [inst_1 : TopologicalSpace M] → [inst_2 : ChartedSpace H M] → [HasGroupoid M G] → Structomorph G M M
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- A morphism in `C` descends to a cochain map between injective resolutions.  -/
CategoryTheory.InjectiveResolution.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        (Z ⟶ Y) →
          (I : CategoryTheory.InjectiveResolution Y) →
            (J : CategoryTheory.InjectiveResolution Z) → J.cocomplex ⟶ I.cocomplex
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_mul_le_of_le : ∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] {a₁ a₂ : α} {r₁ r₂ : NNReal},
  ‖a₁‖₊ ≤ r₁ → ‖a₂‖₊ ≤ r₂ → ‖a₁ * a₂‖₊ ≤ r₁ * r₂
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.balance'_lemma : ∀ {α : Type u_2} {l : Ordnode α} {l' : ℕ} {r : Ordnode α} {r' : ℕ},
  Ordnode.BalancedSz l' r' →
    l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l' → 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` and
has a right derivative at `f' x` for all `x` in `[a, b)`, and `f'` is integrable on `[a, b]` then
`∫ y in a..b, f' y` equals `f b - f a`.  -/
intervalIntegral.integral_eq_sub_of_hasDeriv_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm_nnreal_eq_lintegral : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {μ : MeasureTheory.Measure α} {f : α → ε}
  {p : NNReal}, p ≠ 0 → MeasureTheory.eLpNorm f (↑p) μ = (∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanImportMetaKind : Lean.FromJson Lean.Lsp.LeanImportMetaKind
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.pow_apply : ∀ {G : Type u_1} [inst : Add G] {a : G} (f : AddConstMap G G a a) (n : ℕ) (x : G), (f ^ n) x = (⇑f)^[n] x
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₁] [P.IsClosedUnderIsomorphisms],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₂ → P T.obj₃ → P T.obj₁
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.fromOver_over : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (X : CategoryTheory.Over S), X.left ↘ S = X.hom
-- Std.Data.String.ToInt
String.Slice.isInt_copy : ∀ {s : String.Slice}, s.copy.isInt = s.isInt
-- Mathlib.GroupTheory.PGroup
IsPGroup.eq_1 : ∀ (p : ℕ) (G : Type u_1) [inst : Group G], IsPGroup p G = ∀ (g : G), ∃ k, g ^ p ^ k = 1
-- Mathlib.Order.Category.Preord
/-- `OrderDual` as a functor.  -/
Preord.dual : CategoryTheory.Functor Preord Preord
-- Mathlib.CategoryTheory.Dialectica.Monoidal
/-- The braiding isomorphism `X ⊗ Y ≅ Y ⊗ X` in `Dial C`.  -/
CategoryTheory.Dial.braiding : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        (X Y : CategoryTheory.Dial C) →
          CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X
-- Mathlib.Algebra.Homology.HomologySequence
/-- The functor `HomologicalComplex C c ⥤ ComposableArrows C 3` that maps `K` to the
diagram `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j`.  -/
HomologicalComplex.HomologySequence.composableArrows₃Functor : (C : Type u_1) →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Preadditive C] →
        {c : ComplexShape ι} →
          ι →
            ι →
              [CategoryTheory.CategoryWithHomology C] →
                CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ComposableArrows C 3)
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.ofFractionRing.inj : ∀ {K : Type u} {inst : CommRing K} {toFractionRing toFractionRing_1 : FractionRing (Polynomial K)},
  { toFractionRing := toFractionRing } = { toFractionRing := toFractionRing_1 } → toFractionRing = toFractionRing_1
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.toQuotient_relation : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A) (r : relations.R),
  relations.toQuotient (relations.relation r) = 0
-- Mathlib.Condensed.AB
Condensed.instHasLimitsOfSizeModuleCat : ∀ (R : Type (u + 1)) [inst : Ring R], CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (ModuleCat R)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rco_eq_some : ∀ {m n : ℤ} {i : ℕ}, i < (n - m).toNat → (m...n).toList[i]? = some (m + ↑i)
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Expressing `HasFDerivWithinAt f f' s x` in terms of `HasDerivWithinAt`  -/
hasFDerivWithinAt_iff_hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F},
  HasFDerivWithinAt f f' s x ↔ HasDerivWithinAt f (f' 1) s x
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.toMonoidHom_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M), f.toMonoidHom x = f x
-- Mathlib.Data.Set.Image
Set.preimage_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} {t : Set α}, s ⊆ f '' t → Set.InjOn f (f ⁻¹' s) → f ⁻¹' s ⊆ t
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_iSup_u : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → β), l (⨆ i, u (f i)) = ⨆ i, f i
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- See `zero_lt_four'` for a version with the type explicit.  -/
zero_lt_four : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 4
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of the results of subtracting a default base point
from the given points, added to that base point, as an affine map on
the weights.  This is intended to be used when the sum of the weights
is 1, in which case it is an affine combination (barycenter) of the
points with the given weights; that condition is specified as a
hypothesis on those lemmas that require it.  -/
Finset.affineCombination : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [S : AddTorsor V P] → {ι : Type u_4} → Finset ι → (ι → P) → (ι → k) →ᵃ[k] P
-- Mathlib.CategoryTheory.Sites.Finite
CategoryTheory.Precoverage.instHasIsosFinite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.Precoverage.finite C).HasIsos
-- Mathlib.Order.RelClasses
Std.Irrefl.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Irrefl r], Std.Irrefl (Function.swap r)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ),
  (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.U R n) =
    (2 * ↑k + 3) * Polynomial.X * (⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.U R n) -
      ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n)
-- Mathlib.Algebra.Lie.Basic
/-- The constant 0 map is a Lie module morphism.  -/
LieModuleHom.instZero : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → Zero (M →ₗ⁅R,L⁆ N)
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_lt_iff_lt_coe : ∀ {q : ℚ} {p : ℚ≥0}, 0 ≤ q → (q.toNNRat < p ↔ q < ↑p)
-- Init.Data.Function
/-- `HasRightInverse f` means that `f` has an unspecified right inverse.  -/
Function.HasRightInverse : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop
-- Batteries.Data.List.Pairwise
List.pwFilter_sublist : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] (l : List α), (List.pwFilter R l).Sublist l
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The addition morphism of an additive monoid object.  -/
CategoryTheory.AddMonObj.add : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} → [self : CategoryTheory.AddMonObj X] → CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X
-- Lean.Meta.CongrTheorems
/-- (Tries to) cast free variable `fvarId` to the given type using the equations `eqs`.
`deps` contains the indices of the relevant equalities.
Remark: deps is sorted.
 -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.mkCast : Lean.FVarId → Lean.Expr → Array ℕ → Array (Option Lean.Meta.EqInfo✝) → Lean.MetaM Lean.Expr
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.tendsto_nhdsWithin_image : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) (f '' s))
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.nnorm_le_mul' : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F} {K : NNReal},
  LipschitzWith K f → f 1 = 1 → ∀ (x : E), ‖f x‖₊ ≤ K * ‖x‖₊
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rci α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Rci α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mk : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} →
                (baseSet : ι → Set B) →
                  (∀ (i : ι), IsOpen (baseSet i)) →
                    (indexAt : B → ι) →
                      (∀ (x : B), x ∈ baseSet (indexAt x)) →
                        (coordChange : ι → ι → B → F →L[R] F) →
                          (∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), (coordChange i i x) v = v) →
                            (∀ (i j : ι), ContinuousOn (coordChange i j) (baseSet i ∩ baseSet j)) →
                              (∀ (i j k : ι),
                                  ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
                                    ∀ (v : F), (coordChange j k x) ((coordChange i j x) v) = (coordChange i k x) v) →
                                VectorBundleCore R B F ι
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by `i + j` is the same as shifting by `i` and then shifting by `j`.  -/
CategoryTheory.shiftFunctorAdd : (C : Type u) →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (i j : A) →
            CategoryTheory.shiftFunctor C (i + j) ≅
              (CategoryTheory.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C j)
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView.tactic : Lean.Elab.WhereFinallyView → Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.ae_lt_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ∀ᵐ (x : α) ∂μ, f x < ⊤
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_neg : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : NonUnitalSubalgebra R A}
  (x : ↥S), ↑(-x) = -↑x
-- Lean.Message
Lean.instFromJsonBaseMessage : {α : Type} → [Lean.FromJson α] → Lean.FromJson (Lean.BaseMessage α)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β},
  k ∉ t₂ → Std.ExtDTreeMap.Const.getD (t₁.union t₂) k fallback = Std.ExtDTreeMap.Const.getD t₁ k fallback
-- Mathlib.Algebra.Group.ULift
ULift.addLeftCancelSemigroup : {α : Type u} → [AddLeftCancelSemigroup α] → AddLeftCancelSemigroup (ULift.{u_1, u} α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k a : α} {v : β}, (t.insertIfNew k v).getKey! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey! a
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap.map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {P : CategoryTheory.MorphismProperty C} {F : CategoryTheory.Functor C D} {X Y : C} {f : X ⟶ Y},
  P f → P.strictMap F (F.map f)
-- Mathlib.Data.Nat.Digits.Defs
Nat.toDigitsCore_lens_eq : ∀ (b f n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.refl_target : ∀ {α : Type u_1}, (PartialEquiv.refl α).target = Set.univ
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_one : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 1 → M), ∏ i, f i = f 0
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.ReflectsEpimorphisms.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f) → F.ReflectsEpimorphisms
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_singleton : ∀ {α : Type u_2} [inst : AddMonoid α] (a : α) (n : ℕ), n • {a} = {n • a}
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- This is the `List.sum` version of `add_neg`  -/
List.sum_neg : ∀ {K : Type u_8} [inst : SubtractionCommMonoid K] (L : List K), -L.sum = (List.map (fun x => -x) L).sum
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods.pre : Lean.Meta.Sym.Simp.Methods → Lean.Meta.Sym.Simp.Simproc
-- Lean.Elab.Term.TermElabM
/-- Disables incremental tactic reuse for `act` if `cond` is true.  -/
Lean.Elab.Term.withoutTacticReuse : {m : Type → Type} →
  {α : Type} → [Monad m] → [MonadWithReaderOf Lean.Elab.Term.Context m] → [Lean.MonadOptions m] → Bool → m α → m α
-- Mathlib.Algebra.Exact.Basic
Function.Exact.eq_1 : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} (f : M → N) (g : N → P) [inst : Zero P],
  Function.Exact f g = ∀ (y : N), g y = 0 ↔ y ∈ Set.range f
-- Mathlib.Algebra.Group.Units.Hom
/-- If a map `g : M → AddUnits N` agrees with a homomorphism `f : M →+ N`, then this map
is an AddMonoid homomorphism too.  -/
AddUnits.liftRight : {M : Type u} →
  {N : Type v} →
    [inst : AddMonoid M] →
      [inst_1 : AddMonoid N] → (f : M →+ N) → (g : M → AddUnits N) → (∀ (x : M), ↑(g x) = f x) → M →+ AddUnits N
-- Mathlib.Analysis.Normed.Group.Bounded
Bornology.IsBounded.exists_pos_norm_lt' : ∀ {E : Type u_2} [inst : SeminormedGroup E] {s : Set E}, Bornology.IsBounded s → ∃ R > 0, ∀ x ∈ s, ‖x‖ < R
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.ext_iff : ∀ {X : SSet} {n : ℕ} (x y : X.obj (Opposite.op { len := n })),
  { dim := n, simplex := x } = { dim := n, simplex := y } ↔ x = y
-- Mathlib.Data.Complex.Basic
Complex.mul_I_re : ∀ (z : ℂ), (z * Complex.I).re = -z.im
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.ofComplex_apply_of_im_nonpos : ∀ {w : ℂ}, w.im ≤ 0 → ↑UpperHalfPlane.ofComplex w = Classical.choice ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.cast_eq_self : ∀ {X : SSet} (s : X.N) {d : ℕ} (hd : s.dim = d), s.cast hd = s
-- Mathlib.Data.Nat.Find
_private.Mathlib.Data.Nat.Find.0.Nat.findGreatest.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects colimits, then `F : C ⥤ Dᵒᵖ` reflects limits.  -/
CategoryTheory.Limits.reflectsLimits_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimits F.leftOp],
  CategoryTheory.Limits.ReflectsLimits F
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_erase_eq_of_not_compare_eq_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).max? = t.max?
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_addMon_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
-- Mathlib.Combinatorics.Hindman
Hindman.FP.below.tail' : ∀ {M : Type u_1} [inst : Semigroup M] {motive : (a : Stream' M) → (a_1 : M) → Hindman.FP a a_1 → Prop} (a : Stream' M)
  (m : M) (h : Hindman.FP a.tail m), Hindman.FP.below h → motive a.tail m h → Hindman.FP.below ⋯
-- Mathlib.Topology.Connected.Basic
IrreducibleSpace.connectedSpace : ∀ (α : Type u) [inst : TopologicalSpace α] [IrreducibleSpace α], ConnectedSpace α
-- Mathlib.CategoryTheory.Action.Limits
/-- `F.mapAction : Action V G ⥤ Action W G` preserves colimits of some size if
`V` has colimits of that size and `F` preserves colimits of that size.  -/
Action.Functor.preservesColimitsOfSize_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w₂, w₁, v_1, v_2, u_1, u_3} F]
  [CategoryTheory.Limits.HasColimitsOfSize.{w₂, w₁, v_1, u_1} V],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w₂, w₁, v_1, v_2, max (max u_1 u_4) v_1, max (max u_3 u_4) v_2}
    (F.mapAction G)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.freeAddGroupCongr_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeAddGroup α),
  (FreeAddGroup.freeAddGroupCongr e) a = (FreeAddGroup.map ⇑e) a