mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.filterMapM.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [inst_1 : Monad n]
  [inst_2 : MonadAttach n] [inst_3 : MonadLiftT m n] (f : β → n (Option γ)) (it : Std.IterM m β),
  Std.IterM.filterMapM f it =
    Std.IterM.filterMapWithPostcondition (fun b => Std.Iterators.PostconditionT.attachLift (f b)) it
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A version of `isNoetherian_iff_of_finite_iSup_eq_top` using `Scheme.OpenCover`.  -/
AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover : ∀ {X : AlgebraicGeometry.Scheme} {𝒰 : X.OpenCover} [Finite 𝒰.I₀] [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)],
  AlgebraicGeometry.IsNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑((𝒰.X i).presheaf.obj (Opposite.op ⊤))
-- Init.Data.Fin.Lemmas
Fin.rev_addNat : ∀ {n : ℕ} (k : Fin n) (m : ℕ), (k.addNat m).rev = Fin.castAdd m k.rev
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f c b < slope f a b`.  -/
lineMap_lt_map_iff_slope_lt_slope_right : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < (1 - r) * (b - a) →
    ((AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔
      slope f ((AffineMap.lineMap a b) r) b < slope f a b)
-- Std.Time.DateTime
/-- Subtract `Minute.Offset` from a `DateTime`.
 -/
Std.Time.DateTime.subMinutes : Std.Time.DateTime → Std.Time.Minute.Offset → Std.Time.DateTime
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.sigmaOpenCover_f : ∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ] (b : σ),
  (AlgebraicGeometry.sigmaOpenCover g).f b = CategoryTheory.Limits.Sigma.ι g b
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.IsGalois.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] (X X_1 : C),
  X = X_1 → CategoryTheory.PreGaloisCategory.IsGalois X = CategoryTheory.PreGaloisCategory.IsGalois X_1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesMapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (iso : K ≅ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], (HomologicalComplex.cyclesMapIso iso i).inv = HomologicalComplex.cyclesMap iso.inv i
-- Mathlib.Data.Nat.Size
Nat.size_shiftLeft : ∀ {m : ℕ}, m ≠ 0 → ∀ (n : ℕ), (m <<< n).size = m.size + n
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.symm_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A),
  P.symm.i₀ = P.i₁
-- Mathlib.Order.SupClosed
supClosure_mono : ∀ {α : Type u_3} [inst : SemilatticeSup α], Monotone ⇑supClosure
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_modify_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : β k → β k}, m.WF → (m.modify k f).get? k = Option.map f (m.get? k)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
  CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ = γ.φH
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHomRight : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] (d : D) (x x_1 : C) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f = (F.map f).app d
-- Mathlib.AlgebraicGeometry.Scheme
/-- An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.  -/
AlgebraicGeometry.Scheme.Hom.homeomorph : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [CategoryTheory.IsIso f] → ↥X ≃ₜ ↥Y
-- Mathlib.Order.LatticeIntervals
Set.Ici.orderTop : {α : Type u_1} → [inst : Preorder α] → [OrderTop α] → {a : α} → OrderTop ↑(Set.Ici a)
-- Init.Data.List.Zip
_private.Init.Data.List.Zip.0.instDecidableEqProd.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α × β → Sort u_3) (a' : α) (b' : β)
  (h_1 : (a' : α) → (b' : β) → motive (a', b')),
  (match (a', b') with
    | (a', b') => h_1 a' b') =
    h_1 a' b'
-- Mathlib.RingTheory.Ideal.Over
/-- Consider the following commutative diagram of ring maps
```
A → B
↓   ↓
C → D
```
and let `P` be an ideal of `B`. The image in `C` of the ideal of `A` under `P` is included
in the ideal of `C` under the image of `P` in `D`.
 -/
Ideal.map_under_le_under_map : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (P : Ideal B)
  {C : Type u_5} {D : Type u_6} [inst_3 : CommSemiring C] [inst_4 : Semiring D] [inst_5 : Algebra A C]
  [inst_6 : Algebra C D] [inst_7 : Algebra A D] [inst_8 : Algebra B D] [IsScalarTower A C D] [IsScalarTower A B D],
  Ideal.map (algebraMap A C) (Ideal.under A P) ≤ Ideal.under C (Ideal.map (algebraMap B D) P)
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgEquiv.toBialgIso_trans : ∀ {R : Type u} [inst : CommRing R] {X Y Z : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : Ring Z]
  [inst_4 : Bialgebra R X] [inst_5 : Bialgebra R Y] [inst_6 : Bialgebra R Z] (e : X ≃ₐc[R] Y) (f : Y ≃ₐc[R] Z),
  (e.trans f).toBialgIso = e.toBialgIso ≪≫ f.toBialgIso
-- Mathlib.RingTheory.Discriminant
/-- Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we define
`discr A ι b` as the determinant of `traceMatrix A ι b`.  -/
Algebra.discr : {ι : Type w} →
  [DecidableEq ι] →
    (A : Type u) →
      {B : Type v} → [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → [Fintype ι] → (ι → B) → A
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.eq_num_div_den : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (f : HomogeneousLocalization 𝒜 x), f.val = Localization.mk f.num ⟨f.den, ⋯⟩
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} {Φ : J.Point} {F : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D} [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P : CategoryTheory.Functor Dᵒᵖ A} {T : A}
  {f g : (Φ.map F K).presheafFiber.obj P ⟶ T},
  f = g ↔
    ∀ (X : C) (x : Φ.fiber.obj X),
      CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) f =
        CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k a : α}
  {fallback v : β},
  Std.DTreeMap.Const.getD (t.insertIfNew k v) a fallback =
    if cmp k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Const.getD t a fallback
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.mul` -/
MeromorphicAt.fun_mul : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'},
  MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (fun i => f i * g i) x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- The structured arrow category `StructuredArrow d T` depends on the chosen domain `d : D` in a
