mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Ring.NamePolyVars
/-- The command `name_poly_vars` names variables in
`MvPolynomial (Fin n) R` for the appropriate value of `n`.
The notation introduced by this command is local.

Usage:

```lean
variable (R : Type) [CommRing R]

name_poly_vars X, Y, Z over R

#check Y -- Y : MvPolynomial (Fin 3) R
```
 -/
Mathlib.Tactic.namePolyVarsOver : Lean.ParserDescr
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_inj : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] (i : ι) {x y : M i},
  Pi.mulSingle i x = Pi.mulSingle i y ↔ x = y
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const_def : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} (c : ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl c =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons 0
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis_tl c)
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.GroupTheory.OrderOfElement
/-- If `x ^ p = 1` for some odd `p`, then every power of `x` is an even power of `x`.  -/
exists_pow_eq_pow_two_mul : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {p : ℕ}, x ^ p = 1 → Odd p → ∀ (n : ℕ), ∃ m, x ^ n = x ^ (2 * m)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.comp_apply : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [inst : VAdd M X]
  {Y : Type u_6} [inst_1 : VAdd N Y] {Z : Type u_7} [inst_2 : VAdd P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y)
  [inst_3 : CompTriple φ ψ χ] (x : X), (g.comp f) x = g (f x)
-- Mathlib.SetTheory.Cardinal.EventuallyConst
Ordinal.eventuallyConst_of_antitone : ∀ {β : Type v} [inst : PartialOrder β] {f : Ordinal.{v} → β} [Small.{v, v} β],
  Antitone f → Filter.EventuallyConst f Filter.atTop
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.Fin.circulant_injective : ∀ {α : Type u_1} (n : ℕ), Function.Injective fun v => Matrix.circulant v
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The coproduct functor can be decomposed.  -/
CategoryTheory.Limits.coprod.functorLeftComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
      (X Y : C) →
        CategoryTheory.Limits.coprod.functor.obj (X ⨿ Y) ≅
          (CategoryTheory.Limits.coprod.functor.obj Y).comp (CategoryTheory.Limits.coprod.functor.obj X)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom : ∀ {R : Type u_1} {M : Type u_8} {N : Type u_9} {O : Type u_10} [inst : CommSemiring R] [inst_1 : AddMonoid M]
  [inst_2 : AddMonoid N] [inst_3 : AddMonoid O] (f : N →+ O) (g : M →+ N) (x : AddMonoidAlgebra R M),
  (AddMonoidAlgebra.mapDomainBialgHom R f) ((AddMonoidAlgebra.mapDomainBialgHom R g) x) =
    (AddMonoidAlgebra.mapDomainBialgHom R (f.comp g)) x
-- Init.Data.SInt.Basic
/-- The number of distinct values representable by `ISize`, that is, `2^System.Platform.numBits`.  -/
ISize.size : ℕ
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.continuous_sumAssoc_symm : ∀ (X : Type u) (Y : Type v) (Z : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z], Continuous ⇑(Equiv.sumAssoc X Y Z).symm
-- Mathlib.Data.Nat.Choose.Sum
Finset.sum_powerset_neg_one_pow_card : ∀ {α : Type u_2} [inst : DecidableEq α] {x : Finset α}, ∑ m ∈ x.powerset, (-1) ^ m.card = if x = ∅ then 1 else 0
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.support_smul : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M] {b : R} {g : α →₀ M},
  (b • g).support ⊆ g.support
-- Mathlib.Analysis.ConstantSpeed
HasUnitSpeedOn.union : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s t : Set ℝ} {x : ℝ},
  HasUnitSpeedOn f s → HasUnitSpeedOn f t → IsGreatest s x → IsLeast t x → HasUnitSpeedOn f (s ∪ t)
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Solve equations for `K⟮X⟯` by working in `FractionRing K[X]`.  -/
RatFunc.tacticFrac_tac : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.IsWeak
LinearMap.IsWeak.mk : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [t : TopologicalSpace E] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜},
  t = TopologicalSpace.induced (fun x1 x2 => (B x1) x2) Pi.topologicalSpace → B.IsWeak
