mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
/-- Day's reflection theorem.

Let `D` be a symmetric monoidal closed category and let `C` be a reflective subcategory. Denote by
`R : C ⥤ D` the inclusion functor and by `L : D ⥤ C` the reflector. Let `u` denote the unit of the
adjunction `L ⊣ R`. Denote the internal hom by `[-,-]`. The following are equivalent:

1. `u : [d, Rc] ⟶ RL[d, Rc]` is an isomorphism,
2. `[u, 𝟙] : [RLd, Rc] ⟶ [d, Rc]` is an isomorphism,
3. `L(u ▷ d') : L(d ⊗ d') ⟶ L(RLd ⊗ d')` is an isomorphism,
4. `L(u ⊗ u) : L(d ⊗ d') ⟶ L(RLd ⊗ RLd')` is an isomorphism,

where `c, d, d'` are arbitrary objects of `C`/`D`, quantified over separately in each condition.
 -/
CategoryTheory.Monoidal.Reflective.isIso_tfae : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory D]
  [CategoryTheory.SymmetricCategory D] [inst_4 : CategoryTheory.MonoidalClosed D] {R : CategoryTheory.Functor C D}
  [R.Faithful] [R.Full] {L : CategoryTheory.Functor D C} (adj : L ⊣ R),
  [∀ (c : C) (d : D), CategoryTheory.IsIso (adj.unit.app (d ⟹ R.obj c)),
      ∀ (c : C) (d : D), CategoryTheory.IsIso ((CategoryTheory.MonoidalClosed.pre (adj.unit.app d)).app (R.obj c)),
      ∀ (d d' : D),
        CategoryTheory.IsIso (L.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight (adj.unit.app d) d')),
      ∀ (d d' : D),
        CategoryTheory.IsIso
          (L.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app d) (adj.unit.app d')))].TFAE
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVec_injective_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n] {M : Matrix m n R},
  Function.Injective M.mulVec ↔ LinearIndependent R M.col
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.ρ.eq_1 : UpperHalfPlane.ρ = { coe := { re := -1 / 2, im := √3 / 2 }, coe_im_pos := UpperHalfPlane.ρ._proof_1 }
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- Every `R`-linear map between two topological `R`-modules, where the source has the module
topology, is continuous.  -/
IsModuleTopology.continuous_of_distribMulActionHom : ∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Semiring R] {A : Type u_3} [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_4} [inst_4 : AddCommMonoid B]
  [inst_5 : Module R B] [aB : TopologicalSpace B] [ContinuousAdd B] [ContinuousSMul R B] (φ : A →+[R] B), Continuous ⇑φ
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.span_apply : ∀ {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι')
  (i : ↥s), ↑((OrthonormalBasis.span h s) i) = v' ↑i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.diff_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.diff t₂ = t₁ \ t₂
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoRightHomology.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hg : S.g = 0),
  S.opcyclesIsoRightHomology hg = S.opcyclesIsoRightHomology hg
-- Mathlib.GroupTheory.Generators
/-- The transport of a generating family along a surjective homomorphism.  -/
Group.Generators.map : {G : Type u_1} →
  {H : Type u_2} →
    {ι : Type u_3} →
      [inst : Group G] →
        [inst_1 : Group H] → Group.Generators G ι → (f : G →* H) → Function.Surjective ⇑f → Group.Generators H ι
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult.yes.sizeOf_spec : ∀ (expectedType : Lean.Expr), sizeOf (Lean.Elab.Term.UseImplicitLambdaResult.yes expectedType) = 1 + sizeOf expectedType
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.ι_eq_app_zero : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  (t : CategoryTheory.Limits.Trident f), t.ι = t.π.app CategoryTheory.Limits.WalkingParallelFamily.zero
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.«term__²» : Lean.TrailingParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.distinctKeys_cons_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys (⟨k, v⟩ :: l) ↔
    Std.Internal.List.DistinctKeys l ∧ Std.Internal.List.containsKey k l = false
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerRight_id' : ∀ {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] {G : CategoryTheory.Functor C D}
  (F : CategoryTheory.Functor D E),
  CategoryTheory.Functor.whiskerRight (CategoryTheory.CategoryStruct.id G) F =
    CategoryTheory.CategoryStruct.id (G.comp F)
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
/-- Define a continuous linear map between `E →SLₚₜ[σ] F` and `D →SLₚₜ[τ] G`.

Use `PointwiseConvergenceCLM.precomp` for the special case of the adjoint operator.  -/
PointwiseConvergenceCLM.mkCLM : {𝕜₁ : Type u_3} →
  {𝕜₂ : Type u_4} →
    {𝕜₃ : Type u_5} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₃ →+* 𝕜₂} →
                {D : Type u_6} →
                  {E : Type u_7} →
                    (F : Type u_8) →
                      (G : Type u_9) →
                        [inst_3 : AddCommGroup E] →
                          [inst_4 : TopologicalSpace E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : NormedAddCommGroup F] →
                                [inst_7 : NormedSpace 𝕜₂ F] →
                                  [inst_8 : AddCommGroup D] →
                                    [inst_9 : TopologicalSpace D] →
                                      [inst_10 : Module 𝕜₃ D] →
                                        [inst_11 : NormedAddCommGroup G] →
                                          [inst_12 : NormedSpace 𝕜₂ G] →
                                            (A : (E →SL[σ] F) →ₗ[𝕜₂] D →SL[τ] G) →
                                              (∀ (f : D),
                                                  ∃ s C,
                                                    ∀ (B : E →SL[σ] F), ∃ g, ∃ (_ : g ∈ s), ‖(A B) f‖ ≤ C • ‖B g‖) →
                                                (E →SLₚₜ[σ] F) →L[𝕜₂] D →SLₚₜ[τ] G
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
/-- An alternate constructor for `RootPairing.Base` which demands the axioms for roots but not for
coroots.  -/
RootPairing.Base.mk' : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [Finite ι] →
          [inst : AddCommGroup M] →
            [inst_1 : AddCommGroup N] →
              [inst_2 : Field R] →
                [CharZero R] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module R N] →
                      (P : RootPairing ι R M N) →
                        [P.IsRootSystem] →
                          [P.IsCrystallographic] →
                            [P.IsReduced] →
                              (s : Set ι) →
                                LinearIndepOn R (⇑P.root) s →
                                  (∀ (i : ι),
                                      P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨
                                        -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)) →
                                    P.Base
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isZero_of_isStrictlyLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n i : ℤ),
  autoParam (n < i) CochainComplex.isZero_of_isStrictlyLE._auto_1 →
    ∀ [K.IsStrictlyLE n], CategoryTheory.Limits.IsZero (K.X i)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.toMonoidWithZeroHom_coe_eq_coe : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  ⇑v.toMonoidWithZeroHom = ⇑v
