mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.mkIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : CategoryTheory.CommMon C} (e e_1 : M.X ≅ N.X) (e_e : e = e_1)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.MonObj.mul),
  CategoryTheory.CommMon.mkIso e one_f mul_f = CategoryTheory.CommMon.mkIso e_1 ⋯ ⋯
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Restrict the domain of a bounded continuous function to a set.  -/
BoundedContinuousFunction.domRestrict : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] → BoundedContinuousFunction α β → (s : Set α) → BoundedContinuousFunction (↑s) β
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.iIndepFun_congr`. -/
ProbabilityTheory.Kernel.iIndepFun.congr : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_10}
  {m : (x : ι) → MeasurableSpace (β x)} {f : (x : ι) → Ω → β x},
  ⇑κ =ᵐ[μ] ⇑η → ProbabilityTheory.Kernel.iIndepFun f κ μ → ProbabilityTheory.Kernel.iIndepFun f η μ
-- Std.Data.DTreeMap.Lemmas
_private.Std.Data.DTreeMap.Lemmas.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- Every Hilbert basis indexed by `ℕ` is a Schauder basis (`SchauderBasis`) with
coordinate functionals `x ↦ ⟪b i, x⟫`. The expansion `x = ∑ i, ⟪b i, x⟫ • b i` converges.  -/
HilbertBasis.toSchauderBasis : {𝕜 : Type u_2} →
  [inst : RCLike 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → HilbertBasis ℕ 𝕜 E → SchauderBasis 𝕜 E
-- Mathlib.Algebra.Group.Action.Defs
isScalarTower_iff_smulCommClass_of_commMonoid : ∀ (R₁ : Type u_9) (R : Type u_10) [inst : Monoid R₁] [inst_1 : CommMonoid R] [inst_2 : MulAction R₁ R],
  SMulCommClass R₁ R R ↔ IsScalarTower R₁ R R
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.isClosed_topologicalClosure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G] (s : AddSubgroup G),
  IsClosed ↑s.topologicalClosure
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.reverse_inj : ∀ {V : Type u_2} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a b : V} (f g : a ⟶ b),
  Quiver.reverse f = Quiver.reverse g ↔ f = g
-- Mathlib.Data.DFinsupp.Order
DFinsupp.single_le_single : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)] {i : ι}
  {a b : α i} [inst_2 : DecidableEq ι], ((fun₀ | i => a) ≤ fun₀ | i => b) ↔ a ≤ b
-- Mathlib.LinearAlgebra.Charpoly.BaseChange
LinearMap.charpoly_baseChange : ∀ {R : Type u_3} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) (A : Type u_1) [inst_5 : CommRing A]
  [inst_6 : Algebra R A], (LinearMap.baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly
-- Mathlib.Order.Comparable
instSymmIncompRel : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Symm (IncompRel r)
-- Mathlib.RingTheory.RingHom.FinitePresentation
/-- Being finitely-presented is a local property of rings.  -/
RingHom.finitePresentation_isLocal : RingHom.PropertyIsLocal @RingHom.FinitePresentation
-- Mathlib.LinearAlgebra.Matrix.FiniteDimensional
/-- Linear maps over a `k`-algebra are finite dimensional (over `k`) if both the source and
target are, as they form a subspace of all `k`-linear maps.  -/
LinearMap.finiteDimensional' : ∀ {K : Type u_1} [inst : Field K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module K W] [FiniteDimensional K W] {A : Type u_4}
  [inst_7 : Ring A] [inst_8 : Algebra K A] [inst_9 : Module A V] [IsScalarTower K A V] [inst_11 : Module A W]
  [inst_12 : IsScalarTower K A W], FiniteDimensional K (V →ₗ[A] W)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] (t t_1 : Std.DTreeMap.Raw α β cmp)
  (e_t : t = t_1) (a : α) (h : a ∈ t), t.get a h = t_1.get a ⋯
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Relations.tensor_R : ∀ {A : Type u} [inst : CommRing A] (relations₁ : Module.Relations A) (relations₂ : Module.Relations A),
  (relations₁.tensor relations₂).R = (relations₁.R × relations₂.G ⊕ relations₁.G × relations₂.R)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Concyclic.Cospherical : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P}, EuclideanGeometry.Concyclic ps → EuclideanGeometry.Cospherical ps
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.isNilpotent_pi_of_bounded_class`.

---

