mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.CompProd
/-- Composition-Product of kernels. For s-finite kernels, it satisfies
`∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)`
(see `ProbabilityTheory.Kernel.lintegral_compProd`).
If either of the kernels is not s-finite, `compProd` is given the junk value 0.  -/
ProbabilityTheory.Kernel.compProd : {α : Type u_4} →
  {β : Type u_5} →
    {γ : Type u_6} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} →
            ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel (α × β) γ → ProbabilityTheory.Kernel α (β × γ)
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instGeneralizedCoheytingAlgebra : {V : Type u} → {G : SimpleGraph V} → GeneralizedCoheytingAlgebra G.Finsubgraph
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι} {F' : ι → α → β},
  TendstoUniformlyOn F f p s → (∀ᶠ (n : ι) in p, Set.EqOn (F n) (F' n) s) → TendstoUniformlyOn F' f p s
-- Lean.Declaration
Lean.ConstantVal.type : Lean.ConstantVal → Lean.Expr
-- Std.Async.Signal
/-- I/O now possible.
 -/
Std.Async.Signal.sigio : Std.Async.Signal
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addFundamentalFrontier_vadd : ∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α)
  [inst_2 : AddGroup H] [inst_3 : AddAction H α] [VAddCommClass H G α] (g : H),
  MeasureTheory.addFundamentalFrontier G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalFrontier G s
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_comp : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  {T : Type u_2} [inst_3 : CommRing S] [inst_4 : CommRing T] (f : T →+* R) (g : R →+* S),
  Matrix.GeneralLinearGroup.map (g.comp f) = (Matrix.GeneralLinearGroup.map g).comp (Matrix.GeneralLinearGroup.map f)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- If `s ≅ t` and `IsKan (s.whisker h)`, then `IsKan (t.whisker h)`.  -/
CategoryTheory.Bicategory.RightLift.IsKan.whiskerOfCommute : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (s t : CategoryTheory.Bicategory.RightLift f g) →
            (s ≅ t) → {x : B} → (h : x ⟶ c) → (s.whisker h).IsKan → (t.whisker h).IsKan
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Scalar multiplication as an endomorphism of `Γ(M, U)`.  -/
AlgebraicGeometry.Scheme.Modules.smul : {X : AlgebraicGeometry.Scheme} →
  {M : X.Modules} →
    {U : X.Opens} → ↑(X.presheaf.obj (Opposite.op U)) →+* CategoryTheory.End (M.presheaf.obj (Opposite.op U))
-- Mathlib.Analysis.Calculus.Deriv.Comp
fderiv_comp_deriv_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F} (x : 𝕜)
  {l : F → E} {y : F},
  DifferentiableAt 𝕜 l y → DifferentiableAt 𝕜 f x → y = f x → deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U),
  (X.restrictStalkIso h x).inv = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (X.ofRestrict h) x
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.originForm.injEq : ∀ (path : Std.Http.URI.Path) (query : Option Std.Http.URI.Query) (path_1 : Std.Http.URI.Path)
  (query_1 : Option Std.Http.URI.Query),
  (Std.Http.RequestTarget.originForm path query = Std.Http.RequestTarget.originForm path_1 query_1) =
    (path = path_1 ∧ query = query_1)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.curryMid_uncurryMid : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (p : Fin (n + 1))
  (f : Ei p →L[𝕜] Ei (p.succAbove i) [×n]→L[𝕜] G),
  ContinuousMultilinearMap.curryMid p (ContinuousLinearMap.uncurryMid p f) = f
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.isZero_eTruncGE_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) [t.IsLE X n] (j : EInt),
  WithBotTop.coe n < j → CategoryTheory.Limits.IsZero ((t.eTruncGE.obj j).obj X)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.updateFVar! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → Lean.FVarId → Lean.Compiler.LCNF.Arg pu
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `sub_nonneg`. -/
le_of_sub_nonneg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, 0 ≤ a - b → b ≤ a
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_9 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ),
  Lean.Grind.CommRing.Expr.denoteS ctx (Lean.Grind.CommRing.Expr.intCast k) = 0
