mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfConeEquiv_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C},
  CategoryTheory.Limits.coconeRightOpOfConeEquiv.counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeRightOp c),
            map := fun {X Y} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun c => CategoryTheory.Limits.coconeRightOpOfCone (Opposite.unop c),
          map := fun {X Y} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f))
      (CategoryTheory.ChosenPullbacksAlong.snd R.hom T.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom)
      (CategoryTheory.Over.Hom.left f)
-- Init.Data.List.Lemmas
List.foldlM_append : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [LawfulMonad m] {f : β → α → m β} {b : β}
  {l l' : List α},
  List.foldlM f b (l ++ l') = do
    let init ← List.foldlM f b l
    List.foldlM f init l'
-- Mathlib.RingTheory.Smooth.IntegralClosure
/-- Localization preserves integral closure.  -/
TensorProduct.toIntegralClosure_bijective_of_isLocalization : ∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (M : Submonoid R) [IsLocalization M S],
  Function.Bijective ⇑(TensorProduct.toIntegralClosure R S B)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_insertMany_list_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)}, (t.insertMany l).size ≤ t.size + l.length
-- Mathlib.NumberTheory.NumberField.CMField
/-- A totally complex abelian extension of `ℚ` is CM.
 -/
NumberField.IsCMField.of_isAbelianGalois : ∀ (K : Type u_2) [inst : Field K] [inst_1 : CharZero K] [Algebra.IsIntegral ℚ K] [NumberField.IsTotallyComplex K]
  [IsAbelianGalois ℚ K], NumberField.IsCMField K
