mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- The canonical isomorphism `F.leftDerived 0 ≅ F` when `F` is right exact
(i.e. preserves finite colimits).  -/
CategoryTheory.Functor.leftDerivedZeroIsoSelf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasProjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) →
                [inst_5 : F.Additive] → [CategoryTheory.Limits.PreservesFiniteColimits F] → F.leftDerived 0 ≅ F
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.eq_1 : ∀ {G : Type u_1} [inst : Add G] (A B : Finset G) (a0 b0 : G),
  UniqueAdd A B a0 b0 = ∀ ⦃a b : G⦄, a ∈ A → b ∈ B → a + b = a0 + b0 → a = a0 ∧ b = b0
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.differentiableAt_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {R : Type u_1} [inst_1 : CommSemiring R]
  [inst_2 : Algebra R 𝕜] (q : Polynomial R), DifferentiableAt 𝕜 (fun x => (Polynomial.aeval x) q) x
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.mem_over_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C}
  {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y),
  S ∈ (J.over X) Y ↔ (CategoryTheory.Sieve.overEquiv Y) S ∈ J Y.left
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.instCoe : {L : FirstOrder.Language} →
  {M : Type u_1} → [inst : L.Structure M] → Coe (L.ElementarySubstructure M) (L.Substructure M)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- The pseudoemetric space structure associated to a Riemannian metric on a manifold. Designed
so that the topology is defeq to the original one.

This should only be used when constructing data in specific situations. To develop the theory,
one should rather assume that there is an already existing emetric space structure, which satisfies
additionally the predicate `IsRiemannianManifold I M`.  -/
PseudoEMetricSpace.ofRiemannianMetric : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            (M : Type u_3) →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] →
                    [inst_6 : IsManifold I 1 M] →
                      [IsContinuousRiemannianBundle E fun x => TangentSpace I x] →
                        [RegularSpace M] → PseudoEMetricSpace M
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstMulInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.Defs.Basic
/-- The property `BaireSpace α` means that the topological space `α` has the Baire property:
any countable intersection of open dense subsets is dense.
Formulated here when the source space is ℕ.
Use `dense_iInter_of_isOpen` which works for any countable index type instead.  -/
BaireSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.quotientKerEquivOfSurjective.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P)
  (hf : Function.Surjective ⇑f),
  AddCon.quotientKerEquivOfSurjective f hf = AddCon.quotientKerEquivOfRightInverse f (Exists.choose ⋯) ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRight_obj_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRight L r hr).obj X).right = X.right
-- Mathlib.Data.PFun
PFun.id_comp : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β), (PFun.id β).comp f = f
-- Batteries.Tactic.Case
/-- * `case _ : t => tac` finds the first goal that unifies with `t` and then solves it
using `tac` or else fails. Like `show`, it changes the type of the goal to `t`.
The `_` can optionally be a case tag, in which case it only looks at goals
whose tag would be considered by `case` (goals with an exact tag match,
followed by goals with the tag as a suffix, followed by goals with the tag as a prefix).

* `case _ n₁ ... nₘ : t => tac` additionally names the `m` most recent hypotheses with
inaccessible names to the given names. The names are renamed before matching against `t`.
The `_` can optionally be a case tag.

* `case _ : t := e` is short for `case _ : t => exact e`.

* `case _ : t₁ | _ : t₂ | ... => tac`
is equivalent to `(case _ : t₁ => tac); (case _ : t₂ => tac); ...`
but with all matching done on the original list of goals --
each goal is consumed as they are matched, so patterns may repeat or overlap.

* `case _ : t` will make the matched goal be the first goal.
`case _ : t₁ | _ : t₂ | ...` makes the matched goals be the first goals in the given order.

* `case _ : t := _` and `case _ : t := ?m` are the same as `case _ : t` but in the `?m` case the
goal tag is changed to `m`.
In particular, the goal becomes metavariable `?m`.
 -/
Batteries.Tactic.casePatt : Lean.ParserDescr
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.isGroupoidProd : ∀ {α : Type u} {β : Type u₂} [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.Category.{v₂, u₂} β]
  [CategoryTheory.IsGroupoid α] [CategoryTheory.IsGroupoid β], CategoryTheory.IsGroupoid (α × β)
