mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_sdiff_right`. -/
Set.union_diff_right : ∀ {α : Type u_1} {s t : Set α}, (s ∪ t) \ t = s \ t
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, CategoryTheory.Sieve.generate ⊥ = ⊥
-- Mathlib.Algebra.Module.Submodule.Map
/-- If `s ≤ t`, then we can view `s` as a submodule of `t` by taking the comap
of `t.subtype`.  -/
Submodule.comapSubtypeEquivOfLe : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {p q : Submodule R M} → p ≤ q → ↥(Submodule.comap q.subtype p) ≃ₗ[R] ↥p
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_zpow : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a : ℚ) (n : ℤ),
  Lean.Grind.Field.NormNum.ofRat (a ^ n) = Lean.Grind.Field.NormNum.ofRat a ^ n
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- Map a fractional ideal `I` to a submodule by forgetting that `∃ a, a I ⊆ R`.

This coercion is typically called `coeToSubmodule` in lemma names
(or `coe` when the coercion is clear from the context),
not to be confused with `IsLocalization.coeSubmodule : Ideal R → Submodule R P`
(which we use to define `coe : Ideal R → FractionalIdeal S P`).
 -/
FractionalIdeal.instCoeOutSubmodule : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → CoeOut (FractionalIdeal S P) (Submodule R P)
-- Mathlib.Topology.MetricSpace.Gluing
/-- The right injection of a space in a disjoint union is an isometry  -/
Metric.isometry_inr : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y], Isometry Sum.inr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpNatIso.eq_1 : ∀ {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 F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (e : F ≅ F'),
  CategoryTheory.Functor.mapAddGrpNatIso e =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.AddGrp.mkIso (e.app X.X) ⋯ ⋯) ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldrM.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (init : δ) (x : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.foldrM f init x =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => pure init
    | Std.DTreeMap.Internal.Impl.inner size k v l r => do
      let right ← Std.DTreeMap.Internal.Impl.foldrM f init r
      let middle ← f k v right
      Std.DTreeMap.Internal.Impl.foldrM f middle l
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instCommMonoidCoeOfSubmonoidClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → CommMonoid (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)],
  RestrictedProduct.instCommMonoidCoeOfSubmonoidClass R = Function.Injective.commMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- A `LinearPMap` is contained in its closure.  -/
LinearPMap.le_closure : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] (f : E →ₗ.[R] F), f ≤ f.closure
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDeriv_mul_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_3} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f g : E → A}
  {N : WithTop ℕ∞},
  ContDiff 𝕜 N f →
    ContDiff 𝕜 N g →
      ∀ (x : E) {n : ℕ},
        ↑n ≤ N →
          ‖iteratedFDeriv 𝕜 n (fun y => f y * g y) x‖ ≤
            ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_inj : ∀ {a b : BitVec System.Platform.numBits}, ISize.ofBitVec a = ISize.ofBitVec b ↔ a = b
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.isoOfComponents_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I)
  (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (a : X.I),
  (CategoryTheory.Limits.FormalCoproduct.isoOfComponents e h).hom.f a = e a
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.complexConj_apply_eq_self : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (x : ↥(NumberField.maximalRealSubfield K)),
  (NumberField.IsCMField.complexConj K) ↑x = ↑x
-- Mathlib.Topology.Homeomorph.Quotient
/-- Quotient spaces for equal relations are homeomorphic.  -/
Homeomorph.Quotient.congrRight : {X : Type u_1} →
  [inst : TopologicalSpace X] → {r r' : Setoid X} → (∀ (x₁ x₂ : X), r x₁ x₂ ↔ r' x₁ x₂) → Quotient r ≃ₜ Quotient r'
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.assoc_symm_tmul : ∀ (R : Type uR) (S : Type uS) {T : Type u_2} (A : Type uA) {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Algebra S C]
  [inst_10 : IsScalarTower R S C] [inst_11 : Semiring D] [inst_12 : Algebra R D] [inst_13 : CommSemiring T]
  [inst_14 : Algebra R T] [inst_15 : Algebra S T] [inst_16 : Algebra T A] [inst_17 : IsScalarTower R T A]
  [inst_18 : IsScalarTower S T A] (a : A) (b : C) (c : D),
  (Algebra.TensorProduct.assoc R S T A C D).symm (a ⊗ₜ[S] (b ⊗ₜ[R] c)) = a ⊗ₜ[S] b ⊗ₜ[R] c
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.ofCommSemiring : {α : Type u} → [inst : Lean.Grind.CommSemiring α] → Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkLambdaS : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] → Lean.Name → Lean.BinderInfo → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.IsIso f],
  CategoryTheory.Presheaf.IsLocallySurjective J f
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- The 2-isomorphisms underlying the strong naturality constraint.  -/
CategoryTheory.Pseudofunctor.StrongTrans.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          (self : F.StrongTrans G) →
            {a b : B} →
              (f : a ⟶ b) →
                CategoryTheory.CategoryStruct.comp (F.map f) (self.app b) ≅
                  CategoryTheory.CategoryStruct.comp (self.app a) (G.map f)
-- Init.Data.Int.DivMod.Lemmas
Int.sign_emod : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → (a % b).sign = if b ∣ a then 0 else 1
-- Mathlib.Algebra.Group.Units.Hom
/-- If two homomorphisms from a subtraction monoid to an additive monoid are equal at an
additive unit `x`, then they are equal at `-x`.  -/
IsAddUnit.eq_on_neg : ∀ {F : Type u_1} {G : Type u_2} {N : Type u_3} [inst : SubtractionMonoid G] [inst_1 : AddMonoid N]
  [inst_2 : FunLike F G N] [AddMonoidHomClass F G N] {x : G}, IsAddUnit x → ∀ (f g : F), f x = g x → f (-x) = g (-x)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω),
  μ s = μ.mass * μ.normalize s
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_ε : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [inst_4 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_5 :
    ∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_6 :
    ∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  (X : C) (x : Φ.fiber.obj X),
  CategoryTheory.Functor.LaxMonoidal.ε Φ.presheafFiber =
    Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A))
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.InfinitePlace.inertiaDeg.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L),
  v.inertiaDeg w = if x : w.LiesOver v then ⊥.inertiaDeg v.Completion else 0
-- Mathlib.Logic.Equiv.Prod
Equiv.curry_apply : ∀ (α : Type u_9) (β : Type u_10) (γ : Sort u_11), ⇑(Equiv.curry α β γ) = Function.curry
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableOn.coordChange : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e']
  [inst_20 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M → B} {g : M → F},
  MDiff[s] f →
    MDiff[s] g → Set.MapsTo f s e.baseSet → Set.MapsTo f s e'.baseSet → MDiff[s] fun y => e.coordChange e' (f y) (g y)
-- Lean.Data.PersistentArray
Lean.PersistentArray.instGetElemNatLtSizeOfInhabited : {α : Type u} → [Inhabited α] → GetElem (Lean.PersistentArray α) ℕ α fun as i => i < as.size
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Complex.cosh_eq_tsum : ∀ (z : ℂ), Complex.cosh z = ∑' (n : ℕ), z ^ (2 * n) / ↑(2 * n).factorial
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_pos_iff : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b : R}, 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
-- Mathlib.RingTheory.RegularLocalRing.Defs
/-- A Noetherian local ring is said to be regular if its maximal ideal
can be generated by `dim R` elements.  -/
IsRegularLocalRing : (R : Type u_1) → [CommRing R] → Prop
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_of_contMDiff_inr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M' : Type u_16}
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H M'] {n : WithTop ℕ∞} {E' : Type u_17}
  [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_18} [inst_8 : TopologicalSpace H']
  {J : ModelWithCorners 𝕜 E' H'} {N : Type u_20} {N' : Type u_21} [inst_9 : TopologicalSpace N]
  [inst_10 : TopologicalSpace N'] [inst_11 : ChartedSpace H' N] [inst_12 : ChartedSpace H' N'] {g : M' → N'},
  ContMDiff I J n (Sum.inr ∘ g) → ContMDiff I J n g
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g : α → M) (m n : ℕ) (x : α),
  birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)
-- Mathlib.Data.Bool.Basic
Bool.toNat_beq_zero : ∀ (b : Bool), (b.toNat == 0) = !b
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂'_apply : ∀ {R : Type u_1} {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring S₁]
  [inst_4 : Semiring S₂] [inst_5 : Module S₁ N₂] [inst_6 : Module S₂ N₂] [inst_7 : SMulCommClass S₁ R N₂]
  [inst_8 : SMulCommClass S₂ R N₂] [inst_9 : SMulCommClass S₂ S₁ N₂] [inst_10 : Fintype n] [inst_11 : Fintype m]
  [inst_12 : DecidableEq n] [inst_13 : DecidableEq m] (B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) (i : n) (j : m),
  (LinearMap.toMatrix₂' R) B i j = (B (Pi.single i 1)) (Pi.single j 1)
-- Init.Data.Ord.Basic
Ordering.eq_eq_of_isLE_of_isLE_swap : ∀ {o : Ordering}, o.isLE = true → o.swap.isLE = true → o = Ordering.eq
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_zpow_near_of_one_lt' : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G},
  1 < a → ∀ (g : G), ∃! k, 1 ≤ g / a ^ k ∧ g / a ^ k < a
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.normedGroup.eq_1 : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedGroup E] [inst_1 : NormedGroup F],
  Prod.normedGroup =
    { toNorm := Prod.seminormedGroup.toNorm, toGroup := Prod.seminormedGroup.toGroup,
      toPseudoMetricSpace := Prod.seminormedGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.id_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (U : CategoryTheory.Over X),
  CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.id U) = CategoryTheory.CategoryStruct.id U.left
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.comp_d₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (self : CochainComplex.ConnectData K L) {Z : C} (h : L.X 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.d 1 0) (CategoryTheory.CategoryStruct.comp self.d₀ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Topology.NhdsSet
nhdsSet_iUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Sort u_4} (s : ι → Set X), nhdsSet (⋃ i, s i) = ⨆ i, nhdsSet (s i)
-- Mathlib.Topology.MetricSpace.DilationEquiv
IsometryEquiv.toDilationEquiv_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵢ Y) (x : X),
  e.toDilationEquiv x = e x
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.left_le_veblen : ∀ (o a : Ordinal.{u_1}), o ≤ Ordinal.veblen o a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Init.Control.Lawful.Instances
StateT.run_monadLift : ∀ {m : Type u → Type u_1} {n : Type u → Type u_2} {α σ : Type u} [inst : Monad m] [inst_1 : MonadLiftT n m] (x : n α)
  (s : σ),
  (monadLift x).run s = do
    let a ← monadLift x
    pure (a, s)
-- Mathlib.Order.Ideal
Order.Cofinal.above_mem : ∀ {P : Type u_1} [inst : Preorder P] (D : Order.Cofinal P) (x : P), D.above x ∈ D
-- Init.Data.SInt.Lemmas
Int16.toInt8_sub : ∀ (a b : Int16), (a - b).toInt8 = a.toInt8 - b.toInt8
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.descH.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0),
  h.descH k hk = CategoryTheory.CategoryStruct.comp h.ι (h.descQ k hk)
-- Lean.DocString.DeferredCheck
/-- The check was deferred in docstring of a declaration.  -/
Lean.Doc.DeferredCheckSite.decl : Lean.Name → Lean.Doc.DeferredCheckSite
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.instCoeSortType : CoeSort CategoryTheory.Cat (Type u)
-- Mathlib.Algebra.Colimit.Ring
Ring.instCommRingDirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] → (f : (i j : ι) → i ≤ j → G i → G j) → CommRing (Ring.DirectLimit G f)
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.monoOver_terminal_to_subterminals_comp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C],
  (CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.comp (CategoryTheory.subterminalInclusion C) =
    (CategoryTheory.MonoOver.forget (⊤_ C)).comp (CategoryTheory.Over.forget (⊤_ C))
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranObjObjIsoLimit_hom_π_assoc : ∀ {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) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H)
  [inst_4 : L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) {Z : H}
  (h : F.obj ((CategoryTheory.StructuredArrow.proj X L).obj f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) h) =
    CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom)
      (CategoryTheory.CategoryStruct.comp ((L.ranCounit.app F).app f.right) h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.instIsIsoWhiskerLeft : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') [CategoryTheory.IsIso θ],
  CategoryTheory.IsIso (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldRevM_eq_foldrM_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRevM (fun d a x => f d a) init ↑m = Array.foldrM (fun a b => f b a) init (↑m).keysArray
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.sum_nonneg : ∀ {ι : Type uι} {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] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (x : M), 0 ≤ ∑ᶠ (i : ι), (f i) x
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.biUnionTagged_memBaseSet : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} {l : BoxIntegral.IntegrationParams}
  {r : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.Prepartition I}
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J},
  (∀ J ∈ π, l.MemBaseSet J c r (πi J)) →
    (∀ J ∈ π, (πi J).IsPartition) →
      (l.bDistortion = true → π.compl.distortion ≤ c) → l.MemBaseSet I c r (π.biUnionTagged πi)
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.permutationsAux2.match_3.splitter : {α : Type u_1} →
  {β : Type u_3} →
    (motive : List α → (List α → β) → Sort u_2) →
      (x : List α) →
        (x_1 : List α → β) →
          ((x : List α → β) → motive [] x) →
            ((y : α) → (ys : List α) → (f : List α → β) → motive (y :: ys) f) → motive x x_1
-- Init.Data.Array.Lemmas
Array.eq_push_of_size_ne_zero : ∀ {α : Type u_1} {xs : Array α}, xs.size ≠ 0 → ∃ bs c, xs = bs.push c
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Adding the first vector passed to `oangle` to the second vector does not change the sign of
the angle.  -/
Orientation.oangle_sign_add_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle x (x + y)).sign = (o.oangle x y).sign
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.coe_eq_one : ∀ {𝕜 : Type u_1} [inst : SeminormedRing 𝕜] [inst_1 : NormOneClass 𝕜] {a : ↑(Metric.closedBall 0 1)}, ↑a = 1 ↔ a = 1
-- Mathlib.CategoryTheory.Opposites
Quiver.Hom.op_inj : ∀ {C : Type u₁} [inst : Quiver C] {X Y : C}, Function.Injective Quiver.Hom.op
-- Batteries.Data.UnionFind.Basic
/-- Add a new node to a union-find structure, unlinked with any other nodes  -/
Batteries.UnionFind.push : Batteries.UnionFind → Batteries.UnionFind
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (X : CategoryTheory.SimplicialObject C),
  (CategoryTheory.Idempotents.DoldKan.isoN₁.hom.app X).f = AlgebraicTopology.DoldKan.PInfty
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.instMembershipSet : {G : Type u} → [inst : AddGroup G] → Membership (Set G) (AddGroupFilterBasis G)
-- Lean.ParserCompiler
Lean.ParserCompiler.Context.categoryAttr : {α : Type} → Lean.ParserCompiler.Context α → Lean.KeyedDeclsAttribute α
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.mem_ideal_iff : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {s : ↑(X.presheaf.obj (Opposite.op U))} {I : Ideal ↑(X.presheaf.obj (Opposite.op U))},
      s ∈ I ↔
        ∀ (x : ↥X) (h : x ∈ U),
          (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈
            Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for bitwise or of `BitVec`s.  -/
BitVec.reduceOr : Lean.Meta.Simp.DSimproc
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yz_sub : ∀ {a : ℕ} (a1 : 1 < a) {m n : ℕ}, n ≤ m → Pell.yz a1 (m - n) = Pell.xz a1 n * Pell.yz a1 m - Pell.xz a1 m * Pell.yz a1 n