mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.shiftedGenWeightSpace.instSubtypeMemLieSubmodule : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) [inst_8 : LieModule.LinearWeights R L M],
  LieModule R L ↥(LieModule.shiftedGenWeightSpace R L M χ)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ↪r s⦄, (∀ (x : α), f x = g x) → f = g
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.stabilizerSubmonoid.eq_1 : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] (a : α),
  MulAction.stabilizerSubmonoid M a = { carrier := {m | m • a = a}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.instFullιHeart : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (H : Type u') [inst_6 : CategoryTheory.Category.{v', u'} H]
  [inst_7 : CategoryTheory.Preadditive H] [inst_8 : t.Heart H], t.ιHeart.Full
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.dvd_of_ysq_dvd : ∀ {a : ℕ} (a1 : 1 < a) {n t : ℕ}, Pell.yn a1 n * Pell.yn a1 n ∣ Pell.yn a1 t → Pell.yn a1 n ∣ t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_eq_getLast_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey he = t.keys.getLast ⋯
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then for every `x : R`,
the image of `y ↦ f (x * y) / f y` is bounded above.  -/
seminormFromBounded_bddAbove_range : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → ∀ (x : R), BddAbove (Set.range fun y => f (x * y) / f y)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on `s` and `f 0 = 0` and `a : X → A` is continuous on
`t : Set X`, and `a x` is nonnegative for all `x ∈ t` and `s` is a common neighborhood of the
quasispectra of `a x` for all `x ∈ t`, then `fun x ↦ cfcₙ f (a x)` is continuous on `t`.

This is weaker than `ContinuousOn.cfcₙ_nnreal` since it requires `f` to be continuous on a
*neighborhood* of the quasispectra, but in practice it is often easier to apply because `s` is not
required to be compact, nor does it require an indexed family of compact sets. This is proven using
`ContinuousOn.cfcₙ_nnreal` and `upperHemicontinuous_quasispectrum_nnreal` to produce the necessary
family of compact sets.  -/
ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet : ∀ {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]
  [CompleteSpace A] [inst_13 : TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X},
  s ∈ nhdsSet (⋃ x ∈ t, quasispectrum NNReal (a x)) →
    ContinuousOn a t →
      autoParam (∀ x ∈ t, 0 ≤ a x) ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet._auto_3 →
          autoParam (f 0 = 0) ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet._auto_5 → ContinuousOn (fun x => cfcₙ f (a x)) t
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.pi_apply : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → AddZeroClass (f i)] {γ : Type w} [inst_1 : AddZeroClass γ]
  (g : (i : I) → γ →+ f i) (x : γ) (i : I), (AddMonoidHom.pi g) x i = (g i) x
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a meromorphic function `f` at `z₀` equals an integer `n` iff `f` can locally be
written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic and does not vanish at `z₀`.  -/
meromorphicOrderAt_eq_int_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {n : ℤ},
  MeromorphicAt f x →
    (meromorphicOrderAt f x = ↑n ↔
      ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = (z - x) ^ n • g z)
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.w_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (D : ℝ) (x : E), 0 ≤ ExistsContDiffBumpBase.w D x
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_le_ofNat : ∀ {n x y : ℕ}, BitVec.ofNat n x ≤ BitVec.ofNat n y ↔ x % 2 ^ n ≤ y % 2 ^ n
-- Init.Data.Int.Lemmas
Int.add_left_neg : ∀ (a : ℤ), -a + a = 0
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.mk.inj : ∀ {impl : Lean.AttributeImpl} {ext : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)}
  {impl_1 : Lean.AttributeImpl}
  {ext_1 : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)},
  { impl := impl, ext := ext } = { impl := impl_1, ext := ext_1 } → impl = impl_1 ∧ ext = ext_1
-- Mathlib.Order.BooleanAlgebra.Basic
eq_compl_comm : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x = yᶜ ↔ y = xᶜ
-- Mathlib.Data.Finsupp.Single
Finsupp.single_of_embDomain_single : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (l : α →₀ M) (f : α ↪ β) (a : β) (b : M),
  b ≠ 0 → (Finsupp.embDomain f l = fun₀ | a => b) → ∃ x, (l = fun₀ | x => b) ∧ f x = a
-- Mathlib.Algebra.DirectSum.Internal
SetLike.natCast_mem_graded : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : Zero ι] [inst_1 : AddMonoidWithOne R] [inst_2 : SetLike σ R]
  [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedOne A] (n : ℕ), ↑n ∈ A 0
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.Flat f],
  AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.snd f g)