functorial way, inducing a functor `Dᵒᵖ ⥤ Cat`.  -/
CategoryTheory.StructuredArrow.functor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor Dᵒᵖ CategoryTheory.Cat
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryGT!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGT! k = t₂.getEntryGT! k
-- Mathlib.Order.WithBotTop
WithBotTop.top_ne_bot : ∀ {ι : Type u_1}, ⊤ ≠ ⊥
-- Std.Internal.UV.System
/-- Gets the system uptime in seconds.
 -/
Std.Internal.UV.System.uptime : IO UInt64
-- Mathlib.Topology.Compactness.Compact
/-- If `s : Set (X × Y)` belongs to `l ×ˢ 𝓝 y` for all `y` from a compact set `K`,
then it belongs to `l ×ˢ (𝓝ˢ K)`,
i.e., there exist `t ∈ l` and an open `U ⊇ K` such that `t ×ˢ U ⊆ s`.  -/
IsCompact.mem_prod_nhdsSet_of_forall : ∀ {Y : Type v} [inst : TopologicalSpace Y] {K : Set Y} {X : Type u_2} {l : Filter X} {s : Set (X × Y)},
  IsCompact K → (∀ y ∈ K, s ∈ l ×ˢ nhds y) → s ∈ l ×ˢ nhdsSet K
-- Mathlib.Data.Finmap
Finmap.Disjoint.symm : ∀ {α : Type u} {β : α → Type v} (x y : Finmap β), x.Disjoint y → y.Disjoint x
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instCompactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [CompactSpace α], CompactSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.GroupTheory.NoncommCoprod
AddHom.noncommCoprod_apply : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : AddSemigroup P] (f : M →ₙ+ P)
  (g : N →ₙ+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) (mn : M × N),
  (f.noncommCoprod g comm) mn = f mn.1 + g mn.2
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.toMeasureEquiv_apply : ∀ {α : Type u_2} (self : MeasureTheory.LevyProkhorov α),
  MeasureTheory.LevyProkhorov.toMeasureEquiv self = self.toMeasure
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.derivedSeries_eq_bot_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k : ℕ), LieAlgebra.derivedSeries R (↥I) k = ⊥ ↔ LieAlgebra.derivedSeriesOfIdeal R L k I = ⊥
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivAevalXAddC_eq_iff : ∀ {R : Type u_3} [inst : CommRing R] (t t' : R),
  Polynomial.algEquivAevalXAddC t = Polynomial.algEquivAevalXAddC t' ↔ t = t'
-- Mathlib.Order.ULift
ULift.down_inf : ∀ {α : Type u} [inst : Min α] (a b : ULift.{u_1, u} α), (a ⊓ b).down = a.down ⊓ b.down
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier : CategoryTheory.ConcreteCategory PartOrdEmb fun x1 x2 => ↑x1 ↪o ↑x2
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α},
  StrictConvexOn 𝕜 (f '' s) g →
    StrictConvexOn 𝕜 s f → StrictMonoOn g (f '' s) → Set.InjOn f s → StrictConvexOn 𝕜 s (g ∘ f)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsTriangulatedMinus : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.minus.IsTriangulated
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- The diagonal morphism `X ⟶ Δ_{X/Y}` for a morphism `f : X ⟶ Y`.  -/
CategoryTheory.Limits.pullback.diagonal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      (f : X ⟶ Y) → [inst_1 : CategoryTheory.Limits.HasPullback f f] → X ⟶ CategoryTheory.Limits.pullback.diagonalObj f
-- Batteries.Data.List.Lemmas
List.countBefore_nil : ∀ {α : Type u_1} {x : α} {i : ℕ} [inst : BEq α], List.countBefore x [] i = 0
-- Mathlib.Geometry.Manifold.ChartedSpace
mem_achart_source : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), x ∈ (↑(achart H x)).source
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.piFinTwo_apply : ∀ (α : Fin 2 → Type u_3) [inst : (i : Fin 2) → PseudoEMetricSpace (α i)] (f : (i : Fin 2) → α i),
  (IsometryEquiv.piFinTwo α) f = (f 0, f 1)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.Hom.toRationalMap.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y), f.toRationalMap = f.toPartialMap.toRationalMap
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_self_atTop_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x : G),
  MapClusterPt x Filter.atTop fun x_1 => x ^ x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.map_uniq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  (F G : CategoryTheory.Limits.ImageMap sq), F.map = G.map
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.hasExt_of_hasDerivedCategory : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] [HasDerivedCategory C],
  CategoryTheory.HasExt C
