mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
/-- A finite product of functions nonnegative and monotone on `u` is monotone on `u`. See also
`MonotoneOn.finsetProd'` for the case of an ordered commutative multiplicative monoid.  -/
MonotoneOn.finsetProd : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {s : Finset ι} {γ : Type u_4} [inst_4 : Preorder γ] {u : Set γ} {f : ι → γ → R},
  (∀ i ∈ s, MonotoneOn (f i) u) → (∀ i ∈ s, ∀ x ∈ u, 0 ≤ f i x) → MonotoneOn (fun x => ∏ i ∈ s, f i x) u
-- Init.Data.Format.Instances
instToFormatArray : {α : Type u_1} → [Std.ToFormat α] → Std.ToFormat (Array α)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.refl_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A], ↑(CoalgEquiv.refl R A) = CoalgHom.id R A
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Iio_sub_Iio' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  MeasureTheory.IntegrableOn f (Set.Iio b) μ →
    MeasureTheory.IntegrableOn f (Set.Iio a) μ →
      ∫ (x : ℝ) in Set.Iio b, f x ∂μ - ∫ (x : ℝ) in Set.Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
-- Init.Data.Sum.Lemmas
Sum.LiftRel.mono_left : ∀ {α : Type u_1} {α_1 : Type u_2} {r₁ r₂ : α → α_1 → Prop} {β : Type u_3} {β_1 : Type u_4} {s : β → β_1 → Prop}
  {x : α ⊕ β} {y : α_1 ⊕ β_1}, (∀ (a : α) (b : α_1), r₁ a b → r₂ a b) → Sum.LiftRel r₁ s x y → Sum.LiftRel r₂ s x y
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- A family of power series converges iff it converges coefficientwise  -/
MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_3}
  (f : ι → MvPowerSeries σ R) (u : Filter ι) (g : MvPowerSeries σ R),
  Filter.Tendsto f u (nhds g) ↔
    ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (MvPowerSeries.coeff d) (f i)) u (nhds ((MvPowerSeries.coeff d) g))
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.intersperseTR.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (x : α) → motive [x])
  (h_3 : (x y : α) → (xs : List α) → motive (x :: y :: xs)),
  (match [] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: xs => h_3 x y xs) =
    h_1 ()
-- Mathlib.LinearAlgebra.DFinsupp
AddSubmonoid.comap.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f f_1 : F),
  f = f_1 → ∀ (S S_1 : AddSubmonoid N), S = S_1 → AddSubmonoid.comap f S = AddSubmonoid.comap f_1 S_1
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_tensorHom : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C}
  [inst_3 : X₂.HasTensor X₃] [inst_4 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_5 : Y₂.HasTensor Y₃] [inst_6 : Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)]
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ f₃) j) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (f₁ i₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (f₂ i₂) (f₃ i₃)))
      (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.collectParams : {pu : Lean.Compiler.LCNF.Purity} → Array (Lean.Compiler.LCNF.Param pu) → Lean.FVarIdHashSet → Lean.FVarIdHashSet
-- Mathlib.LinearAlgebra.Orientation
Orientation.map_apply : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  (ι : Type u_4) (e : M ≃ₗ[R] N) (v : M [⋀^ι]→ₗ[R] R) (hv : v ≠ 0),
  (Orientation.map ι e) (rayOfNeZero R v hv) = rayOfNeZero R (v.compLinearMap ↑e.symm) ⋯
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.version.getMajor : Unit → ℕ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.zero_def : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  0 = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.sub_mem_sup : ∀ {R' : Type u_4} {M' : Type u_5} [inst : Ring R'] [inst_1 : AddCommGroup M'] [inst_2 : Module R' M']
  {S T : Submodule R' M'} {s t : M'}, s ∈ S → t ∈ T → s - t ∈ S ⊔ T
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isZero_of_isStrictlyGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n i : ℤ),
  autoParam (i < n) CochainComplex.isZero_of_isStrictlyGE._auto_1 →
    ∀ [K.IsStrictlyGE n], CategoryTheory.Limits.IsZero (K.X i)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The information needed for doing a grewrite.  -/
Mathlib.Tactic.ClickSuggestions.GrwInfo : Type
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- The first two terms of the Taylor expansion of `det (1 + r • M)` at `r = 0`.  -/
Matrix.det_one_add_smul : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (r : R)
  (M : Matrix n n R),
  (1 + r • M).det = 1 + M.trace * r + Polynomial.eval r (1 + Polynomial.X • M.map ⇑Polynomial.C).det.divX.divX * r ^ 2
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.append_blocks : ∀ {n m : ℕ} (c₁ : Composition m) (c₂ : Composition n), (c₁.append c₂).blocks = c₁.blocks ++ c₂.blocks
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instPartialOrder : {M : Type u_1} → [inst : AddZeroClass M] → PartialOrder (SaturatedAddSubmonoid M)
-- Mathlib.Computability.Partrec
Computable.bind_decode_iff : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → Option σ}, (Computable₂ fun a n => (Encodable.decode n).bind (f a)) ↔ Computable₂ f
-- Lean.LocalContext
Lean.instInhabitedLocalDeclKind : Inhabited Lean.LocalDeclKind
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_iff_lt_colLen : ∀ {μ : YoungDiagram} {i j : ℕ}, (i, j) ∈ μ ↔ i < μ.colLen j
-- Mathlib.Data.Finite.Perm
Equiv.Perm.isCyclic_of_card_le_two : ∀ {α : Type u_1} [Finite α], Nat.card α ≤ 2 → IsCyclic (Equiv.Perm α)
-- Mathlib.Data.List.MinMax
List.le_max_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] {l : List α} {a x : α},
  x ∈ l → a ≤ x → a ≤ List.foldr max ⊥ l
