mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_mul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (f₁ f₂ : M →ₗ[A] M)
  (g₁ g₂ : N →ₗ[R] N),
  TensorProduct.AlgebraTensorModule.map (f₁ * f₂) (g₁ * g₂) =
    TensorProduct.AlgebraTensorModule.map f₁ g₁ * TensorProduct.AlgebraTensorModule.map f₂ g₂
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ioi_add_Ici_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [AddLeftStrictMono α]
  [AddRightStrictMono α] [inst_5 : LocallyFiniteOrderTop α] (a b : α), Finset.Ioi a + Finset.Ici b ⊆ Finset.Ioi (a + b)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.mem_support_iff_exists_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v},
  p.IsPath → (w ∈ p.support ↔ ∃ q r, q.IsPath ∧ r.IsPath ∧ p = q.append r)
-- Mathlib.Order.Hom.Bounded
TopHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β] {f g : TopHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousWithinAt.upperSemicontinuousWithinAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ},
  ContinuousWithinAt f s x → UpperSemicontinuousWithinAt f s x
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatTrans_comp_assoc : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF'' LF' LF : CategoryTheory.Functor D H) {F F' F'' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α'' : L.comp LF'' ⟶ F'') (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] [inst_4 : LF.IsLeftDerivedFunctor α W] [inst_5 : LF'.IsLeftDerivedFunctor α' W]
  (τ' : F'' ⟶ F') (τ : F' ⟶ F) {Z : CategoryTheory.Functor D H} (h : LF ⟶ Z),
  CategoryTheory.CategoryStruct.comp (LF''.leftDerivedNatTrans LF' α'' α' W τ')
      (CategoryTheory.CategoryStruct.comp (LF'.leftDerivedNatTrans LF α' α W τ) h) =
    CategoryTheory.CategoryStruct.comp (LF''.leftDerivedNatTrans LF α'' α W (CategoryTheory.CategoryStruct.comp τ' τ)) h
-- Mathlib.MeasureTheory.Group.Prod
/-- A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A].
Note that if `f` is the characteristic function of a measurable set `t` this states that
`μ t = c * μ s` for a constant `c` that does not depend on `μ`.

Note: There is a gap in the last step of the proof in [Halmos].
In the last line, the equality `g(x⁻¹)ν(sx⁻¹) = f(x)` holds if we can prove that
`0 < ν(sx⁻¹) < ∞`. The first inequality follows from §59, Th. D, but the second inequality is
not justified. We prove this inequality for almost all `x` in
`MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero`.  -/
MeasureTheory.measure_lintegral_div_measure : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant],
  MeasurableSet s →
    ν' s ≠ 0 →
      ν' s ≠ ⊤ →
        ∀ (f : G → ENNReal),
          Measurable f → μ' s * ∫⁻ (y : G), f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (x : G), f x ∂μ'
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}
  {x_2 : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x_3 : α), (hnp.comp hmn) x_3 = hnp (hmn x_3)
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP_cons : ∀ {α : Type u_1} {p : α → Bool} (x : α) (xs : List α),
  List.splitOnP p (x :: xs) =
    if p x = true then [] :: List.splitOnP p xs else List.modifyHead (List.cons x) (List.splitOnP p xs)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal : ∀ {X : AlgebraicGeometry.Scheme}, StrictMono AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Mathlib.Probability.Process.LocalProperty
/-- A stochastic process `X` is said to satisfy a property `p` locally with respect to a
filtration `𝓕` if there exists a localizing sequence `(τ_n)` such that for all `n`, the stopped
process `fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)` satisfies `p`.  -/
ProbabilityTheory.Locally : {ι : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        [inst : LinearOrder ι] →
          [OrderBot ι] →
            [inst_2 : TopologicalSpace ι] →
              [OrderTopology ι] →
                [Zero E] →
                  ((ι → Ω → E) → Prop) →
                    MeasureTheory.Filtration ι mΩ →
                      (ι → Ω → E) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.Locally._auto_1 → Prop
-- Init.Data.Array.Basic
Array.repr : {α : Type u} → [Repr α] → Array α → Std.Format
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.mk : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      {M : Type u_4} →
        {N : Type u_5} →
          [inst : CommRing S] →
            [inst_1 : LinearOrder S] →
              [inst_2 : CommRing R] →
                [inst_3 : Algebra S R] →
                  [inst_4 : AddCommGroup M] →
                    [inst_5 : Module R M] →
                      [inst_6 : AddCommGroup N] →
                        [inst_7 : Module R N] →
                          {P : RootPairing ι R M N} →
                            [inst_8 : P.IsValuedIn S] →
                              (form : LinearMap.BilinForm R M) →
                                LinearMap.IsSymm form →
                                  (∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i)) →
                                    (∀ (i j : ι), ∃ s, (algebraMap S R) s = (form (P.root i)) (P.root j)) →
                                      (∀ (i : ι), ∃ s > 0, (algebraMap S R) s = (form (P.root i)) (P.root i)) →
                                        RootPairing.RootPositiveForm S P
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.tensorUnit_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- Rescaling a set by a factor `r` multiplies its measure by `abs (r ^ dim)`.  -/
MeasureTheory.Measure.addHaar_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (r : ℝ) (s : Set E),
  μ (r • s) = ENNReal.ofReal |r ^ Module.finrank ℝ E| * μ s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} {he : t ≠ ∅},
  (cmp (t.max he) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.hom_id : ∀ {M : AddMonCat}, AddMonCat.Hom.hom (CategoryTheory.CategoryStruct.id M) = AddMonoidHom.id ↑M
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
PartOrdEmb.Limits.CoconePt.isCardinalFiltered_pt : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : Type u} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsCardinalFiltered J κ] {F : CategoryTheory.Functor J PartOrdEmb}
  {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))}
  (hc : CategoryTheory.Limits.IsColimit c),
  (∀ (j : J), CategoryTheory.IsCardinalFiltered (↑(F.obj j)) κ) →
    CategoryTheory.IsCardinalFiltered (PartOrdEmb.Limits.CoconePt hc) κ
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Given two functors into a codiscrete category, the trivial natural transformation is a
natural isomorphism.  -/
CategoryTheory.Codiscrete.natIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} → {F G : CategoryTheory.Functor C (CategoryTheory.Codiscrete A)} → F ≅ G
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- **Alias** of the forward direction of `QuasispectrumRestricts.mul_comm_iff`. -/
QuasispectrumRestricts.mul_comm : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] [IsScalarTower S A A] [SMulCommClass S A A]
  {f : S → R} {a b : A}, QuasispectrumRestricts (a * b) f → QuasispectrumRestricts (b * a) f
