mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instCoeMonCat.eq_1 : CommMonCat.instCoeMonCat = { coe := (CategoryTheory.forget₂ CommMonCat MonCat).obj }
-- Mathlib.Data.Set.Lattice
Set.iUnion_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : α ⊕ β → Set γ}, ⋃ x, s x = (⋃ x, s (Sum.inl x)) ∪ ⋃ x, s (Sum.inr x)
-- Init.Data.String.Basic
String.Pos.utf8ByteSize_byte : ∀ {s : String} {pos : s.Pos} {h : pos ≠ s.endPos}, (pos.byte h).utf8ByteSize ⋯ = (pos.get h).utf8Size
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Ioo : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → ∀ (b c : G₀), (fun x => a * x) '' Set.Ioo b c = Set.Ioo (a * b) (a * c)
-- Init.Control.Lawful.MonadLift.Instances
Except.bind.eq_2 : ∀ {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → Except ε β) (v : α), (Except.ok v).bind f = f v
-- Mathlib.Data.Finset.Fold
Finset.fold_sup_bot_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Finset.fold (fun x1 x2 => x1 ⊔ x2) ⊥ singleton s = s
-- Mathlib.Logic.Basic
dec_em' : ∀ (p : Prop) [Decidable p], ¬p ∨ p
-- Mathlib.Algebra.Group.ULift
ULift.mulOneClass.eq_1 : ∀ {α : Type u} [inst : MulOneClass α], ULift.mulOneClass = Function.Injective.mulOneClass ⇑Equiv.ulift ⋯ ⋯ ⋯
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.isQuotientMap_nsmul : ∀ {α : Type u_2} [inst : TopologicalSpace α] {M : Type u_4} {β : Type u_5} [inst_1 : Semiring M]
  [inst_2 : AddCommMonoid α] [inst_3 : Module M α] [ContinuousConstSMul M α] [inst_5 : AddMonoid β] (f : α →+ β)
  [inst_6 : TopologicalSpace β],
  Topology.IsQuotientMap ⇑f → ∀ (n : ℕ), IsUnit ↑n → Topology.IsQuotientMap fun x => n • x
-- Mathlib.Order.Interval.Set.Defs
Set.Ioi.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (b : α), Set.Ioi b = {x | b < x}
-- Mathlib.Algebra.DirectSum.Module
AddHomClass.toAddHom.congr_simp : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Batteries.Data.List.Basic
/-- If all elements of `xs` are `some xᵢ`, `allSome xs` returns the `xᵢ`. Otherwise
it returns `none`.
```
allSome [some 1, some 2] = some [1, 2]
allSome [some 1, none  ] = none
```
 -/
List.allSome : {α : Type u_1} → List (Option α) → Option (List α)
-- Init.Data.SInt.Basic
/-- Constructs an `Int64` from an `Int`, clamping if the value is too small or too large.  -/
Int64.ofIntTruncate : ℤ → Int64
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withUsed : {α : Type} →
  Array Lean.Elab.Command.InductiveElabStep2 →
    Array Lean.Expr → List Lean.InductiveType → (Array Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- An additive action of an additive group is quasipreprimitive if any normal subgroup
that has no fixed point acts pretransitively  -/
AddAction.IsQuasiPreprimitive : (G : Type u_1) → (X : Type u_2) → [inst : AddGroup G] → [AddAction G X] → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.δ₁_mk₂_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 1))
      (CategoryTheory.ComposableArrows.mk₂ f g) =
    CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.CategoryStruct.comp f g)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instPropAsSPredTautologyEntailsPureTrue : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, Std.Do.SPred.Tactic.PropAsSPredTautology (⊢ₛ P) P
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono : ∀ {X : AlgebraicGeometry.Scheme}, Monotone AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens
-- Mathlib.Analysis.Analytic.ChangeOrigin
AnalyticAt.eventually_analyticAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {x : E}, AnalyticAt 𝕜 f x → ∀ᶠ (y : E) in nhds x, AnalyticAt 𝕜 f y
-- Std.Data.DTreeMap.Internal.Operations
/-- Inserts an element at the end of the tree.  -/
Std.DTreeMap.Internal.Impl.insertMax : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Std.DTreeMap.Internal.Impl.Tree α β (t.size + 1)
-- Mathlib.FieldTheory.Finite.Basic
Algebra.IsAlgebraic.algEquivEquivAlgHom.congr_simp : ∀ (K : Type u_1) (L : Type u_2) [inst : CommRing K] [inst_1 : IsDomain K] [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Module.IsTorsionFree K L] [inst_5 : Algebra.IsAlgebraic K L],
  Algebra.IsAlgebraic.algEquivEquivAlgHom K L = Algebra.IsAlgebraic.algEquivEquivAlgHom K L