Products of nilpotent groups are nilpotent if their nilpotency class is bounded.  -/
isNilpotent_pi_of_bounded_class : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [∀ (i : η), Group.IsNilpotent (Gs i)] (n : ℕ),
  (∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n) → Group.IsNilpotent ((i : η) → Gs i)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_smul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (r : 𝕜) (f : E →L[𝕜] F) (g : G →L[𝕜] H),
  TensorProduct.mapL (r • f) g = r • TensorProduct.mapL f g
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.coeff_add_of_supDegree_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p q : AddMonoidAlgebra R A} [inst_3 : AddZeroClass A] [inst_4 : Add B],
  (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
    ∀ [AddLeftStrictMono B] [AddRightStrictMono B],
      Function.Injective D →
        ∀ {ap aq : A},
          AddMonoidAlgebra.supDegree D p ≤ D ap →
            AddMonoidAlgebra.supDegree D q ≤ D aq → (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.Std.Internal.Do.Except.wpInst.match_1.eq_2 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (el : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (el : ε) → motive (Except.error el)),
  (match Except.error el with
    | Except.ok a => h_1 a
    | Except.error el => h_2 el) =
    h_2 el
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.«proofWidgetsJsxAttr_=_» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.continuousOn_smul : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} {𝕜 : Type u_9} [inst_4 : NormedRing 𝕜]
  [inst_5 : Module 𝕜 E] [IsBoundedSMul 𝕜 E] [T2Space X] [SecondCountableTopologyEither X 𝕜] {g : X → E},
  MeasureTheory.IntegrableOn g K μ →
    ∀ {f : X → 𝕜}, ContinuousOn f K → IsCompact K → MeasureTheory.IntegrableOn (fun x => f x • g x) K μ
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.SubmonoidPresheaf.mk.injEq : ∀ {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (obj : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ↑(F.obj U))
  (map :
    ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
      obj U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (obj V))
  (obj_1 : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ↑(F.obj U))
  (map_1 :
    ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
      obj_1 U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (obj_1 V)),
  ({ obj := obj, map := map } = { obj := obj_1, map := map_1 }) = (obj = obj_1)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_eq_one : ∀ {x : ℝ}, ↑x = 1 ↔ x = 1
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instCanLiftSubmoduleToSubmoduleForallForallForallMemBracket : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M],
  CanLift (Submodule R M) (LieSubmodule R L M) (fun x => ↑x) fun N => ∀ {x : L} {m : M}, m ∈ N → ⁅x, m⁆ ∈ N
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.modify.eq_def : ∀ {α : Type u} [inst : BEq α] {β : Type v} (a : α) (f : β → β) (x : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.Const.modify a f x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => Std.DHashMap.Internal.AssocList.nil
    | Std.DHashMap.Internal.AssocList.cons k v l =>
      if (k == a) = true then Std.DHashMap.Internal.AssocList.cons a (f v) l
      else Std.DHashMap.Internal.AssocList.cons k v (Std.DHashMap.Internal.AssocList.Const.modify a f l)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.birdDet.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive n
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instNeg : (A : Type u_3) → (E : Type u_4) → [Neg E] → Neg (WithCStarModule A E)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerTotal_mkQ_single_mul : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x y z : S),
  ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | x * y => z) =
    ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | y => z * x) +
      (KaehlerDifferential.kerTotal R S).mkQ fun₀ | x => z * y
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.natDegree_pos_of_monic_of_aeval_eq_zero : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [Nontrivial R] [inst_2 : Semiring S] [inst_3 : Algebra R S]
  [FaithfulSMul R S] {p : Polynomial R}, p.Monic → ∀ {x : S}, (Polynomial.aeval x) p = 0 → 0 < p.natDegree
-- Mathlib.CategoryTheory.Preadditive.Comma
/-- If we have additive functors `L : A ⥤ T` and `R : B ⥤ T` between preadditive categories,
then the category `Comma L R` is preadditive.
 -/
CategoryTheory.instPreadditiveComma : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    [inst_1 : CategoryTheory.Preadditive A] →
      {B : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_3 : CategoryTheory.Preadditive B] →
            {T : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} T] →
                [inst_5 : CategoryTheory.Preadditive T] →
                  (L : CategoryTheory.Functor A T) →
                    [L.Additive] →
                      (R : CategoryTheory.Functor B T) →
                        [R.Additive] → CategoryTheory.Preadditive (CategoryTheory.Comma L R)
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.zoom_fill : ∀ {α : Type u_1} {cut : α → Ordering} {t : RBTree.RBNode α} {path : RBTree.RBNode.Path α} {t' : RBTree.RBNode α}
  {path' : RBTree.RBNode.Path α}, RBTree.RBNode.zoom cut t path = (t', path') → path.fill t = path'.fill t'
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesMk₁_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥(groupCohomology.cocycles₁ A)),
  groupCohomology.cocyclesMk ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ A).inv) ⇑x) ⋯ =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₁ A).inv) x