-- Mathlib.Algebra.Opposites
/-- Auxiliary type to implement `MulOpposite` and `AddOpposite`.

It turns out to be convenient to have `MulOpposite α = AddOpposite α` true by definition, in the
same way that it is convenient to have `Additive α = α`; this means that we also get the defeq
`AddOpposite (Additive α) = MulOpposite α`, which is convenient when working with quotients.

This is a compromise between making `MulOpposite α = AddOpposite α = α` (what we had in Lean 3) and
having no defeqs within those three types (which we had as of https://github.com/leanprover-community/mathlib4/pull/1036).  -/
PreOpposite : Type u_3 → Type u_3
-- Mathlib.Topology.ClusterPt
MapClusterPt.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι) (u : ι → X),
  MapClusterPt x F u = ClusterPt x (Filter.map u F)
-- Init.Data.String.Subslice
/-- Given a subslice of `s` and a proof that `s.copy = t.copy`, obtain the corresponding
subslice of `t`.
 -/
String.Slice.Subslice.cast : {s t : String.Slice} → s.copy = t.copy → s.Subslice → t.Subslice
-- Mathlib.Order.Preorder.Chain
IsChain.image_embedding_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : LE α] [inst_1 : LE β] {φ : α ↪o β},
  IsChain (fun x1 x2 => x1 ≤ x2) (⇑φ '' s) ↔ IsChain (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.fderivWithin_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [inst_1 : CommSemiring R]
  [inst_2 : Algebra R 𝕜] (q : Polynomial R),
  UniqueDiffWithinAt 𝕜 s x →
    fderivWithin 𝕜 (fun x => (Polynomial.aeval x) q) s x =
      ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_μ_δ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {C' : Type u₁'}
  [inst_4 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal]
  (G : CategoryTheory.Functor D C') (X Y : C) {Z : C'}
  (h : G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.LaxMonoidal.μ F X Y))
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)) h) =
    h
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.frobeniusAlgEquivOfAlgebraic_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Algebra.IsAlgebraic K L] (a : L), (FiniteField.frobeniusAlgEquivOfAlgebraic K L) a = a ^ Fintype.card K
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- A signed measure `s` is said to `HaveLebesgueDecomposition` with respect to a measure `μ`
if the positive part and the negative part of `s` both `HaveLebesgueDecomposition` with
respect to `μ`.  -/
MeasureTheory.SignedMeasure.HaveLebesgueDecomposition : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.SignedMeasure α → MeasureTheory.Measure α → Prop
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (f : ↥(α →₁ₛ[μ] G)),
  ‖f‖ =
    ∑ x ∈ (MeasureTheory.Lp.simpleFunc.toSimpleFunc f).range,
      μ.real (⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) ⁻¹' {x}) * ‖x‖
