mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instSemigroupWithZero : {α : Type u_1} → [SemigroupWithZero α] → SemigroupWithZero αᵐᵒᵖ
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- An isomorphism of multilinear maps given an isomorphism between their codomains.

This is `LinearMap.compMultilinearMap` as an `S`-linear equivalence,
and the multilinear version of `LinearEquiv.congrRight`.  -/
LinearEquiv.multilinearMapCongrRight : {R : Type uR} →
  (S : Type uS) →
    {ι : Type uι} →
      {M₁ : ι → Type v₁} →
        {M₂ : Type v₂} →
          {M₃ : Type v₃} →
            [inst : Semiring R] →
              [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
                [inst_2 : (i : ι) → Module R (M₁ i)] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : Module R M₂] →
                      [inst_5 : Semiring S] →
                        [inst_6 : Module S M₂] →
                          [inst_7 : SMulCommClass R S M₂] →
                            [inst_8 : AddCommMonoid M₃] →
                              [inst_9 : Module S M₃] →
                                [inst_10 : Module R M₃] →
                                  [inst_11 : SMulCommClass R S M₃] →
                                    [LinearMap.CompatibleSMul M₂ M₃ S R] →
                                      [LinearMap.CompatibleSMul M₃ M₂ S R] →
                                        (M₂ ≃ₗ[R] M₃) → MultilinearMap R M₁ M₂ ≃ₗ[S] MultilinearMap R M₁ M₃
-- Mathlib.Order.InitialSeg
InitialSeg.leAdd_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (a : α), (InitialSeg.leAdd r s) a = Sum.inl a
-- Mathlib.Algebra.Ring.Hom.Defs
/-- `RingHomClass F α β` states that `F` is a type of (semi)ring homomorphisms.
You should extend this class when you extend `RingHom`.

This extends from both `MonoidHomClass` and `MonoidWithZeroHomClass` in
order to put the fields in a sensible order, even though
`MonoidWithZeroHomClass` already extends `MonoidHomClass`.  -/
RingHomClass : (F : Type u_5) →
  (α : outParam (Type u_6)) →
    (β : outParam (Type u_7)) → [NonAssocSemiring α] → [NonAssocSemiring β] → [FunLike F α β] → Prop
-- Mathlib.Data.Set.Monotone
Monotone.domRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ (s : Set α), Monotone (s.domRestrict f)
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation_toSubmonoid : ∀ {M : Type u_1} [inst : MulOneClass M] {b : SaturatedSubmonoid M}, b.saturation = b
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- A subgroup of a seminormed group is also a seminormed group,
with the restriction of the norm.  -/
Subgroup.seminormedGroup : {E : Type u_1} → [inst : SeminormedGroup E] → {s : Subgroup E} → SeminormedGroup ↥s
-- Mathlib.Analysis.Complex.Tietze
RCLike.instTietzeExtensionTVS : ∀ {𝕜 : Type v} [inst : RCLike 𝕜] {E : Type w} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] [FiniteDimensional 𝕜 E],
  TietzeExtension E
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the convergents of `g` by evaluating the fraction described by `g` up to a given
position `n`. For example, `convs' [9; (1, 2), (3, 4), (5, 6)] 2 = 9 + 1 / (2 + 3 / 4)` and
`convs' [9; (1, 2), (3, 4), (5, 6)] 0 = 9`
 -/
GenContFract.convs' : {K : Type u_2} → [DivisionRing K] → GenContFract K → ℕ → K
-- Lean.Meta.Tactic.Apply
_private.Lean.Meta.Tactic.Apply.0.Lean.MVarId.apply.go : Lean.MVarId →
  Lean.Meta.ApplyConfig →
    Option Lean.MessageData →
      Lean.Expr → Lean.Expr → Std.Rco ℕ → ℕ → Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsometryEquiv.prodComm_toFun : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (a : M₁ × M₂),
  (QuadraticMap.IsometryEquiv.prodComm Q₁ Q₂) a = a.swap
-- Std.Data.TreeMap.Raw.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.TreeMap.Raw.forIn : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} → [Monad m] → (α → β → δ → m (ForInStep δ)) → δ → Std.TreeMap.Raw α β cmp → m δ
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq_mul_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (k : ℤ) (y : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.of_var_eq_mul_cert x k y p =
    p.beq' (Int.Internal.Linear.Poly.add 1 x (Int.Internal.Linear.Poly.add (-k) y (Int.Internal.Linear.Poly.num 0)))
-- Mathlib.Data.Int.Lemmas
Int.succ_natCast_pos : ∀ (n : ℕ), 0 < ↑n + 1
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.isUnit_exp : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸]
  [CompleteSpace 𝔸] (A : Matrix m m 𝔸), IsUnit (NormedSpace.exp A)
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The left adjoint of the adjunction which induces the comonad `(U, ε_ U, δ_ U)`.  -/
CategoryTheory.Cokleisli.Adjunction.fromCokleisli : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Comonad C) → CategoryTheory.Functor (CategoryTheory.Cokleisli U) C
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instCompleteLattice : {R : Type u} → {M : Type v} → [inst : SMul R M] → CompleteLattice (SubMulAction R M)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_le_of_mem : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n i : ι} {ω : Ω}, n ≤ i → u i ω ∈ s → MeasureTheory.hittingAfter u s n ω ≤ ↑i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l →
        ∀ {h' : k' ∈ Std.DTreeMap.Raw.Const.unitOfList l cmp},
          (Std.DTreeMap.Raw.Const.unitOfList l cmp).getKey k' h' = k