-- Mathlib.LinearAlgebra.LinearPMap
/-- Given two partial linear maps `f`, `g`, the set of points `x` such that
both `f` and `g` are defined at `x` and `f x = g x` form a submodule.  -/
LinearPMap.eqLocus : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → (E →ₛₗ.[σ] F) → (E →ₛₗ.[σ] F) → Submodule R E
-- Init.Data.UInt.Lemmas
UInt8.toFin.ofNat : ∀ {n : ℕ}, (UInt8.ofNat n).toFin = Fin.ofNat UInt8.size n
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_add' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α},
  interior s + interior t ⊆ interior (s + t)
-- Lean.Elab.Tactic.RCases
/-- An `rcases` pattern can be one of the following, in a nested combination:

* A name like `foo`
* The special keyword `rfl` (for pattern matching on equality using `subst`)
* A hyphen `-`, which clears the active hypothesis and any dependents.
* A type ascription like `pat : ty` (parentheses are optional)
* A tuple constructor like `⟨p1, p2, p3⟩`
* An alternation / variant pattern `p1 | p2 | p3`

Parentheses can be used for grouping; alternation is higher precedence than type ascription, so
`p1 | p2 | p3 : ty` means `(p1 | p2 | p3) : ty`.

N-ary alternations are treated as a group, so `p1 | p2 | p3` is not the same as `p1 | (p2 | p3)`,
and similarly for tuples. However, note that an n-ary alternation or tuple can match an n-ary
conjunction or disjunction, because if the number of patterns exceeds the number of constructors in
the type being destructed, the extra patterns will match on the last element, meaning that
`p1 | p2 | p3` will act like `p1 | (p2 | p3)` when matching `a1 ∨ a2 ∨ a3`. If matching against a
type with 3 constructors,  `p1 | (p2 | p3)` will act like `p1 | (p2 | p3) | _` instead.
 -/
Lean.Elab.Tactic.RCases.RCasesPatt : Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.containsThenInsert_snd : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β k}, (m.containsThenInsert k v).2 = m.insert k v
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ), (PowerSeries.coeff m) (PowerSeries.X ^ n) = if m = n then 1 else 0
-- Mathlib.Topology.Constructions
instLocallyCompactSpaceMultiplicative : ∀ {X : Type u} [inst : TopologicalSpace X] [LocallyCompactSpace X], LocallyCompactSpace (Multiplicative X)
-- Mathlib.Analysis.Convex.Exposed
IsExposed.sInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A : Set E} [IsOrderedRing 𝕜]
  [ContinuousAdd 𝕜] {F : Finset (Set E)}, F.Nonempty → (∀ B ∈ F, IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).maxKey? = Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.maxKey?
-- Mathlib.Analysis.Distribution.Sobolev
/-- The directional derivative maps `H ^ s` to `H ^ {s - 1}`.  -/
TemperedDistribution.MemSobolev.lineDerivOp : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F},
  TemperedDistribution.MemSobolev s 2 f →
    ∀ {m : E}, TemperedDistribution.MemSobolev (s - 1) 2 (LineDeriv.lineDerivOp m f)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ArbitraryShiftTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {m n : ℕ} {target : aig.RefVec m}
  {distance : aig.RefVec n} {n_1 : ℕ} {target_1 : aig.RefVec m} {distance_1 : aig.RefVec n_1},
  { n := n, target := target, distance := distance } = { n := n_1, target := target_1, distance := distance_1 } →
    n = n_1 ∧ target = target_1 ∧ distance ≍ distance_1
-- Mathlib.Analysis.Normed.Lp.lpSpace
natCast_memℓp_infty : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ℕ),
  Memℓp ↑n ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, Array.find? (fun x => x.fst == k) (↑m).toArray = none ↔ m.contains k = false
-- Mathlib.Analysis.Normed.Group.Pointwise
ediam_mul_le : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (x y : Set E), Metric.ediam (x * y) ≤ Metric.ediam x + Metric.ediam y
-- Mathlib.MeasureTheory.Measure.Restrict
/-- **Alias** of `MeasureTheory.Measure.restrict_inter_add_sdiff`. -/
MeasureTheory.Measure.restrict_inter_add_diff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasurableSet t → μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
AlgHom.map_det : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type w}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] {T : Type z} [inst_5 : CommRing T] [inst_6 : Algebra R T] (f : S →ₐ[R] T)
  (M : Matrix n n S), f M.det = (f.mapMatrix M).det
