mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.isMultiplicative_zeta : ArithmeticFunction.zeta.IsMultiplicative
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d₀_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (self : CochainComplex.ConnectData K L) {Z : C} (h : L.X 1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.d₀ (CategoryTheory.CategoryStruct.comp (L.d 0 1) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.add_eq_lt : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] {a₁ b₁ a₂ b₂ : α},
  a₁ = b₁ → a₂ < b₂ → a₁ + a₂ < b₁ + b₂
-- Mathlib.Order.Sublocale
_private.Mathlib.Order.Sublocale.0.Sublocale.restrictAux.eq_1 : ∀ {X : Type u_1} [inst : Order.Frame X] (S : Sublocale X) (a : X), Sublocale.restrictAux✝ S a = sInf {s | a ≤ ↑s}
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.toNorm : {E : Type u_8} → [self : NormedAddCommGroup E] → Norm E
-- Lean.Meta.Tactic.Simp.Main
/-- Simplify `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
otherwise, where `proof' : prop'` and `prop'` is the simplified `prop`.

This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context.  -/
Lean.Meta.simpStep : Lean.MVarId →
  Lean.Expr →
    Lean.Expr →
      Lean.Meta.Simp.Context →
        optParam Lean.Meta.Simp.SimprocsArray #[] →
          optParam (Option Lean.Meta.Simp.Discharge) none →
            optParam Bool true →
              optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Option (Lean.Expr × Lean.Expr) × Lean.Meta.Simp.Stats)
-- Mathlib.CategoryTheory.Idempotents.Basic
/-- In a preadditive category, when `p : X ⟶ X` is idempotent,
then `𝟙 X - p` is also idempotent.  -/
CategoryTheory.Idempotents.idem_of_id_sub_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X : C}
  (p : X ⟶ X),
  CategoryTheory.CategoryStruct.comp p p = p →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X - p)
        (CategoryTheory.CategoryStruct.id X - p) =
      CategoryTheory.CategoryStruct.id X - p
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instFourierTransformInv : {E : Type u_1} →
  {F : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : MeasurableSpace E] →
        [inst_2 : BorelSpace E] →
          [inst_3 : NormedAddCommGroup F] →
            [InnerProductSpace ℂ F] →
              [CompleteSpace F] →
                [inst_6 : InnerProductSpace ℝ E] →
                  [inst_7 : FiniteDimensional ℝ E] →
                    FourierTransformInv ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
                      ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_add : ∀ {α : Type u_1} [inst : Add α] (a b : Lex α), ofLex (a + b) = ofLex a + ofLex b
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.match_1.splitter : (motive : List ℕ → Sort u_1) →
  (x : List ℕ) → (Unit → motive []) → ((ys : List ℕ) → (ys = [] → False) → motive ys) → motive x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.nodup_toList : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] {a : α}, (*...=a).toList.Nodup