-- Mathlib.Algebra.GroupWithZero.Associated
eq_of_prime_pow_eq : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [IsCancelMulZero R] [Subsingleton Rˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ},
  Prime p₁ → Prime p₂ → 0 < k₁ → p₁ ^ k₁ = p₂ ^ k₂ → p₁ = p₂
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.one_le_prod_max_one_norm_roots : ∀ (p : Polynomial ℂ), 1 ≤ (Multiset.map (fun a => max 1 ‖a‖) p.roots).prod
-- Init.Data.Int.LemmasAux
Int.toNat_eq_zero : ∀ {n : ℤ}, n.toNat = 0 ↔ n ≤ 0
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.emptyIsInitial_to : AlgebraicGeometry.emptyIsInitial.to = AlgebraicGeometry.Scheme.emptyTo
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_pred_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioc b (Order.pred a) = Set.Ioo b a
-- Mathlib.Tactic.Linter.UpstreamableDecl
/-- If set to `true`, the `upstreamableDecl` linter will add warnings on definitions.

The linter does not place a warning on any declaration depending on a definition in the current file
(while it does place a warning on the definition itself), since we often create a new file for a
definition on purpose.
 -/
Mathlib.Linter.linter.upstreamableDecl.defs : Lean.Option Bool
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isRetrocompact_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} (s : ↑(X.presheaf.obj (Opposite.op ⊤))), IsRetrocompact ↑(X.basicOpen s)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁), (AffineEquiv.equivUnitsAffineMap.symm u).symm a = ↑u⁻¹ a
-- Mathlib.AlgebraicGeometry.Scheme
/-- Given a morphism of schemes `f : X ⟶ Y`, and open sets `U ⊆ Y`, `V ⊆ f ⁻¹' U`,
this is the induced map `Γ(Y, U) ⟶ Γ(X, V)`.

This is treated as a suffix in lemma names.  -/
AlgebraicGeometry.Scheme.Hom.appLE : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (U : Y.Opens) →
      (V : X.Opens) →
        V ≤ (TopologicalSpace.Opens.map f.base).obj U →
          (Y.presheaf.obj (Opposite.op U) ⟶ X.presheaf.obj (Opposite.op V))
