mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Ergodic.Ergodic
PreErgodic.ae_empty_or_univ : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  PreErgodic f μ → MeasurableSet s → f ⁻¹' s = s → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis'.encard_eq_eRk : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → I.encard = M.eRk X
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
then its derivative at `x₀` has norm bounded by `C`.  -/
HasDerivAt.le_of_lipschitz : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x₀ : 𝕜},
  HasDerivAt f f' x₀ → ∀ {C : NNReal}, LipschitzWith C f → ‖f'‖ ≤ ↑C
-- Init.Data.Array.Lemmas
List.reverse_toArray : ∀ {α : Type u_1} {l : List α}, l.toArray.reverse = l.reverse.toArray
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_sub_mul : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (d - c * x) = c⁻¹ • ∫ (x : ℝ) in d - c * b..d - c * a, f x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.srange.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N),
  f.srange = (AddSubsemigroup.map f ⊤).copy (Set.range ⇑f) ⋯
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.CommMonoid.sum_insertIdx : ∀ {M : Type u_4} [inst : AddCommMonoid M] {a : M} {l : List M} {i : ℕ}, i ≤ l.length → (l.insertIdx i a).sum = a + l.sum
-- Init.Data.Nat.Lemmas
Nat.mul_div_lt_iff_not_dvd : ∀ {n d : ℕ}, d * (n / d) < n ↔ ¬d ∣ n
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd.inj : ∀ {a b : ℤ} {c₁ c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {a_1 b_1 : ℤ}
  {c₁_1 c₂_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr},
  Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd a b c₁ c₂ =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd a_1 b_1 c₁_1 c₂_1 →
    a = a_1 ∧ b = b_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_toList : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldlM f init t = List.foldlM (fun a b => f a b.fst b.snd) init t.toList
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instPow : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Pow (DoubleCentralizer 𝕜 A) ℕ
-- Mathlib.RingTheory.HahnSeries.PowerSeries
Polynomial.algebraMap_hahnSeries_injective : ∀ (Γ : Type u_1) {R : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring Γ] [inst_2 : PartialOrder Γ]
  [inst_3 : IsStrictOrderedRing Γ], Function.Injective ⇑(algebraMap (Polynomial R) (HahnSeries Γ R))
-- Init.Data.RArray
_private.Init.Data.RArray.0.Lean.RArray.getImpl.match_1.splitter : {α : Type u_1} →
  (motive : Lean.RArray α → Sort u_2) →
    (a : Lean.RArray α) →
      ((x : α) → motive (Lean.RArray.leaf x)) →
        ((p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)) → motive a
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.minView.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3)
  (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size)
  (h_1 :
    (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hl hlr)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size
                    r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hl, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hl, hlr => h_1 hl hlr
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hl, hlr => h_2 size k' v' l' r' hl hlr) =
    h_1 hl hlr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.le_norm_expr_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] [inst_1 : LE α] [inst_2 : LT α] [inst_3 : Std.IsPreorder α]
  [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α) (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_cnstr_nc_cert lhs rhs lhs' rhs' = true →
    (Lean.Grind.CommRing.Expr.denote ctx lhs ≤ Lean.Grind.CommRing.Expr.denote ctx rhs) =
      (Lean.Grind.CommRing.Expr.denote ctx lhs' ≤ Lean.Grind.CommRing.Expr.denote ctx rhs')
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.cocones_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : C} (f : X ⟶ Y),
  F.cocones.map f = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp g ((CategoryTheory.Functor.const J).map f)
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Helper Lemma: Identify the support of `d` as the mulsupport of the product defining the factorized
rational function.
 -/
Function.FactorizedRational.mulSupport : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (d : 𝕜 → ℤ),
  (Function.mulSupport fun u => (fun x => x - u) ^ d u) = Function.support d
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- `toLowerSet` is the identity function to the `WithLowerSet` of a type.  -/
Topology.WithLowerSet.toLowerSet : {α : Type u_1} → α ≃ Topology.WithLowerSet α
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_sub : ∀ (a b : BitVec 32), Int32.ofBitVec (a - b) = Int32.ofBitVec a - Int32.ofBitVec b
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
/-- Construction of a left adjoint to the functor `pushforward.{v} φ` by using the
pullback of presheaves of modules and the sheafification.  -/
SheafOfModules.PullbackConstruction.adjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      [inst_3 : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint] →
                        [inst_4 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] →
                          [inst_5 : K.WEqualsLocallyBijective AddCommGrpCat] →
                            (SheafOfModules.forget S).comp
                                ((PresheafOfModules.pullback φ.hom).comp
                                  (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj))) ⊣
                              SheafOfModules.pushforward φ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α} {c : ℕ},
  (Std.DHashMap.Raw.emptyWithCapacity c).get? a = none