-- Init.Data.String.Basic
String.Slice.Pos.ofSlice_slice : ∀ {s : String.Slice} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁},
  String.Slice.Pos.ofSlice (pos.slice p₀ p₁ h₁ h₂) = pos
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CaseTrace.mk.injEq : ∀ (expr : Lean.Expr) (i num : ℕ) (source : Lean.Meta.Grind.SplitSource) (expr_1 : Lean.Expr) (i_1 num_1 : ℕ)
  (source_1 : Lean.Meta.Grind.SplitSource),
  ({ expr := expr, i := i, num := num, source := source } =
      { expr := expr_1, i := i_1, num := num_1, source := source_1 }) =
    (expr = expr_1 ∧ i = i_1 ∧ num = num_1 ∧ source = source_1)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.domRestrict.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_5} {S : Type u_6} [inst_1 : AddZeroClass N] [inst_2 : SetLike S M]
  [inst_3 : AddSubmonoidClass S M] (f : M →+ N) (s : S), f.domRestrict s = f.comp (AddSubmonoidClass.subtype s)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Down.compression.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)),
  Down.compression a 𝒜 = {s ∈ 𝒜 | s.erase a ∈ 𝒜}.disjUnion ({s ∈ Finset.image (fun s => s.erase a) 𝒜 | s ∉ 𝒜}) ⋯
-- Lean.Parser.Basic
Lean.Parser.eoi : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [inst_2 : Quiver C]
  [inst_3 : (a b : C) → Quiver (a ⟶ b)] [inst_4 : SizeOf B] [inst_5 : SizeOf C] (toPrefunctor : B ⥤q C)
  (map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor.map f ⟶ toPrefunctor.map g)),
  sizeOf { toPrefunctor := toPrefunctor, map₂ := map₂ } = 1 + sizeOf toPrefunctor
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.mem_nhds : ∀ {α : Type u} [t : TopologicalSpace α] {a : α} {s : Set α} {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → s ∈ b → a ∈ s → s ∈ nhds a
-- Mathlib.Tactic.Recover
/-- auxiliary function for `getUnassignedGoalMVarDependencies`  -/
_private.Mathlib.Tactic.Recover.0.Mathlib.Tactic.getUnassignedGoalMVarDependencies.go : Lean.MVarId → StateRefT' IO.RealWorld (Std.HashSet Lean.MVarId) Lean.MetaM Unit
-- Mathlib.Algebra.Category.Ring.Under.Basic
/-- The natural isomorphism `S ⊗[R] A ≅ pushout A.hom (algebraMap R S)` in `Under S`.  -/
CommRingCat.tensorProdObjIsoPushoutObj : {R : CommRingCat} →
  (S : CommRingCat) →
    [inst : Algebra ↑R ↑S] →
      (A : CategoryTheory.Under R) →
        S.mkUnder (TensorProduct ↑R ↑S ↑A.right) ≅
          (CategoryTheory.Under.pushout (CommRingCat.ofHom (algebraMap ↑R ↑S))).obj A
-- Mathlib.Data.QPF.Univariate.Basic
QPF.fixToW.eq_1 : ∀ {F : Type u → Type u} [q : QPF F], QPF.fixToW = Quotient.lift QPF.Wrepr ⋯
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.unop_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : Cᵒᵖ} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g),
  h.unop.r =
    CategoryTheory.Arrow.homMk (CategoryTheory.Arrow.Hom.right h.i).unop (CategoryTheory.Arrow.Hom.left h.i).unop ⋯
-- Lean.Parser.Do
Lean.Parser.Term.doCatch.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Int.DivMod.Lemmas
Int.one_ediv : ∀ (b : ℤ), 1 / b = if b.natAbs = 1 then b else 0
-- Mathlib.Data.Finset.Insert
Finset.empty_ne_singleton : ∀ {α : Type u_1} (a : α), ∅ ≠ {a}
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplit.k : Lean.Meta.Grind.Arith.Cutsat.CooperSplit → ℕ
-- Mathlib.Algebra.Order.Ring.GeomSum
/-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of
`m ≥ 2` is less than `m ^ n`.  -/
Nat.geomSum_lt : ∀ {m n : ℕ} {s : Finset ℕ}, 2 ≤ m → (∀ k ∈ s, k < n) → ∑ k ∈ s, m ^ k < m ^ n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
not_isAddCyclic_iff_exponent_eq_prime : ∀ {α : Type u_1} [inst : AddGroup α] {p : ℕ},
  Nat.Prime p → Nat.card α = p ^ 2 → (¬IsAddCyclic α ↔ AddMonoid.exponent α = p)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.var.injEq : ∀ (a a_1 : ℕ), (Mathlib.Tactic.ITauto.IProp.var a = Mathlib.Tactic.ITauto.IProp.var a_1) = (a = a_1)
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.head : ∀ {n : ℕ}, Nat.Partrec' ↑List.Vector.head
-- Mathlib.Order.ULift
ULift.instMin_mathlib : {α : Type u} → [Min α] → Min (ULift.{v, u} α)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          (complex : ChainComplex C ℕ) →
            autoParam (∀ (n : ℕ), CategoryTheory.Projective (complex.X n))
                CategoryTheory.ProjectiveResolution.projective._autoParam →
              [hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology complex i] →
                (π : complex ⟶ (ChainComplex.single₀ C).obj Z) →
                  autoParam (QuasiIso π) CategoryTheory.ProjectiveResolution.quasiIso._autoParam →
                    CategoryTheory.ProjectiveResolution Z
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.smul_mem : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  (t : R) {x : L}, x ∈ L' → t • x ∈ L'
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_lt_one_cert.eq_1 : ∀ (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.zero_lt_one_cert p = (p == Lean.Grind.Linarith.Poly.add (-1) 0 Lean.Grind.Linarith.Poly.nil)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.Context.mk.sizeOf_spec : ∀ (ringId : ℕ) (checkCoeffDvd : Bool),
  sizeOf { ringId := ringId, checkCoeffDvd := checkCoeffDvd } = 1 + sizeOf ringId + sizeOf checkCoeffDvd
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigits_digits_sum_eq : ∀ {x : ℝ} {b : ℕ} [inst : NeZero b],
  x ∈ Set.Ico 0 1 → ∀ (n : ℕ), ↑b ^ n * ∑ i ∈ Finset.range n, Real.ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.leadingCoeff_smul_integralNormalization : ∀ {S : Type v} [inst : CommSemiring S] (p : Polynomial S),
  p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Expr.denoteN.match_1.eq_6 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (a b : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)),
  (match a.add b with
    | a.sub b => h_1 a b
    | a.neg => h_2 a
    | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
    | Lean.Grind.Linarith.Expr.zero => h_4 ()
    | Lean.Grind.Linarith.Expr.var v => h_5 v
    | a.add b => h_6 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) =
    h_6 a b
