mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    ∀ {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : CategoryTheory.CategoryStruct.comp f g = fg),
      CategoryTheory.Limits.IsZero ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)) →
        CategoryTheory.Epi ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg hfg))
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.type : Lean.Elab.Structural.EqnInfo → Lean.Expr
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntryD.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) (fallback : α × β)
  (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      (fallback : α × β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r),
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1),
      fallback => h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h fallback) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ fallback
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- The tensor product of two monoid algebras is the monoid algebra of their product.  -/
AddMonoidAlgebra.tensorEquiv : (R : Type u_1) →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommSemiring R] →
        TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R N) ≃ₗ[R] AddMonoidAlgebra R (M × N)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.colimitsOfShape_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] {Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.colimitsOfShape J ≤ Q.colimitsOfShape J
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.sizeOf_spec : sizeOf Std.Tactic.BVDecide.LRAT.Internal.Assignment.both = 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.mopFunctor_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.mopFunctor C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit Cᴹᵒᵖ)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_le : ∀ {a b : ℝ}, a ≤ b → a.sigmoid ≤ b.sigmoid
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_of_epi₂ : ∀ {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 ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, CategoryTheory.Epi T.mor₂ → T.mor₃ = 0
-- Batteries.Control.Nondet.Basic
Nondet.mk.sizeOf_spec : ∀ {σ : Type} {m : Type → Type} [inst : Lean.MonadBacktrack σ m] {α : Type} [inst_1 : SizeOf σ]
  [inst_2 : (a : Type) → SizeOf (m a)] [inst_3 : SizeOf α] (toMLList : MLList m (α × σ)),
  sizeOf { toMLList := toMLList } = 1 + sizeOf toMLList
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {v : β k} {h₁ : a ∈ t.insert k v},
  (t.insert k v).get a h₁ = if h₂ : cmp k a = Ordering.eq then cast ⋯ v else t.get a ⋯
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_C_mul : ∀ {R : Type u} [inst : Semiring R] (a : R) (p : Polynomial R) (k : ℕ),
  (⇑Polynomial.derivative)^[k] (Polynomial.C a * p) = Polynomial.C a * (⇑Polynomial.derivative)^[k] p
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sum_left' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ],
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance (fun ω => ∑ i ∈ s, X i ω) Y μ = ∑ i ∈ s, ProbabilityTheory.covariance (X i) Y μ
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.instIsModuleConvexSpaceFinsupp : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Convexity.ConvexSpace R M]
  [Convexity.IsModuleConvexSpace R M] {ι : Type u_6}, Convexity.IsModuleConvexSpace R (ι →₀ M)
-- Mathlib.Order.Nucleus
Nucleus.monotone : ∀ {X : Type u_1} [inst : SemilatticeInf X] {n : Nucleus X}, Monotone ⇑n
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.nsmul_replicate : ∀ {α : Type u_1} {a : α} (n m : ℕ), n • Multiset.replicate m a = Multiset.replicate (n * m) a
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- Reinterpret a `NonUnitalSubring` as a `NonUnitalSubsemiring`.  -/
NonUnitalSubring.toNonUnitalSubsemiring : {R : Type u} → [inst : NonUnitalNonAssocRing R] → NonUnitalSubring R → NonUnitalSubsemiring R
-- Std.Http.Data.URI.Encoding
/-- A percent-encoded URI query parameter. Valid characters are `pchar / "/" / "?"` with '+' for spaces.
 -/
Std.Http.URI.EncodedQueryParam : Type
-- Mathlib.MeasureTheory.Group.Measure
/-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then
it is a Haar measure.  -/
MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (K : Set G),
  IsCompact K → (interior K).Nonempty → μ K ≠ 0 → μ K ≠ ⊤ → μ.IsHaarMeasure
-- Mathlib.Data.FinEnum
FinEnum.instUniqueOfIsEmpty : {α : Type u} → [IsEmpty α] → Unique (FinEnum α)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- To prove something for almost all `x` w.r.t. a σ-finite measure, it is sufficient to show that
this holds almost everywhere in sets where the measure has finite value.  -/
MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (P : α → Prop),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x) → ∀ᵐ (x : α) ∂μ, P x
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- The tensor product of a pair of linear maps between modules.  -/
TensorProduct.map : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {M : Type u_7} →
            {N : Type u_8} →
              {M₂ : Type u_12} →
                {N₂ : Type u_14} →
                  [inst_2 : AddCommMonoid M] →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : AddCommMonoid N₂] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module R N] →
                              [inst_8 : Module R₂ M₂] →
                                [inst_9 : Module R₂ N₂] →
                                  (M →ₛₗ[σ₁₂] M₂) →
                                    (N →ₛₗ[σ₁₂] N₂) → TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_neg : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f : ContIntertwiningMap π₁ π₂),
  (-f).toContinuousLinearMap = -f.toContinuousLinearMap
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkHCongrProof' : Lean.Expr → Lean.Expr → ℕ → Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minEntry?_insertEntry.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (w : (a : α) × β a) → motive (some w)),
  (match none with
    | none => h_1 ()
    | some w => h_2 w) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.W_of_isLocallyBijective : ∀ {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]
  [J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y)
  [CategoryTheory.Presheaf.IsLocallyInjective J f] [CategoryTheory.Presheaf.IsLocallySurjective J f], J.W f