-- Mathlib.Analysis.MellinTransform
mellinConvergent_of_isBigO_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ},
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    (f =O[Filter.atTop] fun x => x ^ (-a)) →
      s.re < a → (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → b < s.re → MellinConvergent f s
-- Mathlib.Analysis.Convex.Hull
/-- **Alias** of the reverse direction of `convexHull_eq_self`. -/
Convex.convexHull_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → (convexHull 𝕜) s = s
-- Mathlib.MeasureTheory.Group.Measure
/-- If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to
any open set.  -/
MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] (K : Set G),
  IsCompact K → μ K ≠ 0 → μ.IsOpenPosMeasure
-- Lean.Meta.HasNotBit
Lean.mkHasNotBit : Lean.Expr → Array ℕ → Lean.Expr
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.smul_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {R₁ : Type u_5} {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
  [inst_4 : DistribMulAction R₁ R] [inst_5 : SMulCommClass R₁ R R] (r : R₁) (x y : PiTensorProduct R fun i => s i),
  r • (x + y) = r • x + r • y
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.separatingLeft_iff_linear_nontrivial : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}, B.SeparatingLeft ↔ ∀ (x : M₁), B x = 0 → x = 0
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_iff_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, a ≡ b [PMOD p] ↔ ∃ m, m • p = b - a
-- Init.Data.UInt.Basic
instMaxUInt8 : Max UInt8
-- Init.Prelude
/-- The homogeneous version of `HShiftRight`: `a >>> b : α` where `a b : α`.  -/
ShiftRight : Type u → Type u
-- Mathlib.Combinatorics.Quiver.Basic
/-- Given an arrow in `Vᵒᵖ`, we can take the "unopposite" back in `V`.  -/
Quiver.Hom.unop : {V : Type u_1} → [inst : Quiver V] → {X Y : Vᵒᵖ} → (X ⟶ Y) → (Opposite.unop Y ⟶ Opposite.unop X)
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_sdiff_cancel' : ∀ {α : Type u_1} {s t u : Set α}, s ⊆ t → t ⊆ u → t ∪ u \ s = u
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- The valuation subring of a valued field is closed.  -/
Valued.isClosed_valuationSubring : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] (K : Type u) [inst_1 : Field K] [hv : Valued K Γ₀],
  IsClosed ↑Valued.v.valuationSubring
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_compact_support : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  HasCompactSupport ExistsContDiffBumpBase.u
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_of_not_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬b ≤ a → Set.uIoo a b = Set.Ioo a b
-- Mathlib.CategoryTheory.Bicategory.Product
/-- `sectR b C` is the strictly unitary pseudofunctor `C ⥤ B × C` given by `Y ↦ (b, Y)`.  -/
CategoryTheory.Bicategory.Prod.sectR : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    B → (C : Type u₂) → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.StrictlyUnitaryPseudofunctor C (B × C)
-- Mathlib.Data.List.Range
/-- The lengths of the members of `l.ranges` are those given by `l`  -/
List.ranges_length : ∀ (l : List ℕ), List.map List.length l.ranges = l
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a finsupp
`x : G × G →₀ A` satisfying the 2-boundary condition, produces a 2-boundary for the
representation on `A` induced by the `DistribMulAction`.  -/
groupHomology.boundariesOfIsBoundary₂ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              (x : G × G →₀ A) →
                groupHomology.IsBoundary₂ x → ↥(groupHomology.boundaries₂ (Rep.ofDistribMulAction k G A))
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- Given a discrete valuation `v`, `Valuation.IsRankOneDiscrete.generator` is an element of `Γ`
which is a generator of the value group that is `< 1`.  -/
Valuation.IsRankOneDiscrete.generator : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} → [inst_1 : Ring A] → (v : Valuation A Γ) → [v.IsRankOneDiscrete] → Γˣ
-- Std.Async.Signal
/-- Window size change.