-- Mathlib.Data.Sum.Interval
Sum.Ioo_inr_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₂ : α) (b₁ : β), Finset.Ioo (Sum.inr b₁) (Sum.inl a₂) = ∅
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.mk : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Name → Lean.Expr → Lean.FVarId → Array (Lean.Compiler.LCNF.Alt pu) → Lean.Compiler.LCNF.Cases pu
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- Given a morphism of presheaves of commutative rings `φ : S ⟶ R`,
this is the type of relative `φ`-derivation of a presheaf of `R`-modules `M`.  -/
PresheafOfModules.Derivation' : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
      PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)) → (S' ⟶ R) → Type (max (max u₂ u) v)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.exp : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  AEMeasurable f μ → AEMeasurable (fun x => Real.exp (f x)) μ
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- An abbreviation for `HasColimitsOfShape (Discrete f)`.  -/
CategoryTheory.Limits.HasCoproductsOfShape : Type v → (C : Type u_1) → [CategoryTheory.Category.{u_2, u_1} C] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- Extract an isomorphism between left components from an isomorphism in
`CatCospanTransform F G F' G'`.  -/
CategoryTheory.Limits.CatCospanTransform.leftIso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                  (ψ ≅ ψ') → (ψ.left ≅ ψ'.left)
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_Icc : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a b : R},
  Int.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curry_obj_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) {X Y : C}
  (f : X ⟶ Y) (Y_1 : D),
  ((CategoryTheory.Functor.curry.obj F).map f).app Y_1 =
    F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y_1))
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_pow_of_prime_ne_two : ∀ {p : ℕ} (n : ℕ), Nat.Prime p → p ≠ 2 → ArithmeticFunction.carmichael (p ^ n) = (p ^ n).totient
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.endsWith_string_eq_false_iff : ∀ {pat : String} {s : String.Slice}, s.endsWith pat = false ↔ ¬pat.toList <:+ s.copy.toList
-- Lean.Meta.WHNF
Lean.Meta.smartUnfoldingMatch? : Lean.Expr → Option Lean.Expr
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_intCast_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (m : ℤ) (a : R),
  Int.fract (↑m + a) = Int.fract a
-- Mathlib.Analysis.LocallyConvex.Basic
absorbs_iff_eventually_nhds_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s t : Set E}, 0 ∈ s → (Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in nhds 0, Set.MapsTo (fun x => c • x) t s)
-- Init.Data.String.Lemmas.TakeDrop
String.drop_toSlice : ∀ {s : String} {n : ℕ}, s.toSlice.drop n = s.drop n
-- Init.Data.UInt.Lemmas
UInt8.sub_right_inj : ∀ {a b : UInt8} (c : UInt8), c - a = c - b ↔ a = b
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_def : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f)
  (x : R), (seminormFromConst hf1 hc hpm) x = seminormFromConst' c f x
-- Lean.CoreM
Lean.DeclNameGenerator.parentIdxs : Lean.DeclNameGenerator → List ℕ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  (g : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f),
  ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).obj g).hom = g.hom.left
