mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.nhdsWithin_basis_eball`. -/
EMetric.nhdsWithin_basis_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α},
  (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.eball x ε ∩ s
-- Mathlib.Algebra.Category.ModuleCat.Projective
/-- The category of modules has enough projectives, since every module is a quotient of a free
module.  -/
ModuleCat.enoughProjectives : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R], CategoryTheory.EnoughProjectives (ModuleCat R)
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalBinderInfo : Lean.Meta.ReduceEval Lean.BinderInfo
-- Mathlib.Algebra.Lie.Derivation.Killing
/-- Every derivation of a finite-dimensional Killing Lie algebra is an inner derivation.  -/
LieDerivation.IsKilling.exists_eq_ad : ∀ {R : Type u_1} {L : Type u_2} [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Module.Finite R L]
  [LieAlgebra.IsKilling R L] (D : LieDerivation R L L), ∃ x, (LieDerivation.ad R L) x = D
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- The right homotopy in the opposite category that is deduced from a left homotopy.  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {P : HomotopicalAlgebra.Precylinder X} → {f g : X ⟶ Y} → P.LeftHomotopy f g → P.op.RightHomotopy f.op g.op
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.sum_ite_eq`.  -/
Fintype.sum_ite_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι)
  (f : ι → M), (∑ j, if i = j then f j else 0) = f i
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `continuous_mul_const`. -/
continuous_mul_right : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] (m : M),
  Continuous fun x => x * m
-- Mathlib.Logic.Equiv.Basic
/-- The product over `Option α` of `β a` is the binary product of the
product over `α` of `β (some α)` and `β none`  -/
Equiv.piOptionEquivProd : {α : Type u_10} → {β : Option α → Type u_9} → ((a : Option α) → β a) ≃ β none × ((a : α) → β (some a))
-- Mathlib.Analysis.CStarAlgebra.Classes
/-- The class of non-unital (complex) C⋆-algebras.  -/
NonUnitalCStarAlgebra : Type u_1 → Type u_1
-- Mathlib.Data.List.Nodup
List.Nodup.notMem : ∀ {α : Type u} {l : List α} {a : α}, (a :: l).Nodup → a ∉ l
-- Mathlib.Topology.JacobsonSpace
JacobsonSpace.of_isClosedEmbedding : ∀ {X : Type u_2} {Y : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [JacobsonSpace Y],
  Topology.IsClosedEmbedding f → JacobsonSpace X
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.add_mul_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (R : C)
  [inst_2 : CategoryTheory.MonObj R] [inst_3 : CategoryTheory.AddMonObj R],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add R)
        CategoryTheory.MonObj.mul =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.fst R R)
              R)
            CategoryTheory.MonObj.mul)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.snd R R)
              R)
            CategoryTheory.MonObj.mul))
        CategoryTheory.AddMonObj.add ↔
    ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.categoryOfElements.hcongr_3 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (F : CategoryTheory.Functor C (Type w)) (F' : CategoryTheory.Functor C' (Type w)),
          F ≍ F' → CategoryTheory.categoryOfElements F ≍ CategoryTheory.categoryOfElements F'
-- Init.Data.Vector.OfFn
Vector.toArray_ofFnM : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {f : Fin n → m α},
  Vector.toArray <$> Vector.ofFnM f = Array.ofFnM f
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
measurable_id : ∀ {α : Type u_1} {x : MeasurableSpace α}, Measurable id
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_congr_ae₂ : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} {x : MeasurableSpace β} {ν : MeasureTheory.Measure β} {f g : α → β → G},
  (∀ᵐ (a : α) ∂μ, f a =ᵐ[ν] g a) → ∫ (a : α), ∫ (b : β), f a b ∂ν ∂μ = ∫ (a : α), ∫ (b : β), g a b ∂ν ∂μ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_inverse_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor SimplexCategory Cᵒᵖ),
  (CategoryTheory.simplicialCosimplicialEquiv C).inverse.obj F = Opposite.op F.leftOp
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The edge given by a `1`-simplex.  -/
SSet.Edge.mk' : {X : SSet} →
  (s : X.obj (Opposite.op { len := 1 })) →
    SSet.Edge ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) s)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {a b : α} {fallback : β},
      cmp a b = Ordering.eq → Std.DTreeMap.Raw.Const.getD t a fallback = Std.DTreeMap.Raw.Const.getD t b fallback
