mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Whiskering
/-- Auxiliary definition for `whiskeringLeft₃`.  -/
CategoryTheory.Functor.whiskeringLeft₃ObjObjMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          {D₃ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        (E : Type u_7) →
                          [inst_6 : CategoryTheory.Category.{v_7, u_7} E] →
                            (F₁ : CategoryTheory.Functor C₁ D₁) →
                              (F₂ : CategoryTheory.Functor C₂ D₂) →
                                {F₃ F₃' : CategoryTheory.Functor C₃ D₃} →
                                  (F₃ ⟶ F₃') →
                                    (CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃ ⟶
                                      CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃')
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instInhabitedPosition.default : Lean.Lsp.Position
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.State.mk.inj : ∀ {cache : Lean.Meta.Simp.Cache} {failureCache : Lean.ExprSet} {numSteps : ℕ} {msgLog : List String}
  {morTheorems transitionTheorems : Mathlib.Meta.FunProp.GeneralTheorems} {cache_1 : Lean.Meta.Simp.Cache}
  {failureCache_1 : Lean.ExprSet} {numSteps_1 : ℕ} {msgLog_1 : List String}
  {morTheorems_1 transitionTheorems_1 : Mathlib.Meta.FunProp.GeneralTheorems},
  { cache := cache, failureCache := failureCache, numSteps := numSteps, msgLog := msgLog, morTheorems := morTheorems,
        transitionTheorems := transitionTheorems } =
      { cache := cache_1, failureCache := failureCache_1, numSteps := numSteps_1, msgLog := msgLog_1,
        morTheorems := morTheorems_1, transitionTheorems := transitionTheorems_1 } →
    cache = cache_1 ∧
      failureCache = failureCache_1 ∧
        numSteps = numSteps_1 ∧
          msgLog = msgLog_1 ∧ morTheorems = morTheorems_1 ∧ transitionTheorems = transitionTheorems_1
-- Mathlib.Algebra.Group.Action.Sum
Sum.FaithfulSMulLeft : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] [FaithfulSMul M α],
  FaithfulSMul M (α ⊕ β)
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.Context.mk.injEq : ∀ (elimInfo : Lean.Elab.Term.ElabElimInfo) (expectedType : Lean.Expr) (elimInfo_1 : Lean.Elab.Term.ElabElimInfo)
  (expectedType_1 : Lean.Expr),
  ({ elimInfo := elimInfo, expectedType := expectedType } =
      { elimInfo := elimInfo_1, expectedType := expectedType_1 }) =
    (elimInfo = elimInfo_1 ∧ expectedType = expectedType_1)
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lintegral_le_of_lmarginal_le : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [inst_3 : Fintype δ] (s : Finset δ)
  {f g : ((i : δ) → X i) → ENNReal},
  Measurable f →
    Measurable g →
      ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ →
        ∫⁻ (x : (i : δ) → X i), f x ∂MeasureTheory.Measure.pi μ ≤
          ∫⁻ (x : (i : δ) → X i), g x ∂MeasureTheory.Measure.pi μ
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.liftOn.congr_simp : ∀ {K : Type u_1} [inst : CommRing K] {P : Sort u_2} (x x_1 : RatFunc K),
  x = x_1 →
    ∀ (f f_1 : Polynomial K → Polynomial K → P) (e_f : f = f_1)
      (H :
        ∀ {p q p' q' : Polynomial K},
          q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q'),
      x.liftOn f H = x_1.liftOn f_1 ⋯
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivWithinAt.add` -/
HasDerivWithinAt.fun_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → HasDerivWithinAt g g' s x → HasDerivWithinAt (fun i => f i + g i) (f' + g') s x
-- Mathlib.Data.Set.Card
Set.encard_eq_coe_toFinset_card : ∀ {α : Type u_1} (s : Set α) [inst : Fintype ↑s], s.encard = ↑s.toFinset.card
-- Mathlib.Algebra.Algebra.StrictPositivity
Units.isStrictlyPositive_of_le : ∀ {A : Type u_1} [inst : LE A] [inst_1 : Monoid A] [inst_2 : Zero A] {a : Aˣ}, 0 ≤ ↑a → IsStrictlyPositive ↑a
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.mapsTo : ∀ {α : Type u_6} {β : Type u_7} {r : α → α → Prop} (f : β → α) {s : Set α} {t : Set β},
  Set.MapsTo f t s → s.WellFoundedOn r → t.WellFoundedOn (Function.onFun r f)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Given a natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of types,
where `G` is locally-full and cover-dense, and `ℱ'` is a sheaf,
we may obtain a natural transformation between sheaves.
 -/
CategoryTheory.Functor.IsCoverDense.Types.presheafHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {G : CategoryTheory.Functor C D} →
            {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} →
              {ℱ' : CategoryTheory.Sheaf K (Type v)} →
                [G.IsCoverDense K] → [G.IsLocallyFull K] → (G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) → (ℱ ⟶ ℱ'.obj)
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_le_of_embedding : ∀ {α : Type u_1} {β : Type u_2} [Finite β] (f : α ↪ β), Nat.card α ≤ Nat.card β
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.norm_rpow_of_nonneg : ∀ {x y : ℝ}, 0 ≤ x → ‖x ^ y‖ = ‖x‖ ^ y
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rco_eq_none : ∀ {m n : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m...n).toList[i]? = none
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact_iff_δ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} (S : CategoryTheory.ComposableArrows C (n + 2)),
  S.Exact ↔
    (CategoryTheory.ComposableArrows.mk₂ (S.map' 0 1 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_2 ⋯)
          (S.map' 1 2 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4 ⋯)).Exact ∧
      S.δ₀.Exact
-- Init.Data.Char.Ordinal
Char.ordinal_injective : Function.Injective Char.ordinal
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.commAlgEquiv.eq_1 : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N],
  AddMonoidAlgebra.commAlgEquiv R =
    (AddMonoidAlgebra.curryAlgEquiv R).symm.trans
      ((AddMonoidAlgebra.domCongr R A AddEquiv.prodComm).trans (AddMonoidAlgebra.curryAlgEquiv R))
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f f_1 : M →ₗ[R] N →ₗ[R] N) (e_f : f = f_1)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x), CliffordAlgebra.foldr Q f hf = CliffordAlgebra.foldr Q f_1 ⋯
-- Batteries.Data.MLList.Basic
/-- Take the initial segment of the lazy list, until the function `f` first returns `false`.  -/
MLList.takeWhile : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → (α → Bool) → MLList m α → MLList m α
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The set of machine states accessible from an initial TM2 statement.  -/
Turing.TM2to1.trStmts₁ : {K : Type u_1} →
  {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Turing.TM2.Stmt Γ Λ σ → Finset (Turing.TM2to1.Λ' K Γ Λ σ)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.map : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → {f : Polynomial R} → IsAdjoinRoot S f → Polynomial R →ₐ[R] S
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The associativity diagram of a group object is Cartesian.

In fact, any monoid object whose associativity diagram is Cartesian can be made into a group object
(we do not prove this in this file), so we should expect that many properties of group objects
follow from this result.  -/
CategoryTheory.GrpObj.isPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.GrpObj A],
  CategoryTheory.IsPullback (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul A)
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.MonObj.mul))
    CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul
-- Mathlib.Order.SupClosed
SupClosed.finsetSup_mem : ∀ {α : Type u_3} [inst : SemilatticeSup α] {ι : Type u_5} {f : ι → α} {s : Set α} {t : Finset ι} [inst_1 : OrderBot α],
  SupClosed s → t.Nonempty → (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabHAndThen : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Tactic.FunProp.Theorems
/-- Name of function property  -/
Mathlib.Meta.FunProp.LambdaTheorem.funPropName : Mathlib.Meta.FunProp.LambdaTheorem → Lean.Name
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.reverse_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {X Y : C} (f : X ⟶ Y),
  Quiver.reverse f = CategoryTheory.Groupoid.inv f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_mul_mul_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj M],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
        CategoryTheory.MonObj.mul) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
      CategoryTheory.MonObj.mul
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.cyclesOpIso_inv_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
  {Z : Cᵒᵖ} (h : S₁.op.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ).op
      (CategoryTheory.CategoryStruct.comp S₁.cyclesOpIso.inv h) =
    CategoryTheory.CategoryStruct.comp S₂.cyclesOpIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.ShortComplex.opMap φ))
        h)