-- Mathlib.Util.SleepHeartbeats
/-- A low level command to sleep for at least a given number of heartbeats by running in a loop
until the desired number of heartbeats is hit.
Warning: this function relies on interpreter / compiler
behaviour that is not guaranteed to function in the way that is relied upon here.
As such this function is not to be considered reliable, especially after future updates to Lean.
This should be used with caution and basically only for demo / testing purposes
and not in compiled code without further testing.  -/
sleepAtLeastHeartbeats : ℕ → IO Unit
-- Init.Grind.AC
Lean.Grind.AC.Expr.var : Lean.Grind.AC.Var → Lean.Grind.AC.Expr
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Weighted generalized mean inequality, version for sums over finite sets, with `ℝ≥0`-valued
functions and real exponents.  -/
NNReal.rpow_arith_mean_le_arith_mean_rpow : ∀ {ι : Type u} (s : Finset ι) (w z : ι → NNReal),
  ∑ i ∈ s, w i = 1 → ∀ {p : ℝ}, 1 ≤ p → (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.coe_lmapDomain : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_9} (f : α → α'), ⇑(Finsupp.lmapDomain M R f) = Finsupp.mapDomain f
-- Mathlib.Tactic.Widget.SelectPanelUtils
SelectInsertParams.mk.inj : ∀ {pos : Lean.Lsp.Position} {goals : Array Lean.Widget.InteractiveGoal}
  {selectedLocations : Array Lean.SubExpr.GoalsLocation} {replaceRange : Lean.Lsp.Range} {pos_1 : Lean.Lsp.Position}
  {goals_1 : Array Lean.Widget.InteractiveGoal} {selectedLocations_1 : Array Lean.SubExpr.GoalsLocation}
  {replaceRange_1 : Lean.Lsp.Range},
  { pos := pos, goals := goals, selectedLocations := selectedLocations, replaceRange := replaceRange } =
      { pos := pos_1, goals := goals_1, selectedLocations := selectedLocations_1, replaceRange := replaceRange_1 } →
    pos = pos_1 ∧ goals = goals_1 ∧ selectedLocations = selectedLocations_1 ∧ replaceRange = replaceRange_1
-- Init.Data.Nat.Lemmas
Nat.lt_iff_le_pred : ∀ {m n : ℕ}, 0 < n → (m < n ↔ m ≤ n - 1)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.closure_eq_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I X → M.closure I = M.closure X
-- Mathlib.Topology.Separation.Basic
CofiniteTopology.continuous_of : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], Continuous ⇑CofiniteTopology.of
-- Lean.Elab.Util
/-- If `x` throws an exception, catch it and turn it into a log message (using `logException`).
 -/