-- Mathlib.Data.Set.Insert
Set.preimage_snd_singleton_eq_range : ∀ {α : Type u_3} {β : Type u_4} {b : β}, Prod.snd ⁻¹' {b} = Set.range fun x => (x, b)
-- Mathlib.Order.Hom.Bounded
/-- `id` as a `BoundedOrderHom`.  -/
BoundedOrderHom.id : (α : Type u_2) → [inst : Preorder α] → [inst_1 : BoundedOrder α] → BoundedOrderHom α α
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_add : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] [inst_6 : ContinuousAdd M₁]
  (x y : M₁),
  ContinuousLinearMap.toSpanSingleton R₁ (x + y) =
    ContinuousLinearMap.toSpanSingleton R₁ x + ContinuousLinearMap.toSpanSingleton R₁ y
-- Mathlib.CategoryTheory.Monad.Limits
/-- A comonadic functor creates any limits of shapes it preserves.  -/
CategoryTheory.comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} J] →
            (R : CategoryTheory.Functor D C) →
              [CategoryTheory.ComonadicLeftAdjoint R] →
                [CategoryTheory.Limits.PreservesLimitsOfShape J R] → CategoryTheory.CreatesLimitsOfShape J R
-- Init.Prelude
/-- A `MonadRef` is a monad that has a `ref : Syntax` in the read-only state.
This is used to keep track of the location where we are working; if an exception
is thrown, the `ref` gives the location where the error will be reported,
assuming no more specific location is provided.
 -/
Lean.MonadRef : (Type → Type) → Type 1
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.revChars.eq_1 : ∀ (s : String), s.revChars = s.toSlice.revChars
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.ext' : ∀ (F : PFunctor.{uA, uB}) (x y : F.M), (∀ (i : ℕ), x.approx i = y.approx i) → x = y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eq_some_iff_getKey?_eq_some_getValue?_eq_some : ∀ {α : Type u} [inst : BEq α] {β : Type v} {l : List ((_ : α) × β)} {k k' : α} {v : β},
  Std.Internal.List.getEntry? k l = some ⟨k', v⟩ ↔
    Std.Internal.List.getKey? k l = some k' ∧ Std.Internal.List.getValue? k l = some v
-- Mathlib.Data.Fin.VecNotation
Matrix.tail_cons : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α), Matrix.vecTail (Matrix.vecCons x u) = u
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.box.eq_1 : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] (ν : ι → ℤ),
  BoxIntegral.unitPartition.box n ν =
    { lower := fun i => ↑(ν i) / ↑n, upper := fun i => (↑(ν i) + 1) / ↑n, lower_lt_upper := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The composition `t.truncLT b ⋙ t.truncGE a`.  -/
CategoryTheory.Triangulated.TStructure.truncGELT : {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] →
              CategoryTheory.Triangulated.TStructure C → ℤ → ℤ → CategoryTheory.Functor C C
-- Batteries.Data.List.Lemmas
List.countBefore_of_ge_length : ∀ {α : Type u_1} {i : ℕ} {x : α} [inst : BEq α] {xs : List α}, xs.length ≤ i → List.countBefore x xs i = List.count x xs
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instModule : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → (S : NonUnitalStarSubalgebra R A) → Module R ↥S
-- Mathlib.Algebra.Homology.Embedding.Extend
ComplexShape.Embedding.instFaithfulHomologicalComplexExtendFunctor : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C], (e.extendFunctor C).Faithful
-- Init.Data.BitVec.Lemmas
BitVec.cast_setWidth : ∀ {v v' w : ℕ} (h : v = v') (x : BitVec w), BitVec.cast h (BitVec.setWidth v x) = BitVec.setWidth v' x
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
/-- The forgetful functor `AddCommMonCat.{u} ⥤ Type u` is corepresentable.  -/
AddCommMonCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (AddCommMonCat.of (ULift.{u, 0} ℕ))) ≅ CategoryTheory.forget AddCommMonCat
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicValued_apply' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)),
  Valued.v ((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)) x) =
    (IsDedekindDomain.HeightOneSpectrum.valuation K v)
      ((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)) x)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A version of `linearIndepOn_iff` where the linear combination is a `Finset` sum