-- Mathlib.Data.ZMod.Basic
ZMod.cast_cast_zmod_of_le : ∀ {m n : ℕ} [hm : NeZero m], m ≤ n → ∀ (a : ZMod m), a.cast.cast = a
-- Init.Data.List.Erase
List.Sublist.erase : ∀ {α : Type u_1} [inst : BEq α] (a : α) {l₁ l₂ : List α}, l₁.Sublist l₂ → (l₁.erase a).Sublist (l₂.erase a)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.lTensor_id : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W},
  Representation.IntertwiningMap.lTensor ρ (Representation.IntertwiningMap.id σ) =
    Representation.IntertwiningMap.id (ρ.tprod σ)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Configurations that avoid a family `F` of patterns are stable under the shift.

Formally: if `x` avoids every `p ∈ F` at every position, then for any `h : G`,
the shifted configuration `mulShift h x` also avoids every `p ∈ F` at every position.  -/
SymbolicDynamics.FullShift.Pattern.mapsTo_mulShift_mulForbidden : ∀ {A : Type u_3} {G : Type u_4} [inst : Inhabited A] [inst_1 : Monoid G]
  (F : Set (SymbolicDynamics.FullShift.Pattern A G)) (h : G),
  Set.MapsTo (SymbolicDynamics.FullShift.mulShift h) (SymbolicDynamics.FullShift.mulForbidden F)
    (SymbolicDynamics.FullShift.mulForbidden F)
-- Init.Prelude
/-- Does this name have hygienic macro scopes?  -/
Lean.Name.hasMacroScopes : Lean.Name → Bool
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.fg_def : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : IntermediateField F E},
  S.FG ↔ ∃ t, t.Finite ∧ IntermediateField.adjoin F t = S
-- Mathlib.CategoryTheory.Limits.Cones
/-- Functorially precompose a cocone for `F` by a natural transformation `G ⟶ F` to give a cocone
for `G`.  -/
CategoryTheory.Limits.Cocone.precompose : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (G ⟶ F) → CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone G)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed : ∀ (K : Type u_1) [inst : Field K] (A : Type u_2) [inst_1 : Field A] [CharZero A] [inst_3 : CharZero K]
  [Algebra.IsAlgebraic ℚ K] [IsAlgClosed A], Nonempty (K →+* A)
-- Mathlib.Data.Finset.Image
Finset.attach_map_val : ∀ {α : Type u_1} {s : Finset α}, Finset.map (Function.Embedding.subtype fun x => x ∈ s) s.attach = s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k}, a ∈ (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl → compare k a ≠ Ordering.eq → a ∈ t
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_ground : ∀ {α : Type u} (M : Matroid α), M.cRk M.E = M.cRank
-- Mathlib.Data.Set.Image
Subtype.coe_preimage_self : ∀ {α : Type u_1} (s : Set α), Subtype.val ⁻¹' s = Set.univ
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.condIndep' : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {p1 p2 : Set (Set Ω)},
  (∀ s ∈ p1, MeasurableSet s) →
    (∀ s ∈ p2, MeasurableSet s) →
      IsPiSystem p1 →
        IsPiSystem p2 →
          ProbabilityTheory.CondIndepSets m' hm' p1 p2 μ →
            ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) hm' μ
-- Mathlib.Algebra.Polynomial.GroupRingAction
/-- the product of `(X - g • x)` over distinct `g • x`.  -/
prodXSubSMul : (G : Type u_2) →
  [inst : Group G] → [Fintype G] → (R : Type u_3) → [inst_2 : CommRing R] → [MulSemiringAction G R] → R → Polynomial R
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path includes the data of `n` 1-simplices in `X`.  -/
SSet.Path.arrow : {X : SSet} → {n : ℕ} → X.Path n → Fin n → X.obj (Opposite.op { len := 1 })
-- Mathlib.Analysis.PSeries
ENNReal.le_tsum_schlomilch : ∀ {u : ℕ → ℕ} {f : ℕ → ENNReal},
  (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) →
    (∀ (n : ℕ), 0 < u n) →
      StrictMono u → ∑' (k : ℕ), f k ≤ ∑ k ∈ Finset.range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
