mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideEqualizer.condition : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y))
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] (j₁ j₂ : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (f j₁) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (f j₂)
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.AbsoluteLspSemanticToken.mk.inj : ∀ {pos tailPos : Lean.Lsp.Position} {type : Lean.Lsp.SemanticTokenType} {priority : ℕ}
  {pos_1 tailPos_1 : Lean.Lsp.Position} {type_1 : Lean.Lsp.SemanticTokenType} {priority_1 : ℕ},
  { pos := pos, tailPos := tailPos, type := type, priority := priority } =
      { pos := pos_1, tailPos := tailPos_1, type := type_1, priority := priority_1 } →
    pos = pos_1 ∧ tailPos = tailPos_1 ∧ type = type_1 ∧ priority = priority_1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.ofCocone_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Cocone F)
  (j : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.Cofork.ofCocone t).ι.app j =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.coe_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  {U : Subalgebra S A}, ↑(Subalgebra.restrictScalars R U) = ↑U
-- Lean.Data.Lsp.Basic
/-- A map of change annotations that can be referenced in
`AnnotatedTextEdit`s or create, rename and delete file / folder
operations.

Whether clients honor this property depends on the client capability
`workspace.changeAnnotationSupport`.  -/
Lean.Lsp.WorkspaceEdit.changeAnnotations? : Lean.Lsp.WorkspaceEdit → Option (Std.TreeMap String Lean.Lsp.ChangeAnnotation compare)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.mapHom_apply : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F) (I : Ideal R), (Ideal.mapHom f) I = Ideal.map f I
-- Batteries.CodeAction.Match
/-- Flattens an Infotree into an array of Info-nodes that fulfill p.  -/
Batteries.CodeAction.findAllInfos : (Lean.Elab.Info → Bool) → Lean.Elab.InfoTree → Array Lean.Elab.Info
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.linearIndepOn : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → ∀ (s : Set ι), LinearIndepOn R v s
-- Mathlib.NumberTheory.ClassNumber.FunctionField
/-- The class number in a function field is the (finite) cardinality of the class group.  -/
FunctionField.classNumber : (Fq : Type u_1) →
  (F : Type u_2) →
    [inst : Field Fq] →
      [Fintype Fq] →
        [inst_2 : Field F] →
          [inst_3 : Algebra (Polynomial Fq) F] →
            [inst_4 : Algebra (RatFunc Fq) F] →
              [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] →
                [FunctionField Fq F] → [Algebra.IsSeparable (RatFunc Fq) F] → ℕ
-- Lean.Data.KVMap
Lean.instCoeStringDataValue : Coe String Lean.DataValue
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.neg_add_of_eq : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, ↑u = a → ↑(-u) + a = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonAssocRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : MulOneClass M],
  MonoidAlgebra.nonAssocRing =
    { toNonUnitalNonAssocRing := MonoidAlgebra.nonUnitalNonAssocRing, toOne := MonoidAlgebra.nonAssocSemiring.toOne,
      one_mul := ⋯, mul_one := ⋯, toNatCast := MonoidAlgebra.nonAssocSemiring.toNatCast, natCast_zero := ⋯,
      natCast_succ := ⋯, intCast := fun z => MonoidAlgebra.single 1 ↑z, intCast_ofNat := ⋯, intCast_negSucc := ⋯ }
-- Mathlib.Analysis.Convex.Side
/-- The points `x` and `y` are strictly on opposite sides of `s`.  -/
AffineSubspace.SOppSide : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : PartialOrder R] →
          [IsStrictOrderedRing R] →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module R V] → [inst_5 : AddTorsor V P] → AffineSubspace R P → P → P → Prop
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_single_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {a a' : M} {b : R} [inst_1 : Decidable (a = a')],
  (MonoidAlgebra.single a b).coeff a' = if a = a' then b else 0
-- Mathlib.Algebra.Order.IsBotOne
one_max : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : One α] [IsBotOneClass α] (a : α), max 1 a = a
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (a : X ⟶ Y) {Z : ↑(F.obj b₂)}
  (h : (F.map fg).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
        (CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app Y) h)) =
    CategoryTheory.CategoryStruct.comp ((F.map fg).toFunctor.map a) h
-- Mathlib.Data.Multiset.Sort
Multiset.sort.congr_simp : ∀ {α : Type u_1} (s s_1 : Multiset α),
  s = s_1 →
    ∀ (r r_1 : α → α → Prop) (e_r : r = r_1) {inst : DecidableRel r} [inst_1 : DecidableRel r_1] [inst_2 : IsTrans α r]
      [inst_3 : Std.Antisymm r] [inst_4 : Std.Total r], s.sort r = s_1.sort r_1
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.skipToNewline : Lean.Parser.ParserFn
-- Init.Data.SInt.Basic
instHashableISize : Hashable ISize
-- Mathlib.RingTheory.WittVector.Complete
/-- If `k` is a perfect ring of characteristic `p`, a Witt vector `x : 𝕎 k` falls in ideal generated by
`p ^ n` if and only if its initial `n` coefficients are `0`.
 -/