-- Mathlib.Analysis.Convolution
MeasureTheory.ConvolutionExistsAt.distrib_add : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g g' : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G] {x : G},
  MeasureTheory.ConvolutionExistsAt f g x L μ →
    MeasureTheory.ConvolutionExistsAt f g' x L μ →
      MeasureTheory.convolution f (g + g') L μ x =
        MeasureTheory.convolution f g L μ x + MeasureTheory.convolution f g' L μ x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.tensorAddUnit_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddMonObj.zero = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.restr_invFun : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : Equidecomp X G) (A : Set X) (a : X),
  (f.restr A).invFun a = ↑f.symm a
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_compRight : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (f : M₁ →ₗ[R₁] M₁),
  (LinearMap.BilinForm.toMatrix b) (B.compRight f) = (LinearMap.BilinForm.toMatrix b) B * (LinearMap.toMatrix b b) f
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
/-- `ζ 0 = 0`, otherwise `ζ x = 1`. The Dirichlet Series is the Riemann `ζ`.  -/
ArithmeticFunction.zeta.termζ : Lean.ParserDescr
-- Mathlib.RingTheory.PicardGroup
/-- Promote the canonical map `Mᵛ ⊗[R] M → R` to a linear equivalence for invertible `M`.  -/
Module.Invertible.linearEquiv : (R : Type u) →
  (M : Type v) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [Module.Invertible R M] → TensorProduct R (Module.Dual R M) M ≃ₗ[R] R
-- Init.NotationExtra
Lean.expandExplicitBindersAux : Lean.Syntax → Array Lean.Syntax → Option Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [CompactSpace α], MeasureTheory.IsFiniteMeasure μ ↔ MeasureTheory.IsFiniteMeasureOnCompacts μ
-- Mathlib.Order.Disjoint
IsCompl.left_unique : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl x z → IsCompl y z → x = y
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.isColimitOfPreserves.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  (F : CategoryTheory.Functor C D) {c : CategoryTheory.Limits.Cocone K} (t t_1 : CategoryTheory.Limits.IsColimit c),
  t = t_1 →
    ∀ [inst_3 : CategoryTheory.Limits.PreservesColimit K F],
      CategoryTheory.Limits.isColimitOfPreserves F t = CategoryTheory.Limits.isColimitOfPreserves F t_1
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.instTypeNameInlayHint : TypeName Lean.Elab.InlayHint
-- Batteries.Data.List.Lemmas
List.union_def : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α), l₁ ∪ l₂ = List.foldr List.insert l₂ l₁
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.of_isRepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  [inst_1 : F.IsRepresentable], F.IsRepresentedBy F.reprx
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.uniqueUpToIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t), (P.uniqueUpToIso Q).hom = P.descCoconeMorphism t
-- Mathlib.Order.Category.BoolAlg
BoolAlg.instInhabited : Inhabited BoolAlg
-- Mathlib.RingTheory.RamificationInertia.Basic
/-- Let `S/R` be a finite flat extension of integral domains, and let `p` be prime ideal of `R`.
Assume that `R` is the invariant subring of a finite group `G` acting on `S`. Then the sum over
all prime ideals `q` of `S` lying over `p` of the ramification index of `q` times the inertia
degree of `q` equals the cardinality of `G`.  -/
Ideal.sum_ramification_inertia_eq_card : ∀ {R : Type u_1} [inst : CommRing R] (p : Ideal R) [p.IsPrime] (S : Type u_2) [inst_2 : CommRing S]
  [inst_3 : Algebra R S] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S]
  [inst_8 : Fintype ↑(p.primesOver S)] {G : Type u_3} [inst_9 : Group G] [inst_10 : MulSemiringAction G S]
  [IsGaloisGroup G R S], ∑ q, (↑q).ramificationIdx R * (↑q).inertiaDeg R = Nat.card G
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.pullback_mem_iff_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C}
  {i : X ⟶ Y} [CategoryTheory.IsIso i] {S : CategoryTheory.Sieve Y}, CategoryTheory.Sieve.pullback i S ∈ J X ↔ S ∈ J Y
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.ofMulDist.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : Group E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)),
  NormedGroup.ofMulDist h₁ h₂ =
    { toNorm := (SeminormedGroup.ofMulDist h₁ h₂).toNorm, toGroup := (SeminormedGroup.ofMulDist h₁ h₂).toGroup,
      toPseudoMetricSpace := (SeminormedGroup.ofMulDist h₁ h₂).toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯,
      dist_eq := ⋯ }