-- Mathlib.Data.Fin.Tuple.Take
/-- `take` commutes with `update` for indices in the range of `take`.  -/
Fin.take_update_of_lt : ∀ {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m) (x : α (Fin.castLE h i)),
  Fin.take m h (Function.update v (Fin.castLE h i) x) = Function.update (Fin.take m h v) i x
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.whiskerRight_comp_assoc : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (Q : CategoryTheory.LocalizedMonoidal L W ε) {X Y Z : CategoryTheory.LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : CategoryTheory.LocalizedMonoidal L W ε} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Q) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Q)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Q) h)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_lt_logb_iff : ∀ {b x y : ℝ}, 1 < b → 0 < x → 0 < y → (Real.logb b x < Real.logb b y ↔ x < y)
-- Init.Data.String.Pattern.Basic
/-- The default implementation of `ToBackwardSearcher` repeatedly tries to match the pattern using
the given `BackwardPattern` instance.

It is sometimes possible to give a more efficient implementation; see `ToBackwardSearcher`
for more details.
 -/
String.Slice.Pattern.ToBackwardSearcher.defaultImplementation : {ρ : Type} →
  {pat : ρ} →
    [String.Slice.Pattern.BackwardPattern pat] →
      String.Slice.Pattern.ToBackwardSearcher pat (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher pat)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.Data.Multiset.Sym
/-- `m.sym2` is the multiset of all unordered pairs of elements from `m`, with multiplicity.
If `m` has no duplicates then neither does `m.sym2`.  -/
Multiset.sym2 : {α : Type u_1} → Multiset α → Multiset (Sym2 α)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instPartialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder (WithZero α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ {k : α} {fallback : β} {f : β → β},
      Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.modify t k f) k fallback =
        (Option.map f (Std.DTreeMap.Raw.Const.get? t k)).getD fallback
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.diff_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ \ t₃).Equiv (t₂ \ t₃)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.π₂_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (x : CategoryTheory.Limits.CategoricalPullback F G),
  (CategoryTheory.Limits.CategoricalPullback.π₂ F G).obj x = x.snd
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M), AddLocalization S = AddOreLocalization S M
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_eq_self_sub_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (q.projection p ⋯) x = x - (p.projection q hpq) x
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.instHasFilteredColimitsOfSize : CategoryTheory.Limits.HasFilteredColimitsOfSize.{u, u, u, u + 1} PartOrdEmb
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
coprime_card_of_isAddCyclic_prod : ∀ (M : Type u_4) (N : Type u_5) [inst : AddGroup M] [inst_1 : AddGroup N] [cyc : IsAddCyclic (M × N)] [Finite M]
  [Finite N], (Nat.card M).Coprime (Nat.card N)
-- Std.Data.ByteSlice
/-- The underlying byte array.
 -/
Std.Slice.Internal.ByteSliceData.byteArray : Std.Slice.Internal.ByteSliceData → ByteArray
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Product of `NonUnitalSubring`s is isomorphic to their product as rings.  -/
NonUnitalSubring.prodEquiv : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] →
      [inst_1 : NonUnitalNonAssocRing S] → (s : NonUnitalSubring R) → (t : NonUnitalSubring S) → ↥(s.prod t) ≃+* ↥s × ↥t
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.enorm_integral_le_of_enorm_le_const : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {C : ENNReal},
  (∀ᵐ (x : X) ∂μ.variation, ‖f x‖ₑ ≤ C) → ‖∫ᵛ (x : X), f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation Set.univ
-- Mathlib.Algebra.Order.Module.Defs
smul_nonneg_iff_nonneg_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosMono α β] [SMulPosReflectLE α β], 0 < b → (0 ≤ a • b ↔ 0 ≤ a)
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.tendsto_one_div_one_add_pow_nhds_one : ∀ {R : Type u_1} [inst : Field R] {v : AbsoluteValue R ℝ} {a : R},
  v a < 1 → Filter.Tendsto (fun n => (WithAbs.equiv v).symm (1 / (1 + a ^ n))) Filter.atTop (nhds 1)
-- Mathlib.Data.Finset.Defs
/-- decidable equality for functions whose domain is bounded by finsets  -/
Finset.decidableEqPiFinset : {α : Type u_1} →
  {s : Finset α} → {β : α → Type u_4} → [_h : (a : α) → DecidableEq (β a)] → DecidableEq ((a : α) → a ∈ s → β a)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- Typeclass saying that a subgroup of `GL(n, R)` is contained in `SL(n, R)`. Necessary so that