-- Init.Data.Vector.Lemmas
Vector.leftpad_mk : ∀ {α : Type u_1} {m n : ℕ} {a : α} {xs : Array α} (h : xs.size = m),
  Vector.leftpad n a (Vector.mk xs h) = Vector.mk (Array.leftpad n a xs) ⋯
-- Mathlib.Data.Set.Prod
Set.diag_preimage_prod_self : ∀ {α : Type u_1} (s : Set α), Function.diag ⁻¹' s ×ˢ s = s
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.IsIrreducible.nonneg : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R},
  A.IsIrreducible → ∀ (i j : n), 0 ≤ A i j
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
/-- The restriction of scalars of presheaves of modules, on objects.  -/
PresheafOfModules.restrictScalarsObj : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} → PresheafOfModules R' → (R ⟶ R') → PresheafOfModules R
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of `Polynomial.Splits.of_natDegree_eq_zero`. -/
Polynomial.splits_of_natDegree_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.natDegree = 0 → f.Splits
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.mul_ne_cert : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.isCompact_range : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} [inst_2 : TopologicalSpace β],
  HasCompactSupport f → Continuous f → IsCompact (Set.range f)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `I`-adic valuation of a generator of `I` equals `(-1 : ℤᵐ⁰)`  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_singleton : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  r ≠ 0 → v.asIdeal = Ideal.span {r} → v.intValuation r = WithZero.exp (-1)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPosAssignment.eq_3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.hasPosAssignment = true
-- Mathlib.LinearAlgebra.Dimension.Constructions
Subalgebra.finrank_toSubmodule : ∀ {F : Type u_2} {E : Type u_3} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E]
  (S : Subalgebra F E), Module.finrank F ↥(Subalgebra.toSubmodule S) = Module.finrank F ↥S
-- Init.Data.SInt.Lemmas
Int64.lt_of_lt_of_le : ∀ {a b c : Int64}, a < b → b ≤ c → a < c
-- Mathlib.Order.KrullDimension
Order.coheight_of_noMaxOrder : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] (a : α), Order.coheight a = ⊤
-- Init.Data.Array.Lemmas
Array.getElem_modify_self : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (f : α → α) (h : i < (xs.modify i f).size), (xs.modify i f)[i] = f xs[i]
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ioo_mem : ∀ {α : Type u_1} [inst : LinearOrder α] (s t : Set α), IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ioo l u = S}
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsColimitsCardinalClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w}),
  (P.colimitsCardinalClosure κ).IsClosedUnderIsomorphisms
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_list_sum : ∀ (l : List ℂ), Complex.exp l.sum = (List.map Complex.exp l).prod
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain 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.IsCrystallographic] {i j : ι},
  RootPairing.chainBotCoeff i j = 0 ↔
    ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j - P.root i ∉ Set.range ⇑P.root
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousAt.sub : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (f - g) x
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.decl.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Lean.Meta.Grind.Origin.decl declName) = 1 + sizeOf declName
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.size : Lean.Compiler.LCNF.CtorInfo → ℕ
-- Lean.Elab.InfoTree.Types
/-- Specifies that the given free variables should be considered semantically identical.
The free variable `baseId` might not be in the current local context
because it has been cleared.
Used for e.g. connecting variables before and after `match` generalization.
 -/
Lean.Elab.FVarAliasInfo : Type
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.Precoverage.morphismProperty_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C], ⊥.morphismProperty = ⊥
-- Mathlib.Order.Disjoint
Disjoint.eq_bot_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → b ≤ a → b = ⊥
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- The *image* of a hypergraph `H : Hypergraph α` under a function `f : α → β` is the hypergraph
`Hᶠ : Hypergraph β` where the vertex set of `Hᶠ` is the image of `V(H)` under `f` and the edge set
of `Hᶠ` is the set of images of the edges (subsets of vertices) in `E(H)`.  -/
Hypergraph.image : {α : Type u_1} → {β : Type u_2} → Hypergraph α → (α → β) → Hypergraph β
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtTreeMap.getD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → β → β
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_mul_right' : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {b : α}, (fun x => x * b⁻¹) '' t = (fun x => x * b) ⁻¹' t
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.mem_basicOpen : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
  x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
-- Mathlib.Topology.MetricSpace.Bounded
/-- A totally bounded set is bounded  -/
TotallyBounded.isBounded : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, TotallyBounded s → Bornology.IsBounded s
-- Lean.Compiler.InitAttr
/-- Like `runInitAttrs`, but walks only the given module indices. Used by `--incr-load`: the indices
identify modules with non-empty `regularInitAttr` entries, so the loader skips page-faulting
dep-region pages for modules without `[init]` work. Assumes the host process has already
initialized the saved env's native `builtin_initialize` side effects (typically because the
statically-linked Lean runtime ran them at startup) and skips `runModInit` for the omitted modules.
 -/