-- Init.Data.SInt.Lemmas
ISize.ofIntTruncate_int16ToInt : ∀ (x : Int16), ISize.ofIntClamp x.toInt = x.toISize
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.of.injEq : ∀ (carrier : Type u_1) [str : GroupWithZero carrier] (carrier_1 : Type u_1) (str_1 : GroupWithZero carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.CategoryTheory.Enriched.HomCongr
CategoryTheory.Iso.eHomCongr_inv : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y X₁ Y₁ : C}
  (α : X ≅ X₁) (β : Y ≅ Y₁),
  (CategoryTheory.Iso.eHomCongr V α β).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V α.hom Y₁)
      (CategoryTheory.eHomWhiskerLeft V X β.inv)
-- Mathlib.MeasureTheory.Function.Holder
/-- The natural pairing between `Lp E p μ` and `Lp F q μ` (for Hölder conjugate `p q : ℝ≥0∞`) with
values in a space `G` induced by a bilinear map `B : E →L[𝕜] F →L[𝕜] G`.

This is given by `∫ x, B (f x) (g x) ∂μ`.

In the special case when `B := (NormedSpace.inclusionInDoubleDual 𝕜 E).flip`, which is
definitionally the same as `B := ContinuousLinearMap.id 𝕜 (E →L[𝕜] 𝕜)`, this is the
natural map `Lp (StrongDual 𝕜 E) p μ →L[𝕜] StrongDual 𝕜 (Lp E q μ)`.  -/
ContinuousLinearMap.lpPairing : {α : Type u_1} →
  {𝕜 : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        {G : Type u_5} →
          {m : MeasurableSpace α} →
            (μ : MeasureTheory.Measure α) →
              (p q : ENNReal) →
                [inst : NontriviallyNormedField 𝕜] →
                  [inst_1 : NormedAddCommGroup E] →
                    [inst_2 : NormedAddCommGroup F] →
                      [inst_3 : NormedAddCommGroup G] →
                        [inst_4 : NormedSpace 𝕜 E] →
                          [inst_5 : NormedSpace 𝕜 F] →
                            [inst_6 : NormedSpace 𝕜 G] →
                              [inst_7 : Fact (1 ≤ p)] →
                                [inst_8 : Fact (1 ≤ q)] →
                                  [p.HolderConjugate q] →
                                    [inst_10 : NormedSpace ℝ G] →
                                      [SMulCommClass ℝ 𝕜 G] →
                                        [CompleteSpace G] →
                                          (E →L[𝕜] F →L[𝕜] G) →
                                            ↥(MeasureTheory.Lp E p μ) →L[𝕜] ↥(MeasureTheory.Lp F q μ) →L[𝕜] G
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.StableUnderInverse.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  P.StableUnderInverse → P.op.StableUnderInverse
-- Init.Data.UInt.Lemmas
UInt64.toFin_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toFin = OfNat.ofNat n
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- If each `R i` is weakly locally compact, each `A i` is open, and all but finitely many `A i`s
are also compact, then the restricted product `Πʳ i, [R i, A i]` is weakly locally compact.  -/
RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ [∀ (i : ι), WeaklyLocallyCompactSpace (R i)],
      (∀ᶠ (i : ι) in Filter.cofinite, IsCompact (A i)) →
        WeaklyLocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => A i) Filter.cofinite)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωSup_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (a : α),
  (OmegaCompletePartialOrder.ContinuousHom.ωSup c) a =
    OmegaCompletePartialOrder.ωSup ((c.map OmegaCompletePartialOrder.ContinuousHom.toMono).map (OrderHom.apply a))
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_two_of_utf8Size_eq_three : ∀ {c : Char} (h : c.utf8Size = 3), (String.utf8EncodeChar c)[2].toBitVec = 2#2 ++ BitVec.extractLsb' 0 6 c.val.toBitVec
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasFDerivAt_list_prod_finRange' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝔸 : Type u_6} [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {n : ℕ} {x : Fin n → 𝔸},
  HasFDerivAt (fun x => (List.map x (List.finRange n)).prod)
    (∑ i,
      (List.map x (List.take (↑i) (List.finRange n))).prod •
        MulOpposite.op (List.map x (List.drop (↑i).succ (List.finRange n))).prod • ContinuousLinearMap.proj i)
    x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.run : {α : Type} → ℕ → Lean.Meta.Grind.Arith.CommRing.RingM α → Lean.Meta.Grind.GoalM α
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instHasZeroMorphisms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.AddGrp C)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_base : ∀ {R S : CommRingCat} (f : R ⟶ S),
  (AlgebraicGeometry.Spec.map f).base =
    TopCat.ofHom { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.topCharacteristic : ∀ {G : Type u_1} [inst : Group G], ⊤.Characteristic
-- Mathlib.Topology.UniformSpace.Cauchy
/-- An auxiliary sequence of sets approximating a Cauchy filter.  -/
SequentiallyComplete.setSeqAux : {α : Type u} →
  [uniformSpace : UniformSpace α] →
    {f : Filter α} →
      Cauchy f → {U : ℕ → SetRel α α} → (∀ (n : ℕ), U n ∈ uniformity α) → (n : ℕ) → { s // s ∈ f ∧ s ×ˢ s ⊆ U n }
-- Mathlib.RingTheory.SimpleModule.Basic
isSemisimpleModule_iff_exists_linearEquiv_dfinsupp : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsSemisimpleModule R M ↔ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mapOfLE_comp_valuation : ∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S), ⇑(R.mapOfLE S h) ∘ ⇑R.valuation = ⇑S.valuation
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.mk.inj : ∀ {α : Type u} {inst : Preorder α} {toOrderHom toOrderHom_1 : ℕ →o α},
  { toOrderHom := toOrderHom } = { toOrderHom := toOrderHom_1 } → toOrderHom = toOrderHom_1
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.one_le_op : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] {a : α}, 1 ≤ MulOpposite.op a ↔ 1 ≤ a
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.edist_le_edist_pi_of_edist_lt : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → EDist (F i)] {x y : (i : ι) → F i} {i : ι},
  edist x y < 2⁻¹ ^ Encodable.encode i → edist (x i) (y i) ≤ edist x y
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mem_toNonUnitalSubring : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] [inst_3 : Star A]
  {S : NonUnitalStarSubalgebra R A} {x : A}, x ∈ S.toNonUnitalSubring ↔ x ∈ S