WittVector.mem_span_p_pow_iff_le_coeff_eq_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] [PerfectRing k p]
  (x : WittVector p k) (n : ℕ), x ∈ Ideal.span {↑p ^ n} ↔ ∀ m < n, x.coeff m = 0
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.irreducible_mk : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {a : M}, Irreducible (Associates.mk a) ↔ Irreducible a
-- Mathlib.SetTheory.ZFC.Class
ZFSet.choice_isFunc : ∀ (x : ZFSet.{u}), ∅ ∉ x → x.IsFunc x.sUnion x.choice
-- Mathlib.CategoryTheory.Enriched.HomCongr
/-- `eHomCongr` respects composition of morphisms. Recall that for any
composable pair of arrows `f : X ⟶ Y` and `g : Y ⟶ Z` in `C`, the composite
`f ≫ g` in `C` defines a morphism `𝟙_ V ⟶ (X ⟶[V] Z)` in `V`. Composing with
the isomorphism `eHomCongr V α γ` yields a morphism in `V` that can be factored
through the enriched composition map as shown:
`𝟙_ V ⟶ 𝟙_ V ⊗ 𝟙_ V ⟶ (X₁ ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z₁) ⟶ (X₁ ⟶[V] Z₁)`.  -/
CategoryTheory.Iso.eHomCongr_comp_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : V}
  (h : (X₁ ⟶[V] Z₁) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.eHomCongr V α γ).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).hom)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X₁ ⟶[V] Y₁)
            (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g)
              (CategoryTheory.Iso.eHomCongr V β γ).hom))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X₁ Y₁ Z₁) h)))
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_X : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)),
  ((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).obj P).X = P.X.X
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- Given a `k`-linear `G`-representation `V`, `Extⁿ(k, V)` (where `k` is a trivial `k`-linear
`G`-representation) is isomorphic to the `n`th cohomology group of `Hom(P, V)`, where `P` is the
standard resolution of `k` called `standardComplex k G`.  -/
Rep.standardResolution.extIso : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (V : Rep.{u, u, u} k G) →
        (n : ℕ) →
          ((Ext k (Rep.{u, u, u} k G) n).obj (Opposite.op (Rep.trivial k G k))).obj V ≅
            HomologicalComplex.homology ((Rep.standardComplex k G).linearYonedaObj k V) n
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- The equivalence between `X` and the underlying type of its fundamental groupoid.
This is useful for transferring constructions (instances, etc.)
from `X` to `πₓ X`.  -/
FundamentalGroupoid.equiv : (X : Type u_3) → FundamentalGroupoid X ≃ X
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap : (α : Type u) → Type v → [BEq α] → [Hashable α] → Type (max u v)
-- Mathlib.GroupTheory.OrderOfElement
pow_injOn_Iio_orderOf : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, Set.InjOn (fun x_1 => x ^ x_1) (Set.Iio (orderOf x))
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.sumArrowHomeomorphProdArrow_symm_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8} (p : (ι → X) × (ι' → X)) (a : ι ⊕ ι'),
  Homeomorph.sumArrowHomeomorphProdArrow.symm p a = Sum.elim p.1 p.2 a
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
/-- Note that unlike the operator norm for linear maps, this norm is _not_ submultiplicative:
we do _not_ necessarily have `‖f.comp g‖ ≤ ‖f‖ * ‖g‖`. See `norm_comp_le` for what we can say.  -/
ContinuousAffineMap.hasNorm : {𝕜 : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      [inst : SeminormedAddCommGroup V] →
        [inst_1 : SeminormedAddCommGroup W] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 V] → [inst_4 : NormedSpace 𝕜 W] → Norm (V →ᴬ[𝕜] W)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} [inst : Inhabited β] {f : Option β → Option β},
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k =
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isSymm_neg : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B : LinearMap.BilinForm R₁ M₁}, (-B).IsSymm ↔ B.IsSymm
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.rightRel_pi : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → AddGroup (β i)] (s' : (i : ι) → AddSubgroup (β i)),
  QuotientAddGroup.rightRel (AddSubgroup.pi Set.univ s') = piSetoid
-- Mathlib.Topology.ContinuousOn
ContinuousOn.isOpen_inter_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {t : Set β}, ContinuousOn f s → IsOpen s → IsOpen t → IsOpen (s ∩ f ⁻¹' t)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.startsWith_char_eq_false_iff_forall_append : ∀ {c : Char} {s : String}, s.startsWith c = false ↔ ∀ (t : String), s ≠ String.singleton c ++ t
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app : ∀ {X Y Z : AlgebraicGeometry.Scheme} {U : X.Opens} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (M : Z.Modules),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.restrictFunctorComp f g).hom.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Lean.Data.PersistentHashMap
/-- A more efficient `m.findEntry? a |>.map (·.1) |>.getD a₀`
 -/
Lean.PersistentHashMap.findKeyD : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → α → α → α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The difference between two points lies in their `vectorSpan`.  -/
vsub_mem_vectorSpan_pair : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p₁ p₂ : P), p₁ -ᵥ p₂ ∈ vectorSpan k {p₁, p₂}
-- Mathlib.Control.Monad.Cont
instLawfulMonadContReaderT : ∀ {m : Type u → Type v} {ρ : Type u} [inst : Monad m] [inst_1 : MonadCont m] [LawfulMonadCont m],
  LawfulMonadCont (ReaderT ρ m)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- An independence predicate on `Finset α` that obeys the finite matroid axioms determines a
finitary matroid on `α`.  -/
IndepMatroid.ofFinset : {α : Type u_1} →
  [inst : DecidableEq α] →
    (E : Set α) →
      (Indep : Finset α → Prop) →
        Indep ∅ →
          (∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I) →
            (∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) →
              (∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E) → IndepMatroid α
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.instMulDistribMulActionSemiHomClassCoeMonoidHom : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (φ : M →* N) (A : Type u_4) [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] (B : Type u_5) [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B],
  MulDistribMulActionSemiHomClass (A →ₑ*[φ] B) (⇑φ) A B
-- Mathlib.Data.FinEnum
FinEnum.card_UInt16 : FinEnum.card UInt16 = 2 ^ 16
-- Init.Data.Option.Monadic
Option.sequence_join : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Applicative m] [LawfulApplicative m] {o : Option (Option (m α))},
  o.join.sequence = Option.join <$> (Option.map Option.sequence o).sequence
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- The `AddSubmonoid` generated by a set includes the set.  -/
AddSubmonoid.subset_closure : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(AddSubmonoid.closure s)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Reindexing a simplex along an `Equiv` of index types does not change the circumcenter.  -/
Affine.Simplex.circumcenter_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P m) (e : Fin (m + 1) ≃ Fin (n + 1)),
  (s.reindex e).circumcenter = s.circumcenter
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.bind_assoc_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} (s : Stream'.WSeq α) (f : α → Stream'.WSeq β) (g : β → Stream'.WSeq γ),
  (s.bind f).bind g ~ʷ s.bind ((fun y => y.bind g) ∘ f)
-- Mathlib.Combinatorics.Matroid.Closure
/-- A flat is a maximal set having a given basis  -/
Matroid.IsFlat : {α : Type u_2} → Matroid α → Set α → Prop
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
CategoryTheory.FunctorToTypes.instHasImagesFunctorType : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.Limits.HasImages (CategoryTheory.Functor C (Type u_2))
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgHom_eq_eval₂AlgHom_CAlgHom : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Polynomial.mapAlgHom f = Polynomial.eval₂AlgHom (Polynomial.CAlgHom.comp f) Polynomial.X ⋯
-- Mathlib.FieldTheory.SeparableClosure
Field.insepDegree_le_of_left_le : ∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra F K] {E₁ E₂ : IntermediateField F K},
  E₁ ≤ E₂ → Field.insepDegree (↥E₂) K ≤ Field.insepDegree (↥E₁) K
