mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_addX : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P Q : Fin 3 → A), (W'.baseChange B).addX (⇑f ∘ P) (⇑f ∘ Q) = f ((W'.baseChange A).addX P Q)
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.lin_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)) (l : β) (k : α) (r : K →+* ℂ),
  a k l * (NumberField.house.newBasis✝ K) r =
    ∑ u, ↑(NumberField.house.a'✝ K a k l r u) * (NumberField.house.newBasis✝ K) u
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabInfo.mk : Lean.Elab.ElabInfo → Lean.Name → Lean.Elab.DocElabKind → Lean.Elab.DocElabInfo
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.toSetoid_top : ∀ {M : Type u_1} [inst : Add M], ⊤.toSetoid = ⊤
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Z : C}
  (h : AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K
        (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (A.pull θ)) h)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo_le : ∀ {n : ℕ} (c : Composition n) (i : ℕ), c.sizeUpTo i ≤ n
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.PublishDiagnosticsParams.uri : Lean.Lsp.PublishDiagnosticsParams → Lean.Lsp.DocumentUri
-- Mathlib.Topology.Algebra.Order.Group
LinearOrderedCommGroup.toIsTopologicalGroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G], IsTopologicalGroup G
-- Lean.Data.KVMap
Lean.DataValue.ofNat : ℕ → Lean.DataValue
-- Mathlib.RepresentationTheory.Coinduced
/-- Given a monoid homomorphism `φ : G →* H`, the coinduction functor `Rep k G ⥤ Rep k H` is right
adjoint to the restriction functor along `φ`.  -/
Rep.resCoindAdjunction : (k : Type u) →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] → [inst_2 : Monoid H] → (φ : G →* H) → Rep.resFunctor φ ⊣ Rep.coindFunctor k φ
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.comapDomain_zero : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f),
  MonoidAlgebra.comapDomain f hf 0 = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 → (W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2))
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.combine_Nonneg : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly), p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.combine p₂).NonnegCoeffs
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.prodFun_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (p : F × G) in nhds (φ.prodFun φ.pt), φ.prodFun (φ.implicitFunction p.1 p.2) = p
-- Mathlib.Order.Antichain
Set.Subsingleton.isStrongAntichain : ∀ {α : Type u_1} {s : Set α}, s.Subsingleton → ∀ (r : α → α → Prop), IsStrongAntichain r s
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a monoid, if it admits a surjective map that preserves `1`
and `*` to a monoid. See note [reducible non-instances].  -/
Function.Surjective.monoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : One M₂] →
        [inst_2 : Pow M₂ ℕ] →
          [inst_3 : Monoid M₁] →
            (f : M₁ → M₂) →
              Function.Surjective f →
                f 1 = 1 → (∀ (x y : M₁), f (x * y) = f x * f y) → (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → Monoid M₂
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.fin_two_induction : ∀ {R : Type v} [inst : CommRing R] (P : Matrix.SpecialLinearGroup (Fin 2) R → Prop),
  (∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩) → ∀ (g : Matrix.SpecialLinearGroup (Fin 2) R), P g
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.cancel_iso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ≅ Y) (g g' : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.comp f.hom g' ↔ g = g'
-- Mathlib.Analysis.Real.Hyperreal
instInhabitedHyperreal : Inhabited ℝ*
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- Given an embedding, there is an induced embedding of colorings.  -/
SimpleGraph.recolorOfEmbedding : {V : Type u} → (G : SimpleGraph V) → {α : Type u_4} → {β : Type u_5} → (α ↪ β) → G.Coloring α ↪ G.Coloring β
-- Mathlib.Order.Bounds.Basic
/-- **Alias** of `IsCoinitialFor.of_subset`. -/
HasSubset.Subset.iscoinitialfor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsCoinitialFor s t
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapAux.mapMap_D₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
      (L.D₁ c₁₂ i₁₂ i₁₂') =
    CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂')
      (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
-- Mathlib.Probability.Distributions.Beta
/-- The normalizing constant in the beta distribution.  -/
ProbabilityTheory.beta : ℝ → ℝ → ℝ
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_coe_atBot : Filter.Tendsto Real.toEReal Filter.atBot (nhds ⊥)
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.symm_toProd : ∀ {V : Type u_1} {G : SimpleGraph V} (d : G.Dart), d.symm.toProd = d.swap
-- Mathlib.RingTheory.Ideal.Operations
Ideal.primeCompl_le_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] (P : Ideal R) [inst_2 : P.IsPrime],
  P.primeCompl ≤ nonZeroDivisors R
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.of_isEmpty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [IsEmpty ι] (v : ι → E), Orthonormal 𝕜 v
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.eval_neg : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) (f : σ → R),
  (MvPolynomial.eval f) (-p) = -(MvPolynomial.eval f) p
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLTι_app : ∀ {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) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ (X : C), t.IsLE X n₀ ↔ CategoryTheory.IsIso ((t.truncLTι n₁).app X)
-- Lean.Compiler.InitAttr
Lean.registerInitAttr : Lean.Name → Bool → autoParam Lean.Name Lean.registerInitAttr._auto_1 → IO (Lean.ParametricAttribute Lean.Name)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k a : α} {h' : a ∈ t.erase k}, (t.erase k)[a] = t[a]
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcomp₁_obj_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)),
  ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).right = X.right
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_strictMono : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1],
  StrictMono fun x => ↑x
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.neg_zsmul : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (i : ℤ) (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.zsmul (-i) a = Lean.Grind.Ring.OfSemiring.neg (Lean.Grind.Ring.OfSemiring.zsmul i a)
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.instDecidableEqStained : DecidableEq Mathlib.Linter.Flexible.Stained✝
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Vertical composition of strong natural transformations.  -/
CategoryTheory.Lax.StrongTrans.vComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          CategoryTheory.Lax.StrongTrans F G → CategoryTheory.Lax.StrongTrans G H → CategoryTheory.Lax.StrongTrans F H
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The weighted order with respect to `w : σ → ℕ`. This is the minimum value
of `weight w d` over all exponents `d` with nonzero coefficient `coeff d f`.  -/
MvPowerSeries.weightedOrder : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → (σ → ℕ) → MvPowerSeries σ R → ℕ∞
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_toDFinsupp : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : Π₀ (x : ι), M), f.toFinsupp.toDFinsupp = f
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.toArray_eq_fold : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.toArray = Std.IterM.fold (fun xs out => xs.push out) #[] it
-- Mathlib.Algebra.Algebra.Unitization
/-- **Alias** of the reverse direction of `Unitization.isStarProjection_inr_iff`. -/
IsStarProjection.inr : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] {p : A}, IsStarProjection p → IsStarProjection ↑p
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.comp : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂}, g.IsInvertible → f.IsInvertible → (g ∘SL f).IsInvertible
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.map_inv₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : Group M} {x_1 : MulOneClass N} {x_2 : CommGroup P} (f : M →* N →* P)
  (m : M) (n : N), (f m⁻¹) n = ((f m) n)⁻¹
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrict'_comp : ∀ (A : Type u_1) {K : Type u_2} {L : Type u_3} {L₂ : Type u_4} {L₃ : Type u_5} (B : Type u_6) (B₂ : Type u_7)
  (B₃ : Type u_8) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : CommRing B₃]
  [inst_4 : Algebra A B] [inst_5 : Algebra A B₂] [inst_6 : Algebra A B₃] [inst_7 : Field K] [inst_8 : Field L]
  [inst_9 : Field L₂] [inst_10 : Field L₃] [inst_11 : Algebra A K] [inst_12 : Algebra K L] [inst_13 : Algebra A L]
  [inst_14 : IsScalarTower A K L] [inst_15 : Algebra K L₂] [inst_16 : Algebra A L₂] [inst_17 : IsScalarTower A K L₂]
  [inst_18 : Algebra K L₃] [inst_19 : Algebra A L₃] [inst_20 : IsScalarTower A K L₃] [inst_21 : Algebra B L]
  [inst_22 : IsScalarTower A B L] [inst_23 : IsIntegralClosure B A L] [inst_24 : Algebra B₂ L₂]
  [inst_25 : IsScalarTower A B₂ L₂] [inst_26 : IsIntegralClosure B₂ A L₂] [inst_27 : Algebra B₃ L₃]
  [inst_28 : IsScalarTower A B₃ L₃] [inst_29 : IsIntegralClosure B₃ A L₃] (σ : L →ₐ[K] L₂) (σ' : L₂ →ₐ[K] L₃),
  galRestrict' A B B₃ (σ'.comp σ) = (galRestrict' A B₂ B₃ σ').comp (galRestrict' A B B₂ σ)
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for completely multiplicative functions.

If `f : ℕ →*₀ F`, where `F` is a complete normed field and `‖f ·‖` is summable, then
`∏' p : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n`.
This version is stated in terms of `HasProd`.  -/
EulerProduct.eulerProduct_completely_multiplicative_hasProd : ∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →*₀ F},
  (Summable fun x => ‖f x‖) → HasProd (fun p => (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measurePreserving_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (g : G), MeasureTheory.MeasurePreserving (fun x => x * g) μ μ
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_mul_right_image : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, ⋃ a ∈ t, (fun x => x * a) '' s = s * t
-- Mathlib.Data.Setoid.Partition
/-- This lemma is analogous to `Quotient.mk_out'`.  -/
IndexedPartition.out_proj : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α),
  hs.out (hs.proj x) = hs.some (hs.index x)
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- A category `C` has the `w`-IPC property for shape `ι` if `w`-sized filtered colimits commute
with products of shape `ι`.  -/
CategoryTheory.Limits.IsIPCOfShape : (ι : Type u_3) →
  (C : Type u_4) → [inst : CategoryTheory.Category.{v_2, u_4} C] → [CategoryTheory.Limits.HasProductsOfShape ι C] → Prop
-- Mathlib.Topology.Algebra.Field
/-- The (topological-space) closure of a subfield of a topological field is
itself a subfield.  -/
Subfield.topologicalClosure : {α : Type u_2} →
  [inst : Field α] → [inst_1 : TopologicalSpace α] → [IsTopologicalDivisionRing α] → Subfield α → Subfield α
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A helper lemma that is essentially the same as `RelCWComplex.iUnion_openCell_eq_skeletonLT`.
Use that lemma instead.  -/
_private.Mathlib.Topology.CWComplex.Classical.Basic.0.Topology.RelCWComplex.iUnion_openCell_eq_iUnion_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ∞),
  D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.openCell m j =
    D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.closedCell m j
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.MatcherKey.mk.inj : ∀ {value : Lean.Expr} {compile isPrivate : Bool} {value_1 : Lean.Expr} {compile_1 isPrivate_1 : Bool},
  { value := value, compile := compile, isPrivate := isPrivate } =
      { value := value_1, compile := compile_1, isPrivate := isPrivate_1 } →
    value = value_1 ∧ compile = compile_1 ∧ isPrivate = isPrivate_1