-- Mathlib.Tactic.FunProp.FunctionData
/-- Get `FunctionData` for `f`. Throws if `f` can't be put into funProp-normal form.  -/
Mathlib.Meta.FunProp.getFunctionData : Lean.Expr → Lean.MetaM Mathlib.Meta.FunProp.FunctionData
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forM_eq_forM_toArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit.{w + 1}},
  Std.DHashMap.forM f m = Array.forM (fun a => f a.fst a.snd) m.toArray
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.centerCongr_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] (e : R ≃+* S)
  (r : ↥(Subsemigroup.center R)), ↑((NonUnitalSubsemiring.centerCongr e) r) = e ↑r
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv.eq_1 : ∀ {α : Type u_2} [inst : Inv α], Set.inv = { inv := Set.preimage Inv.inv }
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexMap._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexMap._auto_3),
  (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (X.H n₀).map (CategoryTheory.ComposableArrows.homMk₁ (α.app 2) (α.app 3) ⋯)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- An open normal additive subgroup of a compact topological additive group has finite index.  -/
OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [CompactSpace G] → [ContinuousAdd G] → OpenNormalAddSubgroup G → FiniteIndexNormalAddSubgroup G
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsRevMatch.ne_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat pos → pos ≠ s.endPos
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All n-simplices among cospherical points in an n-dimensional
subspace have the same circumcenter.  -/
EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
  ps ⊆ ↑s →
    ∀ [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction],
      Module.finrank ℝ ↥s.direction = n →
        EuclideanGeometry.Cospherical ps →
          ∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
-- Mathlib.Analysis.BoundedVariation
/-- Eta-expanded form of `LocallyBoundedVariationOn.smul` -/
LocallyBoundedVariationOn.fun_smul : ∀ {α : Type u_2} [inst : LinearOrder α] {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [inst_3 : NormedRing 𝕜] [inst_4 : NormedAlgebra ℝ 𝕜] [inst_5 : Module 𝕜 F]
  [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {s : Set α},
  LocallyBoundedVariationOn f s → LocallyBoundedVariationOn g s → LocallyBoundedVariationOn (fun i => f i • g i) s
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- An intermediate field `S` is finitely generated if there exists `t : Finset E` such that
`IntermediateField.adjoin F t = S`.

We use the class `Algebra.EssFiniteType F E` instead of `(⊤ : IntermediateField F E).FG` to say that
`E` is finitely generated as an `F` extension.
See `IntermediateField.fg_top_iff`.  -/
IntermediateField.FG : {F : Type u_1} →
  [inst : Field F] → {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E → Prop
-- Mathlib.Topology.Order.PartialSups
Filter.Tendsto.partialSups_apply : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {α : Type u_2} {l : Filter α}
  {f : ℕ → α → L} {g : ℕ → L} {n : ℕ},
  (∀ k ≤ n, Filter.Tendsto (f k) l (nhds (g k))) →
    Filter.Tendsto (fun a => (partialSups fun x => f x a) n) l (nhds ((partialSups g) n))
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.Context.commonMCtx? : Aesop.EqualUpToIdsM.Context → Option Lean.MetavarContext
-- Mathlib.Analysis.Distribution.TestFunction
/-- Reformulation of the universal property of the topology on `𝓓^{n}(Ω, F)`, in the form of a
custom constructor for continuous linear maps `𝓓^{n}(Ω, F) →L[𝕜] V`, where `V` is an arbitrary
locally convex topological vector space. See also `limitCLM`.  -/
TestFunction.mkCLM : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω : TopologicalSpace.Opens E} →
            {F : Type u_4} →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    {n : ℕ∞} →
                      {V : Type u_6} →
                        [inst_6 : AddCommGroup V] →
                          [inst_7 : Module ℝ V] →
                            [t : TopologicalSpace V] →
                              [IsTopologicalAddGroup V] →
                                [ContinuousSMul ℝ V] →
                                  [LocallyConvexSpace ℝ V] →
                                    [inst_11 : Algebra ℝ 𝕜] →
                                      [inst_12 : IsScalarTower ℝ 𝕜 F] →
                                        [inst_13 : Module 𝕜 V] →
                                          [IsScalarTower ℝ 𝕜 V] →
                                            (toFun : TestFunction Ω F n → V) →
                                              (∀ (f g : TestFunction Ω F n), toFun (f + g) = toFun f + toFun g) →
                                                (∀ (c : 𝕜) (f : TestFunction Ω F n), toFun (c • f) = c • toFun f) →
                                                  (∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω),
                                                      Continuous (toFun ∘ TestFunction.ofSupportedIn K_sub_Ω)) →
                                                    TestFunction Ω F n →L[𝕜] V
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.foldlM_filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.mk.injEq : ∀ {X Y : TopPair} {f g : X ⟶ Y} (fst : TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g))
  (snd : TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g))
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
          fst.h =
        CategoryTheory.CategoryStruct.comp snd.h TopPair.map)
      TopPair.Homotopy.w._autoParam)
  (fst_1 : TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g))
  (snd_1 : TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g))
  (w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
          fst_1.h =
        CategoryTheory.CategoryStruct.comp snd_1.h TopPair.map)
      TopPair.Homotopy.w._autoParam),
  ({ fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := w_1 }) = (fst = fst_1 ∧ snd = snd_1)
-- Mathlib.Topology.Compactification.OnePoint.Basic
_private.Mathlib.Topology.Compactification.OnePoint.Basic.0.instReprOnePoint.match_1.eq_2 : ∀ {X : Type u_1} (motive : OnePoint X → Sort u_2) (a : X) (h_1 : Unit → motive none) (h_2 : (a : X) → motive (some a)),
  (match some a with
    | none => h_1 ()
    | some a => h_2 a) =
    h_2 a
