mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.Digits.Defs
/-- `digits b n` gives the digits, in little-endian order,
of a natural number `n` in a specified base `b`.

In any base, we have `ofDigits b L = L.foldr (fun x y ↦ x + b * y) 0`.
* For any `2 ≤ b`, we have `l < b` for any `l ∈ digits b n`,
  and the last digit is not zero.
  This uniquely specifies the behaviour of `digits b`.
* For `b = 1`, we define `digits 1 n = List.replicate n 1`.
* For `b = 0`, we define `digits 0 n = [n]`, except `digits 0 0 = []`.

Note this differs from the existing `Nat.toDigits` in core, which is used for printing numerals.
In particular, `Nat.toDigits b 0 = ['0']`, while `digits b 0 = []`.
 -/
Nat.digits : ℕ → ℕ → List ℕ
-- Mathlib.Data.Multiset.Fintype
Multiset.consEquiv_symm_some : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {v : α} {x : m.ToType},
  Multiset.consEquiv.symm (some x) = ⟨x.fst, Fin.castLE ⋯ x.snd⟩
-- Init.Data.SInt.Basic
/-- Converts an 16-bit signed integer into the 16-bit unsigned integer that is its two's complement
encoding.
 -/
Int16.toUInt16 : Int16 → UInt16
-- Lean.Expr
/-- `.mdata m e` is now the preferred form.
 -/
Lean.mkMData : Lean.MData → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.whiskeringRight₂_obj_obj_obj_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (D : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  (X_1 : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) (X_2 : B),
  ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).obj X).obj X_1).obj Y).obj X_2 =
    (X.obj (X_1.obj X_2)).obj (Y.obj X_2)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.instMonadRingOfMonadLift : (m n : Type → Type) →
  [MonadLift m n] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → Lean.Meta.Grind.Arith.CommRing.MonadRing n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Var : Type
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_addSubgroupOf_sup_of_le_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] {H N : AddSubgroup G},
  H ≤ AddSubgroup.normalizer ↑N → (N.addSubgroupOf (H ⊔ N)).Normal
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is associative  -/
NonUnitalRing.mul_assoc : ∀ {α : Type u_1} [self : NonUnitalRing α] (a b c : α), a * b * c = a * (b * c)
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.norm_resolvent_le_inv_infDist_support : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : MeasurableSpace 𝕜] [CompleteSpace 𝕜]
  [inst_3 : NormedDivisionRing A] [inst_4 : NormedAlgebra 𝕜 A] {μ : MeasureTheory.Measure 𝕜} {a : A},
  a ∉ ⇑(algebraMap 𝕜 A) '' μ.support →
    ∀ {x : 𝕜}, x ∈ μ.support → ‖resolvent a x‖ ≤ (Metric.infDist a (⇑(algebraMap 𝕜 A) '' μ.support))⁻¹
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.toSheafify_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.toSheafify J Q) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyMap J η)
-- Mathlib.Algebra.Algebra.Tower
/-- R ⟶ S induces S-Alg ⥤ R-Alg  -/
AlgEquiv.restrictScalars : (R : Type u) →
  {S : Type v} →
    {A : Type w} →
      {B : Type u₁} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Algebra S A] →
                    [inst_6 : Algebra S B] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] → [IsScalarTower R S A] → [IsScalarTower R S B] → (A ≃ₐ[S] B) → A ≃ₐ[R] B
-- Batteries.Data.Fin.Lemmas
Fin.findSomeRev?_succ : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → Option α},
  Fin.findSomeRev? f = (f (Fin.last n)).or (Fin.findSomeRev? fun i => f i.castSucc)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the morphisms in the covering of `S`  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.f : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {S : C} → (self : F.PreOneHypercoverDenseData S) → (i : self.I₀) → F.obj (self.X i) ⟶ S
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Max β] (f g : MeasureTheory.SimpleFunc α β),
  ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Lean.Expr
/-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or panics if out of bounds.  -/
Lean.Expr.getArg! : (e : Lean.Expr) → ℕ → optParam ℕ e.getAppNumArgs → Lean.Expr
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.map_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X ⟶ Z},
  CategoryTheory.Limits.biprod.map f g =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl) +
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd
        (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.smul_map : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : Module R S] (x : R)
  (f : ArithmeticFunction S) (n : ℕ), (x • f) n = x • f n