of a function with support contained in the `Finset`.  -/
linearIndepOn_iff'' : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v : ι → M},
  LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc_normNoninc : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} {cond : CategoryTheory.CategoryStruct.comp f g = 0},
  (SemiNormedGrp.Hom.hom g).NormNoninc → (SemiNormedGrp.Hom.hom (SemiNormedGrp.explicitCokernelDesc cond)).NormNoninc
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.chromaticNumber_eq_two_iff : ∀ {V : Type u_1} {G : SimpleGraph V}, G.chromaticNumber = 2 ↔ G.IsBipartite ∧ G ≠ ⊥
-- Lean.Util.Trace
Lean.TraceElem : Type
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Every `BinaryFan` is isomorphic to an application of `BinaryFan.mk`.  -/
CategoryTheory.Limits.isoBinaryFanMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (c : CategoryTheory.Limits.BinaryFan X Y) → c ≅ CategoryTheory.Limits.BinaryFan.mk c.fst c.snd
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (a a_1 : T₁.obj₁ ⟶ T₂.obj₁) (e_a : a = a_1)
  (b b_1 : T₁.obj₂ ⟶ T₂.obj₂) (e_b : b = b_1)
  (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁),
  CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm =
    CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a_1 b_1 ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.postcomp_mk₀_injective_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (L : C) {M N : C} (f : M ⟶ N) [hf : CategoryTheory.Mono f],
  Function.Injective ⇑((CategoryTheory.Abelian.Ext.mk₀ f).postcomp L ⋯)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_le_size_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, m.size ≤ (m.erase k).size + 1
-- Init.Prelude
/-- `Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`. -/
Or : Prop → Prop → Prop
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.liftCycles_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
  [inst_2 : S.HasLeftHomology], CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) S.iCycles = k
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.augmentedCechConerve.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom],
  CategoryTheory.CosimplicialObject.augmentedCechConerve = CategoryTheory.CosimplicialObject.augmentedCechConerve
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : α →Co β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Init.Data.Int.Repr
Int.instRepr : Repr ℤ
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_subset_Iic_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} [DenselyOrdered α], Set.Iio b ⊆ Set.Iic a ↔ b ≤ a
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_eq_natCast_iff' : ∀ (a b c : ℕ), ↑a = ↑b ↔ a % c = b % c
-- Mathlib.Order.Ideal
/-- The carrier of a `Cofinal` is the underlying set.  -/
Order.Cofinal.carrier : {P : Type u_2} → [inst : Preorder P] → Order.Cofinal P → Set P
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
isIntegral_zero : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B], IsIntegral R 0
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- The vertices of a simplicial complex are its zero-dimensional faces.  -/
Geometry.SimplicialComplex.vertices : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] → [inst_3 : Module 𝕜 E] → Geometry.SimplicialComplex 𝕜 E → Set E
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingCone.triangleRotateShortComplex_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangleRotateShortComplex φ).X₁ = (CochainComplex.mappingCone.triangle φ).rotate.obj₁
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_neg : ∀ {R : Type u_3} (A : Type u_4) [inst : Neg R] [inst_1 : AddGroup A] (r : R), Unitization.inl (-r) = -Unitization.inl r
-- Mathlib.Data.List.Lex
List.Lex.to_ne : ∀ {α : Type u} {l₁ l₂ : List α}, List.Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂ → l₁ ≠ l₂
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_congr_fun : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f g : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  Set.EqOn f g s → MeasurableSet s → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn g s μ)
-- Std.Http.Data.Body.Any
/-- Closes the body stream.
 -/
Std.Http.Body.Any.close : Std.Http.Body.Any → Std.Async.Async Unit
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_mul : ∀ (a b : UInt8), (a * b).toUInt16 = a.toUInt16 * b.toUInt16 % 256
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparison_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (F.obj A) (F.obj B)) =
    F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd A B)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_iso_top : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H), SimpleGraph.Subgraph.map e.toHom ⊤ = ⊤
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic.0.CategoryTheory.Abelian.Ext.zero_hom' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X Y : C) (n : ℕ), CategoryTheory.Abelian.Ext.hom' 0 = 0
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.bisim : ∀ {P : PFunctor.{uA, uB}} (R : P.M → P.M → Prop),
  (∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)) →
    ∀ (x y : P.M), R x y → x = y