-- Mathlib.CategoryTheory.Category.Pairwise
_private.Mathlib.CategoryTheory.Category.Pairwise.0.CategoryTheory.Pairwise.diagramMap.match_1.splitter : {ι : Type u_1} →
  (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) →
    (x x_1 : CategoryTheory.Pairwise ι) →
      (x_2 : x ⟶ x_1) →
        ((i : ι) →
            motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
              (CategoryTheory.Pairwise.Hom.id_single i)) →
          ((i j : ι) →
              motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
                (CategoryTheory.Pairwise.Hom.id_pair i j)) →
            ((i j : ι) →
                motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
                  (CategoryTheory.Pairwise.Hom.left i j)) →
              ((i j : ι) →
                  motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
                    (CategoryTheory.Pairwise.Hom.right i j)) →
                motive x x_1 x_2
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.scomp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'}
  {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'},
  HasDerivWithinAt g₁ g₁' t' y →
    HasDerivWithinAt h h' s x → Set.MapsTo h s t' → y = h x → HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_equiv : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p}, f ≈ g → f.norm = g.norm
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_zpow : ∀ {a b : ℝ} {n : ℤ},
  0 ≤ n ∨ n ≠ -1 ∧ 0 ∉ Set.uIcc a b → ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- If `K` is compact and `V` has nonempty interior, then the index `(K : V)` is well-defined,
there is a finite set `t` satisfying the desired properties.  -/
MeasureTheory.Measure.haar.addIndex_defined : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {K V : Set G},
  IsCompact K → (interior V).Nonempty → ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g + h) ⁻¹' V}
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.liftAlgHom_toRingHom : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] {A : Type u_4} [inst_5 : CommSemiring A]
  [inst_6 : Algebra A R] [inst_7 : Algebra A S] [inst_8 : Algebra A P] [inst_9 : IsScalarTower A R S] {f : R →ₐ[A] P}
  (hf : IsUnit (f x)), (IsLocalization.Away.liftAlgHom x hf).toRingHom = IsLocalization.Away.lift x hf
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNewUnit.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (hd : α) → (tl : List α) → motive (hd :: tl)),
  (match [] with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_1 ()
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A block of a group action is invariant iff it is fixed.  -/
MulAction.isInvariantBlock_iff_isFixedBlock : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsInvariantBlock G B ↔ MulAction.IsFixedBlock G B
-- Std.Data.DHashMap.RawLemmas
_private.Std.Data.DHashMap.RawLemmas.0.Std.DHashMap.Raw.Option.map_cast_apply : ∀ {γ γ' : Type u} (h : γ = γ') (x : Option γ), Option.map (cast h) x = cast ⋯ x
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.source_subset_preimage_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (self : Manifold.LocalPresentationAt I J n f x P), self.domChart.source ⊆ f ⁻¹' self.codChart.source
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction' : ∀ {ι : Type u_1} {T : Type u_4} {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] [Finite ι]
  {μ : MeasureTheory.Measure ((i : ι) → X i)} {ν : MeasureTheory.Measure T}
  {ξ : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂ξ = (∫ (x : (i : ι) → X i), f x ∂μ) * ∫ (t : T), g t ∂ν) →
    ξ = μ.prod ν
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.BinaryCofan.isVanKampen_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y)
  (cofans : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y)
  (colimits : (X Y : C) → CategoryTheory.Limits.IsColimit (cofans X Y))
  (cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PullbackCone f g)
  (limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.IsLimit (cones f g)),
  (∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
      CategoryTheory.CategoryStruct.comp αX c.inl = CategoryTheory.CategoryStruct.comp (cofans X' Y').inl f →
        CategoryTheory.CategoryStruct.comp αY c.inr = CategoryTheory.CategoryStruct.comp (cofans X' Y').inr f →
          CategoryTheory.IsPullback (cofans X' Y').inl αX f c.inl ∧
            CategoryTheory.IsPullback (cofans X' Y').inr αY f c.inr) →
    ∀
      (h₂ :
        {Z : C} →
          (f : Z ⟶ c.pt) →
            CategoryTheory.Limits.IsColimit
              (CategoryTheory.Limits.BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)),
      CategoryTheory.IsVanKampenColimit c
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instIsCharPInt32HPowNatOfNat : Lean.Grind.IsCharP Int32 (2 ^ 32)
-- Mathlib.MeasureTheory.Function.FactorsThrough
/-- If a function `g` is measurable with respect to the pullback along some function `f`,
then there exists some measurable function `h : Y → Z` such that `g = h ∘ f`.  -/
Measurable.exists_eq_measurable_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z} [Nonempty Z]
  [inst : MeasurableSpace Z] [StandardBorelSpace Z], Measurable g → ∃ h, Measurable h ∧ g = h ∘ f
