mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- returns the characteristic morphism of the subobject `(m : U ⟶ X) [Mono m]`  -/
CategoryTheory.HasSubobjectClassifier.χ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasSubobjectClassifier C] →
      {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ CategoryTheory.HasSubobjectClassifier.Ω C
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_inter_add_sdiff₀`. -/
MeasureTheory.measureReal_inter_add_diff₀ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet t μ →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_inter_add_sdiff₀._auto_1 → μ.real (s ∩ t) + μ.real (s \ t) = μ.real s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β},
  m.getKey? k = some k' →
    Std.DHashMap.Const.getD (Std.DHashMap.filter f m) k fallback =
      (Option.filter (fun x => f k' x) (Std.DHashMap.Const.get? m k)).getD fallback
-- Mathlib.CategoryTheory.Products.Associator
/-- The associator isomorphism is compatible with `functorProdToProdFunctor`.  -/
CategoryTheory.prod.functorProdToProdFunctorAssociator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (A : Type u₄) →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} A] →
                (CategoryTheory.prod.associativity C D E).congrRight.functor.comp
                    ((CategoryTheory.functorProdToProdFunctor A C (D × E)).comp
                      ((CategoryTheory.Functor.id (CategoryTheory.Functor A C)).prod
                        (CategoryTheory.functorProdToProdFunctor A D E))) ≅
                  (CategoryTheory.functorProdToProdFunctor A (C × D) E).comp
                    (((CategoryTheory.functorProdToProdFunctor A C D).prod
                          (CategoryTheory.Functor.id (CategoryTheory.Functor A E))).comp
                      (CategoryTheory.prod.associativity (CategoryTheory.Functor A C) (CategoryTheory.Functor A D)
                          (CategoryTheory.Functor A E)).functor)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_inj : ∀ {a b : ℝ}, a.sigmoid = b.sigmoid ↔ a = b
-- Mathlib.Algebra.Group.Defs
IsDedekindFiniteMonoid.mk : ∀ {M : Type u_2} [inst : MulOne M], (∀ {a b : M}, a * b = 1 → b * a = 1) → IsDedekindFiniteMonoid M
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_left_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (X_1 : SimplexCategoryᵒᵖ), X.rightOpLeftOpIso.inv.left.app X_1 = CategoryTheory.CategoryStruct.id (X.left.obj X_1)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_unit_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : C} (f f' : e.inverse.obj (e.functor.obj Y) ⟶ X),
  CategoryTheory.CategoryStruct.comp (e.unit.app Y) f = CategoryTheory.CategoryStruct.comp (e.unit.app Y) f' ↔ f = f'
-- Init.Control.Lawful.MonadLift.Lemmas
liftM_seqLeft : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β),
  liftM (x <* y) = liftM x <* liftM y
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
summable_unop : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → αᵐᵒᵖ}, Summable (fun a => MulOpposite.unop (f a)) L ↔ Summable f L
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.map`  -/
TensorProduct.AlgebraTensorModule.map : {R : Type uR} →
  {A : Type uA} →
    {M : Type uM} →
      {N : Type uN} →
        {P : Type uP} →
          {Q : Type uQ} →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Algebra R A] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : Module R M] →
                      [inst_5 : Module A M] →
                        [inst_6 : IsScalarTower R A M] →
                          [inst_7 : AddCommMonoid N] →
                            [inst_8 : Module R N] →
                              [inst_9 : AddCommMonoid P] →
                                [inst_10 : Module R P] →
                                  [inst_11 : Module A P] →
                                    [inst_12 : IsScalarTower R A P] →
                                      [inst_13 : AddCommMonoid Q] →
                                        [inst_14 : Module R Q] →
                                          (M →ₗ[A] P) → (N →ₗ[R] Q) → TensorProduct R M N →ₗ[A] TensorProduct R P Q
-- Mathlib.Topology.Order
TopologicalSpace.nhds_mkOfNhds : ∀ {α : Type u} (n : α → Filter α) (a : α), pure ≤ n → (∀ (a : α), ∀ s ∈ n a, ∀ᶠ (y : α) in n a, s ∈ n y) → nhds a = n a
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X Y : G.Elements}
  (f : X ⟶ Y), ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.map f).base = ↑f
