mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_div_of_nonneg_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  a ≤ b → 0 ≤ c → a / c ≤ b / c
-- Mathlib.Data.ENNReal.BigOperators
/-- **Alias** of `ENNReal.ofNNReal_finsetSum`. -/
ENNReal.coe_finset_sum : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Init.Omega.IntList
Lean.Omega.IntList.set_cons_zero : ∀ {x : ℤ} {xs : List ℤ} {y : ℤ}, Lean.Omega.IntList.set (x :: xs) 0 y = y :: xs
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- a map on indices  -/
TotalComplexShape.π : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) → (c₁₂ : ComplexShape I₁₂) → [self : TotalComplexShape c₁ c₂ c₁₂] → I₁ × I₂ → I₁₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_filter_key_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.DTreeMap.filter (fun a x => f a) t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f (t.getKey k h) = true
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.opEquiv_apply : ∀ {M : Type u_2} [inst : AddZeroClass M] (x : AddSubmonoid M), AddSubmonoid.opEquiv x = x.op
-- Lean.Meta.Tactic.Grind.Proof
/-- Returns a proof that `a = b`.
It assumes `a` and `b` are in the same equivalence class.
 -/
Lean.Meta.Grind.mkEqProofImpl : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- Serre derivative of weight $k$.
 -/
Derivative.serreDerivative : ℂ → (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.umod_congr : ∀ {w : ℕ} (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → lhs' % rhs' = lhs % rhs
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.instQuasiCompactOfUniversallyClosed : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.UniversallyClosed f], AlgebraicGeometry.QuasiCompact f
-- Mathlib.Computability.NFA
NFA.mk : {α : Type u} → {σ : Type v} → (σ → α → Set σ) → Set σ → Set σ → NFA α σ
-- Mathlib.Order.Interval.Lex
NonemptyInterval.instPreorderLex : {α : Type u_1} → [inst : Preorder α] → Preorder (Lex (NonemptyInterval α))
-- Mathlib.RingTheory.HahnSeries.Lex
/-- The inverse of `finiteArchimedeanClassOrderHomLex`.  -/
HahnSeries.finiteArchimedeanClassOrderHomInvLex : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : LinearOrder Γ] →
      [inst_1 : LinearOrder R] →
        [inst_2 : AddCommGroup R] →
          [inst_3 : IsOrderedAddMonoid R] →
            Lex (Γ × FiniteArchimedeanClass R) →o FiniteArchimedeanClass (Lex (HahnSeries Γ R))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion 0 = 0
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.mateEquiv_leftUnitor_hom_rightUnitor_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {l : a ⟶ b} {r : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction l r),
  (CategoryTheory.Bicategory.mateEquiv adj adj)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor l).hom
        (CategoryTheory.Bicategory.rightUnitor l).inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor r).hom
      (CategoryTheory.Bicategory.leftUnitor r).inv
-- Mathlib.Analysis.Convex.Function
ConvexOn.le_left_of_right_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ openSegment 𝕜 x y → f y ≤ f z → f z ≤ f x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Bot.isAddCyclic : ∀ {α : Type u_1} [inst : AddGroup α], IsAddCyclic ↥⊥
-- Mathlib.Analysis.Complex.Trigonometric
_private.Mathlib.Analysis.Complex.Trigonometric.0.Complex.sinh_add_aux : ∀ {a b c d : ℂ}, (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d)
-- Init.Data.BitVec.Lemmas
BitVec.mul_sub : ∀ {w : ℕ} {x y z : BitVec w}, x * (y - z) = x * y - x * z
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The glue data of presheafed spaces associated to a family of glue data of sheafed spaces.  -/
AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    AlgebraicGeometry.SheafedSpace.GlueData C → AlgebraicGeometry.PresheafedSpace.GlueData C
-- Mathlib.Order.SuccPred.CompleteLinearOrder
csSup_mem_of_not_isSuccLimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α},
  s.Nonempty → BddAbove s → ¬Order.IsSuccLimit (sSup s) → sSup s ∈ s
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_subset_Ico_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ici a ⊆ Set.Ico a b ∪ Set.Ici b
-- Mathlib.MeasureTheory.Integral.Layercake
/-- An auxiliary version of the layer cake formula (Cavalieri's principle, tail probability
formula), with a measurability assumption that would also essentially follow from the
integrability assumptions.
Compared to `lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite`, we remove
the sigma-finite assumption.