-- Mathlib.Analysis.Normed.Group.Subgroup
SubgroupClass.normedCommGroup.eq_1 : ∀ {E : Type u_1} [inst : NormedCommGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : SubgroupClass S E] (s : S),
  SubgroupClass.normedCommGroup s =
    { toNorm := (SubgroupClass.seminormedCommGroup s).toNorm, toCommGroup := SubgroupClass.toCommGroup s,
      toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }
-- Mathlib.Combinatorics.Enumerative.DyckWord
instDecidableEqDyckWord.decEq : (x x_1 : DyckWord) → Decidable (x = x_1)
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.match.sizeOf_spec : ∀ (gen? : Option Lean.Meta.Grind.GenPatternInfo) (pat e : Lean.Expr),
  sizeOf (Lean.Meta.Grind.EMatch.Cnstr.match gen? pat e) = 1 + sizeOf gen? + sizeOf pat + sizeOf e
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.mk.sizeOf_spec : ∀ (toProfinite : Profinite) [addGroup : AddGroup ↑toProfinite.toTop]
  [topologicalAddGroup : IsTopologicalAddGroup ↑toProfinite.toTop],
  sizeOf { toProfinite := toProfinite, addGroup := addGroup, topologicalAddGroup := topologicalAddGroup } =
    1 + sizeOf toProfinite + sizeOf addGroup + sizeOf topologicalAddGroup
-- Mathlib.Analysis.Convex.Gauge
mul_gauge_le_norm : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {r : ℝ} {x : E},
  Metric.ball 0 r ⊆ s → r * gauge s x ≤ ‖x‖
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis_iff_maximal : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  autoParam (X ⊆ M.E) Matroid.isBasis_iff_maximal._auto_1 → (M.IsBasis I X ↔ Maximal (fun I => M.Indep I ∧ I ⊆ X) I)
-- Mathlib.Topology.Compactness.Lindelof
IsHereditarilyLindelof.isLindelof_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsHereditarilyLindelof s → t ⊆ s → IsLindelof t
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
equals the product of their L-series, assuming both L-series converge.  -/
ArithmeticFunction.LSeriesHasSum_mul : ∀ {f g : ArithmeticFunction ℂ} {s a b : ℂ},
  LSeriesHasSum (fun n => f n) s a → LSeriesHasSum (fun n => g n) s b → LSeriesHasSum (fun n => (f * g) n) s (a * b)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.ColimitCocone.mk.sizeOf_spec : ∀ {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 : SizeOf J] [inst_3 : SizeOf C] (cocone : CategoryTheory.Limits.Cocone F)
  (isColimit : CategoryTheory.Limits.IsColimit cocone),
  sizeOf { cocone := cocone, isColimit := isColimit } = 1 + sizeOf cocone + sizeOf isColimit
