mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.lift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α α_1 : M ⟶ K) (e_α : α = α_1) (β β_1 : CochainComplex.HomComplex.Cochain M L (-1)) (e_β : β = β_1)
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0),
  CochainComplex.mappingCocone.lift φ α β hαβ = CochainComplex.mappingCocone.lift φ α_1 β_1 ⋯
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.ComposableArrows.Precomp.obj.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (X : C)
  (i : ℕ) (hi : i + 1 < n + 1 + 1), CategoryTheory.ComposableArrows.Precomp.obj F X ⟨i.succ, hi⟩ = F.obj' i ⋯
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- the denominator of a left fraction  -/
CategoryTheory.MorphismProperty.LeftFraction.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction X Y) → Y ⟶ self.Y'
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.bcount.eq_2 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)] (p : { a // Irreducible a })
  (s : Multiset { a // Irreducible a }), Associates.bcount p (some s) = Multiset.count p s
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.neg.inj : ∀ {J : Type v} {inst : CategoryTheory.SmallCategory J} {F : CategoryTheory.Functor J RingCat}
  {a a_1 : RingCat.Colimits.Prequotient F}, a.neg = a_1.neg → a = a_1
-- Mathlib.RingTheory.Artinian.Algebra
/-- In an `R`-algebra over an Artinian ring `R`, if an element is integral and
is not a zero divisor, then it is a unit.  -/
IsArtinianRing.isUnit_of_isIntegral_of_nonZeroDivisor : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [IsArtinianRing R] [inst_2 : Ring A] [inst_3 : Algebra R A] {a : A},
  IsIntegral R a → a ∈ nonZeroDivisors A → IsUnit a
-- Mathlib.Logic.Encodable.Basic
Directed.sequence.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] {r r_1 : β → β → Prop} (e_r : r = r_1)
  (f f_1 : α → β) (e_f : f = f_1) (hf : Directed r f) (a a_1 : ℕ),
  a = a_1 → Directed.sequence f hf a = Directed.sequence f_1 ⋯ a_1
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for morphisms in `ComposableArrows C 2`.  -/
CategoryTheory.ComposableArrows.homMk₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {f g : CategoryTheory.ComposableArrows C 2} →
      (app₀ : f.obj' 0 _proof_245✝ ⟶ g.obj' 0 _proof_245✝) →
        (app₁ : f.obj' 1 _proof_246✝ ⟶ g.obj' 1 _proof_246✝) →
          (app₂ : f.obj' 2 _proof_247✝ ⟶ g.obj' 2 _proof_247✝) →
            autoParam
                (CategoryTheory.CategoryStruct.comp
                    (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝) app₁ =
                  CategoryTheory.CategoryStruct.comp app₀
                    (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
                _auto_241✝ →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂ =
                    CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_247✝))
                  _auto_243✝ →
                (f ⟶ g)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_rci : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  t.Ordered →
    ∀ (lowerBound : α),
      Std.Slice.toList (Std.Rci.Sliceable.mkSlice t lowerBound...*) =
        List.filter (fun e => (compare e lowerBound).isGE) t.keys
-- Mathlib.Data.Set.Prod
Set.image_swap_prod : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), Prod.swap '' s ×ˢ t = t ×ˢ s
-- Mathlib.CategoryTheory.Subobject.Comma
/-- Projecting and then lifting a quotient recovers the original quotient, because there is at most
one morphism making the projected quotient into a costructured arrow.  -/
CategoryTheory.CostructuredArrow.lift_projectQuotient : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} [inst_2 : CategoryTheory.Limits.HasFiniteColimits C]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T}
  (P : CategoryTheory.Subobject (Opposite.op A))
  {q :
    S.obj
        (Opposite.unop (CategoryTheory.Subobject.underlying.obj (CategoryTheory.CostructuredArrow.projectQuotient P))) ⟶
      T}
  (hq :
    CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q =
      A.hom),
  CategoryTheory.CostructuredArrow.liftQuotient (CategoryTheory.CostructuredArrow.projectQuotient P) hq = P
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁),
  (g ∘SL f) x = g (f x)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalarsSum.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c c_1 : ℕ → 𝕜),
  c = c_1 →
    ∀ (x x_1 : E), x = x_1 → FormalMultilinearSeries.ofScalarsSum c x = FormalMultilinearSeries.ofScalarsSum c_1 x_1
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkEqs : Array Lean.Expr → Array Lean.Expr → optParam Bool true → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
SubmodulesRingBasis.toRing_subgroups_basis : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {B : ι → Submodule R A}, SubmodulesRingBasis B → RingSubgroupsBasis fun i => (B i).toAddSubgroup
-- Mathlib.Data.Set.Prod
Set.prod_empty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s ×ˢ ∅ = ∅
-- Lean.Parser.Command
Lean.Parser.Command.deprecatedSyntax.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_mod_256 : ∀ (n : UInt8), n.toUInt16 % 256 = n.toUInt16
-- Mathlib.Analysis.Normed.Ring.Ultra
IsUltrametricDist.norm_intCast_le_one : ∀ (R : Type u_1) [inst : SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] (z : ℤ), ‖↑z‖ ≤ 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_some_getElem! : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α}, a ∈ m → m[a]? = some m[a]!
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S : C} →
        (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S) →
          toPreZeroHypercover.presieve₀ ∈ J.coverings S → J.ZeroHypercover S
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.pure_apply_self : ∀ {α : Type u_1} (a : α), (PMF.pure a) a = 1
-- Mathlib.Geometry.Manifold.PartitionOfUnity
BumpCovering.toSmoothPartitionOfUnity_toPartitionOfUnity : ∀ {ι : 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 : BumpCovering ι M s)
  (hf : ∀ (i : ι), ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ ⇑(f i)),
  (f.toSmoothPartitionOfUnity hf).toPartitionOfUnity = f.toPartitionOfUnity