-- Mathlib.Topology.Algebra.UniformFilterBasis
AddGroupFilterBasis.cauchy_iff : ∀ {G : Type u_1} [inst : AddCommGroup G] (B : AddGroupFilterBasis G) {F : Filter G},
  Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsNotG2.toIsReduced : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} [self : P.IsNotG2],
  P.IsReduced
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {l : List α} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
      k ∈ l →
        ∀
          {h' :
            Std.DTreeMap.Internal.Impl.contains k'
                ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯) =
              true},
          (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey k' h' =
            k
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.map_smulₛₗ : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : R)
  (x : M), e (c • x) = σ c • e x
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_map_lid_symm_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid M'] [inst_8 : Module R M'] (f : M →ₗ[R] M')
  (g : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.assoc R M' R N).symm ∘ₗ TensorProduct.map f ↑(TensorProduct.lid R N).symm ∘ₗ g =
    TensorProduct.map (TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm) LinearMap.id ∘ₗ g
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
TensorProduct.tensorTensorTensorComm.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) (Q : Type u_8)
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P],
  TensorProduct.tensorTensorTensorComm R M N P Q =
    ((TensorProduct.assoc R (TensorProduct R M N) P Q).symm.trans
          (TensorProduct.congr (TensorProduct.rightComm R M N P) (LinearEquiv.refl R Q))).trans
      (TensorProduct.assoc R (TensorProduct R M P) N Q)
-- Lean.Server.GoTo
Lean.Server.locationLinksFromErrorNameInfo : Lean.Elab.ErrorNameInfo → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.of_not_isRegular : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → ¬c.IsRegular → c.IsSingular
-- Mathlib.Analysis.Convex.EGauge
/-- The extended gauge of a point `x` in an indexed product with finite index type
with respect to a product of balanced sets `U i`,
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.
 -/
egauge_univ_pi : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [Finite ι] {U : (i : ι) → Set (E i)},
  (∀ (i : ι), Balanced 𝕜 (U i)) → ∀ (x : (i : ι) → E i), egauge 𝕜 (Set.univ.pi U) x = ⨆ i, egauge 𝕜 (U i) (x i)
-- Mathlib.Algebra.Category.Ring.Basic
/-- Build a `RingEquiv` from an isomorphism in the category `CommSemiRingCat`.  -/
CategoryTheory.Iso.commSemiRingCatIsoToRingEquiv : {R S : CommSemiRingCat} → (R ≅ S) → ↑R ≃+* ↑S
-- Init.RCases
/-- The syntax category of `rcases` patterns.  -/
Lean.Parser.Category.rcasesPat : Lean.Parser.Category
-- Mathlib.Data.List.OffDiag
List.Nodup.of_offDiag : ∀ {α : Type u_1} {l : List α}, l.offDiag.Nodup → l.Nodup
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.toLinearMap_projectionL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), ↑(p.projectionL q h) = p.projection q ⋯
-- Mathlib.GroupTheory.Transfer
Subgroup.leftTransversals.diff_inv : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  (S T : H.LeftTransversal) [inst_2 : H.FiniteIndex],
  (Subgroup.leftTransversals.diff ϕ S T)⁻¹ = Subgroup.leftTransversals.diff ϕ T S
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.smulRight_id : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.id.smulRight = LinearMap.toSpanSingleton R M
-- Init.Internal.Order.Basic
Lean.Order.CCPO.csup.congr_simp : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {c c_1 : α → Prop} (e_c : c = c_1) (hc : Lean.Order.chain c),
  Lean.Order.CCPO.csup hc = Lean.Order.CCPO.csup ⋯
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- On square matrices, `mul_comm` applies under `det`.  -/
Matrix.det_mul_comm : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] (M N : Matrix m m R),
  (M * N).det = (N * M).det
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.dist_iterate_succ_le_geometric : ∀ {α : Type u} [inst : PseudoMetricSpace α] {K : NNReal} {f : α → α},
  LipschitzWith K f → ∀ (x : α) (n : ℕ), dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n