-- Init.Data.BitVec.Lemmas
BitVec.fill_toNat : ∀ {w : ℕ} {v : Bool}, (BitVec.fill w v).toNat = if v = true then 2 ^ w - 1 else 0
-- Mathlib.Data.Nat.Factorial.Basic
/-- `ascFactorial` implemented using binary splitting.

While this still performs the same number of multiplications,
the big-integer operands to each are much smaller.  -/
Nat.ascFactorialBinary : ℕ → ℕ → ℕ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.eraseMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (l : List α), (t₁.eraseMany l).Equiv (t₂.eraseMany l)
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.assoc_tmul : ∀ {R : Type u_9} {S : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {M₁₂ : Type u_14} {M₂₃ : Type u_15} [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid M₁₂] [inst_7 : AddCommMonoid M₂₃]
  [inst_8 : Module R M₁] [inst_9 : Module R M₂] [inst_10 : Module S M₂] [inst_11 : IsScalarTower R S M₂]
  [inst_12 : Module R M₃] [inst_13 : Module S M₃] [inst_14 : IsScalarTower R S M₃] [inst_15 : Module R M₁₂]
  [inst_16 : Module S M₁₂] [inst_17 : IsScalarTower R S M₁₂] [inst_18 : Module R M₂₃] [inst_19 : Module S M₂₃]
  [inst_20 : IsScalarTower R S M₂₃] {T : Type u_16} [inst_21 : CommSemiring T] [inst_22 : Algebra R T]
  [inst_23 : Module T M₁] [inst_24 : IsScalarTower R T M₁] [inst_25 : Module T M₁₂] [inst_26 : SMulCommClass S T M₁₂]
  [inst_27 : IsScalarTower R T M₁₂] (f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂)
  (hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)) (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) (hg : IsTensorProduct g)
  (x₁ : M₁) (x₂ : M₂) (x₃ : M₃), (IsTensorProduct.assoc f hf g hg) ((f x₁) x₂ ⊗ₜ[S] x₃) = x₁ ⊗ₜ[R] (g x₂) x₃
