mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α → ENNReal) (t : Set α), ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ
-- Mathlib.GroupTheory.GroupAction.Pointwise
image_vadd_setₛₗ : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : VAdd M α]
  [inst_1 : VAdd N β] [inst_2 : FunLike F α β] [AddActionSemiHomClass F σ α β] (f : F) (c : M) (s : Set α),
  ⇑f '' (c +ᵥ s) = σ c +ᵥ ⇑f '' s
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_le : ∀ {a b : ℝ} {x y : ↑(Set.Icc a b)}, x ≤ y → ∀ (t : ↑unitInterval), Set.Icc.convexComb x y t ≤ y
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.subset_sphere : ∀ {P : Type u_2} [inst : MetricSpace P] {ps : Set P} {s : EuclideanGeometry.Sphere P},
  ps ⊆ Metric.sphere s.center s.radius ↔ ∀ p ∈ ps, p ∈ s
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.Faithful.mapCommMon : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} [inst_6 : F.LaxBraided] [F.Faithful], F.mapCommMon.Faithful
-- Mathlib.Topology.Algebra.Monoid
/-- The continuous map `fun y => x + y`  -/
ContinuousMap.addLeft : {X : Type u_5} → [inst : TopologicalSpace X] → [inst_1 : Add X] → [SeparatelyContinuousAdd X] → X → C(X, X)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_Ioi_castAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.castAdd m ⁻¹' Set.Ioi (Fin.castAdd m i) = Set.Ioi i
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- An equality of refl prefunctors gives an equality on objects.  -/
CategoryTheory.ReflPrefunctor.congr_obj : ∀ {U : Type u_1} {V : Type u_2} [inst : CategoryTheory.ReflQuiver U] [inst_1 : CategoryTheory.ReflQuiver V]
  {F G : U ⥤rq V}, F = G → ∀ (X : U), F.obj X = G.obj X