-- Mathlib.Topology.Algebra.Valued.NormedValued
NormedField.valuation.congr_simp : ∀ {K : Type u_1} [hK : NormedField K] [inst : IsUltrametricDist K], NormedField.valuation = NormedField.valuation
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {I₁ I₂ : S.Arrow} {x y : I₁.Relation I₂}, x.Z = y.Z → x.g₁ ≍ y.g₁ → x.g₂ ≍ y.g₂ → x = y
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.differentiableAt_iteratedDeriv_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), DifferentiableAt ℝ (iteratedDeriv n (ProbabilityTheory.mgf X μ)) v
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- This is a slightly more convenient method to verify that a cofork is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.Cofork.IsColimit.mk : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        (t : CategoryTheory.Limits.Cofork f g) →
          (desc : (s : CategoryTheory.Limits.Cofork f g) → t.pt ⟶ s.pt) →
            (∀ (s : CategoryTheory.Limits.Cofork f g), CategoryTheory.CategoryStruct.comp t.π (desc s) = s.π) →
              (∀ (s : CategoryTheory.Limits.Cofork f g) (m : t.pt ⟶ s.pt),
                  CategoryTheory.CategoryStruct.comp t.π m = s.π → m = desc s) →
                CategoryTheory.Limits.IsColimit t
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpointType.partialFixpoint.sizeOf_spec : sizeOf Lean.Elab.PartialFixpointType.partialFixpoint = 1
-- Mathlib.Order.Interval.Set.Image
_private.Mathlib.Order.Interval.Set.Image.0.Set.image_subtype_val_Ixx_Ixi : ∀ {α : Type u_1} {p q r : α → α → Prop} {a b : α} (c : { x // p a x ∧ q x b }),
  (∀ {x : α}, r (↑c) x → p a x) → Subtype.val '' {y | r ↑c ↑y} = {y | r (↑c) y ∧ q y b}
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Alt.mk.inj : ∀ {ref : Lean.Syntax} {idx : ℕ} {rhs : Lean.Expr} {fvarDecls : List Lean.LocalDecl}
  {patterns : List Lean.Meta.Match.Pattern} {cnstrs : List (Lean.Expr × Lean.Expr)} {notAltIdxs : Array ℕ}
  {ref_1 : Lean.Syntax} {idx_1 : ℕ} {rhs_1 : Lean.Expr} {fvarDecls_1 : List Lean.LocalDecl}
  {patterns_1 : List Lean.Meta.Match.Pattern} {cnstrs_1 : List (Lean.Expr × Lean.Expr)} {notAltIdxs_1 : Array ℕ},
  { ref := ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := patterns, cnstrs := cnstrs,
        notAltIdxs := notAltIdxs } =
      { ref := ref_1, idx := idx_1, rhs := rhs_1, fvarDecls := fvarDecls_1, patterns := patterns_1, cnstrs := cnstrs_1,
        notAltIdxs := notAltIdxs_1 } →
    ref = ref_1 ∧
      idx = idx_1 ∧
        rhs = rhs_1 ∧ fvarDecls = fvarDecls_1 ∧ patterns = patterns_1 ∧ cnstrs = cnstrs_1 ∧ notAltIdxs = notAltIdxs_1
-- Mathlib.Data.Option.Basic
Option.coe_get : ∀ {α : Type u_1} {o : Option α} (h : o.isSome = true), some (o.get h) = o
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRco : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Rco α)
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.toLinearEquiv_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g : LinearMap.GeneralLinearGroup R M), (f * g).toLinearEquiv = f.toLinearEquiv * g.toLinearEquiv
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- The functor `G : C ⥤ D` exhibits `(C, J)` as a dense subsite of `(D, K)`
if `G` is cover-dense, locally fully-faithful,
and `S` is a cover of `C` if and only if the image of `S` in `D` is a cover.  -/
CategoryTheory.Functor.IsDenseSubsite : {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] →
        CategoryTheory.GrothendieckTopology C →
          CategoryTheory.GrothendieckTopology D → CategoryTheory.Functor C D → Prop
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- For `u : Opens M`, `x : u` is a boundary point iff `x.val : M` is.  -/
ModelWithCorners.isBoundaryPoint_iff_isBoundaryPoint_val : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {u : TopologicalSpace.Opens M} {x : ↥u},
  I.IsBoundaryPoint x ↔ I.IsBoundaryPoint ↑x
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofLE_toTransfiniteCompositionOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (h : W.TransfiniteCompositionOfShape J f) {W' : CategoryTheory.MorphismProperty C} (hW : W ≤ W'),
  (h.ofLE hW).toTransfiniteCompositionOfShape = h.toTransfiniteCompositionOfShape
-- Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
/-- If a function `f` locally integrable on an open subset `U` of a finite-dimensional real
vector space has zero integral when multiplied by any smooth function compactly supported
in `U`, then `f` vanishes almost everywhere in `U`.  -/
IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] [inst_6 : MeasurableSpace E]
  [BorelSpace E] {f : E → F} {μ : MeasureTheory.Measure E} {U : Set E},
  IsOpen U →
    MeasureTheory.LocallyIntegrableOn f U μ →
      (∀ (g : E → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : E), g x • f x ∂μ = 0) →
        ∀ᵐ (x : E) ∂μ, x ∈ U → f x = 0
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toLinearMap_injective : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂], Function.Injective PositiveLinearMap.toLinearMap
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.containsThenInsert : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Data.Multiset.Count
/-- `count a s` is the multiplicity of `a` in `s`.  -/
Multiset.count : {α : Type u_1} → [DecidableEq α] → α → Multiset α → ℕ