Notes:
- SIGWINCH is raised whenever the runtime detects the console has been resized.
- Under console emulators, or on 32-bit apps on 64-bit systems, SIGWINCH is emulated.
- In these cases, signals may not be delivered timely.
 -/
Std.Async.Signal.sigwinch : Std.Async.Signal
-- Mathlib.Analysis.Calculus.FDeriv.Partial
/-- Suppose that along `l : Filter α` each of `v w : α → E` tends to `u : E` and that along
`l ×ˢ 𝓝[s] u` the derivative of `f : α → E → F` tends to `φ : E →L[𝕜] F`. Then the difference
between `f χ (v χ)` and `f χ (w χ)` is, to first order, `φ (v χ - w χ)`. This can be useful where
`χ : α` stands for a point (or a pair of points) in a space containing `E`, and `v χ` or `w χ` is
its projection (or both are projections).  -/
_private.Mathlib.Analysis.Calculus.FDeriv.Partial.0.isLittleO_sub_sub_fderiv : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] {u : E} {v w : α → E} {l : Filter α},
  Filter.Tendsto v l (nhds u) →
    Filter.Tendsto w l (nhds u) →
      ∀ (s : optParam (Set E) Set.univ),
        autoParam (∀ᶠ (χ : α) in l, segment ℝ (w χ) (v χ) ⊆ s) isLittleO_sub_sub_fderiv._auto_1✝ →
          ∀ {f : α → E → F} {f' : α → E → E →L[𝕜] F},
            (∀ᶠ (p : α × E) in l ×ˢ nhdsWithin u s, HasFDerivWithinAt (f p.1) (f' p.1 p.2) s p.2) →
              ∀ {φ : E →L[𝕜] F},
                Filter.Tendsto (↿f') (l ×ˢ nhdsWithin u s) (nhds φ) →
                  (fun χ => f χ (v χ) - f χ (w χ) - φ (v χ - w χ)) =o[l] fun χ => v χ - w χ
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- Construct a bundled continuous (semi)linear map from a map `f : E → F` and a proof of the fact
that it belongs to the closure of the image of a bounded set `s : Set (E →SL[σ₁₂] F)` under coercion
to function. Coercion to function of the result is definitionally equal to `f`.  -/
ContinuousLinearMap.ofMemClosureImageCoeBounded : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {F : Type u_4} →
      [inst : NormedAddCommGroup F] →
        [inst_1 : NontriviallyNormedField 𝕜] →
          [inst_2 : NontriviallyNormedField 𝕜₂] →
            [inst_3 : NormedSpace 𝕜₂ F] →
              {σ₁₂ : 𝕜 →+* 𝕜₂} →
                {E' : Type u_6} →
                  [inst_4 : SeminormedAddCommGroup E'] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      [inst_6 : RingHomIsometric σ₁₂] →
                        (f : E' → F) →
                          {s : Set (E' →SL[σ₁₂] F)} →
                            Bornology.IsBounded s → f ∈ closure (DFunLike.coe '' s) → E' →SL[σ₁₂] F
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoFinYonedaComponents_hom_apply : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : Profinite) [inst_1 : Finite ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop),
  (CategoryTheory.ConcreteCategory.hom (Condensed.isoFinYonedaComponents F X).hom) y x =
    (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op)) y
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {k : α} {v : β k}, Std.Internal.List.insertEntry k v [] = [⟨k, v⟩]
-- Mathlib.Computability.TuringMachine.Tape
Turing.instInhabitedDir : Inhabited Turing.Dir
-- Mathlib.Topology.Order
generateFrom_union : ∀ {α : Type u} (a₁ a₂ : Set (Set α)),
  TopologicalSpace.generateFrom (a₁ ∪ a₂) = TopologicalSpace.generateFrom a₁ ⊓ TopologicalSpace.generateFrom a₂
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
/-- `circleMap` is injective on `Ι a b` if the distance between `a` and `b` is at most `2π`.  -/
injOn_circleMap_of_abs_sub_le : ∀ {a b R : ℝ} {c : ℂ}, R ≠ 0 → |a - b| ≤ 2 * Real.pi → Set.InjOn (circleMap c R) (Set.uIoc a b)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.size.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.nil.size = 0
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inrHom_apply : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  (TrivSqZeroExt.inrHom R M) m = TrivSqZeroExt.inr m
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- Assume that each `R i` is a locally compact group with `A i` an open subgroup.
Assume also that all but finitely many `A i`s are compact.
Then the restricted product `Πʳ i, [R i, A i]` is a locally compact group.  -/
RestrictedProduct.locallyCompactSpace_of_group : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))]
  [inst_2 : (i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalGroup (R i)]
  [∀ (i : ι), LocallyCompactSpace (R i)],
  (∀ᶠ (i : ι) in Filter.cofinite, IsCompact ↑(B i)) →
    LocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- The integral of `sin x * cos x`, given in terms of sin².
See `integral_sin_mul_cos₂` below for the integral given in terms of cos².  -/
integral_sin_mul_cos₁ : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.sin x * Real.cos x = (Real.sin b ^ 2 - Real.sin a ^ 2) / 2
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaAssoc.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (γ : (a : α) → β a → Type u_3),
  Equiv.sigmaAssoc γ =
    { toFun := fun x => ⟨x.fst.fst, ⟨x.fst.snd, x.snd⟩⟩, invFun := fun x => ⟨⟨x.fst, x.snd.fst⟩, x.snd.snd⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Action.Limits
/-- If `V` has limits of shape `J`, so does `Action V G`.  -/
Action.hasLimitsOfShape : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J] [CategoryTheory.Limits.HasLimitsOfShape J V],
  CategoryTheory.Limits.HasLimitsOfShape J (Action V G)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.map_eq_zero_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {X Y : C} {f : X ⟶ Y}, F.map f = 0 ↔ f = 0
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
norm_jacobiTheta₂_term_fderiv_le : ∀ (n : ℤ) (z τ : ℂ), ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * Real.pi * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_i_p_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [S.HasHomology] (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData),
  S.Exact ↔ CategoryTheory.CategoryStruct.comp h₁.i h₂.p = 0
-- Init.Data.String.Basic
String.Pos.ofSliceFrom_inj : ∀ {s : String} {p₀ : s.Pos} {pos pos' : (s.sliceFrom p₀).Pos},
  String.Pos.ofSliceFrom pos = String.Pos.ofSliceFrom pos' ↔ pos = pos'
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_reindex : ∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (e e' : m ≃ n) (M : Matrix m m R),
  ((Matrix.reindex e e') M).det = ↑↑(Equiv.Perm.sign (e'.trans e.symm)) * M.det
-- Mathlib.Algebra.Module.Presentation.Finite
Module.finitePresentation_iff_exists_presentation : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M],
  Module.FinitePresentation A M ↔ ∃ pres, Finite pres.G ∧ Finite pres.R
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** as a limit.  -/
taylor_tendsto : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ},
  Convex ℝ s →
    x₀ ∈ s →
      ContDiffOn ℝ (↑n) f s →
        Filter.Tendsto (fun x => ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (nhdsWithin x₀ s) (nhds 0)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isHomeomorph_comap_of_bijective : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : R →+* S},
  Function.Bijective ⇑f → IsHomeomorph (PrimeSpectrum.comap f)
-- Qq.Delab
Qq.Impl.delabq : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.Measure.finsetSum_apply`. -/
MeasureTheory.Measure.finset_sum_apply : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (I : Finset ι) (μ : ι → MeasureTheory.Measure α) (s : Set α),
  (∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_nonneg : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, 0 ≤ dist x y
-- Mathlib.RingTheory.HahnSeries.HEval
PowerSeries.coeff_heval_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) (f : PowerSeries R),
  ((PowerSeries.heval x) f).coeff 0 = PowerSeries.constantCoeff f
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- An absolute right Kan lift is a Kan lift such that every 1-morphism commutes with it.  -/
CategoryTheory.Bicategory.RightLift.IsAbsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → CategoryTheory.Bicategory.RightLift f g → Type (max (max u v) w)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.isIso_fromNext_hom_h_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} {f : K ⟶ L} [inst_2 : CategoryTheory.EnoughInjectives C] {n₀ : ℤ}
  (F : CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE✝ f n₀) (n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁),
  ∀ i ≤ n₀,
    CategoryTheory.IsIso
      ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.fromNext✝ F n₁ hn₁).hom.h.f i)
-- Mathlib.Order.Defs.LinearOrder
max_ind : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} {motive : α → Prop},
  (b ≤ a → motive a) → (a ≤ b → motive b) → motive (max a b)