-- Mathlib.Order.Sublocale
/-- A sublocale of a locale `X` is a set `S` which is closed under all meets and such that
`x ⇨ s ∈ S` for all `x : X` and `s ∈ S`.

Note that locales are the same thing as frames, but with reverse morphisms, which is why we assume
`Frame X`. We only need to define locales categorically. See `Locale`.  -/
Sublocale : (X : Type u_2) → [Order.Frame X] → Type u_2
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncTotal_eq_ite : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R)
  {x : σ →₀ ℕ},
  MvPolynomial.coeff x ((MvPowerSeries.truncTotal n) p) = if Finsupp.degree x < n then (MvPowerSeries.coeff x) p else 0
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.GrothendieckTopology.instHasIsosToPrecoverage : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (J : CategoryTheory.GrothendieckTopology C),
  J.toPrecoverage.HasIsos
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.equiv_iff : ∀ {R : Type u} [inst : Ring R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type w}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), Module.IsStablyFree R M ↔ Module.IsStablyFree R N
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.inter_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.inter m₂ = m₁ ∩ m₂
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Sheaf.terminal_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {X : A} (hX : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.Sheaf.terminal J hX).obj = (CategoryTheory.Functor.const Cᵒᵖ).obj X
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.toZeroHom_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Action.Basic
Action.ρAut_apply_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Group G] (A : Action V G)
  (g : G), (A.ρAut g).hom = A.ρ g
-- Mathlib.CategoryTheory.DifferentialObject
/-- A morphism of differential objects is a morphism commuting with the differentials.  -/
CategoryTheory.DifferentialObject.Hom : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            CategoryTheory.DifferentialObject S C → CategoryTheory.DifferentialObject S C → Type v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {f : α → Bool}
  {k : α}, t.WF → (Std.TreeMap.Raw.filter (fun k x => f k) t).getKey? k = Option.filter f (t.getKey? k)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.ae_tendsto_ofReal_norm : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {F : ℕ → α → β} {f : α → β},
  (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
    ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => ENNReal.ofReal ‖F n a‖) Filter.atTop (nhds (ENNReal.ofReal ‖f a‖))
-- Mathlib.Tactic.FunProp.Theorems
/-- TheoremForm to string  -/
Mathlib.Meta.FunProp.instToStringTheoremForm : ToString Mathlib.Meta.FunProp.TheoremForm
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.strictMono_valueGroupEquiv : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀),
  StrictMono ⇑(WithVal.valueGroupEquiv v)
-- Mathlib.GroupTheory.GroupAction.Defs
FixedPoints.instSMulCommClassSubtypeMemSubgroupSubgroup : ∀ (M : Type u) (α : Type v) [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction M α],
  SMulCommClass M (↥(FixedPoints.subgroup M α)) α
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.add_comp : ∀ {R : Type u} [inst : Semiring R] {p q r : Polynomial R}, (p + q).comp r = p.comp r + q.comp r
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
instIsGaloisGroupRingOfIntegersOfNumberField : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [NumberField K] [NumberField L]
  [inst_4 : Algebra K L] (G : Type u_3) [inst_5 : Group G] [inst_6 : MulSemiringAction G L] [IsGaloisGroup G K L],
  IsGaloisGroup G (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)
-- Mathlib.Algebra.Group.Action.Defs
eq_inv_smul_iff : ∀ {G : Type u_3} {α : Type u_5} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a b : α}, a = g⁻¹ • b ↔ g • a = b
-- Lean.Meta.Tactic.Grind.Internalize
/-- Internalizer for nonparametric literals (see `isNonParametricLitValue`).
For this kind of literal, we do **not** internalize its children nor
we activate theorems associated with their function symbol.
This is relevant because we do not want to internalize, for example,
the raw natural value in `OfNat.ofNat`. We also do not want to normalize
the `2` in the integer literal `-2`.