-- Mathlib.Topology.ContinuousOn
/-- If a function is continuous on a set for some topologies, then it is
continuous on the same set with respect to any finer topology on the source space.  -/
ContinuousOn.mono_dom : ∀ {α : Type u_5} {β : Type u_6} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β},
  t₂ ≤ t₁ → ∀ {s : Set α} {f : α → β}, ContinuousOn f s → ContinuousOn f s
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite sums of analytic functions are analytic  -/
Finset.analyticWithinAt_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {f : α → E → F} {c : E} {s : Set E} (N : Finset α),
  (∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (∑ n ∈ N, f n) s c
-- Mathlib.Order.Filter.Basic
Filter.eventually_sup : ∀ {α : Type u} {p : α → Prop} {f g : Filter α},
  (∀ᶠ (x : α) in f ⊔ g, p x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in g, p x
-- Mathlib.Data.Set.Sups
Set.sups_union_right : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t₁ t₂ : Set α}, s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂
-- Mathlib.Analysis.Complex.RemovableSingularity
/-- **Removable singularity** theorem: if a function `f : ℂ → E` is complex differentiable on a
punctured neighborhood of `c` and $f(z) - f(c)=o((z-c)^{-1})$, then `f` has a limit at `c`.  -/
Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ},
  (∀ᶠ (z : ℂ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℂ f z) →
    ((fun z => f z - f c) =o[nhdsWithin c {c}ᶜ] fun z => (z - c)⁻¹) →
      Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds ((nhdsWithin c {c}ᶜ).limUnder f))
-- Lean.Meta.Sym.SymM
/-- Reports an issue if `verbose` mode is enabled.  -/
Lean.Meta.Sym.doElemReportIssue!__ : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.collectUsedOrigins.go : Lean.Meta.Grind.EMatch.InstanceMap →
  Lean.Expr → StateM (Std.HashSet Lean.Meta.Sym.ExprPtr × Std.HashSet Lean.Meta.Grind.Origin) Unit
-- Mathlib.Logic.ExistsUnique
ExistsUnique.elim : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃! x, p x) → (∀ (x : α), p x → (∀ (y : α), p y → y = x) → b) → b
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_add_smoothingFn_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ 1 + AkraBazziRecurrence.smoothingFn ↑n
-- Mathlib.Algebra.Order.Hom.Basic
map_sub_rev : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [AddGroupSeminormClass F α β] (f : F) (x y : α), f (x - y) = f (y - x)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_add : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {m n : ℕ} {a : α},
  Std.PRange.succMany? (m + n) a = (Std.PRange.succMany? m a).bind fun x => Std.PRange.succMany? n x
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.mapComp_hom_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] (φ : CategoryTheory.Functor C D)
  (φ' : CategoryTheory.Functor D E) (X : CategoryTheory.FreeGroupoid C),
  (CategoryTheory.FreeGroupoid.mapComp φ φ').hom.app X =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.FreeGroupoid.map (φ.comp φ')).obj X)
-- Mathlib.Tactic.Ring.Common
/-- Subtracts two polynomials `va, vb` to get a normalized result polynomial.

* `a - b = a + -b`
 -/
Mathlib.Tactic.Ring.Common.evalSub : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a b : Q(«$α»)} →
              (rα : Q(CommRing «$α»)) →
                Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                  Mathlib.Tactic.Ring.Common.ExSum bt sα b →
                    Lean.MetaM
                      (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» - «$b»))
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `isMulTorsion_of_finite`.

---