-- Mathlib.Computability.TuringMachine.Computable
/-- A proof that the identity map on α is computable in polytime.  -/
Turing.idComputableInPolyTime : {α αΓ : Type} → [Fintype αΓ] → (ea : α → List αΓ) → Turing.TM2ComputableInPolyTime ea ea id
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_pos : 0 < Cardinal.continuum
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (c : F), fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x
-- Mathlib.Computability.Encoding
Computability.unary_decode_encode_nat : ∀ (n : ℕ), Computability.unaryDecodeNat (Computability.unaryEncodeNat n) = n
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The natural isomorphism expressing that functors `Karoubi C ⥤ Karoubi D` obtained
using `functorExtension₂` actually extend the original functors `C ⥤ D`.  -/
CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso : (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] →
        (CategoryTheory.Idempotents.functorExtension₂ C D).comp
            ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C)
                  (CategoryTheory.Idempotents.Karoubi D)).obj
              (CategoryTheory.Idempotents.toKaroubi C)) ≅
          (CategoryTheory.Functor.whiskeringRight C D (CategoryTheory.Idempotents.Karoubi D)).obj
            (CategoryTheory.Idempotents.toKaroubi D)
-- Mathlib.CategoryTheory.GradedObject.Single
/-- The object `(single j).obj X i` is initial when `i ≠ j`.  -/
CategoryTheory.GradedObject.isInitialSingleObjApply : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Limits.HasInitial C] →
        [inst_2 : DecidableEq J] →
          (j : J) →
            (X : C) → (i : J) → i ≠ j → CategoryTheory.Limits.IsInitial ((CategoryTheory.GradedObject.single j).obj X i)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r : ∀ {X Y : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X ⟶ Y),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).r =
    (AlgebraicGeometry.Scheme.Modules.pushforward f.as.unop).toCatHom
-- Init.MetaTypes
Lean.Meta.Simp.NormCastConfig.mk : Lean.Meta.Simp.Config → Lean.Meta.Simp.NormCastConfig
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
/-- Constructor for cocycles from a single complex.  -/
CochainComplex.HomComplex.Cocycle.fromSingleMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X : C} →
          {K : CochainComplex C ℤ} →
            {p q : ℤ} →
              (f : X ⟶ K.X q) →
                {n : ℤ} →
                  p + n = q →
                    (q' : ℤ) →
                      q + 1 = q' →
                        CategoryTheory.CategoryStruct.comp f (K.d q q') = 0 →
                          CochainComplex.HomComplex.Cocycle ((CochainComplex.singleFunctor C p).obj X) K n
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasStrictFDerivAt.abs_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → 0 < f x → HasStrictFDerivAt (fun x => |f x|) f' x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} (h : (↑m).WF)
  {h' : (Std.DHashMap.Internal.Raw₀.filter f m).contains k = true},
  (Std.DHashMap.Internal.Raw₀.filter f m).get k h' = m.get k ⋯
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_ne_top : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.OrdSet.elems : {α : Type} → [inst : Hashable α] → [inst_1 : BEq α] → Lean.Meta.Try.Collector.OrdSet α → Array α
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.comap_top : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S), Subring.comap f ⊤ = ⊤
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.union_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∪ t₂).Equiv (t₃ ∪ t₄)
-- Mathlib.NumberTheory.Dioph
IsPoly.below.mul : ∀ {α : Type u_1} {motive : (a : (α → ℕ) → ℤ) → IsPoly a → Prop} {f g : (α → ℕ) → ℤ} (a : IsPoly f) (a_1 : IsPoly g),
  IsPoly.below a → motive f a → IsPoly.below a_1 → motive g a_1 → IsPoly.below ⋯
-- Mathlib.Analysis.LConvolution
/-- Convolution of a function with the zero function returns the zero function.  -/
MeasureTheory.mlconvolution_zero : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Mul G] [inst_1 : Inv G] (f : G → ENNReal)
  (μ : MeasureTheory.Measure G), MeasureTheory.mlconvolution f 0 μ = 0
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.ofAbs_inv : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Field R] (v : AbsoluteValue R S)
  (x : WithAbs v), x⁻¹.ofAbs = x.ofAbs⁻¹