-- Mathlib.NumberTheory.MulChar.Duality
/-- The `MulEquiv` between the double dual `MulChar (MulChar M R) R` of `M` and `Mˣ`.
The image `m` of `η : MulChar (MulChar M R) R` is such that, for all `R`-valued multiplicative
character `χ` of `M`, we have `χ m = η χ`, see `MulChar.apply_mulCharEquiv`.
 -/
MulChar.mulCharEquiv : (M : Type u_1) →
  (R : Type u_2) →
    [inst : CommMonoid M] →
      [inst_1 : CommRing R] →
        [Finite M] → [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] → MulChar (MulChar M R) R ≃* Mˣ
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} →
        {L : CochainComplex C ℕ} →
          (d₀ : K.X 0 ⟶ L.X 0) →
            CategoryTheory.CategoryStruct.comp (K.d 1 0) d₀ = 0 →
              CategoryTheory.CategoryStruct.comp d₀ (L.d 0 1) = 0 → CochainComplex.ConnectData K L
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_const_vsub_iff`. -/
Sbtw.const_vsub : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P), Sbtw R x y z → Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z)
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
/-- The measure on `(0, +∞)` that has density `(· ^ n)` with respect to the Lebesgue measure.  -/
MeasureTheory.Measure.volumeIoiPow : ℕ → MeasureTheory.Measure ↑(Set.Ioi 0)
-- Mathlib.Algebra.Free
FreeMagma.length.eq_1 : ∀ {α : Type u} (x_1 : α), (FreeMagma.of x_1).length = 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
max_mul_min : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : CommSemigroup α] (a b : α), max a b * min a b = a * b
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.brecOn_1.eq : ∀ {motive_1 : Lean.Parser.Tactic.MCasesPat → Sort u} {motive_2 : List Lean.Parser.Tactic.MCasesPat → Sort u}
  (t : List Lean.Parser.Tactic.MCasesPat) (F_1 : (t : Lean.Parser.Tactic.MCasesPat) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Parser.Tactic.MCasesPat) → Lean.Parser.Tactic.MCasesPat.below_1 t → motive_2 t),
  Lean.Parser.Tactic.MCasesPat.brecOn_1 t F_1 F_2 = F_2 t (Lean.Parser.Tactic.MCasesPat.brecOn_1.go t F_1 F_2).2
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Generates an expression of the form `∃ (args), inner`. `args` is assumed to be a list of fvars.
When possible, `p ∧ q` is used instead of `∃ (_ : p), q`.  -/
Mathlib.Tactic.MkIff.mkExistsList : List Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul_inv_cancel : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → a * a⁻¹ = 1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeLeftOp_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp),
  (CategoryTheory.Limits.coconeOfConeLeftOp c).pt = Opposite.op c.pt
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
List.stronglyMeasurable_fun_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : Monoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  {m : MeasurableSpace α} (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.StronglyMeasurable f) →
    MeasureTheory.StronglyMeasurable fun x => (List.map (fun f => f x) l).prod
-- Mathlib.Order.Interval.Finset.Floor
Nat.cast_mem_Ico_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a b : α} {n : ℕ},
  ↑n ∈ Set.Ico a b ↔ n ∈ Finset.Ico ⌈a⌉₊ ⌈b⌉₊
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instSetLike : {R : Type u} →
  {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → SetLike (Subalgebra R A) A
-- Mathlib.RingTheory.Flat.CategoryTheory
Module.Flat.rTensor_shortComplex_exact : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) [Module.Flat R ↑M] (C : CategoryTheory.ShortComplex (ModuleCat R)),
  C.Exact → (C.map (CategoryTheory.MonoidalCategory.tensorRight M)).Exact
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.of_le_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B B' : IntermediateField F E},
  A.LinearDisjoint ↥B → B' ≤ B → A.LinearDisjoint ↥B'
-- Mathlib.CategoryTheory.DinatTrans
/-- The component of a natural transformation.  -/
CategoryTheory.DinatTrans.app : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} →
          CategoryTheory.DinatTrans F G → (X : C) → (F.obj (Opposite.op X)).obj X ⟶ (G.obj (Opposite.op X)).obj X
-- Mathlib.Data.Nat.Cast.Defs
two_add_one_eq_three : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], 2 + 1 = 3
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.inv_nonneg : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 ≤ p⁻¹
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union₀' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.AEDisjoint μ s t →
      autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_union₀'._auto_1 →
        autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_union₀'._auto_3 → μ.real (s ∪ t) = μ.real s + μ.real t
-- Mathlib.Topology.Neighborhoods
/-- **Alias** of the reverse direction of `mem_closure_iff_frequently`. -/
Filter.Frequently.mem_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, (∃ᶠ (x : X) in nhds x, x ∈ s) → x ∈ closure s
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instCoeFunHomForallCarrier : (X Y : SemiNormedGrp₁) → CoeFun (X ⟶ Y) fun x => X.carrier → Y.carrier
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W₁ : CategoryTheory.MorphismProperty Cᵒᵖ)
  [W₁.HasTwoOutOfThreeProperty], W₁.unop.HasTwoOutOfThreeProperty
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
SSet.coherentIso.invStructHom_inv : SSet.coherentIso.invStructHom.inv = SSet.coherentIso.inv
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` (where `a ≤ b`) and
has a derivative at `f' x` for all `x` in `(a, b)`, and `f'` is integrable on `[a, b]`, then
`∫ y in a..b, f' y` equals `f b - f a`.  -/
intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E},
  a ≤ b →
    ContinuousOn f (Set.Icc a b) →
      (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
        IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a
-- Mathlib.Algebra.Group.Units.Defs
Units.ext_iff : ∀ {α : Type u} [inst : Monoid α] {u v : αˣ}, u = v ↔ ↑u = ↑v
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.mem_span_map : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : S} {a : Set R},
  x ∈ Ideal.span (⇑(algebraMap R S) '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = IsLocalization.mk' S y z
-- Mathlib.MeasureTheory.Function.EssSup
essInf_eq_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : α → β), essInf f μ = sSup {a | μ {x | f x < a} = 0}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, k ∈ m.keys ↔ k ∈ m
-- Init.Data.SInt.Lemmas
ISize.lt_or_lt_of_ne : ∀ {a b : ISize}, a ≠ b → a < b ∨ b < a
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `FunLike.coe_zero`. -/
ContinuousLinearMap.coe_zero' : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.Analysis.Normed.Group.Uniform
LocallyLipschitz.mul : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E},
  LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz fun x => f x * g x
