mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The forgetful functor from the category of ring objects in `C` to `C`.  -/
CategoryTheory.RingObjCat.forget : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Functor (CategoryTheory.RingObjCat C) C
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.AffineCover.mk.inj : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} {I₀ : Type v}
  {X : I₀ → CommRingCat} {f : (j : I₀) → AlgebraicGeometry.Spec (X j) ⟶ S} {idx : ↥S → I₀}
  {covers : ∀ (x : ↥S), x ∈ Set.range ⇑(f (idx x))}
  {map_prop : autoParam (∀ (j : I₀), P (f j)) AlgebraicGeometry.Scheme.AffineCover.map_prop._autoParam} {I₀_1 : Type v}
  {X_1 : I₀_1 → CommRingCat} {f_1 : (j : I₀_1) → AlgebraicGeometry.Spec (X_1 j) ⟶ S} {idx_1 : ↥S → I₀_1}
  {covers_1 : ∀ (x : ↥S), x ∈ Set.range ⇑(f_1 (idx_1 x))}
  {map_prop_1 : autoParam (∀ (j : I₀_1), P (f_1 j)) AlgebraicGeometry.Scheme.AffineCover.map_prop._autoParam},
  { I₀ := I₀, X := X, f := f, idx := idx, covers := covers, map_prop := map_prop } =
      { I₀ := I₀_1, X := X_1, f := f_1, idx := idx_1, covers := covers_1, map_prop := map_prop_1 } →
    I₀ = I₀_1 ∧ X ≍ X_1 ∧ f ≍ f_1 ∧ idx ≍ idx_1
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- If `c.Rel i j`, then `C.xNext i` is isomorphic to `C.X j`.  -/
HomologicalComplex.xNextIso : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (C : HomologicalComplex V c) → {i j : ι} → c.Rel i j → (C.xNext i ≅ C.X j)
-- Batteries.Data.String.Lemmas
String.rawEndPos_ofList : ∀ (cs : List Char), (String.ofList cs).rawEndPos = { byteIdx := String.utf8Len cs }
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.two_mul_widthInfty_mem_strictPeriods : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)), 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
-- Mathlib.Order.GaloisConnection.Defs
/-- Main property of a Galois coinsertion.  -/
GaloisCoinsertion.u_l_le : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (self : GaloisCoinsertion l u) (x : α), u (l x) ≤ x
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {T : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} T] (L : CategoryTheory.Functor A T)
  {W : CategoryTheory.MorphismProperty T} {X : T} [W.RespectsIso],
  (CategoryTheory.MorphismProperty.structuredArrowObj L W).IsClosedUnderIsomorphisms
-- Mathlib.Topology.Order.IntermediateValue
Continuous.image_Ico_of_strictMono : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ}, Continuous f → StrictMono f → f '' Set.Ico a b = Set.Ico (f a) (f b)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.mk_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) {X A : T} (f : A ⟶ X) (hf : P f),
  (CategoryTheory.MorphismProperty.Over.mk Q f hf).left = A
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  (f : ContDiffBump 0) (x : E), ↑f (-x) = ↑f x
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_one : Polynomial.mahlerMeasure 1 = 1
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNormOneClassOfNonempty : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] [Nonempty α] [inst_4 : One E] [NormOneClass E], NormOneClass C(α, E)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  (m.insertMany l).contains k = (m.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.toSemilatticeSup : {α : Type u_5} → [self : IdemSemiring α] → SemilatticeSup α
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- If `G` preserves kernels and `C` has them, then the fork constructed of the mapped morphisms of
a kernel fork is a limit.
 -/
CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [inst_4 : G.PreservesZeroMorphisms] →
                {X Y : C} →
                  (f : X ⟶ Y) →
                    [inst_5 : CategoryTheory.Limits.HasKernel f] →
                      [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G] →
                        CategoryTheory.Limits.IsLimit
                          (CategoryTheory.Limits.Fork.ofι (G.map (CategoryTheory.Limits.kernel.ι f)) ⋯)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.re_neg : ∀ (z : Complex.UnitDisc), (-z).re = -z.re
-- Mathlib.Analysis.InnerProductSpace.Calculus
Differentiable.norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E},
  Differentiable ℝ f → (∀ (x : G), f x ≠ 0) → Differentiable ℝ fun y => ‖f y‖
-- Batteries.Recycling.RBTree.Basic
/-- This function does the second part of `RBNode.ins`,
which unwinds the stack and rebuilds the tree.
 -/
RBTree.RBNode.Path.ins : {α : Type u_1} → RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBNode α
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.ext : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type w} {x y : Std.Iterators.PostconditionT m α}
  (h : x.Property = y.Property), (fun p => ⟨↑p, ⋯⟩) <$> x.operation = y.operation → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The induced map `∏ᶜ I.left ⟶ ∏ᶜ I.right` via `I.fst` for limiting fans.  -/
CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        (c : CategoryTheory.Limits.Fan I.left) →
          {d : CategoryTheory.Limits.Fan I.right} → CategoryTheory.Limits.IsLimit d → (c.pt ⟶ d.pt)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀_single_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (g : G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ A)) fun₀ | g⁻¹ => a) =
    -(CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ A)) fun₀ | g => (A.ρ g) a
-- Init.Data.List.ToArray
Array.forIn'.loop.eq_2 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)) (b : β) (i_2 : ℕ) (h_2 : i_2 + 1 ≤ as.size),
  Array.forIn'.loop as f i_2.succ h_2 b = do
    let __do_lift ← f as[as.size - 1 - i_2] ⋯ b
    match __do_lift with
      | ForInStep.done b => pure b
      | ForInStep.yield b => Array.forIn'.loop as f i_2 ⋯ b
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instMax : {G : Type u_1} → [inst : Group G] → Max (FiniteIndexNormalSubgroup G)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.mk.injEq : ∀ (eq : Bool) (lhs rhs : Nat.Internal.Linear.Expr) (eq_1 : Bool) (lhs_1 rhs_1 : Nat.Internal.Linear.Expr),
  ({ eq := eq, lhs := lhs, rhs := rhs } = { eq := eq_1, lhs := lhs_1, rhs := rhs_1 }) =
    (eq = eq_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.brecOn.eq : ∀ {motive : Nat.Partrec.Code → Sort u} (t : Nat.Partrec.Code)
  (F_1 : (t : Nat.Partrec.Code) → Nat.Partrec.Code.below t → motive t),
  Nat.Partrec.Code.brecOn t F_1 = F_1 t (Nat.Partrec.Code.brecOn.go t F_1).2
-- Mathlib.Analysis.Convex.Strong
_private.Mathlib.Analysis.Convex.Strong.0.aux_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {a b m : ℝ} {x y : E} {f : E → ℝ},
  0 ≤ a →
    0 ≤ b →
      a + b = 1 →
        a * (f x + m / 2 * ‖x‖ ^ 2) + b * (f y + m / 2 * ‖y‖ ^ 2) - m / 2 * ‖a • x + b • y‖ ^ 2 =
          a * f x + b * f y + m / 2 * a * b * ‖x - y‖ ^ 2
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The empty set is concyclic.  -/
EuclideanGeometry.concyclic_empty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P], EuclideanGeometry.Concyclic ∅
-- Mathlib.Data.Finsupp.Basic
Finsupp.embDomain_trans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] (v : α →₀ M) (f : α ↪ β)
  (g : β ↪ γ), Finsupp.embDomain (f.trans g) v = Finsupp.embDomain g (Finsupp.embDomain f v)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k fallback : α}, t.contains k = true → t.getKeyD k fallback = k
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_card_add : ∀ {α : Type u_1} {n : ℕ} (s : Finset α), 0 < n → Finset.powersetCard (s.card + n) s = ∅
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso : ∀ (R : Type u) [inst : CommRing R],
  (HopfAlgCat.MonoidalCategory.inducingFunctorData R).εIso =
    CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (BialgCat R))
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.getElem_alternatingWord : ∀ {B : Type u_1} (i j : B) (p k : ℕ) (hk : k < p),
  (CoxeterSystem.alternatingWord i j p)[k] = if Even (p + k) then i else j
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVAdd_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₁] (v : V₁) (x : P₁), (AffineEquiv.constVAdd k P₁ v) x = v +ᵥ x
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- If there are no configurations of satellites with `N+1` points, one never uses more than `N`
distinct families in the Besicovitch inductive construction.  -/
Besicovitch.TauPackage.color_lt : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
  {i : Ordinal.{u}}, i < p.lastStep → ∀ {N : ℕ}, IsEmpty (Besicovitch.SatelliteConfig α N p.τ) → p.color i < N