-- Mathlib.CategoryTheory.Limits.Creates
/-- If F creates the limit of K, any cone lifts to a limit.  -/
CategoryTheory.liftsToLimitOfCreates : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.CreatesLimit K F] →
                  (c : CategoryTheory.Limits.Cone (K.comp F)) →
                    (t : CategoryTheory.Limits.IsLimit c) → CategoryTheory.LiftsToLimit K F c t
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.angleDiff_nonneg : ∀ (x y : Circle), 0 ≤ x.angleDiff y
-- Init.Core
/-- `map f x` maps function `f` over the task `x`: that is, it constructs
(and immediately launches) a new task which will wait for the value of `x` to
be available and then calls `f` on the result.

`prio`, if provided, is the priority of the task.
If `sync` is set to true, `f` is executed on the current thread if `x` has already finished and
otherwise on the thread that `x` finished on. `prio` is ignored in this case. This should only be
done when executing `f` is cheap and non-blocking.
 -/
Task.map : {α : Type u_1} →
  {β : Type u_2} → (α → β) → Task α → optParam Task.Priority Task.Priority.default → optParam Bool false → Task β
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.trans : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
  {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =o[l] g → g =o[l] k → f =o[l] k
-- Mathlib.Computability.RecursiveIn
ComputableIn.succ : ∀ {O : Set (ℕ →. ℕ)}, ComputableIn O Nat.succ
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_eq_sdiff_sup : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z ≤ x → x \ (y \ z) = x \ y ⊔ z
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_right : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι),
  P.pairingIn ℤ i (RootPairing.EmbeddedG2.threeShortAddTwoLong P) =
    P.pairingIn ℤ i (RootPairing.EmbeddedG2.short P) + 2 * P.pairingIn ℤ i (RootPairing.EmbeddedG2.long P)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.mul_fst : ∀ {q : ℕ} (x y : LucasLehmer.X q), (x * y).1 = x.1 * y.1 + 3 * x.2 * y.2