-- Mathlib.Algebra.Lie.Prod
LieAlgebra.Prod.instLieRing : {L₁ : Type u_2} → {L₂ : Type u_3} → [LieRing L₁] → [LieRing L₂] → LieRing (L₁ × L₂)
-- Mathlib.Algebra.Regular.Basic
/-- If adding `0` on either side is the identity, `0` is regular.  -/
isAddRegular_zero : ∀ {R : Type u_1} [inst : AddZeroClass R], IsAddRegular 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_iInf : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ι → G.Subgraph) (v : V),
  (⨅ i, f i).neighborSet v = (⋂ i, (f i).neighborSet v) ∩ G.neighborSet v
-- Lean.Expr
Lean.Int.mkInstLT : Lean.Expr
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_add : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f g : α → G},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
_private.Mathlib.Combinatorics.SimpleGraph.Acyclic.0.SimpleGraph.Walk.length.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2) (v v_1 : V) (h : G.Adj u v_1)
  (q : G.Walk v_1 v) (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_2 : V) → (h : G.Adj u v_2) → (q : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons h q)),
  (match v, SimpleGraph.Walk.cons h q with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h q => h_2 v v_2 h q) =
    h_2 v v_1 h q
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Composing an alternating map with the identity linear map in each argument.  -/
AlternatingMap.compLinearMap_id : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N), f.compLinearMap LinearMap.id = f
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- If a `J`-shaped diagram in `FullSubcategory P` has a colimit in `C` whose cocone point lives in
the full subcategory, then this defines a colimit in the full subcategory.  -/
CategoryTheory.Limits.createsColimitFullSubcategoryInclusion : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {P : CategoryTheory.ObjectProperty C} →
          (F : CategoryTheory.Functor J P.FullSubcategory) →
            [inst_2 : CategoryTheory.Limits.HasColimit (F.comp P.ι)] →
              P (CategoryTheory.Limits.colimit (F.comp P.ι)) → CategoryTheory.CreatesColimit F P.ι
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.const : ∀ (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion []), ms.Sorted
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.left_assoc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul self.X)
      (CategoryTheory.CategoryStruct.comp self.actLeft h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X self.X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.actLeft)
        (CategoryTheory.CategoryStruct.comp self.actLeft h))
-- Mathlib.Topology.Order.Basic
pi_Ico_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι]
  {a' b' x' : ι → α} [Nonempty ι], (∀ (i : ι), x' i < a' i) → (∀ (i : ι), b' i < x' i) → Set.Ico b' a' ∈ nhds x'
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasStrictDerivAt.sub` -/
HasStrictDerivAt.fun_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasStrictDerivAt f f' x → HasStrictDerivAt g g' x → HasStrictDerivAt (fun i => f i - g i) (f' - g') x
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangle_map_hom₂ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₂ = F.map f.hom₂
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_injective : ∀ {R : Type u_1} {A : Type u_2} [inst : Zero A], Function.Injective Unitization.inl