-- Init.Data.SInt.Lemmas
Int16.ofIntLE.eq_1 : ∀ (i : ℤ) (_hl : Int16.minValue.toInt ≤ i) (_hr : i ≤ Int16.maxValue.toInt), Int16.ofIntLE i _hl _hr = Int16.ofInt i
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α},
  Std.ExtDHashMap.Const.get? (m₁ ∩ m₂) k = if k ∈ m₂ then Std.ExtDHashMap.Const.get? m₁ k else none
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun.eq_def : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a x : α),
  IncidenceAlgebra.muFun✝ 𝕜 a x =
    let b := x;
    if a = b then 1
    else
      -∑ x_1 ∈ (Finset.Ico a b).attach,
          have h := ⋯;
          have this := ⋯;
          IncidenceAlgebra.muFun✝ 𝕜 a ↑x_1
-- Mathlib.RingTheory.TensorProduct.Basic
/-- If `s` generates `T` as an `R`-algebra,
then `{ 1 ⊗ x | x ∈ s }` generates `A ⊗[R] T` as an `A`-algebra.  -/
Algebra.TensorProduct.adjoin_one_tmul_image_eq_top : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (s : Set B),
  Algebra.adjoin R s = ⊤ → Algebra.adjoin A ((fun x => 1 ⊗ₜ[R] x) '' s) = ⊤
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.cone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.limit.cone F = (CategoryTheory.Limits.getLimitCone F).cone
-- Init.Data.Vector.Perm
Vector.swap.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i j : ℕ) (hi : i < n) (hj : j < n),
  xs.swap i j hi hj = Vector.mk (xs.toArray.swap i j ⋯ ⋯) ⋯
-- Lean.ReducibilityAttrs
Lean.instReprReducibilityStatus : Repr Lean.ReducibilityStatus
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen_coe : ∀ {X : AlgebraicGeometry.Scheme} (U : X.AffineZariskiSite) (f : ↑(X.presheaf.obj (Opposite.op U.toOpens))),
  ↑(U.basicOpen f) = X.basicOpen f
-- Mathlib.Geometry.Manifold.Instances.Quotient
AddAction.instChartedSpaceQuotient : {M : Type u_1} →
  [inst : TopologicalSpace M] →
    {G : Type u_2} →
      [inst_1 : AddGroup G] →
        [inst_2 : AddAction G M] →
          [ProperlyDiscontinuousVAdd G M] →
            [ContinuousConstVAdd G M] →
              [IsCancelVAdd G M] →
                [T2Space M] →
                  [LocallyCompactSpace M] →
                    {H : Type u_3} →
                      [inst_8 : TopologicalSpace H] →
                        [ChartedSpace H M] → ChartedSpace H (AddAction.orbitRel.Quotient G M)
-- Mathlib.RingTheory.Trace.Basic
Module.Basis.trace_mul_traceDual : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι]
  (b : Module.Basis ι K L) (i j : ι), (Algebra.trace K L) (b i * b.traceDual j) = if i = j then 1 else 0
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.traceStep : String → StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Unit
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_injective_image : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [MeasurableSingletonClass α]
  [MeasurableSingletonClass β] {f : β → α},
  Function.Injective f → ∀ (s : Set β), MeasureTheory.Measure.count (f '' s) = MeasureTheory.Measure.count s
-- Mathlib.Data.Int.Fib.Basic
Int.fib_add : ∀ (m n : ℤ), Int.fib (m + n) = Int.fib (m - 1) * Int.fib n + Int.fib m * Int.fib (n + 1)
-- Mathlib.RingTheory.Finiteness.Finsupp
/-- If $M → N → P → 0$ is exact and $M$ and $P$ are finitely generated then so is $N$.

This is the `Module.Finite` version of `Submodule.fg_of_fg_map_of_fg_inf_ker`.  -/
Module.Finite.of_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g → Function.Surjective ⇑g → ∀ [Module.Finite R M] [Module.Finite R P], Module.Finite R N
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.ColimitType.instNeg : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → Neg (CommRingCat.Colimits.ColimitType F)