-- Mathlib.Data.Fin.Embedding
/-- `Fin.addNat` as an `Embedding`, `addNatEmb m i` adds `m` to `i`, generalizes `Fin.succ`.  -/
Fin.addNatEmb : {n : ℕ} → (m : ℕ) → Fin n ↪ Fin (n + m)
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.w_integral : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ},
  0 < D → ∫ (x : E), ExistsContDiffBumpBase.w D x ∂MeasureTheory.Measure.addHaar = 1
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.ForwardSliceSearcher.iter.eq_1 : ∀ (pat s : String.Slice),
  String.Slice.Pattern.ForwardSliceSearcher.iter pat s =
    if h : pat.utf8ByteSize = 0 then
      { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyBefore s.startPos }
    else
      {
        internalState :=
          String.Slice.Pattern.ForwardSliceSearcher.proper pat
            (String.Slice.Pattern.ForwardSliceSearcher.buildTable pat) ⋯ s.startPos.offset pat.startPos.offset ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.id_comp : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
  CategoryTheory.FreeMonoidalCategory.HomEquiv ((CategoryTheory.FreeMonoidalCategory.Hom.id X).comp f) f
-- Mathlib.Data.Finset.Prod
Finset.product_empty : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α), s ×ˢ ∅ = ∅
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_tmod : ∀ (a b : ℤ), (a.tmod b).tmod b = a.tmod b
-- Mathlib.Order.KrullDimension
/-- The Krull dimension is the supremum of the elements' height plus coheight.
 -/
Order.krullDim_eq_iSup_height_add_coheight_of_nonempty : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Order.krullDim α = ↑(⨆ a, Order.height a + Order.coheight a)
-- Batteries.Data.Array.Scan
Array.getElem?_succ_scanl : ∀ {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {i : ℕ} {f : β → α → β},
  (Array.scanl f init as)[i + 1]? = (Array.scanl f init as)[i]?.bind fun x => Option.map (fun y => f x y) as[i]?
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyδOfTriangle_homologyMap_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)),
  DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) CochainComplex.homologyδOfTriangle_homologyMap._auto_1) {Z : C}
      (h_1 : HomologicalComplex.homology T.obj₂ n₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CochainComplex.homologyδOfTriangle T n₀ n₁ h)
          (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap T.mor₁ n₁) h_1) =
        CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_inv_app : ∀ {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] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  (X : CategoryTheory.Functor Cᵒᵖ D), (J.plusFunctorWhiskerRightIso F).inv.app X = (J.plusCompIso F X).inv
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `IsRoot p x` implies `x` is a root of `p`. The evaluation of `p` at `x` is zero  -/
Polynomial.IsRoot : {R : Type u} → [inst : Semiring R] → Polynomial R → R → Prop
-- Lean.Expr
Lean.Expr.mvar.sizeOf_spec : ∀ (mvarId : Lean.MVarId), sizeOf (Lean.Expr.mvar mvarId) = 1 + sizeOf mvarId
-- Mathlib.Tactic.Bound
/-- `bound` tactic for proving inequalities via straightforward recursion on expression structure.

An example use case is

```
-- Calc example: A weak lower bound for `z ↦ z^2 + c`
lemma le_sqr_add (c z : ℝ) (cz : ‖c‖ ≤ ‖z‖) (z3 : 3 ≤ ‖z‖) :
    2 * ‖z‖ ≤ ‖z^2 + c‖ := by
  calc ‖z^2 + c‖
    _ ≥ ‖z^2‖ - ‖c‖ := by bound
    _ ≥ ‖z^2‖ - ‖z‖ := by  bound
    _ ≥ (‖z‖ - 1) * ‖z‖ := by
      rw [mul_comm, mul_sub_one, ← pow_two, ← norm_pow]
    _ ≥ 2 * ‖z‖ := by bound
```

`bound` is built on top of `aesop`, and uses
1. Apply lemmas registered via the `@[bound]` attribute
2. Forward lemmas registered via the `@[bound_forward]` attribute
3. Local hypotheses from the context
4. Optionally: additional hypotheses provided as `bound [h₀, h₁]` or similar. These are added to the
   context as if by `have := hᵢ`.

The functionality of `bound` overlaps with `positivity` and `gcongr`, but can jump back and forth
between `0 ≤ x` and `x ≤ y`-type inequalities.  For example, `bound` proves
  `0 ≤ c → b ≤ a → 0 ≤ a * c - b * c`
by turning the goal into `b * c ≤ a * c`, then using `mul_le_mul_of_nonneg_right`.  `bound` also
contains lemmas for goals of the form `1 ≤ x, 1 < x, x ≤ 1, x < 1`.  Conversely, `gcongr` can prove
inequalities for more types of relations, supports all `positivity` functionality, and is likely
faster since it is more specialized (not built atop `aesop`).  -/
«tacticBound[_]» : Lean.ParserDescr