mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
CategoryTheory.uncurry_expComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  (A B : C),
  CategoryTheory.MonoidalClosed.uncurry ((CategoryTheory.expComparison F A).natTrans.app B) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A (A ⟹ B)))
      (F.map ((CategoryTheory.ihom.ev A).app B))
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.below.succ : ∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop}, Nat.Primrec.below Nat.Primrec.succ
-- Mathlib.RingTheory.Valuation.Basic
/-- Two valuations on `R` are defined to be equivalent if they induce the same preorder on `R`.  -/
Valuation.IsEquiv : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    {Γ'₀ : Type u_5} →
      [inst : Ring R] →
        [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] →
          [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] → Valuation R Γ₀ → Valuation R Γ'₀ → Prop
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
`f : G × G → M` satisfying the multiplicative 2-cocycle condition, produces a 2-cocycle for the
representation on `cochainsIso₁Additive M` induced by the `MulDistribMulAction`.  -/
groupCohomology.cocyclesOfIsMulCocycle₂ : {G M : Type} →
  [inst : Group G] →
    [inst_1 : CommGroup M] →
      [inst_2 : MulDistribMulAction G M] →
        {f : G × G → M} → groupCohomology.IsMulCocycle₂ f → ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction G M))
-- Init.Data.Vector.Monadic
Vector.foldlM_map : ∀ {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {n : ℕ} [inst : Monad m] {f : β₁ → β₂}
  {g : α → β₂ → m α} {xs : Vector β₁ n} {init : α},
  Vector.foldlM g init (Vector.map f xs) = Vector.foldlM (fun x y => g x (f y)) init xs
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` reflects isomorphisms, and we already know that the limit exists in the source and `F`
preserves it, then `F` creates that limit.  -/
CategoryTheory.createsLimitOfReflectsIsomorphismsOfPreserves : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.ReflectsIsomorphisms] →
                  [CategoryTheory.Limits.HasLimit K] →
                    [CategoryTheory.Limits.PreservesLimit K F] → CategoryTheory.CreatesLimit K F
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toStarModule : ∀ {A : Type u_1} [self : NonUnitalCommCStarAlgebra A], StarModule ℂ A
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- This iso witnesses the fact that
given `f : X ⟶ T`, `g : Y ⟶ T`, and `i : T ⟶ S`, the diagram

```
X ×ₜ Y ⟶ X ×ₛ Y
  |         |
  |         |
  ↓         ↓
  T    ⟶  T ×ₛ T
```

is a pullback square.
Also see `pullback_map_diagonal_isPullback`.
 -/
CategoryTheory.Limits.pullbackDiagonalMapIdIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasPullbacks C] →
        {S T : C} →
          (f : X ⟶ T) →
            (g : Y ⟶ T) →
              (i : T ⟶ S) →
                [inst_2 : CategoryTheory.Limits.HasPullback i i] →
                  [inst_3 : CategoryTheory.Limits.HasPullback f g] →
                    [inst_4 :
                        CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i)
                          (CategoryTheory.CategoryStruct.comp g i)] →
                      [inst_5 :
                          CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
                            (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
                              (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯
                              ⋯)] →
                        CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal i)
                            (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
                              (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯
                              ⋯) ≅
                          CategoryTheory.Limits.pullback f g
-- Lean.Message
Lean.MessageData.ofOriginatingSyntax.sizeOf_spec : ∀ (a : Lean.Syntax) (a_1 : Lean.MessageData),
  sizeOf (Lean.MessageData.ofOriginatingSyntax a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toContinuousAffineEquiv_injective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂],
  Function.Injective AffineIsometryEquiv.toContinuousAffineEquiv
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt.go.eq_2 : ∀ {α : Type u_1} (a : List α) (a_1 : ℕ) (a_2 : List α),
  (∀ (x : α) (xs : List α) (n : ℕ), a = x :: xs → a_1 = n.succ → False) →
    List.MergeSort.Internal.splitRevAt.go✝ a a_1 a_2 = (a_2, a)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.mk : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : AddTorsor V P] →
              {n : ℕ} → (points : Fin (n + 1) → P) → AffineIndependent k points → Affine.Simplex k P n
-- Mathlib.Algebra.Module.GradedModule
/-- The `Module` derived from `gmodule A M`.  -/
DirectSum.Gmodule.module : {ιA : Type u_1} →
  {ιB : Type u_2} →
    (A : ιA → Type u_3) →
      (M : ιB → Type u_4) →
        [inst : AddMonoid ιA] →
          [inst_1 : VAdd ιA ιB] →
            [inst_2 : (i : ιA) → AddCommMonoid (A i)] →
              [inst_3 : (i : ιB) → AddCommMonoid (M i)] →
                [inst_4 : DecidableEq ιA] →
                  [DecidableEq ιB] →
                    [inst_6 : DirectSum.GSemiring A] →
                      [DirectSum.Gmodule A M] → Module (DirectSum ιA fun i => A i) (DirectSum ιB fun i => M i)
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_dvd_mul_gcd : ∀ (k m n : ℕ), k.gcd (m * n) ∣ k.gcd m * k.gcd n
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.enorm_single : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i), ‖Pi.single i y‖ₑ = ‖y‖ₑ
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.ofExact_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : C ⥤ₑ D} (α : F ⟶ G), ((CategoryTheory.LeftExactFunctor.ofExact C D).map α).hom = α.hom
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceBNe : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.LocalProperties.Exactness
surjective_of_localized_span : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (f : M →ₗ[R] N),
      (∀ (r : ↑s), Function.Surjective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f)) → Function.Surjective ⇑f
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.quotient_liftOn_mk : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {β : Sort u_2} (f : α → β)
  (h : ∀ (a b : α), (QuotientGroup.leftRel s) a b → f a = f b) (x : α), Quotient.liftOn' (↑x) f h = f x
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.submatrix : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : LT α]
  [inst_1 : Zero R] {f : n → m}, M.BlockTriangular b → (M.submatrix f f).BlockTriangular (b ∘ f)
-- Mathlib.Algebra.Polynomial.Degree.Defs
/-- **Alias** of the reverse direction of `Polynomial.natDegree_le_iff_degree_le`. -/
Polynomial.natDegree_le_of_degree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.degree ≤ ↑n → p.natDegree ≤ n
-- Mathlib.FieldTheory.KrullTopology
/-- A subset of `Gal(L/K)` is a member of `galBasis K L` if and only if it is the underlying set
of `Gal(L/E)` for some finite subextension `E/K`.  -/
mem_galBasis_iff : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (U : Set Gal(L/K)),
  U ∈ galBasis K L ↔ U ∈ (fun g => g.carrier) '' fixedByFinite K L
-- Init.Data.Int.ToString
_private.Init.Data.Int.ToString.0.Int.repr.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((m : ℕ) → motive (Int.ofNat m)) → ((m : ℕ) → motive (Int.negSucc m)) → motive x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f x` has
finite limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then
`(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)`.  -/
intervalIntegral.integral_hasFDerivAt_of_tendsto_ae : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
        Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca) →
          Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb) →
            HasFDerivAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x)
              ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (a, b)