-- Mathlib.CategoryTheory.Action.Monoidal
_private.Mathlib.CategoryTheory.Action.Monoidal.0.Action.diagonalSuccIsoTensorTrivial.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀ : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues₀) Finset.univ.val
-- Batteries.Data.List.Lemmas
List.swap_nil : ∀ {α : Type u_1} {i j : ℕ}, [].swap i j = []
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_sup_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ (S T : Submonoid M), Submonoid.comap f (Submonoid.map f S ⊔ Submonoid.map f T) = S ⊔ T
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point, but with full pullback.  -/
ContMDiffWithinAt.mpullback_vectorField_preimage : ∀ {𝕜 : 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'] {f : M → M'} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t (f x₀) →
    ContMDiffAt I I' n f x₀ →
      (mfderiv% f x₀).IsInvertible →
        m + 1 ≤ n → ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullback I I' f V x⟩) (f ⁻¹' t) x₀
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.decidableMemCenter : {G : Type u_1} → [inst : Group G] → (z : G) → [Decidable (∀ (g : G), g * z = z * g)] → Decidable (z ∈ Subgroup.center G)
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.lift_unique : ∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : CommGroup A] (f : G →* A) (φ : Abelianization G →* A),
  (∀ (x : G), φ (Abelianization.of x) = f x) → ∀ {x : Abelianization G}, φ x = (Abelianization.lift f) x
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- For any element `x` of `M ⊗[R] N`, there exists a finite subset `{ (m_i, n_i) }`
of `M × N` such that each `n_i` is distinct (we represent it as an element of `N →₀ M`),
such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`.  -/
TensorProduct.exists_finsupp_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R M N),
  ∃ S, x = S.sum fun n m => m ⊗ₜ[R] n
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Internal.iter_roc_eq_iter_rcc_of_isSome_succ? : ∀ {α : Type u} [LE α] [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {lo hi : α}
  (h : (Std.PRange.succ? lo).isSome = true),
  (Std.Roc.Internal.iter lo<...=hi) = Std.Rcc.Internal.iter ((Std.PRange.succ? lo).get h)...=hi
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- The `PullbackObjObj` structure given by the pullback of the limits API.  -/
CategoryTheory.Functor.PullbackObjObj.ofHasPullback : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) →
              {X₁ Y₁ : C₁} →
                (f₁ : X₁ ⟶ Y₁) →
                  {X₃ Y₃ : C₃} →
                    (f₃ : X₃ ⟶ Y₃) →
                      [CategoryTheory.Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] →
                        G.PullbackObjObj f₁ f₃
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.coe_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : Set α) (h : IsIrreducible s) (h' : IsClosed s),
  ↑{ carrier := s, isIrreducible' := h, isClosed' := h' } = s
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_memLp_exp_mul : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ (p : NNReal), ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), MeasureTheory.MemLp (fun ω => Real.exp (t * X ω)) (↑p) (κ ω')
-- Mathlib.Data.Finset.Empty
Finset.ne_empty_of_mem : ∀ {α : Type u_1} {a : α} {s : Finset α}, a ∈ s → s ≠ ∅
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.instDecidableEqDischargeResult : DecidableEq Lean.Meta.Simp.DischargeResult
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.affineBasicOpen_le : ∀ (X : AlgebraicGeometry.Scheme) {V : ↑X.affineOpens} (f : ↑(X.presheaf.obj (Opposite.op ↑V))), X.affineBasicOpen f ≤ V
-- Mathlib.RingTheory.Extension.ExtendScalars
/-- Given an extension `P` of `S` over `R` such that `algebraMap R P.Ring` is surjective,
this is the equivalence induced by `P.h1Cotangentι`.  -/
Algebra.Extension.h1CotangentEquivOfSurjective : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : Algebra.Extension R S) → Function.Surjective ⇑(algebraMap R P.Ring) → P.H1Cotangent ≃ₗ[S] P.Cotangent
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_div : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R] (a b : R),
  a ≠ 0 → b ≠ 0 → Differential.logDeriv (a / b) = Differential.logDeriv a - Differential.logDeriv b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
/-- A tensor product of representable functors is representable.  -/
CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj : {C : Type u_2} →
  [inst : CategoryTheory.Category.{v_2, u_2} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {F G : CategoryTheory.Functor Cᵒᵖ (Type v)} →
        {X Y : C} →
          F.RepresentableBy X →
            G.RepresentableBy Y →
              (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).RepresentableBy
                (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.foldl_filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.Analysis.Convex.EGauge
mem_smul_of_egauge_lt : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {c : 𝕜}
  {s : Set E} {x : E}, Balanced 𝕜 s → egauge 𝕜 s x < ‖c‖ₑ → x ∈ c • s
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nat_eq_sum_factorization : ∀ {b : ℝ} (n : ℕ), Real.logb b ↑n = n.factorization.sum fun p t => ↑t * Real.logb b ↑p
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_mem_strictMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y),
  P f → P.strictMap F (F.map f)
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResult : Type
-- Mathlib.RingTheory.Polynomial.ContentIdeal
/-- The content ideal of a polynomial `p` is the ideal generated by its coefficients.  -/
Polynomial.contentIdeal : {R : Type u_1} → [inst : Semiring R] → Polynomial R → Ideal R
-- Init.Data.Fin.Lemmas
Fin.not_le : ∀ {n : ℕ} {a b : Fin n}, ¬a ≤ b ↔ b < a
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.toContinuousMapOn.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R]
  (p p_1 : Polynomial R), p = p_1 → ∀ (X : Set R), p.toContinuousMapOn X = p_1.toContinuousMapOn X
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.mk_coe' : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (f : A₂ → A₁) (h₁ : Function.LeftInverse (⇑e) f)
  (h₂ : Function.RightInverse (⇑e) f)
  (h₃ :
    ∀ (x y : A₂),
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₄ :
    ∀ (x y : A₂),
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₅ :
    ∀ (r : R),
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₂) r) = (algebraMap R A₁) r),
  { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } =
    e.symm
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.ofNatTrans_X₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (ε : CategoryTheory.Functor.id C ⟶ F),
  (CategoryTheory.SmallObject.SuccStruct.ofNatTrans ε).X₀ = CategoryTheory.Functor.id C
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.comp_lift : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] {N : Type u_5} [inst_1 : Monoid N] (g : M →* N) (f : α → M),
  g.comp (FreeMonoid.lift f) = FreeMonoid.lift (⇑g ∘ f)
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.fun.sizeOf_spec : ∀ (depth : ℕ), sizeOf (Mathlib.Tactic.Conv.Path.fun depth) = 1 + sizeOf depth
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weightOfEPs_nil : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : V → V → R) (a : V),
  Quiver.Path.weightOfEPs w Quiver.Path.nil = 1
-- Init.Data.BitVec.Lemmas
BitVec.le_of_zero_length : ∀ {w : ℕ}, w = 0 → ∀ {x y : BitVec w}, x ≤ y
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenCGraph.comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_4}
  [inst_2 : TopologicalSpace γ] {g' : γ → α} {f : α → Set β}, HasOpenCGraph f → Continuous g' → HasOpenCGraph (f ∘ g')
-- Lean.Meta.Tactic.Grind.Internalize
/-- If `Config.matchEqs` is set to `true`, and `f` is `match`-auxiliary function,
adds its equations to `newThms`.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.addMatchEqns : Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.BourbakiWitt
NonemptyChain.ext_iff : ∀ {α : Type u_4} {inst : LE α} {x y : NonemptyChain α}, x = y ↔ x.carrier = y.carrier
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.map.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) (a a_1 : C)
  (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1)
  (h_1 :
    (a a_2 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_2) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_2) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_2, f => h_1 a a_2 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_1 a a_1 f
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.mkPowFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Level → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.toContinuousMap : {α : Type u} →
  {β : Type v} → [inst : TopologicalSpace α] → [inst_1 : PseudoMetricSpace β] → BoundedContinuousFunction α β → C(α, β)
-- Mathlib.Data.PNat.Prime
PNat.Coprime.gcd_mul : ∀ (k : ℕ+) {m n : ℕ+}, m.Coprime n → k.gcd (m * n) = k.gcd m * k.gcd n
-- Init.Grind.Config
Lean.Grind.instInhabitedConfig : Inhabited Lean.Grind.Config
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.volume (interior (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)) =
    MeasureTheory.volume (closure (NumberField.mixedEmbedding.fundamentalCone.normLeOne K))
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hom_ext : ∀ {M N : AddCommMonCat} {f g : M ⟶ N}, AddCommMonCat.Hom.hom f = AddCommMonCat.Hom.hom g → f = g
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_erase_le_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.erase k ≠ ∅ → ∀ {fallback : α}, (cmp ((t.erase k).maxD fallback) (t.maxD fallback)).isLE = true
-- Mathlib.GroupTheory.Nilpotent
/-- An additive subgroup of a nilpotent group is nilpotent.  -/
AddSubgroup.isNilpotent : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [hG : AddGroup.IsNilpotent G], AddGroup.IsNilpotent ↥H
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioc_right : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a b ∪ Set.Ioc a c = Set.Ioc a (max b c)
-- Mathlib.Data.TypeVec
/-- split off the last function of an arrow  -/
TypeVec.lastFun : {n : ℕ} → {α : TypeVec.{u_1} (n + 1)} → {β : TypeVec.{u_2} (n + 1)} → α.Arrow β → α.last → β.last
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toArray_toList : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep2.mk.injEq : ∀ (ctors : List Lean.Constructor) (collectUsedFVars : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit)
  (collectExtraHeaderLMVars : StateRefT' IO.RealWorld Lean.CollectLevelMVars.State Lean.MetaM Unit)
  (checkUniverses : ℕ → Lean.Level → Lean.Elab.TermElabM Unit) (finalizeTermElab : Lean.Elab.TermElabM Unit)
  (prefinalize :
    List Lean.Name →
      Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3)
  (ctors_1 : List Lean.Constructor)
  (collectUsedFVars_1 : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit)
  (collectExtraHeaderLMVars_1 : StateRefT' IO.RealWorld Lean.CollectLevelMVars.State Lean.MetaM Unit)
  (checkUniverses_1 : ℕ → Lean.Level → Lean.Elab.TermElabM Unit) (finalizeTermElab_1 : Lean.Elab.TermElabM Unit)
  (prefinalize_1 :
    List Lean.Name →
      Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3),
  ({ ctors := ctors, collectUsedFVars := collectUsedFVars, collectExtraHeaderLMVars := collectExtraHeaderLMVars,
        checkUniverses := checkUniverses, finalizeTermElab := finalizeTermElab, prefinalize := prefinalize } =
      { ctors := ctors_1, collectUsedFVars := collectUsedFVars_1,
        collectExtraHeaderLMVars := collectExtraHeaderLMVars_1, checkUniverses := checkUniverses_1,
        finalizeTermElab := finalizeTermElab_1, prefinalize := prefinalize_1 }) =
    (ctors = ctors_1 ∧
      collectUsedFVars = collectUsedFVars_1 ∧
        collectExtraHeaderLMVars = collectExtraHeaderLMVars_1 ∧
          checkUniverses = checkUniverses_1 ∧ finalizeTermElab = finalizeTermElab_1 ∧ prefinalize = prefinalize_1)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- If two finite measures `μ` and `ν` are not mutually singular, there exists some `ε > 0` and
a measurable set `E`, such that `ν(E) > 0` and `E` is positive with respect to `μ - εν`.

This lemma is useful for the Lebesgue decomposition theorem.  -/
MeasureTheory.Measure.exists_positive_of_not_mutuallySingular : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  ¬μ.MutuallySingular ν →
    ∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ μ (A ∩ E)
-- Aesop.Tree.Data
Aesop.Goal.setUnsafeRulesSelected : Bool → Aesop.Goal → Aesop.Goal
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.comp_hom'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N K : CategoryTheory.AddMon C} (f : M ⟶ N) (g : N ⟶ K) {Z : C} (h : K.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
under the map to the underlying equivalence relation.  -/
Con.sInf_toSetoid : ∀ {M : Type u_1} [inst : Mul M] (S : Set (Con M)), (sInf S).toSetoid = sInf (Con.toSetoid '' S)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instToStreamStreamProd : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.ToStream (RBTree.RBMap α β cmp) (RBTree.RBNode.Stream (α × β))
-- Init.Data.String.Iterate
/-- Creates an iterator over all bytes in {name}`s`, starting from the last one and iterating towards
the first one.

Examples:
 * {lean}`"abc".toSlice.revBytes.toList = [99, 98, 97]`
 * {lean}`"ab∀c".toSlice.revBytes.toList = [99, 128, 136, 226, 98, 97]`
 -/
String.Slice.revBytes : String.Slice → Std.Iter UInt8
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.Props.mk : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef →
  Lean.Server.WithRpcRef IO.CancelToken → ProofWidgets.RefreshComponent.Props
-- Mathlib.Order.ModularLattice
/-- `a ⊔ b` covers `a` and `b` if `a` and `b` both cover `a ⊓ b`.  -/
IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy : ∀ {α : Type u_2} {inst : Lattice α} [self : IsWeakUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKey?_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).minKey? = some k ↔
        (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.braiding_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom t.snd = s.fst
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Pattern to get `Walk.cons` with the vertices as explicit arguments.  -/
SimpleGraph.Walk.cons' : {V : Type u} → {G : SimpleGraph V} → (u v w : V) → G.Adj u v → G.Walk v w → G.Walk u w