See `MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul` and
`MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul` for the main formulations of the layer
cake formula.  -/
MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α),
  0 ≤ f →
    Measurable f →
      (∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
        Measurable g →
          (∀ t > 0, 0 ≤ g t) →
            ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
              ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
-- Mathlib.Algebra.Order.Floor.Ring
Int.natCast_ceil_eq_ceil_of_neg_one_lt : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, -1 < a → ↑⌈a⌉₊ = ⌈a⌉
-- Mathlib.Topology.Homotopy.Path
/-- Suppose `p` is a path, then we have a homotopy from `p` to `p.reparam f` by the convexity of `I`.
 -/
Path.Homotopy.reparam : {X : Type u} →
  [inst : TopologicalSpace X] →
    {x₀ x₁ : X} →
      (p : Path x₀ x₁) →
        (f : ↑unitInterval → ↑unitInterval) →
          (hf : Continuous f) → (hf₀ : f 0 = 0) → (hf₁ : f 1 = 1) → p.Homotopy (p.reparam f hf hf₀ hf₁)
-- Mathlib.RepresentationTheory.Character
/-- The character of a representation `V : FDRep k G` is the function associating to `g : G` the
trace of the linear map `V.ρ g`.  -/
FDRep.character : {k : Type u} → [inst : Field k] → {G : Type v} → [inst_1 : Monoid G] → FDRep k G → G → k
-- Lean.Declaration
/-- `true` when recursive (that is, the inductive type appears as an argument in a constructor).  -/
Lean.InductiveVal.isRec : Lean.InductiveVal → Bool
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.toComon_obj : ∀ (R : Type u) [inst : CommRing R] (X : CoalgCat R), (CoalgCat.toComon R).obj X = X.toComonObj
-- Mathlib.Order.Filter.Extr
isExtrFilter_const : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsExtrFilter (fun x => b) l a
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instSetLike.eq_1 : ∀ (M : Type u_1) [inst : MulOneClass M],
  SaturatedSubmonoid.instSetLike M = { coe := fun x => x.carrier, coe_injective := ⋯ }
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.norm_mod_lt : ∀ (x : GaussianInt) {y : GaussianInt}, y ≠ 0 → Zsqrtd.norm (x % y) < Zsqrtd.norm y
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
/-- The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.  -/
ValuativeRel.«term𝒪[_]» : Lean.ParserDescr
-- Mathlib.Order.MinMax
min_lt_of_right_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, c < a → min b c < a
-- Init.Grind.AC
Lean.Grind.AC.superpose_ac_idempotent_cert.eq_1 : ∀ (x : Lean.Grind.AC.Var) (lhs₁ rhs₁ rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_ac_idempotent_cert x lhs₁ rhs₁ rhs =
    (lhs₁.contains_k x).and' (rhs.beq' (Lean.Grind.AC.Seq.insert x rhs₁))
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.inter : ∀ {α : Type v} {s t : Set α} [inst : LinearOrder α] [WellFoundedLT α],
  Order.cof α ≠ Cardinal.aleph0 → IsClub s → IsClub t → IsClub (s ∩ t)
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumberNat_one : ruzsaSzemerediNumberNat 1 = 0
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.spectralRadius_le_nnnorm : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [NormOneClass A] (a : A), spectralRadius 𝕜 a ≤ ↑‖a‖₊
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.windowsLineEnding.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.StyleError.windowsLineEnding✝ = 1
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- **Alias** of `IsEllipticSequence.id`. -/
isEllSequence_id : IsEllipticSequence id
-- Mathlib.Analysis.Normed.Group.Continuity
Inseparable.enorm_eq_enorm : ∀ {E : Type u_7} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] {u v : E}, Inseparable u v → ‖u‖ₑ = ‖v‖ₑ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k a : α} {v : β k},
  (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
-- Mathlib.Topology.Germ
Filter.Germ.valueMulHom.eq_1 : ∀ {X : Type u_4} {E : Type u_5} [inst : Monoid E] [inst_1 : TopologicalSpace X] {x : X},
  Filter.Germ.valueMulHom = { toFun := Filter.Germ.value, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks.0.CategoryTheory.Limits.WidePushoutShape.mkCocone.match_1.eq_2 : ∀ {J : Type u_1} (motive : CategoryTheory.Limits.WidePushoutShape J → Sort u_2) (j : J) (h_1 : Unit → motive none)
  (h_2 : (j : J) → motive (some j)),
  (match some j with
    | none => h_1 ()
    | some j => h_2 j) =
    h_2 j
-- Aesop.Stats.Basic
Aesop.ScriptGenerated : Type
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.maxKey : {α : Type u} → {β : α → Type v} → (t : Std.DTreeMap.Internal.Impl α β) → t.isEmpty = false → α
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.instCompactSpace : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [DiscreteTopology A] [ContinuousAdd B] [T2Space B] [CompactSpace B],
  CompactSpace (A →ₜ+ B)
-- Mathlib.Algebra.Quandle
/-- The `PreEnvelGroupRel` relation as a `Prop`.  Used as the relation for `PreEnvelGroup.setoid`.
 -/
Rack.PreEnvelGroupRel : (R : Type u) → [Rack R] → Rack.PreEnvelGroup R → Rack.PreEnvelGroup R → Prop
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.colon_ι_app_π_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) (X : C) {Z : C} (h : Φ.quotient.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((Φ.colon Ψ).ι.app X) (CategoryTheory.CategoryStruct.comp (Φ.π.app X) h) =
    CategoryTheory.CategoryStruct.comp ((Φ.colonπ Ψ).app X)
      (CategoryTheory.CategoryStruct.comp (Ψ.ι.app (Φ.quotient.obj X)) h)
-- Mathlib.Geometry.Manifold.ChartedSpace
coe_achart : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), ↑(achart H x) = chartAt H x
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- A charted space is a topological space endowed with an atlas, i.e., a set of local
homeomorphisms taking values in a model space `H`, called charts, such that the domains of the
charts cover the whole space. We express the covering property by choosing for each `x` a member
`chartAt x` of the atlas containing `x` in its source: in the smooth case, this is convenient to
construct the tangent bundle in an efficient way.
The model space is written as an explicit parameter as there can be several model spaces for a
given topological space. For instance, a complex manifold (modelled over `ℂ^n`) will also be seen
sometimes as a real manifold over `ℝ^(2n)`.
 -/
ChartedSpace : (H : Type u_5) → [TopologicalSpace H] → (M : Type u_6) → [TopologicalSpace M] → Type (max u_5 u_6)
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.basic : ∀ {α : Type u_2} {g : Set (Set α)} {s : Set α}, s ∈ g → Filter.CountableGenerateSets g s
-- Mathlib.Data.ZMod.Basic
ZMod.cast_zero : ∀ {n : ℕ} {R : Type u_1} [inst : AddGroupWithOne R], ZMod.cast 0 = 0
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.addLeftMono : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddMonoid N] [inst_2 : LinearOrder N]
  [AddLeftStrictMono N], AddLeftMono (Lex (α →₀ N))