-- Mathlib.CategoryTheory.Comma.Basic
/-- `CommaMorphism.mk'` is the dual of `CommaMorphism.mk`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.CommaMorphism.mk' : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {X Y : CategoryTheory.Comma R L} →
                  (right : Y.right ⟶ X.right) →
                    (left : Y.left ⟶ X.left) →
                      CategoryTheory.CategoryStruct.comp Y.hom (L.map right) =
                          CategoryTheory.CategoryStruct.comp (R.map left) X.hom →
                        CategoryTheory.CommaMorphism Y X
-- Std.Http.Data.URI.Basic
/-- Converts the query to a properly encoded query string format.
Example: "key1=value1&key2=value2&flag"
 -/
Std.Http.URI.Query.toRawString : Std.Http.URI.Query → String
-- Init.Data.UInt.Lemmas
UInt16.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < UInt16.size → b < UInt16.size → (UInt16.ofNat a < UInt16.ofNat b ↔ a < b)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.coe_comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (g : γ → α) (hg : Measurable g), ⇑(κ.comap g hg) = ⇑κ ∘ g
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFieldInfo.sizeOf_spec : ∀ (i : Lean.Elab.FieldInfo), sizeOf (Lean.Elab.Info.ofFieldInfo i) = 1 + sizeOf i
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_add_ofNat : ∀ (r : ENNReal) (n : ℕ) [inst : n.AtLeastTwo], ⌈r + OfNat.ofNat n⌉ₑ = ⌈r⌉ₑ + OfNat.ofNat n
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.inducedFunctor_obj_coe : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) [inst_2 : HasFibers p] (S : 𝒮) (x : HasFibers.Fib p S),
  ↑((HasFibers.inducedFunctor p S).obj x) = (HasFibers.ι S).obj x
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_pos' : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulStrictMono ℚ≥0 α] {s : Finset ι} {f : ι → α},
  (∀ i ∈ s, 0 ≤ f i) → (∃ i ∈ s, 0 < f i) → 0 < s.expect fun i => f i
-- Mathlib.Data.ENNReal.Basic
/-- `ofReal x` returns `x` if it is nonnegative, `0` otherwise.  -/
ENNReal.ofReal : ℝ → ENNReal
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.containsAux : {α : Type u_1} → {β : Type u_2} → [BEq α] → Lean.PersistentHashMap.Node α β → USize → α → Bool
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The objects over `X i` for all `i`  -/
CategoryTheory.Pseudofunctor.DescentData'.obj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  F.DescentData' sq sq₃ → (i : ι) → ↑(F.obj { as := Opposite.op (X i) })
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_finitary : ∀ {α : Type u_1} (M : Matroid α) [M.Finitary] (D : Set α), (M.delete D).Finitary
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.mapRingHom.congr_simp : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f f_1 : α →+* β) (e_f : f = f_1) (hf : Continuous ⇑f),
  UniformSpace.Completion.mapRingHom f hf = UniformSpace.Completion.mapRingHom f_1 ⋯
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.HasSubst.expand : ∀ {σ : Type u_1} {τ : Type u_2} {S : Type u_4} [inst : CommRing S] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst f → MvPowerSeries.HasSubst fun i => (MvPowerSeries.expand p hp) (f i)
-- Mathlib.Topology.NhdsSet
subset_interior_iff_mem_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ interior t ↔ t ∈ nhdsSet s
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- `Filter α` is an atomic type: for every filter there exists an ultrafilter that is less than or
equal to this filter.  -/
instIsAtomicFilter : ∀ {α : Type u}, IsAtomic (Filter α)
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.inter : ∀ {α : Type u} {g : Set (Set α)} {s t : Set α},
  Filter.GenerateSets g s → Filter.GenerateSets g t → Filter.GenerateSets g (s ∩ t)