We used to use this optimization for parametric literals too. However,
it triggered a bug during E-matching because we could have patterns of
the form ``[P #0 (@OfNat.ofNat (Fin _) `[0] _)]``. See issue #11545.

We still have support for parametric `OfNat.ofNat` literals since we don't
want to internalize the raw natural value there. See `internalizeOfNatFinBitVecLiteral`.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizeNonParametricLiteral : Lean.Expr → ℕ → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Combinatorics.Quiver.Path
/-- Given decidable equality on paths of length up to `n`, we can construct
decidable equality on paths of length up to `n + 1`.  -/
Quiver.Path.decidableEqBddPathsOfDecidableEq : {V : Type u_1} →
  [inst : Quiver V] →
    (n : ℕ) →
      DecidableEq V →
        ((v w : V) → DecidableEq (v ⟶ w)) →
          ((v w : V) → DecidableEq (Quiver.Path.BoundedPaths v w n)) →
            (v w : V) → DecidableEq (Quiver.Path.BoundedPaths v w (n + 1))
-- Mathlib.Topology.Semicontinuity.Defs
/-- A real function `f` is lower semicontinuous if, for any `ε > 0`, for any `x`, for all `x'` close
enough to `x`, then `f x'` is at least `f x - ε`. We formulate this in a general preordered space,
using an arbitrary `y < f x` instead of `f x - ε`.  -/
LowerSemicontinuous : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → Prop
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.pappAck.eq_1 : Nat.Partrec.Code.pappAck 0 = Nat.Partrec.Code.succ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.CompletionParams
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- In two linearly ordered additive groups, the closure of an element of one group
is isomorphic (and order-isomorphic) to the closure of an element in the other group.  -/
LinearOrderedAddCommGroup.closure_equiv_closure : {G : Type u_1} →
  {G' : Type u_2} →
    [inst : AddCommGroup G] →
      [inst_1 : LinearOrder G] →
        [IsOrderedAddMonoid G] →
          [inst_3 : AddCommGroup G'] →
            [inst_4 : LinearOrder G'] →
              [IsOrderedAddMonoid G'] →
                (x : G) → (y : G') → (x = 0 ↔ y = 0) → ↥(AddSubgroup.closure {x}) ≃+o ↥(AddSubgroup.closure {y})
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.unop_X₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ}
  (L : Φ.op.RightResolution X₂), L.unop.X₁ = Opposite.unop L.X₁
-- Lean.Data.RArray
/-- The correctness theorem for `ofFn`  -/
Lean.RArray.get_ofFn : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (h : 0 < n) (i : Fin n), (Lean.RArray.ofFn f h).get ↑i = f i
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f` is meromorphic of finite order at a point `x`, the trailing coefficient is defined as the
(unique!) value `g x` for a presentation of `f` in the form `(z - x) ^ order • g z` with `g`
analytic at `x`. In all other cases, the trailing coefficient is defined to be zero.
 -/
meromorphicTrailingCoeffAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → E
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Mk₁.obj.eq_2 : ∀ {C : Type u_1} (X₀ X₁ : C) (isLt : 1 < 2), CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨1, isLt⟩ = X₁
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.sup'_id_eq_csSup : ∀ {α : Type u_2} [inst : ConditionallyCompleteLattice α] (s : Finset α) (hs : s.Nonempty), s.sup' hs id = sSup ↑s
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_arrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (S : CategoryTheory.Sieve Y),
  (CategoryTheory.Sieve.pullback f S).arrows = CategoryTheory.Presieve.pullback f S.arrows
-- Mathlib.Analysis.Analytic.Basic
/-- In a complete space, the sum of a converging power series `p` admits `p` as a power series.
This is not totally obvious as we need to check the convergence of the series.  -/
FormalMultilinearSeries.hasFPowerSeriesOnBall : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
  (p : FormalMultilinearSeries 𝕜 E F), 0 < p.radius → HasFPowerSeriesOnBall p.sum p 0 p.radius
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- pseudoemetric space instance on the product of finitely many pseudoemetric spaces, using the
`L^p` pseudoedistance, and having as uniformity the product uniformity.  -/
PiLp.instPseudoEMetricSpace : (p : ENNReal) →
  {ι : Type u_2} →
    (β : ι → Type u_4) →
      [hp : Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → PseudoEMetricSpace (β i)] → PseudoEMetricSpace (PiLp p β)
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_eq_sInf_n_pos_IsPeriodicPt : ∀ {α : Type u_1} {f : α → α} {x : α}, Function.minimalPeriod f x = sInf {n | n > 0 ∧ Function.IsPeriodicPt f n x}
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- If `f` is an `n` times continuously differentiable homeomorphism,
and if the derivative of `f` at each point is a continuous linear equivalence,
then `f.symm` is `n` times continuously differentiable.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
Homeomorph.contDiff_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  [CompleteSpace E] (f : E ≃ₜ F) {f₀' : E → E ≃L[𝕜] F},
  (∀ (a : E), HasFDerivAt (⇑f) (↑(f₀' a)) a) → ContDiff 𝕜 n ⇑f → ContDiff 𝕜 n ⇑f.symm
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineBasisCover.eq_1 : ∀ (X : AlgebraicGeometry.Scheme),
  X.affineBasisCover =
    CategoryTheory.Precoverage.ZeroHypercover.bind X.affineCover fun x =>
      AlgebraicGeometry.Scheme.affineBasisCoverOfAffine ((fun x => Classical.choose ⋯) x)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.beta.inj : ∀ {e e_1 : Lean.Expr}, Lean.Meta.Grind.SplitSource.beta e = Lean.Meta.Grind.SplitSource.beta e_1 → e = e_1
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.mulEquiv_coe_eq : ∀ {X Y : Type u_1} [inst : Mul X] [inst_1 : Mul Y] (e : X ≃* Y), MagmaCat.Hom.hom (MagmaCat.ofHom ↑e) = ↑e
-- Init.Data.UInt.Lemmas
USize.toBitVec_one : USize.toBitVec 1 = 1#System.Platform.numBits
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_insert : ∀ {α : Type u_1} {s : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α] {a : α}, (insert a s)ᶜ = sᶜ.erase a
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.eq_of_sum_take_eq : ∀ {M : Type u_4} [inst : AddLeftCancelMonoid M] {L L' : List M},
  L.length = L'.length → (∀ i ≤ L.length, (List.take i L).sum = (List.take i L').sum) → L = L'
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral_add : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] (f g : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.integral (f + g) =
    MeasureTheory.L1.SimpleFunc.integral f + MeasureTheory.L1.SimpleFunc.integral g
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.Context.mk : Bool → Lean.Meta.Sym.Canon.Context✝
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.div_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] (a b : X ≃ₜ X), a / b = DivInvMonoid.div' a b
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.irreducible_of_degree_eq_one : ∀ {R : Type u} [inst : Field R] {p : Polynomial R}, p.degree = 1 → Irreducible p
-- Std.Time.Zoned.TimeZone
/-- Creates an `Offset` from a given number of hours and minutes.
 -/
Std.Time.TimeZone.Offset.ofHoursAndMinutes : Std.Time.Hour.Offset → Std.Time.Minute.Offset → Std.Time.TimeZone.Offset
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.transpose_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} (M : CStarMatrix m n A) (i : n) (j : m), M.transpose i j = M j i
-- Init.Data.Vector.Lemmas
Vector.back_append_of_neZero : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} [inst : NeZero m], (xs ++ ys).back = ys.back
-- Lean.Environment
Lean.Kernel.resetDiag : Lean.Environment → Lean.Environment
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.takeWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.takeWhile pat = s.sliceTo (s.skipPrefixWhile pat)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Lift a morphism `k : W ⟶ Y`, equalized by the two morphisms `left` and `right`, along `f`.  -/
CategoryTheory.IsRegularMono.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y W : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.IsRegularMono f] →
          (k : W ⟶ Y) →
            CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.left f) =
                CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.right f) →
              (W ⟶ X)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_finsetSum : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {ι : Type u_9} {s : Finset ι}
  [inst_13 : ContinuousAdd M₂] [inst_14 : ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃) (f : ι → M₁ →SL[σ₁₂] M₂),
  g ∘SL ∑ i ∈ s, f i = ∑ i ∈ s, g ∘SL f i
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.nnorm_le_mul : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F} {K : NNReal},
  LipschitzWith K f → f 0 = 0 → ∀ (x : E), ‖f x‖₊ ≤ K * ‖x‖₊
-- Mathlib.Order.RelClasses
instTrichotomousLe : ∀ {α : Type u} [inst : LinearOrder α], Std.Trichotomous fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- There is an initial functor from a small category.  -/
CategoryTheory.InitiallySmall.initial_smallCategory : ∀ {J : Type u} {inst : CategoryTheory.Category.{v, u} J} [self : CategoryTheory.InitiallySmall J], ∃ S x F, F.Initial
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The underlying function. Use coercion instead.  -/
ContDiffMapSupportedIn.toFun : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → ContDiffMapSupportedIn E F n K → E → F
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_single_mul_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M] [IsCancelAdd M] (x : AddMonoidAlgebra R M)
  (r : R) (m m' : M), (AddMonoidAlgebra.single m r * x).coeff (m + m') = r * x.coeff m'
-- Mathlib.Algebra.Order.Field.Basic
lt_inv_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (a < b⁻¹ ↔ b < a⁻¹)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.equivMvPolynomial_symm_X_0 : ∀ {R : Type u_1} [inst : CommSemiring R],
  (Polynomial.Bivariate.equivMvPolynomial R).symm (MvPolynomial.X 0) = Polynomial.C Polynomial.X
-- Init.Prelude
Nat.le.brecOn : ∀ {n : ℕ} {motive : (a : ℕ) → n.le a → Prop} {a : ℕ} (t : n.le a),
  (∀ (a : ℕ) (t : n.le a), Nat.le.below t → motive a t) → motive a t
-- Lean.Data.AssocList
Lean.AssocList.brecOn.eq : ∀ {α : Type u} {β : Type v} {motive : Lean.AssocList α β → Sort u_1} (t : Lean.AssocList α β)
  (F_1 : (t : Lean.AssocList α β) → Lean.AssocList.below t → motive t),
  Lean.AssocList.brecOn t F_1 = F_1 t (Lean.AssocList.brecOn.go t F_1).2
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_naturality_middle : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h)
      (CategoryTheory.Bicategory.associator f g' h).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h))