-- Init.Data.Vector.Basic
Vector.mk.inj : ∀ {α : Type u} {n : ℕ} {toArray : Array α} {size_toArray : toArray.size = n} {toArray_1 : Array α}
  {size_toArray_1 : toArray_1.size = n},
  Vector.mk toArray size_toArray = Vector.mk toArray_1 size_toArray_1 → toArray = toArray_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α]
  {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.DTreeMap.ofList l cmp).getKey! k' = k
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_add : ∀ {V W : SemiNormedGrp} (f g : V ⟶ W), SemiNormedGrp.Hom.hom (f + g) = SemiNormedGrp.Hom.hom f + SemiNormedGrp.Hom.hom g
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange.congr_simp : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
  (f f_1 : (i : ι) → β₁ i → β₂ i) (e_f : f = f_1) (hf : ∀ (i : ι), f i 0 = 0) (x x_1 : Π₀ (i : ι), β₁ i),
  x = x_1 → DFinsupp.mapRange f hf x = DFinsupp.mapRange f_1 ⋯ x_1
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_abs : ∀ (n : ℤ), |n|.negOnePow = n.negOnePow
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_filter_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] {f : α → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun k x => f k) t ⋯).impl.getKey! k = (Option.filter f (t.getKey? k)).get!
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : SubtractionCommMonoid α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (x - a)) c
-- Mathlib.Algebra.Ring.Idempotent
/-- `b - a` is idempotent when `a * b = a` and `b * a = a`.  -/
IsIdempotentElem.sub : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {a b : R},
  IsIdempotentElem a → IsIdempotentElem b → a * b = a → b * a = a → IsIdempotentElem (b - a)
-- Init.Data.List.MinMax
List.min_eq_get_min? : ∀ {α : Type u_1} [inst : Min α] (l : List α) (hl : l ≠ []), l.min hl = l.min?.get ⋯