-- Init.Grind.Order
Lean.Grind.Order.le_eq_false_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a : α} {k : ℤ}, k.blt' 0 = true → (a ≤ a + ↑k) = False
-- Init.Data.Ord.SInt
Int64.instLawfulEqOrd : Std.LawfulEqOrd Int64
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_succ_self_left : ∀ (n : ℕ), (n + 1).stirlingFirst n = (n + 1).choose 2
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Submodule.codisjoint_span_image_of_codisjoint : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  Submodule.span R (Set.range v) = ⊤ →
    ∀ {s t : Set ι}, Codisjoint s t → Codisjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.mem_ofSimplex_obj_iff : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) {m : SimplexCategoryᵒᵖ} (y : X.obj m),
  y ∈ (SSet.Subcomplex.ofSimplex x).obj m ↔ ∃ f, (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x = y
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_union_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b < a → Set.Ioo b a ∪ {a} = Set.Ioc b a
-- Mathlib.Algebra.Quandle
/-- A quandle is a rack such that each automorphism fixes its corresponding element.
 -/
Quandle : Type u_1 → Type u_1
-- Mathlib.RingTheory.PowerSeries.Evaluation
/-- For `HasEval a`,
the evaluation homomorphism at `a` on `PowerSeries`, as an `AlgHom`.  -/
PowerSeries.aeval : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Type u_2} →
      [inst_1 : CommRing S] →
        {a : S} →
          [inst_2 : UniformSpace R] →
            [inst_3 : UniformSpace S] →
              [IsUniformAddGroup R] →
                [IsTopologicalSemiring R] →
                  [IsUniformAddGroup S] →
                    [T2Space S] →
                      [CompleteSpace S] →
                        [IsTopologicalRing S] →
                          [IsLinearTopology S S] →
                            [inst_11 : Algebra R S] →
                              [ContinuousSMul R S] → PowerSeries.HasEval a → PowerSeries R →ₐ[R] S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_le_minKey?_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k km kme : α} (hkme : (Std.DTreeMap.Internal.Impl.erase! k t).minKey? = some kme),
  t.minKey?.get ⋯ = km → (compare km kme).isLE = true
-- Mathlib.Probability.Kernel.CompProdEqIff
/-- Two finite kernels `κ` and `η` are `μ`-a.e. equal iff the composition-products `μ ⊗ₘ κ`
and `μ ⊗ₘ η` are equal.  -/
ProbabilityTheory.Kernel.compProd_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β]
  [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η],
  μ.compProd κ = μ.compProd η ↔ ⇑κ =ᵐ[μ] ⇑η