-- Init.Data.Vector.Zip
_private.Init.Data.Vector.Zip.0.Array.getElem?_zipWith.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : Option α) (x_1 : Option β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_2 : Option β) → motive x x_2),
  (∀ (a : α) (b : β), x = some a → x_1 = some b → False) →
    (match x, x_1 with
      | some a, some b => h_1 a b
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.beq.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      (Unit → motive [] []) →
        ((a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)) →
          ((x x_2 : List α) →
              (x = [] → x_2 = [] → False) →
                (∀ (a : α) (as : List α) (b : α) (bs : List α), x = a :: as → x_2 = b :: bs → False) → motive x x_2) →
            motive x x_1
-- Lean.Parser.Term
Lean.Parser.Term.matchExprPat : Lean.Parser.Parser
-- Mathlib.Data.Multiset.DershowitzManna
/-- A special case of `IsDershowitzMannaLT`. The transitive closure of it is used to define
an equivalent (proved later) version of the ordering.  -/
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.OneStep : {α : Type u_1} → [Preorder α] → Multiset α → Multiset α → Prop
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
SymmetricAlgebra.rank_eq : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  [Module.Free R M],
  Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) Cardinal.aleph0)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcReleaseParams.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {sessionId : UInt64} {refs : Array Lean.Json} {uri_1 : Lean.Lsp.DocumentUri}
  {sessionId_1 : UInt64} {refs_1 : Array Lean.Json},
  { uri := uri, sessionId := sessionId, refs := refs } = { uri := uri_1, sessionId := sessionId_1, refs := refs_1 } →
    uri = uri_1 ∧ sessionId = sessionId_1 ∧ refs = refs_1
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Ineq.WithStrictness.eq : Mathlib.Ineq.WithStrictness
-- Mathlib.GroupTheory.FiniteAbelian.Basic
/-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`.  -/
AddCommGroup.equiv_directSum_zmod_of_finite : ∀ (G : Type u) [inst : AddCommGroup G] [Finite G],
  ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ DirectSum ι fun i => ZMod (p i ^ e i))
-- Mathlib.RingTheory.PrincipalIdealDomain
IsField.isPrincipalIdealRing : ∀ {R : Type u_1} [inst : Ring R], IsField R → IsPrincipalIdealRing R
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- the first projection `Y j ⟶ X i₁`  -/
CategoryTheory.PreOneHypercover.p₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (self : CategoryTheory.PreOneHypercover S) → ⦃i₁ i₂ : self.I₀⦄ → (j : self.I₁ i₁ i₂) → self.Y j ⟶ self.X i₁
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
finite over `A`.  -/
IsIntegralClosure.finite : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C] [IsScalarTower A C L]
  [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A],
  Module.Finite A C
-- Mathlib.Algebra.Homology.Additive
/-- The `i`-th component of a chain map, as an additive map from chain maps to morphisms.  -/
HomologicalComplex.Hom.fAddMonoidHom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C₁ C₂ : HomologicalComplex V c} → (i : ι) → (C₁ ⟶ C₂) →+ (C₁.X i ⟶ C₂.X i)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.hole.sizeOf_spec : ∀ (name : Lean.TSyntax `Lean.binderIdent), sizeOf (Lean.Parser.Tactic.MRefinePat.hole name) = 1 + sizeOf name
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Real.instContinuousMapUniqueHom : ∀ {A : Type u_2} [inst : TopologicalSpace A] [T2Space A] [inst_2 : Ring A] [inst_3 : StarRing A] [inst_4 : Algebra ℝ A],
  ContinuousMap.UniqueHom ℝ A
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.constantCoeff.eq_1 : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.constantCoeff = MvPowerSeries.constantCoeff
-- Mathlib.Data.Fintype.Card
Fintype.card_punit : Fintype.card PUnit.{u_4 + 1} = 1
-- Mathlib.RingTheory.Invariant.Basic
/-- A technical lemma for `fixed_of_fixed1`.  -/
_private.Mathlib.RingTheory.Invariant.Basic.0.fixed_of_fixed1_aux3 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [NoZeroDivisors B]
  {b : B} {i j : ℕ} {p : Polynomial A},
  Polynomial.map (algebraMap A B) p = (Polynomial.X - Polynomial.C b) ^ i * Polynomial.X ^ j →
    ∀ (f : B ≃ₐ[A] B), i ≠ 0 → f b = b
-- Mathlib.Order.CompleteLattice.Defs
isLUB_sSup : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] (s : Set α), IsLUB s (sSup s)
-- Mathlib.Algebra.Group.Basic
mul_eq_of_eq_inv_mul : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, b = a⁻¹ * c → a * b = c
-- Mathlib.Order.ModularLattice
/-- The diamond isomorphism between the intervals `Set.Iic a` and `Set.Ici b`.  -/
IsCompl.IicOrderIsoIci : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : BoundedOrder α] → [IsModularLattice α] → {a b : α} → IsCompl a b → ↑(Set.Iic a) ≃o ↑(Set.Ici b)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.natCast_mul_comp : ∀ {R : Type u} [inst : Semiring R] {p r : Polynomial R} {n : ℕ}, (↑n * p).comp r = ↑n * p.comp r
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Lp.toTemperedDistributionCLM.congr_simp : ∀ {E : Type u_3} (F : Type u_4) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : CompleteSpace F] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
  (μ : MeasureTheory.Measure E) [inst_7 : μ.HasTemperateGrowth] (p : ENNReal) [hp : Fact (1 ≤ p)],
  MeasureTheory.Lp.toTemperedDistributionCLM F μ p = MeasureTheory.Lp.toTemperedDistributionCLM F μ p