-- Mathlib.Computability.RecursiveIn
/-- If every element of `O` is `Nat.RecursiveIn O'`, then any function which is
`Nat.RecursiveIn O` is also `Nat.RecursiveIn O'`.  -/
Nat.RecursiveIn.subst : ∀ {O O' : Set (ℕ →. ℕ)} {f : ℕ →. ℕ}, Nat.RecursiveIn O f → (∀ g ∈ O, Nat.RecursiveIn O' g) → Nat.RecursiveIn O' f
-- Batteries.Data.List.Perm
List.coe_idxInj : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs ys : List α} {h : xs.Subperm ys} {i : Fin xs.length},
  ↑(h.idxInj i) = List.idxOfNth xs[i] ys (List.countBefore xs[i] xs ↑i)
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.sigmaIsoSigma_hom_ι_assoc : ∀ {ι : Type v} (α : ι → TopCat) (i : ι) {Z : TopCat} (h : TopCat.of ((i : ι) × ↑(α i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι α i)
      (CategoryTheory.CategoryStruct.comp (TopCat.sigmaIsoSigma α).hom h) =
    CategoryTheory.CategoryStruct.comp (TopCat.sigmaι α i) h
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙAux_id : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁],
  (cfcₙAux ⋯ a ha) (ContinuousMapZero.id (quasispectrum 𝕜 a)) = ↑a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeWhile_takeWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, (s.takeWhile pat).takeWhile pat = s.takeWhile pat
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The inclusion into a summand of a biproduct.  -/
CategoryTheory.Limits.biproduct.ι : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) → [inst_2 : CategoryTheory.Limits.HasBiproduct f] → (b : J) → f b ⟶ ⨁ f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries.eq_2 : ∀ (x : ℝ) (n : ℕ), x.sqrtTwoAddSeries n.succ = √(2 + x.sqrtTwoAddSeries n)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pullback a `SMulWithZero` structure along an injective zero-preserving homomorphism.  -/
Function.Injective.smulWithZero : {M₀ : Type u_2} →
  {A : Type u_7} →
    {A' : Type u_8} →
      [inst : Zero M₀] →
        [inst_1 : Zero A] →
          [inst_2 : SMulWithZero M₀ A] →
            [inst_3 : Zero A'] →
              [inst_4 : SMul M₀ A'] →
                (f : ZeroHom A' A) →
                  Function.Injective ⇑f → (∀ (a : M₀) (b : A'), f (a • b) = a • f b) → SMulWithZero M₀ A'
-- Lean.SubExpr
Lean.SubExpr.Pos.isRoot : Lean.SubExpr.Pos → Bool
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- Given an isomorphism `α : Y ≅ Y₁` in C, the enriched composition map
`eComp V X Y Z : (X ⟶[V] Y) ⊗ (Y ⟶[V] Z) ⟶ (X ⟶[V] Z)` factors through the `V`
object `(X ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z)` via the map defined by whiskering in the
middle with `α.hom` and `α.inv`.  -/
CategoryTheory.eHom_whisker_cancel_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C}
  (α : Y ≅ Y₁) {Z_1 : V} (h : (X ⟶[V] Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerLeft V X α.hom) (Y ⟶[V] Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y₁) (CategoryTheory.eHomWhiskerRight V α.inv Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y₁ Z) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a b : F.CoGrothendieck}
  (f g : a ⟶ b),
  f = g ↔ ∃ (hfg : f.base = g.base), f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯)
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.finrank_fixedSubmodule_add_le : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] (e f : V ≃ₗ[K] V),
  Module.finrank K ↥(↑e).fixedSubmodule + Module.finrank K ↥(↑f).fixedSubmodule ≤
    Module.finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + Module.finrank K ↥(↑(e * f)).fixedSubmodule
-- Mathlib.CategoryTheory.ConcreteCategory.Elementwise
CategoryTheory.Limits.colimit.w_apply : ∀ {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.HasColimit F] {j j' : J} (f : j' ⟶ j)
  {F_1 : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_3 : CategoryTheory.ConcreteCategory C F_1] (x : carrier (F.obj j')),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j')) x
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Linear maps `(m → R) →ₗ[R] (n → R)` are linearly equivalent over `Rᵐᵒᵖ` to `Matrix m n R`,
by having matrices act by right multiplication.
 -/
LinearMap.toMatrixRight' : {R : Type u_1} →
  [inst : Semiring R] →
    {m : Type u_3} → {n : Type u_4} → [Fintype m] → [DecidableEq m] → ((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ] Matrix m n R
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  0 ≤ NumberField.mixedEmbedding.norm x
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.constantCoeff_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], MvPowerSeries.constantCoeff 1 = 1
-- Init.Data.List.Nat.Erase
List.eraseIdx_set_eq : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α}, (l.set i a).eraseIdx i = l.eraseIdx i
-- Lean.Data.Options
Lean.MonadOptions.getOptions : {m : Type → Type} → [self : Lean.MonadOptions m] → m Lean.Options
-- Init.Grind.Ring.Field
Lean.Grind.Field.div_div_left : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y z : α}, x / y / z = x / (y * z)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instRightCancelMonoid : {α : Type u_1} → [RightCancelMonoid α] → RightCancelMonoid (Colex α)
-- Mathlib.Algebra.Order.Group.Basic
zpow_le_zpow_left : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {n : ℤ} {a b : α},
  0 ≤ n → a ≤ b → a ^ n ≤ b ^ n
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_left_π : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).left.π =
    X.mapFourδ₄Toδ₃' i₀' i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyFun_empty : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)},
  MeasureTheory.IsProjectiveMeasureFamily P → MeasureTheory.projectiveFamilyFun P ∅ = 0