-- Mathlib.Order.CompleteLattice.Basic
Prod.iSup_mk : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : SupSet α] [inst_1 : SupSet β] (f : ι → α) (g : ι → β),
  ⨆ i, (f i, g i) = (⨆ i, f i, ⨆ i, g i)
-- Mathlib.Analysis.Calculus.AbsolutelyMonotone
/-- Under `UniqueDiffOn`, a function is absolutely monotone on `s` iff it is `C^∞` on `s` with
every iterated derivative within `s` nonnegative.  -/
AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg : ∀ {f : ℝ → ℝ} {s : Set ℝ},
  UniqueDiffOn ℝ s →
    (AbsolutelyMonotoneOn f s ↔ ContDiffOn ℝ (↑⊤) f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableAt_sub_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x}
  {x₀ : B}, MDiffAt (T% s) x₀ → MDiffAt (T% t) x₀ → (MDiffAt fun x => ⟨x, (s - t) x⟩) x₀
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
setIntegral_withDensity_eq_setIntegral_toReal_smul : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {f : X → ENNReal} {s : Set X},
  Measurable f →
    (∀ᵐ (x : X) ∂μ.restrict s, f x < ⊤) →
      ∀ (g : X → E),
        MeasurableSet s → (∫ (x : X) in s, g x ∂μ.withDensity fun x => f x) = ∫ (x : X) in s, (f x).toReal • g x ∂μ