-- Mathlib.Algebra.Star.Subalgebra
Subsemiring.mk.congr_simp : ∀ {R : Type u} [inst : NonAssocSemiring R] (toSubmonoid toSubmonoid_1 : Submonoid R)
  (e_toSubmonoid : toSubmonoid = toSubmonoid_1)
  (add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier)
  (zero_mem' : 0 ∈ toSubmonoid.carrier),
  { toSubmonoid := toSubmonoid, add_mem' := add_mem', zero_mem' := zero_mem' } =
    { toSubmonoid := toSubmonoid_1, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient : ∀ {R : Type u_5} {M : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submonoid R)
  (M' : Submodule R M), IsLocalizedModule p (Submodule.toLocalizedQuotient p M')
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem`. -/
Topology.CWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n},
  i ∉ E.I n → Disjoint (Topology.RelCWComplex.openCell n i) ↑E
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- Recurrent formula for `torusIntegral`, see also `torusIntegral_succ`.  -/
torusIntegral_succAbove : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : (Fin (n + 1) → ℂ) → E}
  {c : Fin (n + 1) → ℂ} {R : Fin (n + 1) → ℝ},
  TorusIntegrable f c R →
    ∀ (i : Fin (n + 1)),
      (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
        ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)
-- Mathlib.Data.PEquiv
PEquiv.coe_mk_apply : ∀ {α : Type u} {β : Type v} (f₁ : α → Option β) (f₂ : β → Option α)
  (h : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b) (x : α), { toFun := f₁, invFun := f₂, inv := h } x = f₁ x
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The canonical isomorphism `(mappingCone φ)⟦n⟧ ≅ mappingCone (φ⟦n⟧')`.  -/
CochainComplex.mappingCone.shiftIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            (n : ℤ) →
              (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (CochainComplex.mappingCone φ) ≅
                CochainComplex.mappingCone ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
-- Init.Data.UInt.Lemmas
UInt64.le_refl : ∀ (a : UInt64), a ≤ a
-- Mathlib.Combinatorics.Graph.Basic
Graph.isLoopAt_iff_inc_not_isNonloopAt : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsLoopAt e x ↔ G.Inc e x ∧ ¬G.IsNonloopAt e x
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.algebraMap_eq_includeRight : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B],
  algebraMap B (TensorProduct R A B) = ↑Algebra.TensorProduct.includeRight
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.convMul_bialgHom_single_one : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Bialgebra R A] [inst_3 : AddCommMonoid M] (f g : WithConv (AddMonoidAlgebra R M →ₐc[R] A)) (x : M),
  (f * g).ofConv (AddMonoidAlgebra.single x 1) =
    f.ofConv (AddMonoidAlgebra.single x 1) * g.ofConv (AddMonoidAlgebra.single x 1)
-- Mathlib.Data.Option.Basic
Option.choice_eq_none : ∀ (α : Type u_5) [IsEmpty α], Option.choice α = none
-- Init.Data.UInt.Lemmas
UInt8.size_lt_usizeSize : UInt8.size < USize.size
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEq_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} (i j : E.I₀),
  CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯ = Equiv.refl (E.I₁ i j)
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor.toPreprocessorBase : Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor → Mathlib.Tactic.Linarith.PreprocessorBase
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instCommRingInt16 : Lean.Grind.CommRing Int16
-- Init.Prelude
/-- Auxiliary unsafe constant used by the Compiler when erasing casts.
 -/
lcCast : {α : Sort u} → {β : Sort v} → α → β
-- Mathlib.Geometry.Manifold.IsManifold.Basic
modelWithCorners_prod_coe_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H)
  (I' : ModelWithCorners 𝕜 E' H'), ↑(I.prod I').symm = Prod.map ↑I.symm ↑I'.symm
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.card_sigma : ∀ {α : Type u_3} {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)), (s.sigma t).card = ∑ a ∈ s, (t a).card
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.range_domRestrict`. -/
Set.range_restrict : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.range (s.domRestrict f) = f '' s
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- An algebra morphism with an underlying epimorphism hom in `C` is an algebra epimorphism.  -/
CategoryTheory.Endofunctor.Algebra.epi_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y) [h : CategoryTheory.Epi f.f], CategoryTheory.Epi f
-- Mathlib.Topology.UnitInterval
/-- `unit_interval` solves the goals `0 ≤ ↑x`, `0 ≤ 1 - ↑x`, `↑x ≤ 1`, and `1 - ↑x ≤ 1` for
any expression `x : I`.
 -/
Mathlib.Tactic.Interactive.tacticUnit_interval : Lean.ParserDescr
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Group β],
  FreeGroup.lift =
    { toFun := fun f => MonoidHom.mk' (Quot.lift (FreeGroup.Lift.aux f) ⋯) ⋯, invFun := fun g => ⇑g ∘ FreeGroup.of,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV : ∀ (K : Type u_2) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : UniformSpace K] [inst_3 : IsUniformAddGroup K]
  [inst_4 : IsValuativeTopology K], Valued.v.Compatible
-- Mathlib.Tactic.Linarith.Parsing
/-- `Sum.scaleByMonom s m` multiplies every monomial in `s` by `m`.  -/
Mathlib.Tactic.Linarith.Sum.scaleByMonom : Mathlib.Tactic.Linarith.Sum → Mathlib.Tactic.Linarith.Monom → Mathlib.Tactic.Linarith.Sum
-- Lean.DocString.Markdown
/-- A way to transform block elements extended with `b` (containing inline elements
extended with `i`) into Markdown lines.
 -/
Lean.Doc.MarkdownBlock : Type u → Type v → Type (max u v)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The distance is induced by the norm.  -/
NonUnitalSeminormedRing.dist_eq : ∀ {α : Type u_5} [self : NonUnitalSeminormedRing α] (x y : α), dist x y = ‖-x + y‖
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the reverse direction of `SimpleGraph.free_congr_left`. -/
SimpleGraph.Free.congr_left : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (e₁ : A ≃g B), B.Free C → A.Free C
-- Mathlib.Algebra.Field.Basic
one_div_mul_add_mul_one_div_eq_one_div_add_one_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b : K}, a ≠ 0 → b ≠ 0 → 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Composition of an almost everywhere equal function and a quasi-measure-preserving function.

See also `AEEqFun.compMeasurePreserving`.  -/
MeasureTheory.AEEqFun.compQuasiMeasurePreserving : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace γ] →
            [inst_2 : MeasurableSpace β] →
              {ν : MeasureTheory.Measure β} →
                (β →ₘ[ν] γ) → (f : α → β) → MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → α →ₘ[μ] γ
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_eq_ofInt : ∀ {n : ℤ} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt), Int8.ofIntLE n h₁ h₂ = Int8.ofInt n
-- Mathlib.NumberTheory.FunctionField
FunctionField.valuedFqtInfty : (F : Type u_1) →
  [inst : Field F] →
    [inst_1 : DecidableEq (RatFunc F)] → Valued (RatFunc.CompletionAtInfty F) (WithZero (Multiplicative ℤ))
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.spineToSimplex_spine_apply : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1)
  (Δ : X.obj (Opposite.op { obj := { len := m }, property := h })), sx.spineToSimplex m h (X.spine m h Δ) = Δ
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.eq_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E F : Topology.RelCWComplex.Subcomplex C), E = F ↔ ↑E = ↑F
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite'' : ∀ {α : Sort u_1} (c0 c1 : Bool) {a b : α}, (bif c0 then a else bif c1 then b else a) = bif !c0 && c1 then b else a
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformlyOn.comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] {γ : Type u_4} [inst_3 : TopologicalSpace γ] {t : Set γ},
  HasSumLocallyUniformlyOn f g s →
    ∀ (h' : γ → β), Set.MapsTo h' t s → ContinuousOn h' t → HasSumLocallyUniformlyOn (fun i y => f i (h' y)) (g ∘ h') t
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (X Y : C),
  CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y =
    (CategoryTheory.Limits.PreservesLimitPair.iso (F.comp FintypeCat.incl) X Y ≪≫
        CategoryTheory.Limits.Types.binaryProductIso (F.obj X).obj (F.obj Y).obj).toEquiv
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The underlying set of the subcomplex.  -/
Topology.RelCWComplex.Subcomplex.carrier : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} → [inst : Topology.RelCWComplex C D] → Topology.RelCWComplex.Subcomplex C → Set X
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported_strictMono : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] [Nontrivial R], StrictMono (MvPolynomial.supported R)
-- Mathlib.Topology.Separation.Regular
hasBasis_nhdsSet_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] (u : Set X),
  IsClosed u → (nhdsSet u).HasBasis (fun s => s ∈ nhdsSet u) closure
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getKey? a (⟨k, v⟩ :: l) = bif k == a then some k else Std.Internal.List.getKey? a l
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_filter_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.TreeSet.filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true
-- Lean.SubExpr
Lean.SubExpr.instFromJsonGoalsLocation.fromJson : Lean.Json → Except String Lean.SubExpr.GoalsLocation
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.isIso_toPshHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], CategoryTheory.IsIso f.toPshHom
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.length_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} [LawfulMonad m] {xs : Vector β n} {pos : ℕ},
  (xs.iterFromIdxM m pos).length = pure { down := n - pos }
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideEqualizer.trident_ι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y))
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f],
  (CategoryTheory.Limits.wideEqualizer.trident f).ι = CategoryTheory.Limits.wideEqualizer.ι f
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `η ▷ (g ⊗ h)`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight.mkEvalWhiskerRightComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.NormalExpr →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Logic.Denumerable
Nat.Subtype.ofNat.eq_1 : ∀ (s : Set ℕ) [inst : DecidablePred fun x => x ∈ s] [inst_1 : Infinite ↑s], Nat.Subtype.ofNat s 0 = ⊥
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.toUnit_comp_curryRightUnitorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {I : C} [inst_2 : CategoryTheory.Closed I] {A : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.curryRightUnitorHom I) =
    CategoryTheory.MonoidalClosed.curry (CategoryTheory.SemiCartesianMonoidalCategory.fst I A)
-- Init.Data.Array.Range
Array.range_succ : ∀ {n : ℕ}, Array.range n.succ = Array.range n ++ #[n]
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope.injEq : ∀ (lctx lctx_1 : Lean.LocalContext),
  (Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope✝ lctx =
      Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope✝ lctx_1) =
    (lctx = lctx_1)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The full subcategory of the over category `C/X` consisting of arrows which belong to a
presieve on `X`.  -/
CategoryTheory.Presieve.category : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Presieve X → Type (max u₁ v₁)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.nondegenerate_toLinearMap₂'_iff : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R},
  ((Matrix.toLinearMap₂' R) M).Nondegenerate ↔ M.Nondegenerate
-- Init.Control.Basic
/-- Right-to-left composition of Kleisli arrows. 

Conventions for notations in identifiers:

 * The recommended spelling of `<=<` in identifiers is `kleisliLeft`. -/
Bind.kleisliLeft : {α : Type u} → {m : Type u_1 → Type u_2} → {β γ : Type u_1} → [Bind m] → (β → m γ) → (α → m β) → α → m γ
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_norm_go : ∀ (ctx : Nat.Internal.Linear.Context) (p r : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote ctx (Nat.Internal.Linear.Poly.norm.go p r) =
    Nat.Internal.Linear.Poly.denote ctx p + Nat.Internal.Linear.Poly.denote ctx r
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.strongHomClass : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.StrongHomClass (L.Embedding M N) M N
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapRight.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)), κ.swapRight = κ.mapOfMeasurable Prod.swap ⋯
-- Init.Data.UInt.Bitwise
instCommutativeUInt16HOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.Algebra.Module.PUnit
PUnit.vadd_eq : ∀ {R : Type u_3} (y : PUnit.{u_4 + 1}) (r : R), r +ᵥ y = PUnit.unit
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.vlt_of_vlt_of_vle`. -/
ValuativeRel.vlt.trans_vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x <ᵥ y → y ≤ᵥ z → x <ᵥ z
-- Mathlib.Data.Seq.Basic
Stream'.Seq.head_dropn : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), (s.drop n).head = s.get? n
-- Mathlib.LinearAlgebra.Projection
LinearMap.linearProjOfIsCompl_apply_right' : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (q : Submodule R E)
  {F : Type u_7} [inst_3 : AddCommGroup F] [inst_4 : Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i)
  (h : IsCompl i.range q), ∀ x ∈ q, (LinearMap.linearProjOfIsCompl q i hi h) x = 0
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo : Type
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_forM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m PUnit.{u + 1}) (xs : List α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => xs.forM (f x)
-- Mathlib.Data.Finset.Density
Finset.dens_le_dens : ∀ {α : Type u_2} [inst : Fintype α] {s t : Finset α}, s ⊆ t → s.dens ≤ t.dens
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false → ∀ {k fallback : α}, (cmp k (t.minKeyD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insertMany_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α},
  t.insertMany (k :: l) = (t.insert k).insertMany l
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma1_mem : ∀ (N : ℕ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  A ∈ CongruenceSubgroup.Gamma1 N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffOn.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℂ n f s → ContDiffOn ℂ n (fun x => Complex.cosh (f x)) s
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β]
  [inst_4 : Min γ] [inst_5 : Top γ] (g : InfTopHom β γ) (f : InfTopHom α β),
  InfTopHom.dual (g.comp f) = (InfTopHom.dual g).comp (InfTopHom.dual f)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_iSup : ∀ {ι : Type u_1} [Finite ι] (u : ι → ℕ → EReal),
  LinearGrowth.linearGrowthSup (⨆ i, u i) = ⨆ i, LinearGrowth.linearGrowthSup (u i)
-- Init.Prelude
/-- State monads provide a value of a given type (the _state_) that can be retrieved or replaced.
Instances may implement these operations by passing state values around, by using a mutable
reference cell (e.g. `ST.Ref σ`), or in other ways.

In this class, `σ` is an `outParam`, which means that it is inferred from `m`. `MonadStateOf σ`
provides the same operations, but allows `σ` to influence instance synthesis.

The mutable state of a state monad is visible between multiple `do`-blocks or functions, unlike
[local mutable state](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=do-notation-let-mut) in `do`-notation.
 -/
MonadState : outParam (Type u) → (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C} {a : C} {str : F.obj a ⟶ a}
  {a_1 : C} {str_1 : F.obj a_1 ⟶ a_1}, { a := a, str := str } = { a := a_1, str := str_1 } → a = a_1 ∧ str ≍ str_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_insertMany_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ} {k : α},
  k ∈ m → k ∈ m.insertMany l
-- Mathlib.Data.NNReal.Defs
NNReal.coe_inv : ∀ (r : NNReal), ↑r⁻¹ = (↑r)⁻¹
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_one : ∀ {α : Type u_1}, FreeMonoid.toList 1 = []
-- Mathlib.InformationTheory.Hamming
/-- `Hamming.toHamming` is the identity function to the `Hamming` of a type.  -/
Hamming.toHamming : {ι : Type u_2} → {β : ι → Type u_3} → ((i : ι) → β i) ≃ Hamming β
-- Mathlib.Data.Matrix.Basis
Matrix.diagonal_single : ∀ {m : Type u_2} {α : Type u_7} [inst : DecidableEq m] [inst_1 : Zero α] (i : m) (r : α),
  Matrix.diagonal (Pi.single i r) = Matrix.single i i r
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a nilpotent group is the smallest natural `n` such that
the `n`-th term of the upper central series is `G`. If `G` is not nilpotent then the nilpotency
class takes the junk value 0.  -/
Group.nilpotencyClass : (G : Type u_1) → [Group G] → ℕ
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.compact_open_induction_on : ∀ {X : AlgebraicGeometry.Scheme} {P : X.Opens → Prop} (S : X.Opens),
  IsCompact ↑S → P ⊥ → (∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)) → P S
-- Mathlib.GroupTheory.Finiteness
Monoid.closure_finite_fg : ∀ {M : Type u_1} [inst : Monoid M] (s : Set M) [Finite ↑s], Monoid.FG ↥(Submonoid.closure s)