Lean.runInitAttrsForModules : Lean.Environment → Array ℕ → Lean.Options → IO Unit
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {X : C} →
        [toAddMonObj : CategoryTheory.AddMonObj X] →
          (neg : X ⟶ X) →
            autoParam
                (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.CartesianMonoidalCategory.lift neg (CategoryTheory.CategoryStruct.id X))
                    CategoryTheory.AddMonObj.add =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                    CategoryTheory.AddMonObj.zero)
                CategoryTheory.AddGrpObj.left_neg._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) neg)
                      CategoryTheory.AddMonObj.add =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                      CategoryTheory.AddMonObj.zero)
                  CategoryTheory.AddGrpObj.right_neg._autoParam →
                CategoryTheory.AddGrpObj X
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppRight_apply_tmul_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι] (m : M) (p : ι →₀ N) (i : ι),
  ((TensorProduct.finsuppRight R S M N ι) (m ⊗ₜ[R] p)) i = m ⊗ₜ[R] p i
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDesc_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {F G H : CategoryTheory.MonoidalCategory.DayFunctor C V}
  (α :
    CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor ⟶
      (CategoryTheory.MonoidalCategory.tensor C).comp H.functor)
  (x y : C) {Z : V} (h : H.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.η G).app (x, y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayFunctor.tensorDesc α).natTrans.app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))
        h) =
    CategoryTheory.CategoryStruct.comp (α.app (x, y)) h
-- Mathlib.Data.Set.Prod
Set.prod_self_ssubset_prod_self : ∀ {α : Type u_1} {s₁ s₂ : Set α}, s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂ ↔ s₁ ⊂ s₂
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.of_algEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {T : Type u_4}
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T) [h : Algebra.IsStandardOpenImmersion R S],
  Algebra.IsStandardOpenImmersion R T
-- Init.Coe
/-- `CoeOut α β` is for coercions that are applied from left-to-right.
 -/
CoeOut : Sort u → semiOutParam (Sort v) → Sort (max (max 1 u) v)
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.instanceReducible.sizeOf_spec : sizeOf Lean.ReducibilityStatus.instanceReducible = 1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1.inj : ∀ {k : ℤ} {c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr} {c₂ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr} {k_1 : ℤ}
  {c₁_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr} {c₂_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr},
  Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1 k c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1 k_1 c₁_1 c₂_1 →
    k = k_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjointMap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X Y : F.PartialLeftAdjointSource} (f : X ⟶ Y),
  F.partialLeftAdjointMap f =
    F.partialLeftAdjointHomEquiv.symm
      (CategoryTheory.CategoryStruct.comp f.hom
        (F.partialLeftAdjointHomEquiv (CategoryTheory.CategoryStruct.id (F.partialLeftAdjointObj Y))))
-- Mathlib.Algebra.Divisibility.Units
/-- `x` and `y` are relatively prime if every common divisor is a unit.  -/
IsRelPrime : {α : Type u_1} → [Monoid α] → α → α → Prop
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Complex.hasDerivAt_Gammaℂ_one : HasDerivAt Complex.Gammaℂ (-(↑Real.eulerMascheroniConstant + Complex.log (2 * ↑Real.pi)) / ↑Real.pi) 1
-- Mathlib.Order.Heyting.Basic
PUnit.inf_eq : ∀ (a b : PUnit.{u + 1}), min a b = PUnit.unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {l : List α} {k : α}, k ∈ t → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKey! k = t.getKey! k
-- Mathlib.Order.Bounds.Basic
upperBounds_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → upperBounds (Set.Ioc a b) = Set.Ici b
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
/-- The multiplicity of an irreducible factor of a nonzero element is exactly the number of times
the normalized factor occurs in the `normalizedFactors`.

For a version using `multiplicity`, see `multiplicity_eq_count_normalizedFactors`.

See also `count_normalizedFactors_eq` which expands the definition of `multiplicity`
to produce a specification for `count (normalizedFactors _) _`..
 -/
UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  [inst_3 : DecidableEq R] {a b : R},
  Irreducible a →
    b ≠ 0 → emultiplicity a b = ↑(Multiset.count (normalize a) (UniqueFactorizationMonoid.normalizedFactors b))
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.instIsStrictlySupportedStupidTrunc_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c')
  [inst_3 : e.IsRelIff] {ι'' : Type u_4} {c'' : ComplexShape ι''} (e' : c''.Embedding c') [K.IsStrictlySupported e'],
  (K.stupidTrunc e).IsStrictlySupported e'
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context : Type
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.uniqueDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  UniqueDiffOn 𝕜 (Set.range ↑I)