mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
/-- The inclusion `H ⥤ C` when `H` is the heart of a t-structure `t` on `C`.  -/
CategoryTheory.Triangulated.TStructure.ιHeart : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                {H : Type u'} →
                  [inst_6 : CategoryTheory.Category.{v', u'} H] →
                    [inst_7 : CategoryTheory.Preadditive H] → [t.Heart H] → CategoryTheory.Functor H C
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.Arg.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (coe : Option Lean.Expr), sizeOf { expr := expr, coe := coe } = 1 + sizeOf expr + sizeOf coe
-- Mathlib.SetTheory.Cardinal.Finite
Set.natCard_pos : ∀ {α : Type u_1} {s : Set α}, s.Finite → (0 < Nat.card ↑s ↔ s.Nonempty)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The underlying monoid homomorphism.  -/
MonCat.Hom.hom' : {A B : MonCat} → A.Hom B → ↑A →* ↑B
-- Init.Data.Int.DivMod.Lemmas
Int.le_mul_iff_le_left : ∀ {x y z : ℤ}, 0 < z → (x ≤ y * z ↔ (x + z - 1) / z ≤ y)
-- Mathlib.CategoryTheory.Opposites
Quiver.Hom.unop_mk : ∀ {C : Type u₁} [inst : Quiver C] {X Y : Cᵒᵖ} (f : X ⟶ Y), Quiver.Hom.unop (Opposite.op f) = f
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoin.powerBasis_gen : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} (hx : IsIntegral K x),
  (IntermediateField.adjoin.powerBasis hx).gen = IntermediateField.AdjoinSimple.gen K x
-- Init.Data.Fin.Lemmas
Fin.forall_fin_zero : ∀ {p : Fin 0 → Prop}, (∀ (i : Fin 0), p i) ↔ True
-- Mathlib.Tactic.GrindAttrs
/-- The `compactness` attribute is a custom grind-set specialized to prove that sets are compact.
It is called by the `compactness` tactic.  -/
Lean.Parser.Attr.compactness!? : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairHomCategory : CategoryTheory.SmallCategory CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isIntTangent_iff_dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [Nontrivial V] {s₁ s₂ : EuclideanGeometry.Sphere P},
  s₁.IsIntTangent s₂ ↔ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, we have that `λ ^ 4` divides `S'.c ^ 3`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.lambda_pow_four_dvd_c_cube : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  (hζ.toInteger - 1) ^ 4 ∣ FermatLastTheoremForThreeGen.Solution'.c✝ S' ^ 3
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.GrothendieckTopology.mem_toPretopology : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (t : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Presieve X),
  S ∈ t.toPretopology.coverings X ↔ CategoryTheory.Sieve.generate S ∈ t X
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run'.match_1.eq_1 : ∀ {α : Type u_1} (n : ℕ) (motive : { l // l.length = (n + 2) / 2 } × { l // l.length = (n + 2 + 1) / 2 } → Sort u_2)
  (l : { l // l.length = (n + 2) / 2 }) (r : { l // l.length = (n + 2 + 1) / 2 })
  (h_1 : (l : { l // l.length = (n + 2) / 2 }) → (r : { l // l.length = (n + 2 + 1) / 2 }) → motive (l, r)),
  (match (l, r) with
    | (l, r) => h_1 l r) =
    h_1 l r
-- Mathlib.Topology.Bornology.Basic
/-- The cobounded filter in a bornology is smaller than the cofinite filter.  -/
Bornology.le_cofinite : ∀ (α : Type u_4) [self : Bornology α], Bornology.cobounded α ≤ Filter.cofinite
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.μ_pullback_left_fst_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {f : R ⟶ X} (R_1 S : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) R_1 S))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R_1 S).hom f)
        (CategoryTheory.Limits.pullback.fst R_1.hom S.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst ((CategoryTheory.Over.pullback f).obj R_1).hom
        ((CategoryTheory.Over.pullback f).obj S).hom)
      (CategoryTheory.Limits.pullback.fst R_1.hom f)
-- Init.Omega.Coeffs
/-- Shim for `IntList.smul`.  -/
Lean.Omega.Coeffs.smul : Lean.Omega.Coeffs → ℤ → Lean.Omega.Coeffs
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.integral_restrict : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} {s : Set β}
  (hs : MeasurableSet s), ∫ (x : β), f x ∂(κ.restrict hs) a = ∫ (x : β) in s, f x ∂κ a
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_univ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal),
  ∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