-- Mathlib.GroupTheory.Congruence.Hom
/-- The natural homomorphism from a magma to its quotient by a congruence relation.  -/
Con.mkMulHom : {M : Type u_1} → [inst : Mul M] → (c : Con M) → M →ₙ* c.Quotient
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instVAddCommClass : ∀ (p : ENNReal) {K : Type u_1} (K' : Type u_2) {V : Type u_4} [inst : VAdd K V] [inst_1 : VAdd K' V]
  [VAddCommClass K K' V], VAddCommClass K K' (WithLp p V)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
isClosedEmbedding_cfcₙHom_of_cfcHom : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p]
  [CompleteSpace R] {a : A} (ha : p a), Topology.IsClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.of_surjective : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] {R' : Type u_3} {S' : Type u_4} [inst_4 : CommRing R'] [inst_5 : CommRing S']
  [inst_6 : Algebra R' S'] (f : R →+* R'),
  Function.Surjective ⇑f →
    ∀ (g : S →+* S'),
      Function.Surjective ⇑g →
        g.comp (algebraMap R S) = (algebraMap R' S').comp f →
          RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f) → IsLocalization (Submonoid.map f M) S'
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_sub : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} {S : Type u_1} [inst_1 : Ring S] (f : R →+* S) {x : S},
  Polynomial.eval₂ f x (p - q) = Polynomial.eval₂ f x p - Polynomial.eval₂ f x q
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.compSubConstCLM_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  (f : SchwartzMap E F) (a x : E), ((SchwartzMap.compSubConstCLM 𝕜 a) f) x = f (x - a)
-- Init.SimpLemmas
and_congr_right : ∀ {a b c : Prop}, (a → (b ↔ c)) → (a ∧ b ↔ a ∧ c)
-- Mathlib.Algebra.Algebra.Operations
Submodule.iSup_mul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {ι : Sort uι} (s : ι → Submodule R A) (t : Submodule R A),
  (⨆ i, s i) * t = ⨆ i, s i * t
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_neg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β) (hf : MeasureTheory.Integrable f μ),
  MeasureTheory.Integrable.toL1 (-f) ⋯ = -MeasureTheory.Integrable.toL1 f hf
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- If matrix A is right invertible, then its inverse equals its right inverse.  -/
Matrix.inv_eq_right_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
  A * B = 1 → A⁻¹ = B
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_whiskerRight_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {F G H : CategoryTheory.Functor C C} {α : F ⟶ G} (X : C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight α H).app X = H.map (α.app X)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.instConcreteCategoryNormedAddGroupHomCarrier : CategoryTheory.ConcreteCategory SemiNormedGrp fun x1 x2 => NormedAddGroupHom x1.carrier x2.carrier
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.exists_pos_of_sum_zero_of_exists_nonzero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] {s : Finset ι}
  [IsOrderedCancelAddMonoid M] (f : ι → M), ∑ i ∈ s, f i = 0 → (∃ i ∈ s, f i ≠ 0) → ∃ i ∈ s, 0 < f i
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.nonempty_left : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G}, AddSubgroup.IsComplement S T → S.Nonempty
-- Init.Data.Array.Count
Array.count_flatten : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xss : Array (Array α)},
  Array.count a xss.flatten = (Array.map (Array.count a) xss).sum
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.iff_finite_comap_preimage_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S],
  Algebra.QuasiFinite R S ↔ ∀ (x : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {x}).Finite
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {section_ : Y ⟶ X}
  {id :
    autoParam (CategoryTheory.CategoryStruct.comp section_ f = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.SplitEpi.id._autoParam}
  {section__1 : Y ⟶ X}
  {id_1 :
    autoParam (CategoryTheory.CategoryStruct.comp section__1 f = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.SplitEpi.id._autoParam},
  { section_ := section_, id := id } = { section_ := section__1, id := id_1 } → section_ = section__1
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.onIoc_apply : ∀ {α : Type u_1} [inst : LinearOrder α] {G : Type u_3} [inst_1 : AddCommGroup G] {f : α → G} {u v : α},
  u ≤ v → (MeasureTheory.AddContent.onIoc f) (Set.Ioc u v) = f v - f u
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_id : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), Submonoid.map (MonoidHom.id M) S = S
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.mk : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_10} →
            [inst_2 : AddMonoid A] →
              [inst_3 : DistribMulAction M A] →
                {B : Type u_11} →
                  [inst_4 : AddMonoid B] →
                    [inst_5 : DistribMulAction N B] →
                      (toMulActionHom : A →ₑ[⇑φ] B) →
                        toMulActionHom.toFun 0 = 0 →
                          (∀ (x y : A),
                              toMulActionHom.toFun (x + y) = toMulActionHom.toFun x + toMulActionHom.toFun y) →
                            A →ₑ+[φ] B
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.aemeasurable_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {f : α → γ} {g : β → γ}
  {μ : autoParam (MeasureTheory.Measure α) ProbabilityTheory.IdentDistrib._auto_1}
  {ν : autoParam (MeasureTheory.Measure β) ProbabilityTheory.IdentDistrib._auto_3},
  ProbabilityTheory.IdentDistrib f g μ ν → AEMeasurable g ν
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- Construct a simplicial complex as a subset of a given simplicial complex.  -/
Geometry.SimplicialComplex.ofSubcomplex : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module 𝕜 E] →
            (K : Geometry.SimplicialComplex 𝕜 E) →
              (faces : Set (Finset E)) → faces ⊆ K.faces → IsLowerSet faces → Geometry.SimplicialComplex 𝕜 E
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {inst_1 : LinearOrder J} {inst_2 : OrderBot J}
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} {f' : F.obj j ⟶ X}
  {w₁ :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f' = f)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam}
  {w₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f' p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam}
  {f'_1 : F.obj j ⟶ X}
  {w₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f'_1 = f)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam}
  {w₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f'_1 p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam},
  { f' := f', w₁ := w₁, w₂ := w₂ } = { f' := f'_1, w₁ := w₁_1, w₂ := w₂_1 } → f' = f'_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.TreeMap.ofList l cmp).isEmpty = l.isEmpty
-- Mathlib.Order.Filter.Extr
IsExtrFilter.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter f l a → ∀ {g : β → γ}, Antitone g → IsExtrFilter (g ∘ f) l a
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.isOrderedCancelMonoid : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α},
  IsOrderedCancelMonoid (Localization s)
-- Mathlib.Algebra.Algebra.Basic
LinearEquiv.extendScalarsOfSurjective_symm : ∀ {R : Type u_1} {S : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_2}
  {N : Type u_3} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M] [inst_6 : Module S M]
  [inst_7 : IsScalarTower R S M] [inst_8 : Module R N] [inst_9 : Module S N] [inst_10 : IsScalarTower R S N]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : M ≃ₗ[R] N),
  (LinearEquiv.extendScalarsOfSurjective h f).symm = LinearEquiv.extendScalarsOfSurjective h f.symm