-- Mathlib.Algebra.Prime.Defs
Irreducible.not_dvd_one : ∀ {M : Type u_1} [inst : CommMonoid M] {p : M}, Irreducible p → ¬p ∣ 1
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.comap_inf : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s t : NonUnitalSubsemiring S) (f : F),
  NonUnitalSubsemiring.comap f (s ⊓ t) = NonUnitalSubsemiring.comap f s ⊓ NonUnitalSubsemiring.comap f t
-- Mathlib.Topology.Instances.ENat
ENat.range_natCast : Set.range Nat.cast = Set.Iio ⊤
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_zero_left : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] (f : α →₀ N),
  Finsupp.neLocus 0 f = f.support
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.commSemiring.injEq : ∀ (id id_1 : ℕ),
  (Lean.Meta.Sym.Arith.ClassifyResult.commSemiring id = Lean.Meta.Sym.Arith.ClassifyResult.commSemiring id_1) =
    (id = id_1)
-- Std.Data.DTreeMap.Basic
/-- Returns an array of all keys present in the tree map in ascending  order.  -/
Std.DTreeMap.keysArray : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Array α
-- Mathlib.Data.List.Chain
List.IsChain.cons_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α} {as m : List α},
  List.IsChain (fun x1 x2 => x1 > x2) (a :: as) →
    List.IsChain (fun x1 x2 => x1 > x2) m → m ≤ as → List.IsChain (fun x1 x2 => x1 > x2) (a :: m)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