-- Mathlib.Topology.UnitInterval
unitInterval.zero_mem : 0 ∈ unitInterval
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.self_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k}, (cmp k (t.insertIfNew k v).maxKey!).isLE = true
-- Batteries.Control.Nondet.Basic
/-- Convert a non-deterministic value into a list in the monad, by discarding the backtrackable state.
 -/
Nondet.toList' : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → Nondet m α → m (List α)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_sub_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ ν : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  (μ - ν).transpose B = μ.transpose B - ν.transpose B
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instSMul : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} →
                                {S : Type u_6} →
                                  [inst_10 : Monoid S] →
                                    [inst_11 : DistribMulAction S W] →
                                      [SMulCommClass R S W] →
                                        [ContinuousConstSMul S W] →
                                          [LinearMap.CompatibleSMul W W S R] → SMul S (ContIntertwiningMap π₁ π₂)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_right_le_size_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₂.size ≤ (m₁ ∪ m₂).size
-- Mathlib.CategoryTheory.Limits.Preserves.Ulift
/-- The functor `uliftFunctor : Type u ⥤ Type (max u v)` preserves colimits of arbitrary size.
 -/
CategoryTheory.Limits.Types.instPreservesColimitsOfSizeUliftFunctor : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)}
  CategoryTheory.uliftFunctor.{v, u}
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.nonempty_support : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E], (Function.support ↑f).Nonempty
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.whiskerLeft_id : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X Y : CategoryTheory.LocalizedMonoidal L W ε),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Filter.biInter_finset_mem`. -/
Finset.iInter_mem_sets : ∀ {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} (is : Finset β), ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
-- Mathlib.Combinatorics.Digraph.Basic
/-- A digraph is a relation `Adj` on a vertex type `V`.
The relation describes which pairs of vertices are adjacent.

In this treatment, a digraph may have self-loops.
 -/
Digraph : Type u_1 → Type u_1
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_vsub_center : ∀ {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 : P) (R : ℝ) (x : P),
  EuclideanGeometry.inversion c R x -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  {f g : α ≃*o β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Galois.Basic
/-- An object whose fiber is inhabited is not initial.  -/
CategoryTheory.PreGaloisCategory.not_initial_of_inhabited : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X : C}
  (x : (F.obj X).obj) (h : CategoryTheory.Limits.IsInitial X), False
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_union_of_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₂ = true → Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.pow : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Pow γ ℕ] [MeasurablePow γ ℕ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ {n : ℕ}, ProbabilityTheory.IdentDistrib (fun x => f x ^ n) (fun x => g x ^ n) μ ν
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The second arrow defining the relation.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {S : J.Cover X} → {I₁ I₂ : S.Arrow} → (self : I₁.Relation I₂) → self.Z ⟶ I₂.Y
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.coroot.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B B_1 : M →ₗ[R] M →ₗ[R] R) (e_B : B = B_1) {x x_1 : M} (e_x : x = x_1) (hx : B.IsReflective x),
  LinearMap.IsReflective.coroot B hx = LinearMap.IsReflective.coroot B_1 ⋯
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.llcomp_apply : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {M : Type u_17} {N : Type u_18}
  {P : Type u_19} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃] [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R₂ N]
  [inst_8 : Module R₃ P] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (f : N →ₛₗ[σ₂₃] P) (g : M →ₛₗ[σ₁₂] N) (x : M), (((LinearMap.llcomp R₃ M N P) f) g) x = f (g x)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.isCompat_apply' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {f : M →ₚₗ[R] N} {S : Type u} [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S] {S' : Type u} [inst_7 : CommSemiring S'] [inst_8 : Algebra R S'] (φ : S →ₐ[R] S')
  (x : TensorProduct R S M),
  (LinearMap.rTensor N φ.toLinearMap) (f.toFun' S x) = f.toFun' S' ((LinearMap.rTensor M φ.toLinearMap) x)
-- Mathlib.Topology.EMetricSpace.Weak
/-- If `α` has a linear order topology, `some : α → WithTop α` is an open embedding with respect to
the order topologies.  -/
WithTop.isOpenEmbedding_some : ∀ {α : Type u} [t : TopologicalSpace α] [inst : LinearOrder α] [inst_1 : OrderTopology α],
  Topology.IsOpenEmbedding WithTop.some
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_of_mul_apply_of_le : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddCommMonoid ι] [inst_5 : PartialOrder ι]
  [CanonicallyOrderedAdd ι] [inst_7 : SetLike.GradedMonoid A] [inst_8 : Sub ι] [OrderedSub ι] [AddLeftReflectLE ι]
  {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun i => ↥(A i)) (n : ι),
  i ≤ n → ↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i))
-- Lean.Server.AsyncList
Lean.AsyncList.delayed : {ε : Type u} → {α : Type v} → Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Lean.AsyncList ε α
-- Init.Data.String.Substring
/-- Checks whether two substrings have the same position and content.

The two substrings do not need to have the same underlying string for this check to succeed.
 -/
Substring.Raw.sameAs : Substring.Raw → Substring.Raw → Bool
-- Mathlib.NumberTheory.Padics.Complex
/-- `PadicAlgCl p` is a valued field, with the valuation corresponding to the `p`-adic norm.  -/
PadicAlgCl.valued : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Valued (PadicAlgCl p) NNReal
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t₁.Equiv t₂ → ∀ (k : α) (f : β → β), (t₁.modify k f).Equiv (t₂.modify k f)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The logarithmic Mahler measure of `X - C z` is the `log⁺` of the absolute value of `z`.  -/
Polynomial.logMahlerMeasure_X_sub_C : ∀ (z : ℂ), (Polynomial.X - Polynomial.C z).logMahlerMeasure = ‖z‖.posLog
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_insert_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.eq_1 : ∀ {p : ℕ} {α : Type u_3} {β : Type u_4} (f : α → β) (x : WittVector p α),
  WittVector.mapFun f x = WittVector.mk p (f ∘ x.coeff)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFn_star : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : (i : α) → StarAddMonoid (E i)] [inst_2 : ∀ (i : α), NormedStarGroup (E i)] (f : ↥(lp E p)),
  ↑(star f) = star ↑f
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The operator norm on `Matrix n n 𝕜` given by the identification with (continuous) linear
endomorphisms of `EuclideanSpace 𝕜 n` makes it into a `L2OpRing`.  -/
Matrix.instCStarRing : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  CStarRing (Matrix n n 𝕜)
-- Lean.Data.NameMap.Basic
/-- `filter f s` returns the `NameSet` consisting of all `x` in `s` where `f x` returns `true`.  -/
Lean.NameSet.filter : (Lean.Name → Bool) → Lean.NameSet → Lean.NameSet
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Given a continuous multilinear map `f` in `n+1` variables, split the first variable to obtain
a continuous linear map into continuous multilinear maps in `n` variables, given by
`x ↦ (m ↦ f (cons x m))`.  -/
ContinuousMultilinearMap.curryLeft : {𝕜 : Type u} →
  {n : ℕ} →
    {Ei : Fin n.succ → Type wEi} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → ContinuousMultilinearMap 𝕜 Ei G → Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G
-- Init.Data.SInt.Bitwise
UInt32.toInt32_or : ∀ (a b : UInt32), (a ||| b).toInt32 = a.toInt32 ||| b.toInt32
-- Mathlib.Algebra.Homology.Homotopy
/-- Compatibility of `nullHomotopicMap` with the application of additive functors  -/
Homotopy.map_nullHomotopicMap : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (G : CategoryTheory.Functor V W) [inst_4 : G.Additive]
  (hom : (i j : ι) → C.X i ⟶ D.X j),
  (G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap hom) = Homotopy.nullHomotopicMap fun i j => G.map (hom i j)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_lt_one : ∀ (x : ℝ), unitInterval.sigmoid x < 1
-- Lean.Language.Basic
/-- Chains two snapshot tasks. The processed syntax and the reporting range are taken from the first
task if not specified; the processed syntax and the reporting range of the second task are
discarded. The cancellation tokens of both tasks are discarded. They are replaced with the given
token if any.  -/
Lean.Language.SnapshotTask.bindIO : {α β : Type} →
  (t : Lean.Language.SnapshotTask α) →
    (α → BaseIO (Lean.Language.SnapshotTask β)) →
      optParam (Option Lean.Syntax) t.stx? →
        optParam Lean.Language.SnapshotTask.ReportingRange t.reportingRange →
          Option IO.CancelToken → optParam Bool false → BaseIO (Lean.Language.SnapshotTask β)
-- Mathlib.Data.Fin.Parity
Fin.even_of_val : ∀ {n : ℕ} {k : Fin n}, Even ↑k → Even k
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The limit cone is limiting.  -/
LightDiagram.isLimit : (self : LightDiagram) → CategoryTheory.Limits.IsLimit self.cone
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_X_self_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R] (i : σ) (k : ℕ),
  MvPolynomial.degreeOf i (MvPolynomial.X i ^ k) = k
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.NormalizedMooreComplex.obj_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  (AlgebraicTopology.NormalizedMooreComplex.obj X).X n =
    CategoryTheory.Subobject.underlying.obj (AlgebraicTopology.NormalizedMooreComplex.objX X n)
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.mk : {S : Type u_2} →
  {M : Type u_3} →
    [inst : SMul S M] →
      (toSetoid : Setoid M) → (∀ (s : S) {x y : M}, toSetoid x y → toSetoid (s • x) (s • y)) → SMulCon S M
-- Mathlib.Data.Set.Basic
Set.sep_ofPred : ∀ {α : Type u} {p q : α → Prop}, {x | x ∈ {y | p y} ∧ q x} = {x | p x ∧ q x}
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_comp_neg_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg)
        f)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      CategoryTheory.AddMonObj.zero
-- Mathlib.Computability.Primrec.Basic
Primrec.snd : ∀ {α : Type u_2} {β : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec Prod.snd
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (k, v) ∈ m.toList ↔ m.getKey? k = some k ∧ m[k]? = some v
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongMono.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} {f : Q ⟶ P} [CategoryTheory.Mono f],
  (∀ (Y X : C) (z : Y ⟶ X),
      CategoryTheory.Epi z → ∀ (v : Y ⟶ Q) (u : X ⟶ P) (sq : CategoryTheory.CommSq v z f u), sq.HasLift) →
    CategoryTheory.StrongMono f
-- Mathlib.Data.Finset.Prod
Finset.empty_product : ∀ {α : Type u_1} {β : Type u_2} (t : Finset β), ∅ ×ˢ t = ∅
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.getVert_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ℕ),
  (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
-- Init.Data.Order.Opposite
Min.max_oppositeMax : ∀ {α : Type u_1} {min : Min α} {a b : α}, a ⊔ b = a ⊓ b
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.lambdaTelescopeImp : {α : Type} →
  Lean.Expr →
    Bool →
      Bool → Bool → Bool → Option ℕ → (Array Lean.Expr → Lean.Expr → Lean.MetaM α) → optParam Bool false → Lean.MetaM α
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {inst_2 : CategoryTheory.Category.{v_3, u_3} C₃}
  {inst_3 : CategoryTheory.Category.{v_4, u_4} C₄} {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {x y : CategoryTheory.CatCommSq T L R B},
  CategoryTheory.CatCommSq.iso T L R B = CategoryTheory.CatCommSq.iso T L R B → x = y
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The map `M.sections → N.sections` induced by a morphisms `M ⟶ N` of presheaves of modules.  -/
PresheafOfModules.sectionsMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M N : PresheafOfModules R} → (M ⟶ N) → M.sections → N.sections