Lean.Elab.withLogging : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [MonadExcept Lean.Exception m] →
        [Lean.AddMessageContext m] → [Lean.MonadOptions m] → [MonadLiftT IO m] → m Unit → m Unit
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_associator_inv_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X
        (CategoryTheory.CategoryStruct.id
                (Opposite.op
                  (CategoryTheory.Comon.MonOpOpToComonObj
                      (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.ComonToMonOpOpObj
                        Z.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.CategoryStruct.id
                  (Opposite.op
                    (CategoryTheory.Comon.MonOpOpToComonObj
                        (CategoryTheory.MonoidalCategoryStruct.tensorObj X.ComonToMonOpOpObj
                          Y.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop
          Z.X))
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isCodetecting_bot_of_isGroupoid : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsGroupoid C], ⊥.IsCodetecting
-- Lean.Environment
_private.Lean.Environment.0.Lean.registerEnvExtension.unsafe_1 : {σ : Type} → Lean.EnvExtension σ → Lean.EnvExtension Lean.EnvExtensionState
-- Mathlib.Topology.Convenient.Category
/-- The functor `TopCat.{v} ⥤ GeneratedByTopCat X`.  -/
TopCat.toGeneratedByTopCat : {ι : Type t} →
  {X : ι → Type u} → [inst : (i : ι) → TopologicalSpace (X i)] → CategoryTheory.Functor TopCat (GeneratedByTopCat X)
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
_private.Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives.0.HomotopyCategory.Plus.isRightDerivabilityStructure.instGuitartExactPlusInjectiveObjectHomFunctorIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.TwoSquare.GuitartExact (HomotopyCategory.Plus.isRightDerivabilityStructure.iso✝ C).hom
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.cancel_left : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} {g : ℬ →+*ᵍ 𝒞} {f₁ f₂ : 𝒜 →+*ᵍ ℬ},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Order.Lattice.Congruence
Setoid.ker.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Setoid.ker f = { r := Function.onFun (fun x1 x2 => x1 = x2) f, iseqv := ⋯ }
-- Mathlib.RingTheory.IsTensorProduct
instIsPushout : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsPushout R R S S
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_union : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (S R : CategoryTheory.Sieve (F.obj X)),
  CategoryTheory.Sieve.functorPullback F (S ⊔ R) =
    CategoryTheory.Sieve.functorPullback F S ⊔ CategoryTheory.Sieve.functorPullback F R
-- Mathlib.CategoryTheory.Category.Pairwise
/-- A helper tactic for `cat_disch` and `CategoryTheory.Pairwise`.  -/
CategoryTheory.Pairwise.pairwiseCases : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Premise.const.injEq : ∀ (declName declName_1 : Lean.Name),
  (Mathlib.Tactic.ClickSuggestions.Premise.const declName = Mathlib.Tactic.ClickSuggestions.Premise.const declName_1) =
    (declName = declName_1)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.add : {R : Type u_1} → {X : Type u_2} → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X
-- Lean.Meta.Sym.AbstractS
/-- Helper function for implementing `abstractFVars` (and possible variants in the future).
 -/
_private.Lean.Meta.Sym.AbstractS.0.Lean.Meta.Sym.abstractFVarsCore : Lean.Expr →
  Lean.LocalContext →
    Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.FVarId) →
      Lean.FVarId → (Lean.FVarId → Option ℕ) → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instConcreteCategoryIntertwiningMapVρ : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] →
      [inst_1 : Monoid G] → CategoryTheory.ConcreteCategory (Rep.{w, u, v} k G) fun A B => A.ρ.IntertwiningMap B.ρ
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.unbox.injEq : ∀ (x x_1 : Lean.IR.VarId), (Lean.IR.Expr.unbox x = Lean.IR.Expr.unbox x_1) = (x = x_1)
-- Mathlib.CategoryTheory.Category.Cat
/-- See through the defeq `objects.obj X = X`.  -/
CategoryTheory.Cat.instCategoryObjObjects : (X : CategoryTheory.Cat) → CategoryTheory.Category.{v, u} (CategoryTheory.Cat.objects.obj X)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.zero_def : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] [inst_3 : Zero X], 0 = 0 -ₒ 0
-- Lean.Meta.Tactic.Subst
Lean.Meta.trySubst : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId
-- Init.Data.SInt.Lemmas
Int32.le_of_lt : ∀ {a b : Int32}, a < b → a ≤ b
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mulEquiv_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {R' : Type u_3} [inst_2 : CommRing R'] [inst_3 : IsDomain R']
  (g : R ≃+* R') (a : ClassGroup R),
  (ClassGroup.mulEquiv g) a =
    (ClassGroup.equiv (FractionRing R')).symm
      ((QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R' (FractionRing R')).range
          (Units.mapEquiv ↑(FractionalIdeal.ringEquivOfRingEquiv (FractionRing R) (FractionRing R') g)) ⋯)
        ((ClassGroup.equiv (FractionRing R)) a))
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.symm_functor : ∀ {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] (e : CategoryTheory.IsoCat C D), e.symm.functor = e.inverse
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
/-- The set of quasi-finite points of a morphism `f : X ⟶ Y` as an `X.Opens`.  -/
AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [AlgebraicGeometry.LocallyOfFiniteType f] → X.Opens
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (p : P.ColimitOfShape J X) (j : J),
  p.toCostructuredArrow.obj j = CategoryTheory.CostructuredArrow.mk (p.ι.app j)
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- If `f` is meromorphic on an open set `U`, if `f` is nowhere locally constant zero, and if the
support of the divisor of `f` is finite, then there exists an analytic function `g` on `U` without
zeros such that `f` is equivalent, modulo equality on codiscrete sets, to the product of `g` and the
factorized rational function associated with the divisor of `f`.
 -/
MeromorphicOn.extract_zeros_poles : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  MeromorphicOn f U →
    (∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤) →
      (MeromorphicOn.divisor f U).support.Finite →
        ∃ g,
          AnalyticOnNhd 𝕜 g U ∧
            (∀ (u : ↑U), g ↑u ≠ 0) ∧
              f =ᶠ[Filter.codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x => x - u) ^ (MeromorphicOn.divisor f U) u) • g
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_isoCycles₁_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ 1) (groupHomology.isoCycles₁ B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).hom (groupHomology.mapCycles₁ f φ)
-- Mathlib.Algebra.Module.Submodule.Finsupp
/-- A subset of a ring `R` has a multiplicative action on submodules of a module over `R`.  -/
Submodule.pointwiseSetMulAction : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [SMulCommClass R R M] → MulAction (Set R) (Submodule R M)
-- Mathlib.Algebra.GCDMonoid.Nat
Int.natAbs_gcd : ∀ (i j : ℤ), (gcd i j).natAbs = i.gcd j
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- When `f` is bilinear then `Matrix.kroneckerMap f` is also bilinear.  -/
Matrix.kroneckerMapBilinear : {R : Type u_1} →
  {S : Type u_2} →
    {α : Type u_3} →
      {β : Type u_5} →
        {γ : Type u_7} →
          {l : Type u_9} →
            {m : Type u_10} →
              {n : Type u_11} →
                {p : Type u_12} →
                  [inst : Semiring S] →
                    [inst_1 : Semiring R] →
                      [inst_2 : AddCommMonoid α] →
                        [inst_3 : AddCommMonoid β] →
                          [inst_4 : AddCommMonoid γ] →
                            [inst_5 : Module R α] →
                              [inst_6 : Module R γ] →
                                [inst_7 : Module S β] →
                                  [inst_8 : Module S γ] →
                                    [inst_9 : SMulCommClass S R γ] →
                                      (α →ₗ[R] β →ₗ[S] γ) →
                                        Matrix l m α →ₗ[R] Matrix n p β →ₗ[S] Matrix (l × n) (m × p) γ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_induce : ∀ {V : Type u} {G : SimpleGraph V} {s : Set V} {u v : V} (w : G.Walk u v) (hw : ∀ x ∈ w.support, x ∈ s),
  SimpleGraph.Walk.map (SimpleGraph.Embedding.induce s).toHom (SimpleGraph.Walk.induce s w hw) = w
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- Homeomorphism between prime spectra induced by an isomorphism of semirings.  -/
PrimeSpectrum.homeomorphOfRingEquiv : {R : Type u} →
  {S : Type v} → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → R ≃+* S → PrimeSpectrum R ≃ₜ PrimeSpectrum S
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.refl_mem_transvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  LinearEquiv.refl R V ∈ LinearEquiv.transvections R V
-- Mathlib.Algebra.Order.Group.Abs
abs_min_le_max_abs_abs : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] {a b : G}, |min a b| ≤ max |a| |b|
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
instPseudoMetricSpaceNNReal : PseudoMetricSpace NNReal
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β},
  m.WF →
    (Std.DHashMap.Raw.Const.modify m k f).getKey? k' =
      if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instR0Space : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [R0Space R], R0Space (ContinuousMapZero X R)
-- Mathlib.Analysis.Convex.BetweenList
List.SortedLE.wbtw : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {l : List R},
  l.SortedLE → List.Wbtw R l
-- Mathlib.CategoryTheory.Limits.ColimitLimit
/-- The universal morphism
$\colim_k \lim_j F(j,k) → \lim_j \colim_k F(j, k)$.
 -/
CategoryTheory.Limits.colimitLimitToLimitColimit : {J : Type u₁} →
  {K : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} J] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            (F : CategoryTheory.Functor (J × K) C) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
                [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                  CategoryTheory.Limits.colimit
                      ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp
                        CategoryTheory.Limits.lim) ⟶
                    CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim)
-- Init.Data.List.Find
List.find?_isSome : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, (List.find? p xs).isSome = true ↔ ∃ x ∈ xs, p x = true
-- Mathlib.Order.Filter.Defs
Filter.le_def : ∀ {α : Type u_1} {f g : Filter α}, f ≤ g ↔ ∀ x ∈ g, x ∈ f
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- If `f` and `f'` are two isomorphic morphisms, and `f` is a transfinite composition
of shape `J`, then `f'` also is.  -/
CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  CategoryTheory.TransfiniteCompositionOfShape J f →
                    {X' Y' : C} →
                      {f' : X' ⟶ Y'} →
                        (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') →
                          CategoryTheory.TransfiniteCompositionOfShape J f'