CategoryTheory.instMonoAppOfFunctor : ∀ {K : Type u} [inst : CategoryTheory.Category.{v, u} K] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Mono f] (k : K),
  CategoryTheory.Mono (f.app k)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Natural homomorphism sending `x : M`, `M` a `CommMonoid`, to the equivalence class of
`(x, 1)` in the Localization of `M` at a Submonoid.  -/
Localization.monoidOf : {M : Type u_1} → [inst : CommMonoid M] → (S : Submonoid M) → S.LocalizationMap (Localization S)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_eq_top_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E]
  {S : Set E}, IntermediateField.adjoin F S = ⊤ ↔ Algebra.adjoin F S = ⊤
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.instIsLowerWithLower : ∀ {α : Type u_1} [inst : Preorder α], Topology.IsLower (Topology.WithLower α)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₂Iso →
            Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.finsetSum_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {ι : Type u_9} {s : Finset ι}
  [inst_13 : ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂), (∑ i ∈ s, g i) ∘SL f = ∑ i ∈ s, g i ∘SL f
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.prod.eq_1 : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Submonoid M) (t : Submonoid N),
  s.prod t = { carrier := ↑s ×ˢ ↑t, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- Let `{ Xᵢ ⟶ Y }` be a family of pairwise disjoint maps that form a cover in `J`. Then its
image under the yoneda embedding to `J`-sheaves is a coproduct.
 -/
CategoryTheory.GrothendieckTopology.isColimitCofanMkYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] →
        {ι : Type u_1} →
          (X : ι → C) →
            {c : CategoryTheory.Limits.Cofan X} →
              CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt →
                [∀ (i : ι), CategoryTheory.Mono (c.inj i)] →
                  (∀ (Y : C) (a : CategoryTheory.Limits.IsInitial Y), ⊥ ∈ J Y) →
                    (∀ {i j : ι},
                        i ≠ j →
                          ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j),
                            CategoryTheory.CategoryStruct.comp a (c.inj i) =
                                CategoryTheory.CategoryStruct.comp b (c.inj j) →
                              Nonempty (CategoryTheory.Limits.IsInitial Y)) →
                      CategoryTheory.Limits.IsColimit
                        (CategoryTheory.Limits.Cofan.mk (J.yoneda.obj c.pt) fun i => J.yoneda.map (c.inj i))