-- Mathlib.Topology.UnitInterval
unitInterval.toNNReal_symm_add_toNNReal : ∀ (x : ↑unitInterval), unitInterval.toNNReal (unitInterval.symm x) + unitInterval.toNNReal x = 1
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The product of strongly measurable functions is measurable.  -/
MeasureTheory.StronglyMeasurable.tprod' : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ContinuousMul E] {L : SummationFilter ι}
  [L.NeBot] [L.filter.IsCountablyGenerated] {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable (∏'[L] (i : ι), f i)
-- Mathlib.Algebra.GroupWithZero.Action.Prod
/-- Construct a `DistribMulAction` by a product monoid from `DistribMulAction`s by the factors.  -/
DistribMulAction.prodOfSMulCommClass : (M : Type u_1) →
  (N : Type u_2) →
    (α : Type u_3) →
      [inst : Monoid M] →
        [inst_1 : Monoid N] →
          [inst_2 : AddMonoid α] →
            [inst_3 : DistribMulAction M α] →
              [inst_4 : DistribMulAction N α] → [SMulCommClass M N α] → DistribMulAction (M × N) α
-- Init.Data.Array.Basic
/-- Removes the first occurrence of a specified element from an array, or does nothing if it is not
present.

This function takes worst-case `O(n)` time because it back-shifts all later elements.

Examples:
* `#[1, 2, 3].erase 2 = #[1, 3]`
* `#[1, 2, 3].erase 5 = #[1, 2, 3]`
* `#[1, 2, 3, 2, 1].erase 2 = #[1, 3, 2, 1]`
* `(#[] : List Nat).erase 2 = #[]`
 -/
Array.erase : {α : Type u} → [BEq α] → Array α → α → Array α
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (m n : σ →₀ ℕ) (a : R),
  (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a) = if m = n then a else 0
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.erased : Lean.IR.IRType
-- Mathlib.Algebra.WithConv
WithConv.ofConv_zero : ∀ {A : Type u_2} [inst : AddMonoid A], WithConv.ofConv 0 = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.termMap : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map_comp_inr : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N'),
  (AddMonoid.Coprod.map f g).comp AddMonoid.Coprod.inr = AddMonoid.Coprod.inr.comp g
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.inhabited : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    (x : P.last.M) → {i : Fin2 n} → [Inhabited (P.drop.B x.head i)] → Inhabited (MvPFunctor.M.Path P x i)
-- Lean.Environment
Lean.EnvExtension.AsyncMode.mainOnly.sizeOf_spec : sizeOf Lean.EnvExtension.AsyncMode.mainOnly = 1
-- Mathlib.Data.Multiset.Bind
/-- `join S`, where `S` is a multiset of multisets, is the lift of the list join
operation, that is, the union of all the sets.
For example, `join {{1, 2}, {1, 2}, {0, 1}} = {0, 1, 1, 1, 2, 2}`.  -/
Multiset.join : {α : Type u_1} → Multiset (Multiset α) → Multiset α
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.localInverse_tendsto : ∀ {𝕜 : 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}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  Filter.Tendsto (HasStrictFDerivAt.localInverse f f' a hf) (nhds (f a)) (nhds a)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm : ∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)],
  PiTensorProduct.injectiveSeminorm ≤ PiTensorProduct.projectiveSeminorm
-- Lean.Meta.Tactic.Grind.Types
/-- Anchors are used to reference terms, local theorems, and case-splits in the `grind` state.
We also use anchors to prune the search space when they are provided as `grind` parameters
and the `finish` tactic.
 -/
Lean.Meta.Grind.AnchorRef : Type
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.instBoundedOrderCarrier : (X : NonemptyFinLinOrd) → BoundedOrder ↑X.toLinOrd
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.mk.sizeOf_spec : ∀ {X : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  (edge : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 }))
  (src_eq :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge =
        x₀)
      SSet.Truncated.Edge.src_eq._autoParam)
  (tgt_eq :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge =
        x₁)
      SSet.Truncated.Edge.tgt_eq._autoParam),
  sizeOf { edge := edge, src_eq := src_eq, tgt_eq := tgt_eq } = 1 + sizeOf edge + sizeOf src_eq + sizeOf tgt_eq
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_smul_left_complex : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {z : ℂ} {x y : E},
  inner A (z • x) y = star z • inner A x y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_hom_app : ∀ (X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ),
  CategoryTheory.Limits.walkingCospanOpEquiv.unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.term𝕎 : Lean.ParserDescr
-- Mathlib.Data.Prod.Lex
Prod.Lex.toLex_gt_toLex : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {x y : α × β},
  toLex y < toLex x ↔ y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 < x.2
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSlice.instToIterator : {α : Type u_1} →
  {β : Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RicSliceData α β)) Id
        (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxcIterator α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
          pure (b.fst, b.snd))
        (α × β)