-- Mathlib.Tactic.Translate.Core
/-- `addTranslationAttr src cfg` adds a translation attribute to `src` with configuration `cfg`.
See the attribute implementation for more details.
It returns an array with names of translated declarations (usually 1, but more if there are nested
`to_additive` calls).  -/
Mathlib.Tactic.Translate.addTranslationAttr : Mathlib.Tactic.Translate.TranslateData →
  Lean.Name →
    Mathlib.Tactic.Translate.Config →
      optParam Lean.AttributeKind Lean.AttributeKind.global → Lean.AttrM (Array Lean.Name)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whisker_assoc_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g') h ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h) h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g' h).inv h_1))
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.notMem_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α}, x ∉ f.support ↔ f x = x
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- **Alias** of `iteratedFDerivWithin_fun_zero`. -/
iteratedFDerivWithin_zero_fun : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {i : ℕ},
  iteratedFDerivWithin 𝕜 i (fun x => 0) s = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.fin3_def : ∀ {R : Type r} (P : Fin 3 → R), ![P 0, P 1, P 2] = P
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C] (toPseudofunctor : CategoryTheory.Pseudofunctor B C)
  (map_id :
    autoParam
      (∀ (X : B),
        toPseudofunctor.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toPseudofunctor.obj X))
      CategoryTheory.StrictlyUnitaryPseudofunctor.map_id._autoParam)
  (mapId_eq_eqToIso :
    autoParam (∀ (X : B), toPseudofunctor.mapId X = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso._autoParam),
  sizeOf { toPseudofunctor := toPseudofunctor, map_id := map_id, mapId_eq_eqToIso := mapId_eq_eqToIso } =
    1 + sizeOf toPseudofunctor
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.ULiftT.run_pure : ∀ {n : Type (max u v) → Type v'} [inst : Monad n] {α : Type u} {a : α}, (pure a).run = pure { down := a }
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_bot_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.addSubgroupOf ⊥ = ⊥
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
fderivWithin_exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => Real.exp (f x)) s x = Real.exp (f x) • fderivWithin ℝ f s x
-- Mathlib.RingTheory.KrullDimension.Basic
/-- Also see `Ideal.IsPrime.isMaximal` for the analogous statement for Dedekind domains.  -/
Ideal.IsPrime.isMaximal' : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] {I : Ideal R}, I.IsPrime → I.IsMaximal
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_mono_set : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedAdd M] (f : ι → M),
  Monotone fun s => ∑ x ∈ s, f x
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.coe_inclusion : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I₁ I₂ : LieIdeal R L}
  (h : I₁ ≤ I₂) (x : ↥I₁), ↑((LieIdeal.inclusion h) x) = ↑x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- A category has a subobject classifier if and only if the subobjects functor is representable.  -/
CategoryTheory.hasSubobjectClassifier_iff_isRepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.HasSubobjectClassifier C ↔ (Subobject.presheaf C).IsRepresentable
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.mk_mem_interedges_iff : ∀ {α : Type u_4} {β : Type u_5} {r : α → β → Prop} [inst : (a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β}
  {a : α} {b : β}, (a, b) ∈ Rel.interedges r s t ↔ a ∈ s ∧ b ∈ t ∧ r a b
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.Option.instDecidableEq.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (b : Option α) → (Unit → motive none) → ((val : α) → motive (some val)) → motive b
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.leftHomologyData_K_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ),
  ↑(CochainComplex.HomComplex.leftHomologyData K L n).K = CochainComplex.HomComplex.Cocycle K L n
-- Mathlib.Data.Set.Prod
Set.uniqueElim_preimage : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Unique ι] (t : (i : ι) → Set (α i)),
  uniqueElim ⁻¹' Set.univ.pi t = t default
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [Nontrivial A]
  (a : A),
  autoParam (p a) IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum._auto_1 →
    IsGreatest ((fun x => ‖x‖) '' spectrum 𝕜 a) ‖a‖
-- Mathlib.Algebra.Star.Basic
/-- Involutive condition.  -/
InvolutiveStar.star_involutive : ∀ {R : Type u} [self : InvolutiveStar R], Function.Involutive star
-- Mathlib.GroupTheory.Perm.Centralizer
/-- The action by conjugation of `Subgroup.centralizer {g}`
on the cycles of a given permutation  -/
Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.cycleFactorsFinset_mulAction : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → (g : Equiv.Perm α) → MulAction ↥(Subgroup.centralizer {g}) ↥g.cycleFactorsFinset
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (m : α) (n : β), (OrderAddMonoidHom.inlₗ α β) m + (OrderAddMonoidHom.inrₗ α β) n = toLex (m, n)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_intCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocDiv hp a (b - ↑m * p) = toIocDiv hp a b - m
-- Init.Data.UInt.Lemmas
UInt64.toFin_ofFin : ∀ (n : Fin UInt64.size), (UInt64.ofFin n).toFin = n
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Star R] →
      [TrivialStar R] →
        [inst_2 : AddCommGroup A] →
          [inst_3 : StarAddMonoid A] →
            [inst_4 : Semiring R] → [inst_5 : Module R A] → [StarModule R A] → Module R ↥(skewAdjoint A)