-- Mathlib.Data.List.FinRange
/-- The list obtained from a permutation of a tuple `f` is permutation equivalent to
the list obtained from `f`.  -/
Equiv.Perm.ofFn_comp_perm : ∀ {n : ℕ} {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin n → α), (List.ofFn (f ∘ ⇑σ)).Perm (List.ofFn f)
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.add : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f g : α → M}
  [MeasurableAdd₂ M], Measurable f → Measurable g → Measurable (f + g)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_listSum : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V] (l : List V),
  WithLp.toLp p l.sum = (List.map (WithLp.toLp p) l).sum
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.Commensurable.isCusp_iff : ∀ {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)}, 𝒢.Commensurable 𝒢' → ∀ {c : OnePoint ℝ}, IsCusp c 𝒢 ↔ IsCusp c 𝒢'
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_alter_eq_sub_one : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∈ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size - 1
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mem_inf : ∀ {M : Type u_1} [inst : MulOneClass M] {p p' : Submonoid M} {x : M}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.measurable_lintegral : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal}, Measurable f → Measurable fun μ => ∫⁻ (x : α), f x ∂μ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).size =
    if k ∈ m ∧ (f (Std.DHashMap.Const.get? m k)).isNone = true then m.size - 1
    else if k ∉ m ∧ (f (Std.DHashMap.Const.get? m k)).isSome = true then m.size + 1 else m.size
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.ϕ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        (P₁ : CategoryTheory.Limits.IndObjectPresentation A) →
          (P₂ : CategoryTheory.Limits.IndObjectPresentation B) →
            CategoryTheory.NonemptyParallelPairPresentationAux.F₁ f g P₁ P₂ ⟶
              CategoryTheory.NonemptyParallelPairPresentationAux.F₂ f g P₁ P₂
-- Mathlib.CategoryTheory.Category.ULift
/-- The type-level equivalence between `C` and `ULiftHom (ULift C)`.  -/
CategoryTheory.ULiftHomULiftCategory.objEquiv : {C : Type u} → C ≃ CategoryTheory.ULiftHom (ULift.{u', u} C)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The function that sends an element of the free group to its maximal reduction.  -/
FreeGroup.toWord : {α : Type u_1} → [DecidableEq α] → FreeGroup α → List (α × Bool)
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps.eq_3 : ∀ {s : String.Slice} (currPos p q : s.Pos) (l_2 : List (String.Slice.Pattern.SearchStep s)),
  String.Slice.Pattern.Model.splitFromSteps✝ currPos (String.Slice.Pattern.SearchStep.matched p q :: l_2) =
    s.subslice! currPos p :: String.Slice.Pattern.Model.splitFromSteps✝ q l_2
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (X : D)
  (X_1 : ↑(((CategoryTheory.Functor.id D).comp (CategoryTheory.CostructuredArrow.functor L)).obj X)),
  (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X).inv.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X_1)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.intCast_val : ∀ {d : ℤ} (n : ℤ), ↑n = { re := n, im := 0 }
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- `CondensedSet.LocallyConstant.functor` is fully faithful.  -/
CondensedSet.LocallyConstant.functorFullyFaithful : CondensedSet.LocallyConstant.functor.FullyFaithful
-- Mathlib.Order.Closure
ClosureOperator.ofPred_isClosed : ∀ {α : Type u_1} [inst : PartialOrder α] (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x ≤ f x) (hfp : ∀ (x : α), p (f x))
  (hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y) (a : α), (ClosureOperator.ofPred f p hf hfp hmin).IsClosed a = p a
-- Mathlib.Analysis.Normed.Group.Constructions
norm_toDual : ∀ {E : Type u_2} [inst : Norm E] (x : E), ‖OrderDual.toDual x‖ = ‖x‖
-- Mathlib.Topology.Irreducible
IsPreirreducible.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set X},
  IsPreirreducible t → ∀ {f : Y → X}, Topology.IsOpenEmbedding f → IsPreirreducible (f ⁻¹' t)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
RingHom.isIntegralElem_zero : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] (f : R →+* B), f.IsIntegralElem 0
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.toSubtype.match_1.splitter : (motive :
    (x : ℕ) →
      (x_1 : TypeVec.{u_1} x) →
        (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) →
          (x_3 : Fin2 x) → { x_4 // TypeVec.ofRepeat (x_2 x_3 x_4) } → Sort u_2) →
  (x : ℕ) →
    (x_1 : TypeVec.{u_1} x) →
      (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) →
        (x_3 : Fin2 x) →
          (x_4 : { x_4 // TypeVec.ofRepeat (x_2 x_3 x_4) }) →
            ((n : ℕ) →
                (x : TypeVec.{u_1} n.succ) →
                  (p : x.Arrow (TypeVec.repeat n.succ Prop)) →
                    (i : Fin2 n) → (x_5 : { x // TypeVec.ofRepeat (p i.fs x) }) → motive n.succ x p i.fs x_5) →
              ((n : ℕ) →
                  (x : TypeVec.{u_1} n.succ) →
                    (x_5 : x.Arrow (TypeVec.repeat n.succ Prop)) →
                      (x_6 : { x // TypeVec.ofRepeat (x_5 Fin2.fz x) }) → motive n.succ x x_5 Fin2.fz x_6) →
                motive x x_1 x_2 x_3 x_4
-- Mathlib.Topology.Order.MonotoneContinuity
/-- An order isomorphism between two linear order `OrderTopology` spaces is a homeomorphism.  -/
OrderIso.toHomeomorph : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : TopologicalSpace α] →
          [inst_3 : TopologicalSpace β] → [OrderTopology α] → [OrderTopology β] → α ≃o β → α ≃ₜ β
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore_mono : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ K → H.normalCore ≤ K.normalCore
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpIndSMul_empty : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} {x : G}, MeasureTheory.condExpIndSMul hm ⋯ ⋯ x = 0
-- Init.Data.Int.Order
Int.mul_pos_of_neg_of_neg : ∀ {a b : ℤ}, a < 0 → b < 0 → 0 < a * b