the typeclass system can detect when the slash action is `ℂ`-linear.  -/
Subgroup.HasDetOne : {n : Type u_1} →
  [inst : Fintype n] → [inst_1 : DecidableEq n] → {R : Type u_2} → [inst_2 : CommRing R] → Subgroup (GL n R) → Prop
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of a subset of a family indexed by a `Fintype`
is finite-dimensional.  -/
finiteDimensional_vectorSpan_image_of_finite : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Finite ι] (p : ι → P) (s : Set ι),
  FiniteDimensional k ↥(vectorSpan k (p '' s))
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instAddGroupWithOne : {q : ℕ} → AddGroupWithOne (LucasLehmer.X q)
-- Mathlib.Analysis.RCLike.Basic
LinearIsometryEquiv.trans_smul : ∀ {𝕜 : Type u_3} {V : Type u_4} {W : Type u_5} {G : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : SeminormedAddCommGroup W] [inst_4 : NormedSpace 𝕜 W]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (α : ↥(unitary 𝕜)) (e : V ≃ₗᵢ[𝕜] G) (f : G ≃ₗᵢ[𝕜] W),
  e.trans (α • f) = α • e.trans f
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.ΨSq_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ}, ↑n ≠ 0 → W.ΨSq n ≠ 0
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.χ_pullback_obj_mk_truth_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (𝒞 : CategoryTheory.Subobject.Classifier C) {X : C} (φ : X ⟶ 𝒞.Ω),
  𝒞.χ ((CategoryTheory.Subobject.pullback φ).obj 𝒞.truth_as_subobject).arrow = φ
-- Mathlib.CategoryTheory.Endomorphism
/-- The inclusion of `Aut X` to `End X` as a monoid homomorphism.  -/
CategoryTheory.Aut.toEnd : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : C) → CategoryTheory.Aut X →* CategoryTheory.End X
-- Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure
_private.Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure.0.MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply_eq_enorm : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.SignedMeasure X) {i j : Set X} (him : MeasurableSet i)
  (hi : MeasureTheory.VectorMeasure.restrict μ i ≤ MeasureTheory.VectorMeasure.restrict 0 i),
  MeasurableSet j → (μ.toMeasureOfLEZero i him hi) j = ‖μ (i ∩ j)‖ₑ
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.prod_mk_fst_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : Monoid.Coprod M N),
  (Monoid.Coprod.fst x, Monoid.Coprod.snd x) = Monoid.Coprod.toProd x
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.instFintypeEdgeLabelingOfDecidableEqOfElemSym2EdgeSet : {V : Type u_1} →
  {G : SimpleGraph V} →
    {K : Type u_3} → [DecidableEq V] → [Fintype ↑G.edgeSet] → [Fintype K] → Fintype (G.EdgeLabeling K)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on a compact set `s` and `f 0 = 0` and `a : X → A` tends to
`a₀ : A` along a filter `l` (such that eventually `0 ≤ a x` and has quasispectrum contained in `s`,
as does `a₀`), then `fun x ↦ cfcₙ f (a x)` tends to `cfcₙ f a₀`.  -/
Filter.Tendsto.cfcₙ_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A} {a₀ : A} {l : Filter X},
      Filter.Tendsto a l (nhds a₀) →
        (∀ᶠ (x : X) in l, quasispectrum NNReal (a x) ⊆ s) →
          (∀ᶠ (x : X) in l, 0 ≤ a x) →
            quasispectrum NNReal a₀ ⊆ s →
              0 ≤ a₀ →
                autoParam (ContinuousOn f s) Filter.Tendsto.cfcₙ_nnreal._auto_1 →
                  autoParam (f 0 = 0) Filter.Tendsto.cfcₙ_nnreal._auto_3 →
                    Filter.Tendsto (fun x => cfcₙ f (a x)) l (nhds (cfcₙ f a₀))
-- Mathlib.Topology.Algebra.Monoid
eventuallyEq_prod : ∀ {ι : Type u_1} {X : Type u_6} {M : Type u_7} [inst : CommMonoid M] {s : Finset ι} {l : Filter X} {f g : ι → X → M},
  (∀ i ∈ s, f i =ᶠ[l] g i) → ∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.regular : Aesop.RuleResult → Aesop.SafeRuleResult
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
summable_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  ¬L.NeBot → ∀ (f : β → α), Summable f L
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- If `f` is harmonic in a neighborhood of `s`, it is harmonic in a neighborhood of every subset.
 -/
InnerProductSpace.HarmonicOnNhd.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s t : Set E},
  InnerProductSpace.HarmonicOnNhd f s → t ⊆ s → InnerProductSpace.HarmonicOnNhd f t