-- Mathlib.Analysis.RCLike.Extend
StrongDual.extendRCLike_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (fr : StrongDual ℝ F) (x : F), fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
-- Mathlib.Topology.Algebra.ConstMulAction
punctured_nhds_smul₀ : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → ∀ (x : α), nhdsWithin (c • x) {c • x}ᶜ = c • nhdsWithin x {x}ᶜ
-- Init.Core
flip_flip : ∀ {α : Sort u} {β : Sort v} {φ : Sort w} {f : α → β → φ}, flip (flip f) = f
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Std.IterStep.successor.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Std.IterStep α β → Sort u_3) →
      (x : Std.IterStep α β) →
        ((it : α) → (out : β) → motive (Std.IterStep.yield it out)) →
          ((it : α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instUniqueOfSubsingleton.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] [inst_1 : Subsingleton M],
  AddSubmonoid.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.IsReduced.of_forall_not_step : ∀ {α : Type u} {L₁ : List (α × Bool)},
  (∀ (L₂ : List (α × Bool)), ¬FreeAddGroup.Red.Step L₁ L₂) → FreeAddGroup.IsReduced L₁
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The sum of weighted homogeneous polynomials of degree `n` is weighted homogeneous of
weighted degree `n`.  -/
MvPolynomial.IsWeightedHomogeneous.sum : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {ι : Type u_4}
  (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : M) {w : σ → M},
  (∀ i ∈ s, MvPolynomial.IsWeightedHomogeneous w (φ i) n) → MvPolynomial.IsWeightedHomogeneous w (∑ i ∈ s, φ i) n
-- Mathlib.Data.PNat.Xgcd
/-- `IsSpecial` holds if the matrix has determinant one.  -/
PNat.XgcdType.IsSpecial : PNat.XgcdType → Prop
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.sliceFrom_endPos : ∀ {s : String.Slice} {p : s.Pos}, p.sliceFrom s.endPos ⋯ = (s.sliceFrom p).endPos
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.iSup_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {ι : Sort u_1}
  (S : ι → CategoryTheory.Subfunctor F) (U : C), (⨆ i, S i).obj U = ⋃ i, (S i).obj U
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.isPreprimitive_congr : ∀ {M : Type u_3} [inst : Group M] {α : Type u_4} [inst_1 : MulAction M α] {N : Type u_5} {β : Type u_6}
  [inst_2 : Group N] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Surjective φ → Function.Bijective ⇑f → (MulAction.IsPreprimitive M α ↔ MulAction.IsPreprimitive N β)
-- Mathlib.Data.Num.Bitwise
PosNum.instHXorNum : HXor PosNum PosNum Num
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- Matrices can be reflected whenever their entries can. We insert a `Matrix.of` to
prevent immediate decay to a function.  -/
Matrix.toExpr : {α : Type u} →
  {m' : Type uₘ} →
    {n' : Type uₙ} →
      [Lean.ToLevel] →
        [Lean.ToLevel] →
          [Lean.ToLevel] →
            [Lean.ToExpr α] →
              [Lean.ToExpr m'] → [Lean.ToExpr n'] → [Lean.ToExpr (m' → n' → α)] → Lean.ToExpr (Matrix m' n' α)
-- Mathlib.Data.ENNReal.Inv
ENNReal.toReal_inv : ∀ (a : ENNReal), a⁻¹.toReal = a.toReal⁻¹
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.natAbs_sub_pos_iff : ∀ {i j : ℤ}, 0 < (i - j).natAbs ↔ i ≠ j
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The left homology map data expressing that null homotopic maps induce the zero
morphism in left homology.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.ofNullHomotopic : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (H₁ : S₁.LeftHomologyData) →
          (H₂ : S₂.LeftHomologyData) →
            (h₀ : S₁.X₁ ⟶ S₂.X₁) →
              (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) →
                (h₁ : S₁.X₂ ⟶ S₂.X₁) →
                  (h₂ : S₁.X₃ ⟶ S₂.X₂) →
                    (h₃ : S₁.X₃ ⟶ S₂.X₃) →
                      (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) →
                        CategoryTheory.ShortComplex.LeftHomologyMapData (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁
                          H₂
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod_μ_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {C' : Type u₁'}
  [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor E C')
  [inst_7 : CategoryTheory.MonoidalCategory C'] [inst_8 : F.LaxMonoidal] [inst_9 : G.LaxMonoidal] (X Y : C × E),
  (CategoryTheory.Functor.LaxMonoidal.μ (F.prod G) X Y).2 = CategoryTheory.Functor.LaxMonoidal.μ G X.2 Y.2