-- Batteries.Data.UnionFind.Basic
/-- Maximum rank of nodes in a union-find structure  -/
Batteries.UnionFind.rankMax : Batteries.UnionFind → ℕ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey! t.maxKey! = t.maxKey!
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.aux : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  (∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)) → ∃ α x, ∃ (_ : CategoryTheory.IsCardinalFiltered α κ), ∃ F, F.Final
-- Mathlib.Algebra.Torsor.Basic
Pi.vsub_apply : ∀ {I : Type u} {fg : I → Type v} [inst : (i : I) → AddGroup (fg i)] {fp : I → Type w}
  [inst_1 : (i : I) → AddTorsor (fg i) (fp i)] (p q : (i : I) → fp i) (i : I), (p -ᵥ q) i = p i -ᵥ q i
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instNeg : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddGroup (β i)] → Neg (Π₀ (i : ι), β i)
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.sInter : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {S : Set (Set E)},
  (∀ s ∈ S, Balanced 𝕜 s) → Balanced 𝕜 (⋂₀ S)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.range_d₁₀_eq_coinvariantsKer : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (ModuleCat.Hom.hom (groupHomology.d₁₀ A)).range = Representation.Coinvariants.ker A.ρ
-- Mathlib.RingTheory.PiTensorProduct
/-- The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)`
 -/
PiTensorProduct.mul : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [∀ (i : ι), SMulCommClass R (A i) (A i)] →
              [∀ (i : ι), IsScalarTower R (A i) (A i)] →
                (PiTensorProduct R fun i => A i) →ₗ[R]
                  (PiTensorProduct R fun i => A i) →ₗ[R] PiTensorProduct R fun i => A i
-- Init.Data.List.Lemmas
List.flatten_singleton : ∀ {α : Type u_1} {l : List α}, [l].flatten = l
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.ae_eq_condLExp₀ : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {Y : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) {P : MeasureTheory.Measure Ω}
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (X : Ω → ENNReal),
  AEMeasurable Y (P.trim hm) →
    (∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P) → Y =ᵐ[P] P⁻[X | mΩ]
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.mk'_eq_one_iff_eq : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] {x : A} {y : ↥(nonZeroDivisors A)}, IsLocalization.mk' K x y = 1 ↔ x = ↑y
-- Mathlib.NumberTheory.LSeries.PrimesInAP
_private.Mathlib.NumberTheory.LSeries.PrimesInAP.0.ArithmeticFunction.vonMangoldt.F' : Nat.Primes × ℕ → ℝ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The setoid used to construct `ValueGroupWithZero R`.  -/
ValuativeRel.valueSetoid : (R : Type u_1) → [inst : Semiring R] → [inst_1 : ValuativeRel R] → Setoid (R × ↥(ValuativeRel.posSubmonoid R))
-- Mathlib.MeasureTheory.Function.Jacobian
/-- If a function is differentiable and injective on a null measurable set,
then the image is null measurable.  -/
MeasureTheory.nullMeasurable_image_of_fderivWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasureTheory.NullMeasurableSet s μ →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → Set.InjOn f s → MeasureTheory.NullMeasurableSet (f '' s) μ
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.ext : ∀ {a b : Lean.Omega.LinearCombo}, a.const = b.const → a.coeffs = b.coeffs → a = b
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_mul_ge_length_sub_length : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W),
  cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)
-- Init.Data.Range.Polymorphic.SInt
ISize.lt.eq_1 : ∀ (a b : ISize), a.lt b = (a.toBitVec.slt b.toBitVec = true)
-- Lean.Meta.Tactic.Grind.SimpUtil
_private.Lean.Meta.Tactic.Grind.SimpUtil.0.Lean.Meta.Grind.addDeclToUnfold : Lean.Meta.SimpTheorems → Lean.Name → Lean.MetaM Lean.Meta.SimpTheorems
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPTR.go.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (a : Array α) (a_1 : Array (List α)) (a_2 : α) (t : List α),
  List.splitOnPTR.go✝ p (a_2 :: t) a a_1 =
    bif p a_2 then List.splitOnPTR.go✝ p t #[] (a_1.push a.toList) else List.splitOnPTR.go✝ p t (a.push a_2) a_1
-- Init.Grind.Tactics
/-- `cutsat` solves linear integer arithmetic goals.

It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver.
Please use `grind` instead if you need additional capabilities.

**Deprecated**: Use `lia` instead.
 -/
Lean.Parser.Tactic.cutsat : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `MulDistribMulActionSemiHomClass F φ A B` states that `F` is a type of morphisms
preserving the monoid structure and equivariant with respect to `φ`.
You should extend this class when you extend `MulDistribMulActionSemiHom`.  -/
MulDistribMulActionSemiHomClass : (F : Type u_10) →
  {M : outParam (Type u_11)} →
    {N : outParam (Type u_12)} →
      outParam (M → N) →
        (A : outParam (Type u_13)) →
          (B : outParam (Type u_14)) →
            [inst : Monoid M] →
              [inst_1 : Monoid N] →
                [inst_2 : Monoid A] →
                  [inst_3 : Monoid B] → [MulDistribMulAction M A] → [MulDistribMulAction N B] → [FunLike F A B] → Prop
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instAdd : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → Add (ProbabilityTheory.Kernel α β)
-- Mathlib.Algebra.Order.BigOperators.Expect
/-- Let `{a | p a}` be an additive subsemigroup of an additive commutative monoid `M`. If `m` is a
subadditive function (`m (a + b) ≤ m a + m b`) preserved under division by a natural, `f` is a
function valued in that subsemigroup and `s` is a nonempty set, then
`m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`.  -/
Finset.le_expect_nonempty_of_subadditive_on_pred : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M]
  [inst_2 : AddCommMonoid N] [inst_3 : PartialOrder N] [IsOrderedAddMonoid N] [inst_5 : Module ℚ≥0 N]
  [PosSMulMono ℚ≥0 N] {m : M → N} {p : M → Prop} {f : ι → M} {s : Finset ι},
  (∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b) →
    (∀ (a b : M), p a → p b → p (a + b)) →
      (∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a) →
        s.Nonempty → (∀ i ∈ s, p (f i)) → m (s.expect fun i => f i) ≤ s.expect fun i => m (f i)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_zero_sub_cancel : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → a + (0 - a) = 0
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.not_isLeftDescent_one : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  ¬cs.IsLeftDescent 1 i
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.c_denom : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → (RatFunc.Luroth.c✝ E).denom = 1
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.ofIsEmpty.congr_simp : ∀ (L : FirstOrder.Language) (L' : FirstOrder.Language) [inst : L.IsAlgebraic] [inst_1 : L.IsRelational],
  FirstOrder.Language.LHom.ofIsEmpty L L' = FirstOrder.Language.LHom.ofIsEmpty L L'
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.comp_snd : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l : Filter α} (l' : Filter β), f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)
-- Mathlib.Topology.ContinuousOn
Topology.IsInducing.map_nhdsWithin_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsInducing f → ∀ (s : Set α) (x : α), Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonSaveOptions : Lean.FromJson Lean.Lsp.SaveOptions
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- The composition `E.saturate ⟶ E.toPreOneHypercover ⟶ E.saturate` is homotopic to the
identity.  -/
CategoryTheory.PreZeroHypercover.fromSaturateToSaturateHomotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} →
      (E : CategoryTheory.PreZeroHypercover S) →
        [inst_1 : E.HasPullbacks] →
          CategoryTheory.PreOneHypercover.Homotopy
            (CategoryTheory.PreOneHypercover.Hom.comp E.fromSaturateOfHasPullbacks E.toSaturateOfHasPullbacks)
            (CategoryTheory.PreOneHypercover.Hom.id E.saturate)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.normSMulClassSeminormedAddCommGroupToProd : ∀ (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] {R : Type u_6} [inst_2 : SeminormedRing R] [inst_3 : Module R α]
  [inst_4 : Module R β] [NormSMulClass R α] [NormSMulClass R β], NormSMulClass R (α × β)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.instHasStrictInitialObjectsOfIsThin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Quiver.IsThin C],
  CategoryTheory.Limits.HasStrictInitialObjects C
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.isIrreducible_iff : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] (A : Matrix n n R),
  A.IsIrreducible ↔ (∀ (i j : n), 0 ≤ A i j) ∧ Quiver.IsSStronglyConnected n
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceLT : Lean.Meta.Simp.Simproc
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Context.config : Lean.Meta.Sym.Context → Lean.Meta.Sym.Config
-- Mathlib.LinearAlgebra.Matrix.StdBasis
/-- The module of finite matrices is free.  -/
Module.Free.matrix : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {m : Type u_3} {n : Type u_4} [Finite m] [Finite n], Module.Free R (Matrix m n M)
-- Mathlib.Algebra.Ring.Defs
NonAssocRing.toNonAssocSemiring : {α : Type u_1} → [self : NonAssocRing α] → NonAssocSemiring α
-- Mathlib.Data.Num.Bitwise
Num.instAndOp : AndOp Num