-- Mathlib.Topology.Order
continuous_coinduced_dom : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : β → γ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace γ},
  Continuous g ↔ Continuous (g ∘ f)
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.Context.mk.injEq : ∀ (paramNamePrefix : Lean.Name) (alreadyUsedPred : Lean.Name → Bool) (except : Lean.LMVarId → Bool)
  (paramNamePrefix_1 : Lean.Name) (alreadyUsedPred_1 : Lean.Name → Bool) (except_1 : Lean.LMVarId → Bool),
  ({ paramNamePrefix := paramNamePrefix, alreadyUsedPred := alreadyUsedPred, except := except } =
      { paramNamePrefix := paramNamePrefix_1, alreadyUsedPred := alreadyUsedPred_1, except := except_1 }) =
    (paramNamePrefix = paramNamePrefix_1 ∧ alreadyUsedPred = alreadyUsedPred_1 ∧ except = except_1)
-- Mathlib.RingTheory.Regular.RegularSequence
_private.Mathlib.RingTheory.Regular.RegularSequence.0.RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing.match_1.splitter : (α : Type u_1) →
  (x : CommRing α) →
    (M : Type u_2) →
      (x_1 : AddCommGroup M) →
        (x_2 : Module α M) →
          (r : α) →
            (rs : List α) →
              (motive :
                  IsSMulRegular M r ∧
                      RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M)
                        (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) →
                    Sort u_3) →
                (x_3 :
                    IsSMulRegular M r ∧
                      RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M)
                        (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) →
                  ((h1 : IsSMulRegular M r) →
                      (h2 :
                          RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M)
                            (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) →
                        motive ⋯) →
                    motive x_3
-- Mathlib.Topology.Order.NhdsSet
nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  a < b → nhdsSet (Set.Ico a b) = nhds a ⊔ Filter.principal (Set.Ioo a b)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.subsingleton_zero_smul_set : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] (s : Set β),
  (0 • s).Subsingleton
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks.0.CategoryTheory.Limits.spanOp.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingSpan → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : Unit → motive (some CategoryTheory.Limits.WalkingPair.left))
  (h_3 : Unit → motive (some CategoryTheory.Limits.WalkingPair.right)),
  (match none with
    | none => h_1 ()
    | some CategoryTheory.Limits.WalkingPair.left => h_2 ()
    | some CategoryTheory.Limits.WalkingPair.right => h_3 ()) =
    h_1 ()
-- Lean.Compiler.LCNF.Basic
/-- Lookup function for compiler extensions with sorted persisted state that works in both `lean` and
`leanir`.

`preferImported` defaults to false because in `leanir`, we do not want to mix information from
`meta` compilation in `lean` with our own state. But in `lean`, setting `preferImported` can help
with avoiding unnecessary task blocks.
 -/
Lean.Compiler.LCNF.findExtEntry? : {σ α β : Type} →
  {α' : Type u_1} →
    [Inhabited σ] →
      Lean.Environment →
        Lean.PersistentEnvExtension α β σ →
          Lean.Name → (Array α → Lean.Name → Option α') → (σ → Lean.Name → Option α') → Option α'
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A block of a group action is invariant iff it is fixed.  -/
AddAction.isInvariantBlock_iff_isFixedBlock : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsInvariantBlock G B ↔ AddAction.IsFixedBlock G B