-- Lean.Declaration
Lean.instInhabitedDefinitionVal.default : Lean.DefinitionVal
-- Mathlib.Algebra.Algebra.Basic
isSMulRegular_algebraMap_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [IsScalarTower R A M] {r : R},
  IsSMulRegular M ((algebraMap R A) r) ↔ IsSMulRegular M r
-- Mathlib.Data.FunLike.IsApply
IsSubApply.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.LinearAlgebra.Prod
Submodule.fst_map_snd : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Submodule.map (LinearMap.snd R M M₂) (Submodule.fst R M M₂) = ⊥
-- Mathlib.Topology.Order.HullKernel
PrimitiveSpectrum.hull.eq_1 : ∀ {α : Type u_1} [inst : SemilatticeInf α] (T : Set α) (a : α), PrimitiveSpectrum.hull T a = Subtype.val ⁻¹' Set.Ici a
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_mono : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, s ⊆ t → μ s ≤ μ t
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (m.insertIfNew k v).contains k = true
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.comp.sizeOf_spec : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.ToPartrec.Cont),
  sizeOf (Turing.ToPartrec.Cont.comp a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `α ▷ f`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight.mkEvalWhiskerRightNil : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m] →
    Mathlib.Tactic.BicategoryLike.Structural → Mathlib.Tactic.BicategoryLike.Mor₁ → m Lean.Expr
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- A bundled version of `AddMonoidAlgebra.divOf`.  -/
AddMonoidAlgebra.divOfHom : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] →
      [inst_1 : AddCommMonoid G] → [IsCancelAdd G] → Multiplicative G →* AddMonoid.End (AddMonoidAlgebra k G)
-- Mathlib.Order.Grade
OrderDual.gradeMinOrder : {𝕆 : Type u_1} →
  {α : Type u_3} → [inst : Preorder 𝕆] → [inst_1 : Preorder α] → [GradeMaxOrder 𝕆 α] → GradeMinOrder 𝕆ᵒᵈ αᵒᵈ
-- Mathlib.RingTheory.IsPrimary
Submodule.IsPrimary.radical_colon_singleton_eq_ite : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Submodule R M},
  S.IsPrimary →
    ∀ (m : M) [inst_3 : Decidable (m ∈ S)], (S.colon {m}).radical = if m ∈ S then ⊤ else (S.colon Set.univ).radical
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_comp : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst : NormedField 𝕜₁]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : Module 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [inst_9 : Module 𝕜₂ F]
  [inst_10 : AddCommGroup G] [inst_11 : TopologicalSpace G] [inst_12 : Module 𝕜₃ G] (g : F →SWOT[σ₂₃] G)
  (f : E →SWOT[σ₁₂] F), (g.comp f).toCLM = g.toCLM ∘SL f.toCLM
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstHAddInt : Lean.Expr → Lean.MetaM Bool
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Mathlib.RingTheory.Polynomial.DegreeLT
/-- Basis for `R[X]_n` given by `X^i` with `i < n`.  -/
Polynomial.degreeLT.basis : (R : Type u_1) → [inst : Semiring R] → (n : ℕ) → Module.Basis (Fin n) R ↥(Polynomial.degreeLT R n)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_indicator₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet s μ → ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Analysis.Normed.Group.Constructions
MulOpposite.nnnorm_unop : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] (a : Eᵐᵒᵖ), ‖MulOpposite.unop a‖₊ = ‖a‖₊
-- Mathlib.Data.Finset.Sort
/-- Given a finset `s` of size at least `k` in a linear order `α`, the map `orderEmbOfCardLe`
is an order embedding from `Fin k` to `α` whose image is contained in `s`. Specifically, it maps
`Fin k` to an initial segment of `s`.  -/
Finset.orderEmbOfCardLe : {α : Type u_1} → [inst : LinearOrder α] → (s : Finset α) → {k : ℕ} → k ≤ s.card → Fin k ↪o α
-- Mathlib.GroupTheory.Commutator.Basic
instCharacteristicCommutator : ∀ (G : Type u_1) [inst : Group G], (commutator G).Characteristic
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.introsS.tacticBuilder : Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- **Alias** of `SimpleGraph.isBridge_iff_forall_cycle_notMem`. -/
SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem : ∀ {V : Type u} {G : SimpleGraph V} {e : Sym2 V},
  e ∈ G.edgeSet → (G.IsBridge e ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges)