-- Init.Data.Order.Ord
Std.TransCmp.lt_of_lt_of_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.lt → cmp b c = Ordering.eq → cmp a c = Ordering.lt
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The function `op` is a continuous linear equivalence.  -/
MulOpposite.opContinuousLinearEquiv : (R : Type u_1) →
  [inst : Semiring R] →
    {M : Type u_2} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : TopologicalSpace M] → M ≃L[R] Mᵐᵒᵖ
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- A finite formal multilinear series sums to its sum at every point.  -/
FormalMultilinearSeries.hasSum_of_finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ},
  (∀ (m : ℕ), n ≤ m → p m = 0) → ∀ (x : E), HasSum (fun n => (p n) fun x_1 => x) (p.sum x)
-- Mathlib.Algebra.Group.Subgroup.Map
/-- Makes the identity isomorphism from a proof two subgroups of a multiplicative
group are equal.  -/
MulEquiv.subgroupCongr : {G : Type u_1} → [inst : Group G] → {H K : Subgroup G} → H = K → ↥H ≃* ↥K
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A category has strong epi images if it has all images and `factorThruImage f` is a strong
epimorphism for all `f`.  -/
CategoryTheory.Limits.HasStrongEpiImages : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasImages C] → Prop
-- Mathlib.Analysis.Convex.Function
ConcaveOn.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f g : E → β}, ConcaveOn 𝕜 s f → ConvexOn 𝕜 s g → ConcaveOn 𝕜 s (f - g)
-- Mathlib.Data.List.Cycle
List.nextOr_nil : ∀ {α : Type u_1} [inst : DecidableEq α] (x d : α), [].nextOr x d = d
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.Indep.notMem_closure_sdiff_of_mem`. -/
Matroid.Indep.notMem_closure_diff_of_mem : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → e ∈ I → e ∉ M.closure (I \ {e})
-- Mathlib.LinearAlgebra.Finsupp.LSum
/-- If `M` and `N` are submodules of an `R`-algebra `S`, `m : ι → M` is a family of elements, then
there is an `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }` to the sum of `m_i * n_i`.
This is used in the definition of linearly disjointness.  -/
Submodule.mulLeftMap : {R : Type u_1} →
  [inst : Semiring R] →
    {S : Type u_4} →
      [inst_1 : Semiring S] →
        [inst_2 : Module R S] →
          [SMulCommClass R R S] →
            [SMulCommClass R S S] →
              {M : Submodule R S} → (N : Submodule R S) → {ι : Type u_5} → (ι → ↥M) → (ι →₀ ↥N) →ₗ[R] S
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.equalizerCondition_iff_isSheaf : ∀ {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] (F : CategoryTheory.Functor Cᵒᵖ D)
  [inst_2 : CategoryTheory.Preregular C]
  [∀ {Y X : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.regularTopology.EqualizerCondition F ↔
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F
-- Mathlib.Topology.Constructions
continuous_inclusion : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} (h : s ⊆ t), Continuous (Set.inclusion h)
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.coe_comp_orderHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedOrderHom β γ)
  (g : BoundedOrderHom α β), ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.RingTheory.Ideal.Operations
Ideal.iInf_sup_eq_top : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} {ι : Type u_1} {s : Finset ι} {J : ι → Ideal R}
  [∀ (i : ι), (J i).IsTwoSided], (∀ i ∈ s, J i ⊔ I = ⊤) → (⨅ i ∈ s, J i) ⊔ I = ⊤
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_inter_ne_top_of_right_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α}, μ t ≠ ⊤ → μ (s ∩ t) ≠ ⊤
-- Mathlib.Data.Set.Image
Set.preimage_image_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' f '' f ⁻¹' s = f ⁻¹' s
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f)).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).hom.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X) h)
-- Mathlib.Data.Part
Part.mem_map_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {o : Part α} {b : β}, b ∈ Part.map f o ↔ ∃ a ∈ o, f a = b
-- Mathlib.Data.Multiset.AddSub
/-- **Alias** of the forward direction of `Multiset.add_le_add_iff_left`. -/
Multiset.le_of_add_le_add_left : ∀ {α : Type u_1} {s t u : Multiset α}, s + t ≤ s + u → t ≤ u
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.forall_pow_eq_one_iff : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (i : ℕ), (∀ (x : Kˣ), x ^ i = 1) ↔ Fintype.card K - 1 ∣ i
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Convexity.StdSimplex.map.eq_1 : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {M : Type v} {N : Type w}
  (g : M → N) (f : Convexity.StdSimplex R M),
  Convexity.StdSimplex.map g f = { weights := Finsupp.mapDomain g f.weights, nonneg := ⋯, total := ⋯ }
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.mk.congr_simp : ∀ {n : ℕ} (parts parts_1 : Multiset ℕ) (e_parts : parts = parts_1) (parts_pos : ∀ {i : ℕ}, i ∈ parts → 0 < i)
  (parts_sum : parts.sum = n),
  { parts := parts, parts_pos := parts_pos, parts_sum := parts_sum } =
    { parts := parts_1, parts_pos := ⋯, parts_sum := ⋯ }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x₁ x₂ : M) (y₁ y₂ : ↥S), f.mk' (x₁ + x₂) (y₁ + y₂) = f.mk' x₁ y₁ + f.mk' x₂ y₂
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Internal.AssocList.step_iter_cons : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : Std.DHashMap.Internal.AssocList α β},
  (Std.DHashMap.Internal.AssocList.cons k v l).iter.step = ⟨Std.IterStep.yield l.iter ⟨k, v⟩, ⋯⟩
-- Init.Prelude
_private.Init.Prelude.0.Lean.assembleParts : List Lean.Name → Lean.Name → Lean.Name
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- A pointwise left Kan extension along the Yoneda embedding is an extension.  -/
CategoryTheory.Presheaf.isExtensionAlongULiftYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ℰ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ] →
        (A : CategoryTheory.Functor C ℰ) →
          [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] →
            CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp
                (CategoryTheory.uliftYoneda.{max v₂ w, v₁, u₁}.leftKanExtension A) ≅
              A
-- Mathlib.CategoryTheory.CommSq
/-- **Alias** of `CategoryTheory.Functor.map_commSq`. -/
CategoryTheory.CommSq.map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y}
  {h : X ⟶ Z} {i : Y ⟶ Z}, CategoryTheory.CommSq f g h i → CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.measurable : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst_2 : MeasurableSpace E] [BorelSpace E],
  ProbabilityTheory.IsKolmogorovProcess X P p q M → ∀ (s : T), Measurable (X s)
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.finBiconeHom : (J : Type v₁) →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] → (j k : CategoryTheory.Bicone J) → Fintype (j ⟶ k)
-- Mathlib.RingTheory.Ideal.Height
/-- An ideal has finite height if it is either the unit ideal or its height is finite.
We include the unit ideal in order to have the instance `IsNoetherianRing R → FiniteHeight I`.  -/
Ideal.FiniteHeight : {R : Type u_1} → [inst : CommRing R] → Ideal R → Prop
-- Mathlib.Topology.Algebra.Group.Basic
IsOpen.left_addCoset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {U : Set G},
  IsOpen U → ∀ (x : G), IsOpen (x +ᵥ U)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Note that as this lemma has an `if` in the statement, we include a `DecidableEq` argument.
This means you may not be able to `simp` using this lemma unless you `open scoped Classical`.  -/
CategoryTheory.Limits.biproduct.ι_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : DecidableEq J] (f : J → C)
  [inst_3 : CategoryTheory.Limits.HasBiproduct f] (j j' : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.π f j') =
    if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
-- Lean.Elab.DefView
Lean.Elab.DefView.mk.injEq : ∀ (kind : Lean.Elab.DefKind) (ref headerRef : Lean.Syntax) (modifiers : Lean.Elab.Modifiers)
  (declId binders : Lean.Syntax) (type? : Option Lean.Syntax) (value : Lean.Syntax)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment))
  (headerSnap? : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.HeaderProcessedSnapshot)))
  (deriving? : Option (Array Lean.Syntax)) (kind_1 : Lean.Elab.DefKind) (ref_1 headerRef_1 : Lean.Syntax)
  (modifiers_1 : Lean.Elab.Modifiers) (declId_1 binders_1 : Lean.Syntax) (type?_1 : Option Lean.Syntax)
  (value_1 : Lean.Syntax) (docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment))
  (headerSnap?_1 : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.HeaderProcessedSnapshot)))
  (deriving?_1 : Option (Array Lean.Syntax)),
  ({ kind := kind, ref := ref, headerRef := headerRef, modifiers := modifiers, declId := declId, binders := binders,
        type? := type?, value := value, docString? := docString?, headerSnap? := headerSnap?, deriving? := deriving? } =
      { kind := kind_1, ref := ref_1, headerRef := headerRef_1, modifiers := modifiers_1, declId := declId_1,
        binders := binders_1, type? := type?_1, value := value_1, docString? := docString?_1,
        headerSnap? := headerSnap?_1, deriving? := deriving?_1 }) =
    (kind = kind_1 ∧
      ref = ref_1 ∧
        headerRef = headerRef_1 ∧
          modifiers = modifiers_1 ∧
            declId = declId_1 ∧
              binders = binders_1 ∧
                type? = type?_1 ∧
                  value = value_1 ∧ docString? = docString?_1 ∧ headerSnap? = headerSnap?_1 ∧ deriving? = deriving?_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffWithinAt.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℂ n f s x → ContDiffWithinAt ℂ n (fun x => Complex.sin (f x)) s x
-- Mathlib.CategoryTheory.EssentialImage
/-- An object in the image is in the essential image.  -/
CategoryTheory.Functor.obj_mem_essImage : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) (Y : D), F.essImage (F.obj Y)
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Functor.mapCone₂_pt : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  {K₁ : CategoryTheory.Functor J₁ C₁} {K₂ : CategoryTheory.Functor J₂ C₂} (c₁ : CategoryTheory.Limits.Cone K₁)
  (c₂ : CategoryTheory.Limits.Cone K₂), (G.mapCone₂ c₁ c₂).pt = (G.obj c₁.pt).obj c₂.pt
-- Mathlib.CategoryTheory.Generator.Basic
/-- For a category `C` and an object `G : C`, `G` is a codetector of `C` if
the functor `C(-, G)` reflects isomorphisms.

While `IsCodetector G : Prop` is the proposition that `G` is a codetector of `C`,
an `HasCodetector C : Prop` is the proposition that such a codetector exists.
Note that `HasCodetector C` is a proposition. It does not designate a favored codetector
and merely asserts the existence of one.
 -/
CategoryTheory.HasCodetector : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- Two points in a projective space are dependent if and only if they are equal.  -/
Projectivization.dependent_pair_iff_eq : ∀ {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (u v : Projectivization K V), Projectivization.Dependent ![u, v] ↔ u = v
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.AddGrp C)
-- Mathlib.CategoryTheory.ObjectProperty.Comma
/-- Given functors `F₁ : C₁ ⥤ D` and `F₂ : C₂ ⥤ D`, and properties
of objects `P₁ : ObjectProperty C₁` and `P₂ : ObjectProperty C₂`,
this is the property of objects in `Comma F₁ F₂` satisfying
by the objects corresponding to morphisms `F₁.obj X₁ ⟶ F₂.obj X₂`
where `P₁ X₁` and `P₂ X₂` hold.  -/
CategoryTheory.ObjectProperty.comma : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            (F₁ : CategoryTheory.Functor C₁ D) →
              (F₂ : CategoryTheory.Functor C₂ D) →
                CategoryTheory.ObjectProperty C₁ →
                  CategoryTheory.ObjectProperty C₂ → CategoryTheory.ObjectProperty (CategoryTheory.Comma F₁ F₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The addition polynomial obtained by substituting the line `Y = ℓ(X - x) + y` into the polynomial
`W(X, Y)` associated to a Weierstrass curve `W`. If such a line intersects `W` at another
nonsingular affine point `(x', y')` on `W`, then the roots of this polynomial are precisely `x`,
`x'`, and the `X`-coordinate of the addition of `(x, y)` and `(x', y')`.

This depends on `W`, and has argument order: `x`, `y`, `ℓ`.  -/
WeierstrassCurve.Affine.addPolynomial : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Affine R → R → R → R → Polynomial R
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (𝒜 𝒜_1 : Finset (Finset α)),
  𝒜 = 𝒜_1 → ∀ (s s_1 : Finset α), s = s_1 → 𝒜.Shatters s = 𝒜_1.Shatters s_1