-- Mathlib.Topology.Algebra.Group.Basic
/-- On an additive topological group, `𝓝 : G → Filter G` can be promoted to an `AddHom`.  -/
nhdsAddHom : {G : Type w} → [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → G →ₙ+ Filter G
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageActionItem.mk.sizeOf_spec : ∀ (title : String), sizeOf { title := title } = 1 + sizeOf title
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.nsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {L : SummationFilter β} [ContinuousAdd α], HasSum f a L → ∀ (n : ℕ), HasSum (fun x => n • f x) (n • a) L
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The upper shadow is monotone.  -/
Finset.upShadow_monotone : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Monotone Finset.upShadow
-- Init.Data.List.Basic
/-- Auxiliary for `countP`: `countP.go p l acc = countP p l + acc`.  -/
List.countP.go : {α : Type u} → (α → Bool) → List α → ℕ → ℕ
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coeAddMonoidHom_apply : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] (self : { x // 0 ≤ x }),
  Nonneg.coeAddMonoidHom self = ↑self
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors'.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a a_1 : α),
  a = a_1 → Associates.factors' a = Associates.factors' a_1
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_pair_eq_toReal : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {x y : α}, {x, y}.infsep = (edist x y).toReal
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The monoidal product is the categorical product.  -/
CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.CartesianMonoidalCategory C] →
      (X Y : C) →
        CategoryTheory.Limits.IsLimit
          (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
            (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.comp_preservesFilteredColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)
-- Std.Sync.SharedMutex
Std.SharedMutex.mutex : {α : Type} → Std.SharedMutex α → Std.BaseSharedMutex
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- An alternative constructor for `Hom`,
taking a morphism without a `[IsAddModHom]` instance, as well as the relevant
equality to put such an instance.  -/
CategoryTheory.AddMod.Hom.mk' : {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.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.AddMonObj A] →
                {M N : CategoryTheory.AddMod D A} →
                  (f : M.X ⟶ N.X) →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd f =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
                            CategoryTheory.AddModObj.vadd)
                        CategoryTheory.AddMod.Hom.mk'._auto_1 →
                      M.Hom N
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
/-- If `K` generates `J`, then any presheaf is a sheaf if and only if it is a sheaf
for all `K`-covers.  -/
CategoryTheory.Precoverage.Generates.isSheaf_type_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C},
  K.Generates J →
    ∀ {F : CategoryTheory.Functor Cᵒᵖ (Type w)},
      CategoryTheory.Presieve.IsSheaf J F ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The objects for the co-Kleisli category of the comonad `U : Comonad C`, which are the same