-- Mathlib.Data.Option.Basic
Option.iget_mem : ∀ {α : Type u_1} [inst : Inhabited α] {o : Option α}, o.isSome = true → o.iget ∈ o
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (x : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote ctx x =
    match x with
    | Lean.Grind.CommRing.Mon.unit => 1
    | Lean.Grind.CommRing.Mon.mult p m => Lean.Grind.CommRing.Power.denote ctx p * Lean.Grind.CommRing.Mon.denote ctx m
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {km fallback : α}, t.maxD fallback = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Topology.Order.Bornology
Nonempty.of_isOrderBornology : ∀ (α : Type u_1) [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α], Nonempty α
-- Lean.AuxRecursor
/-- Is this a `.casesOn`, a constructor elimination or a sparse casesOn?  -/
Lean.isCasesOnLike : Lean.Environment → Lean.Name → Bool
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
/-- Local homeomorphism between a real (semi)normed space and the unit ball.
See also `Homeomorph.unitBall`.  -/
OpenPartialHomeomorph.univUnitBall : {E : Type u_1} → [inst : SeminormedAddCommGroup E] → [NormedSpace ℝ E] → OpenPartialHomeomorph E E
-- Mathlib.Data.Sym.Basic
Sym.val_eq_coe : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n), ↑s = ↑s
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.div_closure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s : Set G},
  IsOpen s → ∀ (t : Set G), s / closure t = s / t
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.infiniteTheory.eq_1 : ∀ (L : FirstOrder.Language), L.infiniteTheory = Set.range (FirstOrder.Language.Sentence.cardGe L)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.right_unitor_inv_hom : ∀ {B : Type u} [inst : Quiver B] {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f).vcomp (CategoryTheory.FreeBicategory.Hom₂.right_unitor f))
    (CategoryTheory.FreeBicategory.Hom₂.id f)
-- Lean.Linter.UnusedVariables
/-- Since declarations attach the declaration info to the `declId`,
we skip that to get to the `.ident` if possible.  -/
_private.Lean.Linter.UnusedVariables.0.Lean.Linter.UnusedVariables.collectReferences.skipDeclIdIfPresent : Lean.Syntax → Lean.Syntax
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.bayesRisk_zero_right : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} [Nonempty 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧),
  ProbabilityTheory.bayesRisk ℓ P 0 = 0
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_lt : ∀ (x : Int32), x.toNatClampNeg < 2 ^ 31
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isNone_max?_eq_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp], t.WF → t.max?.isNone = t.isEmpty
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
/-- **Alias** of the reverse direction of `Matrix.charmatrix_blockTriangular_iff`. -/
Matrix.BlockTriangular.charmatrix : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {α : Type u_5}
  [inst_3 : Preorder α] {M : Matrix n n R} {b : n → α}, M.BlockTriangular b → M.charmatrix.BlockTriangular b
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
dropping the augmentation corresponds to precomposition with
`inclusion : SimplexCategory ⥤ AugmentedSimplexCategory`.  -/
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.comp
        CategoryTheory.CosimplicialObject.Augmented.drop ≅
      (CategoryTheory.Functor.whiskeringLeft SimplexCategory AugmentedSimplexCategory C).obj
        AugmentedSimplexCategory.inclusion
-- Mathlib.RingTheory.Artinian.Module
instIsArtinianRingMatrix : ∀ (n : Type u_1) (R : Type u_2) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Ring R] [IsArtinianRing R],
  IsArtinianRing (Matrix n n R)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_univ_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (n : ℕ) (a : α) (x : γ) (seq : ℕ → Set β),
  Monotone seq →
    ⋃ i, seq i = Set.univ →
      Filter.Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) Filter.atTop
        (nhds (κ.densityProcess κ.fst n a x Set.univ))
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.elabGrindPattern.elabCnstrRHS : Array Lean.Expr → Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.Meta.Grind.CnstrRHS
-- Mathlib.Analysis.Analytic.CPolynomial
CPolynomialAt_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {v : F},
  CPolynomialAt 𝕜 (fun x => v) x
-- Lean.MetavarContext
/-- Add a delayed assignment for the given metavariable. You must make sure that
the metavariable is not already assigned or delayed-assigned.
 -/