-- Mathlib.Dynamics.Newton
Polynomial.newtonMap_apply_of_not_isUnit : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  {x : S}, ¬IsUnit ((Polynomial.aeval x) (Polynomial.derivative P)) → P.newtonMap x = x
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht ht_1 : CategoryTheory.Limits.IsWeakLimit t),
  ht = ht_1 →
    ∀ {W : C} (h h_1 : W ⟶ X) (e_h : h = h_1) (k k_1 : W ⟶ Y) (e_k : k = k_1)
      (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
      CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift ht h k w =
        CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift ht_1 h_1 k_1 ⋯
-- Init.Data.Nat.Lemmas
Nat.le_or_le_of_add_eq_add_pred : ∀ {a c b d : ℕ}, a + c = b + d - 1 → b ≤ a ∨ d ≤ c
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
SzemerediRegularity.bound.eq_1 : ∀ (ε : ℝ) (l : ℕ),
  SzemerediRegularity.bound ε l =
    SzemerediRegularity.stepBound^[⌊4 / ε ^ 5⌋₊] (SzemerediRegularity.initialBound ε l) *
      16 ^ SzemerediRegularity.stepBound^[⌊4 / ε ^ 5⌋₊] (SzemerediRegularity.initialBound ε l)
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.eq_of_comp_left_eq' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y),
  ((fun {Z} h => CategoryTheory.CategoryStruct.comp f h) = fun {Z} h => CategoryTheory.CategoryStruct.comp g h) → f = g
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_sum_eq : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (x : 𝔸), (NormedSpace.expSeries 𝕂 𝔸).sum x = ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.comp_right_injective : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (e : M ≃+ N), Function.Injective fun f => (↑e).comp f
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_or : ∀ {w x y : ℕ}, BitVec.ofNat w (x ||| y) = BitVec.ofNat w x ||| BitVec.ofNat w y
-- Mathlib.LinearAlgebra.Prod
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`.  -/
LinearEquiv.prodProdProdComm : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      (M₃ : Type y) →
        (M₄ : Type z) →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : AddCommMonoid M₄] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] → [inst_8 : Module R M₄] → ((M × M₂) × M₃ × M₄) ≃ₗ[R] (M × M₃) × M₂ × M₄
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformSpace_comap_restrict : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (S : Set ι),
  UniformSpace.comap S.domRestrict (Pi.uniformSpace fun i => α ↑i) = ⨅ i ∈ S, UniformSpace.comap (Function.eval i) (U i)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Use a fresh name generator for creating internal metavariables for theorem instantiation.
This is technique to ensure the metavariables ids do not depend on operations performed before invoking `grind`.
Without this trick, we experience counterintuitive behavior where small changes affect the metavariable ids, and
consequently the hash code for expressions, and operations such as `qsort` using `Expr.quickLt` in
`assignUnassignedLevelMVars`.
This code is correct because the auxiliary metavariables created during theorem instantiation cannot escape.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.withFreshNGen : {α : Type} → Lean.Meta.Grind.EMatch.M α → Lean.Meta.Grind.EMatch.M α
-- Std.Time.Zoned.RecurringRule
/-- Specifies how a DST transition date is expressed.
 -/
Std.Time.TimeZone.TransitionSpec : Type
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonInitializeResult.toJson : Lean.Lsp.InitializeResult → Lean.Json
-- Mathlib.Algebra.Polynomial.Bivariate
/-- The R-algebra automorphism given by `X ↦ Y` and `Y ↦ X`.  -/
Polynomial.Bivariate.swap : {R : Type u_1} → [inst : CommSemiring R] → Polynomial (Polynomial R) ≃ₐ[R] Polynomial (Polynomial R)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [BEq α] [Hashable α] {c : ℕ}, (Std.HashMap.Raw.emptyWithCapacity c).isEmpty = true
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.disjoint_iff : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s → l'.HasBasis p' s' → (Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i'))
-- Mathlib.Data.Semiquot
Semiquot.get.congr_simp : ∀ {α : Type u_1} (q q_1 : Semiquot α) (e_q : q = q_1) (h : q.IsPure), q.get h = q_1.get ⋯
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (hs : CategoryTheory.Limits.IsColimit s),
  Nonempty (CategoryTheory.Limits.IsColimit t) ↔ CategoryTheory.IsIso (hs.desc t)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- A multiplicative morphism property `W` has right calculus of fractions if
any left fraction can be turned into a right fraction and that two morphisms
that can be equalized by postcomposition with a morphism in `W` can also
be equalized by precomposition with a morphism in `W`.  -/
CategoryTheory.MorphismProperty.HasRightCalculusOfFractions : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_eq_right : ∀ {a b : ENNReal}, b ≠ 0 → b ≠ ⊤ → (a * b = b ↔ a = 1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.instHasZeroMorphisms : {D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D] →
      CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.Mon D)
-- Init.Data.Array.Attach
Array.pmap_attachWith : ∀ {α : Type u_1} {q : α → Prop} {β : Type u_2} {xs : Array α} {p : { x // q x } → Prop}
  {f : (a : { x // q x }) → p a → β} (H₁ : ∀ x ∈ xs, q x) (H₂ : ∀ a ∈ xs.attachWith q H₁, p a),
  Array.pmap f (xs.attachWith q H₁) H₂ = Array.pmap (fun a h => f ⟨a, ⋯⟩ ⋯) xs ⋯
-- Mathlib.Data.Finset.Pi
Finset.Pi.cons_injective : ∀ {α : Type u_1} {δ : α → Sort v} [inst : DecidableEq α] {a : α} {b : δ a} {s : Finset α},
  a ∉ s → Function.Injective (Finset.Pi.cons s a b)
-- Mathlib.Order.UpperLower.Basic
isUpperSet_iff_Ioi_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α}, IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Ioi a ⊆ s
-- Mathlib.Topology.MetricSpace.IsometricSMul
ULift.isIsometricSMul : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X],
  IsIsometricSMul (ULift.{u_2, u} M) X
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Induction (recursion) principle on `c : Composition _`
that corresponds to the usual induction on the list of blocks of `c`.  -/
Composition.recOnSingleAppend : {motive : (n : ℕ) → Composition n → Sort u_1} →
  {n : ℕ} →
    (c : Composition n) →
      motive 0 (Composition.ones 0) →
        ((k n : ℕ) → (c : Composition n) → motive n c → motive (k + 1 + n) ((Composition.single (k + 1) ⋯).append c)) →
          motive n c
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.drop.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass.comp : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {γ : Type u_1} {γ' : Type u_2} {g : γ' → γ}
  {op :
    γ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  [h : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op],
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass fun c => op (g c)
-- Mathlib.Topology.Algebra.Support
ContinuousOn.continuous_of_mulTSupport_subset : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] [inst_2 : TopologicalSpace β] {f : α → β}
  {s : Set α}, ContinuousOn f s → IsOpen s → mulTSupport f ⊆ s → Continuous f
-- Lean.Util.FoldConsts
/-- Like `Expr.getUsedConstants`, but produce a `NameSet`.  -/
Lean.Expr.getUsedConstantsAsSet : Lean.Expr → Lean.NameSet
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.priority : Aesop.Frontend.Priority → Aesop.Frontend.Feature
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_top : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock (↥⊤) B ↔ MulAction.IsBlock G B
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.differentiable_qParam : ∀ {h : ℝ}, Differentiable ℂ (Function.Periodic.qParam h)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.X_mul_monomial : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (r : R),
  SkewPolynomial.X * (SkewPolynomial.monomial n) r = (SkewPolynomial.monomial (n + 1)) (SkewPolynomial.φ r)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Subgroup.range_zpowersHom : ∀ {G : Type u_1} [inst : Group G] (g : G), ((zpowersHom G) g).range = Subgroup.zpowers g