-- Mathlib.RepresentationTheory.Invariants
Rep.invariantsFunctor_obj_carrier : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G] (A : Rep.{w, u, v} k G),
  ↑((Rep.invariantsFunctor k G).obj A) = { x // ∀ (g : G), (A.ρ g) x = x }
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.smul : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂},
  f.HasFiniteRange → ∀ (c : K), (c • f).HasFiniteRange
-- Mathlib.CategoryTheory.Discrete.Basic
/-- A wrapper for promoting any type to a category,
with the only morphisms being equalities.  -/
CategoryTheory.Discrete.as : {α : Type u₁} → CategoryTheory.Discrete α → α
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- From a simple graph on `V`, construct the edge labeling on the complete graph of `V` given where
edges are labeled `1` and non-edges are labeled `0`.
 -/
SimpleGraph.toTopEdgeLabeling : {V : Type u_1} → (G : SimpleGraph V) → [DecidableRel G.Adj] → SimpleGraph.TopEdgeLabeling V (Fin 2)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInr.eq_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  T.tensorInr =
    CategoryTheory.Limits.pushout.inr
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap f T.x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap g T.y))
-- Mathlib.RingTheory.Finiteness.Defs
Module.Finite.iff_addGroup_fg : ∀ {G : Type u_6} [inst : AddCommGroup G], Module.Finite ℤ G ↔ AddGroup.FG G
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- The pullback commutes with the Lie bracket of vector fields on manifolds. Version where one
assumes that the map is smooth on a larger set `u` (so that the
condition `x₀ ∈ closure (interior u)`, needed to guarantee the symmetry of the second derivative,
becomes easier to check.)  -/
VectorField.mpullbackWithin_mlieBracketWithin' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [IsManifold I (minSmoothness 𝕜 2) M]
  [inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'] [CompleteSpace E] {n : WithTop ℕ∞} {f : M → M'}
  {V W : (x : M') → TangentSpace I' x} {x₀ : M} {s u : Set M} {t : Set M'},
  MDiffAt[t] (T% V) (f x₀) →
    MDiffAt[t] (T% W) (f x₀) →
      UniqueMDiff[s] →
        UniqueMDiff[u] →
          ContMDiffWithinAt I I' n f u x₀ →
            x₀ ∈ s →
              minSmoothness 𝕜 2 ≤ n →
                f ⁻¹' t ∈ nhdsWithin x₀ s →
                  x₀ ∈ closure (interior u) →
                    s ⊆ u →
                      VectorField.mpullbackWithin I I' f (VectorField.mlieBracketWithin I' V W t) s x₀ =
                        VectorField.mlieBracketWithin I (VectorField.mpullbackWithin I I' f V s)
                          (VectorField.mpullbackWithin I I' f W s) s x₀
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_toSpanSingleton : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  {M₂ : Type u_6} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
  [inst_6 : Module R₁ M₂] [inst_7 : TopologicalSpace R₁] [inst_8 : ContinuousSMul R₁ M₂] [inst_9 : ContinuousSMul R₁ M₁]
  (f : M₁ →L[R₁] M₂) (x : M₁),
  f ∘SL ContinuousLinearMap.toSpanSingleton R₁ x = ContinuousLinearMap.toSpanSingleton R₁ (f x)
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.coe_of : ∀ {L : FirstOrder.Language} {T : L.Theory} {M : Type w} [inst : L.Structure M] [inst_1 : Nonempty M] (h : M ⊨ T),
  ↑h.bundled = M
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mulEquivToUnitHom_symm_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ),
  MulChar.mulEquivToUnitHom.symm f = MulChar.equivToUnitHom.symm f
-- Std.Time.Format.Basic
Std.Time.instInhabitedFormatConfig.default : Std.Time.FormatConfig
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  (X.kernelSequenceOpcycles f g fg h n).X₂ = (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosedIn.exists_algebraMap_eq_of_pow_mem_subalgebra : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Subalgebra R A}
  [IsIntegrallyClosedIn (↥S) A] {x : A} {n : ℕ}, 0 < n → x ^ n ∈ S → ∃ y, (algebraMap (↥S) A) y = x
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tfst_eq_fst_id : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α α' β : Type u} (f : α → α')
  (x : t α β), Bitraversable.tfst (pure ∘ f) x = pure (Bifunctor.fst f x)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.mulAction : {m : Type u_2} →
  {n : Type u_3} → {R : Type u_7} → {α : Type v} → [inst : Monoid R] → [MulAction R α] → MulAction R (Matrix m n α)