Lean.assignDelayedMVar : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → Array Lean.Expr → Lean.MVarId → m Unit
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
is smaller than all elements of `s`, and that this is not the case of any `w>b`.
See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices.  -/
DirectedOn.csInf_eq_of_forall_ge_of_forall_gt_exists_lt : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {b : α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b
-- Batteries.Data.List.Perm
/-- `Perm.idxBij` is a bijective map from `Fin xs.length` to `Fin ys.length`
which exists when we have `xs.Perm ys`: conceptually it represents a permuting of
one list into the other. For example:
```
(by decide : [0, 1, 1, 3, 5] ~ [5, 0, 1, 3, 1]).idxBij 2 = 4
```
 -/
List.Perm.idxBij : {α : Type u_1} → [inst : BEq α] → [ReflBEq α] → {xs ys : List α} → xs.Perm ys → Fin xs.length → Fin ys.length
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.map_zero₂ : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y : N), (f 0) y = 0
-- Lean.Level
Lean.Level.succ : Lean.Level → Lean.Level
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂)[k]? = none
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- A `ConditionallyCompleteLinearOrder` is total.  -/
ConditionallyCompleteLinearOrder.le_total : ∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_div_rnDeriv_eq_div_rnDeriv_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ξ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ξ],
  μ.AbsolutelyContinuous ξ →
    ν.AbsolutelyContinuous ξ →
      (fun x => μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun x => μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero_mul : ∀ (R₁ R₂ θ₁ θ₂ : ℝ), circleMap 0 R₁ θ₁ * circleMap 0 R₂ θ₂ = circleMap 0 (R₁ * R₂) (θ₁ + θ₂)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap'_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData)
  (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData),
  CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ₁ h₁ h₂)
      (CategoryTheory.ShortComplex.opcyclesMap' φ₂ h₂ h₃)
-- Mathlib.Algebra.Group.Conj
ConjClasses.quot_mk_eq_mk : ∀ {α : Type u} [inst : Monoid α] (a : α), Quot.mk (⇑(IsConj.setoid α)) a = ConjClasses.mk a
-- Mathlib.Geometry.Euclidean.Projection
/-- `p` is equidistant from a set of points in `s` if and only if its
`orthogonalProjection` is.  -/
EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {ps : Set P},
  ps ⊆ ↑s →
    ∀ (p : P),
      (ps.Pairwise fun p₁ p₂ => dist p₁ p = dist p₂ p) ↔
        ps.Pairwise fun p₁ p₂ =>
          dist p₁ ↑((EuclideanGeometry.orthogonalProjection s) p) =
            dist p₂ ↑((EuclideanGeometry.orthogonalProjection s) p)
-- Mathlib.Algebra.Opposites
AddOpposite.unop_eq_one_iff : ∀ {α : Type u_1} [inst : One α] {a : αᵃᵒᵖ}, AddOpposite.unop a = 1 ↔ a = 1
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCodetector.hasDetector_of_hasCodetector_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.HasCodetector Cᵒᵖ],
  CategoryTheory.HasDetector C
-- Mathlib.Topology.Connected.TotallyDisconnected
Pi.totallyDisconnectedSpace : ∀ {α : Type u_3} {β : α → Type u_4} [inst : (a : α) → TopologicalSpace (β a)]
  [∀ (a : α), TotallyDisconnectedSpace (β a)], TotallyDisconnectedSpace ((a : α) → β a)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instInhabited : {D : Type u_1} → {Q : Type u_2} → [Group D] → [Group Q] → Inhabited (D ≀ᵣ Q)
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.of_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace Y]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Z],
  Topology.IsInducing g → (Topology.IsInducing (g ∘ f) ↔ Topology.IsInducing f)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddGroup.toAddGroup : {E : Type u_8} → [self : SeminormedAddGroup E] → AddGroup E
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationProps : Type
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaObjObjEquiv_obj_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ}
  {Y Y' : C} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y) {Z : C} (h : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.shrinkCoyonedaObjObjEquiv
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).map g)) f))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv f)
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The Eisenstein series as a function on lattices.
It takes `L` to the sum `∑ l⁻ʳ` over `l ∈ L`.
TODO: Establish connections with the `ModularForm` library.  -/
PeriodPair.G : PeriodPair → ℕ → ℂ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.isLeftRegular : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] {a : α}, MulLECancellable a → IsLeftRegular a
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Given a $C^n$ time-dependent vector field `f` and a $C^n$ curve `α`, the composition `f t (α t)`
is $C^n$ in `t`.  -/
ODE.contDiffOn_comp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {s : Set ℝ}
  {u : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n (Function.uncurry f) (s ×ˢ u) →
    ContDiffOn ℝ n α s → (∀ t ∈ s, α t ∈ u) → ContDiffOn ℝ n (fun t => f t (α t)) s
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.unop} (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op