Finite groups are torsion groups.  -/
isTorsion_of_finite : ∀ {G : Type u_1} [inst : Group G] [Finite G], IsMulTorsion G
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe : ∀ {A : Type uA} [inst : AddCommGroup A] (a : A) (a_1 : ℤ ⧸ Ideal.span {↑(addOrderOf a)}),
  ↑((CharacterModule.intSpanEquivQuotAddOrderOf a).symm a_1) =
    ↑((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange
        (((LinearMap.toSpanSingleton ℤ A a).ker.quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯).symm a_1))
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_of_ge : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, b ≤ a → Set.uIcc a b = Set.Icc b a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.le_of_isAffine : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] {I J : X.IdealSheafData},
  I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩ → I ≤ J
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.instCodescendsAlongOfIsStableUnderCobaseChangeOfHasOfPostcompPropertyOfRespectsLeft : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C}
  [Q.IsStableUnderCobaseChange] [P.HasOfPostcompProperty Q] [P.RespectsLeft Q], P.CodescendsAlong Q
-- Mathlib.Data.Prod.Lex
Prod.Lex.orderBot.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β], Prod.Lex.orderBot = { bot := toLex ⊥, bot_le := ⋯ }
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.ne_zero_of_ofFn_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] {n : ℕ} {v : Fin n → R}, (Polynomial.ofFn n) v ≠ 0 → n ≠ 0
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFold_coe : ∀ {α : Type u_3} (op : α → α → α) [assoc : Std.Associative op] (l : List α)
  (comm : {x | x ∈ ↑l}.Pairwise fun x y => op x y = op y x) (a : α),
  Multiset.noncommFold op (↑l) comm a = List.foldr op a l
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.finset_inf_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [inst_3 : OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {t : Set X}
  {x : X}, (∀ i ∈ s, ContinuousWithinAt (f i) t x) → ContinuousWithinAt (fun a => s.inf fun x => f x a) t x
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between the negation of a nonzero vector and that
vector.  -/
InnerProductGeometry.angle_neg_self_of_nonzero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x : V},
  x ≠ 0 → InnerProductGeometry.angle (-x) x = Real.pi
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Checking exactness of limits of shape `Discrete ℕ` and `Discrete J` for finite `J` is enough for
countable AB4\*.
 -/
CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCountableProducts C]
  [CategoryTheory.Limits.HasFiniteColimits C]
  [∀ (J : Type) [inst_3 : Finite J], CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C]
  [CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete ℕ) C], CategoryTheory.CountableAB4Star C
-- Mathlib.Data.Nat.Digits.Lemmas
List.pairwiseDisjoint_consFixedLengthDigits : ∀ {b : ℕ} (hb : 1 < b) (l : ℕ), (↑(Finset.range b)).PairwiseDisjoint fun d => List.consFixedLengthDigits hb l d
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
CategoryTheory.Limits.instPreservesColimitsOfSizeObjFunctorTypeSigmaConst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C] (R : C),
  CategoryTheory.Limits.PreservesColimitsOfSize.{v', u', w, v, w + 1, u} (CategoryTheory.Limits.sigmaConst.obj R)
-- Mathlib.Data.Finset.Max
Finset.min_singleton : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α}, {a}.min = ↑a
-- Batteries.Control.AlternativeMonad
Option.instLawfulAlternative : LawfulAlternative Option
-- Mathlib.Algebra.Lie.Extension
/-- A surjective Lie algebra homomorphism yields an extension.  -/
LieAlgebra.isExtension_of_surjective : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (f : L →ₗ⁅R⁆ M),
  Function.Surjective ⇑f → LieAlgebra.IsExtension f.ker.incl f
-- Init.Data.Slice.Array.Lemmas
Subarray.instLawfulSliceSizeSubarrayIteratorSubarrayData : ∀ {α : Type u_1}, Std.Slice.LawfulSliceSize (Std.Slice.Internal.SubarrayData α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false} {fallback : α},
      Std.Internal.List.getKeyD (Std.Internal.List.minKey l he) l fallback = Std.Internal.List.minKey l he
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forIn_eq_forIn_keys : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF → ∀ {f : α → δ → m' (ForInStep δ)} {init : δ}, (forIn m init fun a d => f a.1 d) = forIn m.keys init f
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.integral_singleton' : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  [CompleteSpace G] {a : X}, MeasureTheory.StronglyMeasurable f → ∫ᵛ (a : X) in {a}, f a ∂[B; μ] = (B (f a)) (μ {a})
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_restrict : ∀ {ι : Type u_1} {I J J₁ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
  J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ⊓ ↑J'
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toMeasure_injective : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω], Function.Injective MeasureTheory.ProbabilityMeasure.toMeasure