thing as objects of the base category `C`.
 -/
CategoryTheory.Cokleisli : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Comonad C → Type u
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_biUnion₀ : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β} {f : β → Set α},
  s.Countable →
    s.Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) f) →
      (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)
-- Std.Time.DateTime.PlainDateTime
Std.Time.instDecidableEqPlainDateTime : DecidableEq Std.Time.PlainDateTime
-- Mathlib.LinearAlgebra.Dimension.Constructions
finrank_span_le_card : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  (s : Set M) [inst_4 : Fintype ↑s], Module.finrank R ↥(Submodule.span R s) ≤ s.toFinset.card
-- Init.Data.SInt.Lemmas
Int32.toInt8_ofIntTruncate : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n < 2 ^ 31 → (Int32.ofIntClamp n).toInt8 = Int8.ofInt n
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult.mk.sizeOf_spec : ∀ (matcher : Lean.Expr) (counterExamples : Array Lean.Meta.Match.CounterExample) (unusedAltIdxs : List ℕ)
  (addMatcher : Lean.MetaM Unit),
  sizeOf
      { matcher := matcher, counterExamples := counterExamples, unusedAltIdxs := unusedAltIdxs,
        addMatcher := addMatcher } =
    1 + sizeOf matcher + sizeOf counterExamples + sizeOf unusedAltIdxs
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
/-- An upper bound for the summand when `0 ≤ a`.  -/
HurwitzKernelBounds.g_nat : ℕ → ℝ → ℝ → ℕ → ℝ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' fallback : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.getKeyD k' fallback =
    if compare k k' = Ordering.eq then
      if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then k else fallback
    else t.getKeyD k' fallback
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_iff_nsmul : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M}, a ≡ b [PMOD p] ↔ ∃ m n, m • p + a = n • p + b
-- Mathlib.Data.ZMod.QuotientRing
ZMod.prodEquivPi_apply : ∀ {ι : Type u_3} [inst : Fintype ι] (a : ι → ℕ) (coprime : Pairwise (Function.onFun Nat.Coprime a))
  (b : ZMod (∏ i, a i)) (i : ι), (ZMod.prodEquivPi a coprime) b i = (ZMod.castHom ⋯ (ZMod (a i))) b