-- Init.Data.String.Lemmas.Pattern.Split.Char
String.Slice.toList_split_intercalate_beq : ∀ {c : Char} {l : List String.Slice},
  (∀ s ∈ l, c ∉ s.copy.toList) →
    ((((String.singleton c).toSlice.intercalate l).split c).toList == if l = [] then ["".toSlice] else l) = true
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.ι_toIso_inv_assoc : ∀ (X : AlgebraicGeometry.Scheme) {Z : AlgebraicGeometry.Scheme} (h : ↑⊤ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ⊤.ι (CategoryTheory.CategoryStruct.comp X.topIso.inv h) = h
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left' : ∀ {α : Type u_1} {E : Type u_2} {F' : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T T' : Set α → E →L[ℝ] F') (c : ℝ),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) →
    ∀ {f : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.SimpleFunc.setToSimpleFunc T' f = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f
-- Init.Data.List.Find
List.findSome?_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : γ → Option α} {f : β → γ} {l : List β},
  List.findSome? p (List.map f l) = List.findSome? (p ∘ f) l
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- A characterization of weak convergence in terms of integrals of bounded continuous
nonnegative functions.  -/
MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω NNReal),
      Filter.Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (nhds (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.mem_comap_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.Precoverage D} {X : C} {R : CategoryTheory.Presieve X},
  R ∈ (CategoryTheory.Precoverage.comap F J).coverings X ↔ CategoryTheory.Presieve.map F R ∈ J.coverings (F.obj X)
-- Lean.PrettyPrinter.Formatter
/-- Pretty prints `f` and creates a new `Format` of its first line. Preserves tags.
 -/
Lean.PrettyPrinter.OneLine.pretty : Std.Format → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- Given an object `X : FormalCoproduct C` and an equality of indices `i = j`, this is
the induced isomorphism `Xᵢ ≅ Xⱼ`.  -/
CategoryTheory.Limits.FormalCoproduct.objIsoOfEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.Limits.FormalCoproduct C) → {i j : X.I} → i = j → (X.obj i ≅ X.obj j)
-- Lean.Level
Lean.Level.zero : Lean.Level
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Ψ₃ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 3 ≠ 0 → W.Ψ₃.natDegree = 4
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.re_log_comb_nonneg : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {n : ℕ},
  2 ≤ n →
    ∀ {x : ℝ},
      1 < x →
        ∀ (y : ℝ),
          0 ≤
            3 * (-Complex.log (1 - 1 ↑n * ↑n ^ (-↑x))).re +
                4 * (-Complex.log (1 - χ ↑n * ↑n ^ (-(↑x + Complex.I * ↑y)))).re +
              (-Complex.log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * Complex.I * ↑y)))).re
-- Mathlib.Data.Finset.Basic
Finset.disjoint_of_subset_iff_left_eq_empty : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → (Disjoint s t ↔ s = ∅)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivAevalXAddC_apply : ∀ {R : Type u_3} [inst : CommRing R] (t : R) (a : Polynomial R),
  (Polynomial.algEquivAevalXAddC t) a = (Polynomial.aeval (Polynomial.X + Polynomial.C t)) a
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.Hom.δ : {n : ℕ} → Fin (n + 2) → (FreeSimplexQuiver.mk n).Hom (FreeSimplexQuiver.mk (n + 1))
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- **Tangent-Secant Theorem**. The square of the tangent length equals
the product of secant segment lengths.  -/
EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b t p : P} {s : EuclideanGeometry.Sphere P},
  a ∈ s → b ∈ s → p ∈ line[ℝ, a, b] → s.IsTangentAt t line[ℝ, p, t] → dist p t ^ 2 = dist p a * dist p b
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainAddEquiv_trans : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N]
  [inst_3 : Mul O] (e₁ : M ≃ N) (e₂ : N ≃ O),
  MonoidAlgebra.mapDomainAddEquiv R (e₁.trans e₂) =
    (MonoidAlgebra.mapDomainAddEquiv R e₁).trans (MonoidAlgebra.mapDomainAddEquiv R e₂)
-- Std.Sync.Channel
/-- Try to send a value to the channel. If this can be completed right away without blocking return
`true`; otherwise, don't send the value and return `false`.
 -/
Std.Channel.Sync.trySend : {α : Type} → Std.Channel.Sync α → α → BaseIO Bool