-- Mathlib.Topology.MetricSpace.Bounded
/-- In a complete space, if a family of closed sets with diameter tending to `0` is such that each
finite intersection is nonempty, then the total intersection is also nonempty.  -/
Metric.nonempty_iInter_of_nonempty_biInter : ∀ {α : Type u} [inst : PseudoMetricSpace α] [CompleteSpace α] {s : ℕ → Set α},
  (∀ (n : ℕ), IsClosed (s n)) →
    (∀ (n : ℕ), Bornology.IsBounded (s n)) →
      (∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty) →
        Filter.Tendsto (fun n => Metric.diam (s n)) Filter.atTop (nhds 0) → (⋂ n, s n).Nonempty
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_symm_apply_left`. -/
Equiv.Perm.SameCycle.of_symm_apply_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle ((Equiv.symm f) x) y → f.SameCycle x y
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.tendsto_Lp_of_tendsto_eLpNorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] {ι : Type u_4} {fi : Filter ι} [inst_1 : Fact (1 ≤ p)]
  {f : ι → ↥(MeasureTheory.Lp E p μ)} (f_lim : α → E) (f_lim_ℒp : MeasureTheory.MemLp f_lim p μ),
  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑↑(f n) - f_lim) p μ) fi (nhds 0) →
    Filter.Tendsto f fi (nhds (MeasureTheory.MemLp.toLp f_lim f_lim_ℒp))
-- Init.Data.BitVec.Lemmas
BitVec.getElem_shiftConcat_succ : ∀ {w i : ℕ} {x : BitVec w} {b : Bool} (h : i + 1 < w), (x.shiftConcat b)[i + 1] = x[i]
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_top : ∀ {M : Type u_2} [inst : MulOneClass M], ⊤.op = ⊤
-- Mathlib.Data.Vector3
Fin2.left.eq_2 : ∀ (k n : ℕ) (i : Fin2 n), Fin2.left k i.fs = (Fin2.left k i).fs
-- Mathlib.Topology.Category.CompHaus.Limits
CompHaus.instHasExplicitPullbacksTrue : CompHausLike.HasExplicitPullbacks fun x => True
-- Init.Data.SInt.Lemmas
Int16.toUInt16_ofNat' : ∀ {n : ℕ}, (Int16.ofNat n).toUInt16 = UInt16.ofNat n
-- Mathlib.Data.Finset.Sort
Finset.sort_insert : ∀ {α : Type u_1} {s : Finset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] [inst_4 : DecidableEq α] {a : α},
  (∀ b ∈ s, r a b) → a ∉ s → (insert a s).sort r = a :: s.sort r
-- Mathlib.Algebra.GroupWithZero.Defs
GroupWithZero.mk : {G₀ : Type u} →
  [toMonoidWithZero : MonoidWithZero G₀] →
    [toInv : Inv G₀] →
      [toDiv : Div G₀] →
        [toZPow : ZPow G₀] →
          autoParam (∀ (a b : G₀), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
            autoParam (∀ (a : G₀), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : G₀), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : G₀), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) DivInvMonoid.zpow_neg'._autoParam →
                  [toNontrivial : Nontrivial G₀] → 0⁻¹ = 0 → (∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1) → GroupWithZero G₀
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.prop_of_isLimit_kernelFork : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderKernels] {X Y : C} {f : X ⟶ Y}
  {k : CategoryTheory.Limits.KernelFork f} (hk : CategoryTheory.Limits.IsLimit k), P X → P Y → P k.pt
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.min : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] [inst_1 : LinearOrder M] {f g : α → M},
  Function.HasFiniteMulSupport f →
    Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport fun a => min (f a) (g a)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrRightEquiv_trans : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [inst : MulOneClass M] [inst_1 : Monoid N₁]
  [inst_2 : Monoid N₂] [inst_3 : Monoid N₃] (e₁₂ : N₁ ≃* N₂) (e₂₃ : N₂ ≃* N₃),
  (e₁₂.trans e₂₃).monoidHomCongrRightEquiv = e₁₂.monoidHomCongrRightEquiv.trans e₂₃.monoidHomCongrRightEquiv