mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app._auto_1)
  {Z : Cᵒᵖ} (h : (CategoryTheory.shiftFunctor Cᵒᵖ m).obj ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId Cᵒᵖ n m hnm).inv.app X) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app
          (Opposite.op ((CategoryTheory.shiftFunctor C m).obj (Opposite.unop X))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor Cᵒᵖ m).map
            ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app X))
          h))
-- Lean.Language.Basic
/-- Whether the transformation is the identity transformation.  -/
Lean.Language.SnapshotTreeTransform.isIdentity : Lean.Language.SnapshotTreeTransform → Bool
-- LeanSearchClient.Syntax
/-- Search [LeanSearch](https://leansearch.net/) from within Lean.
Queries should be a string that ends with a `.` or `?`. This works as a command, as a term
and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

```lean
#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry
```

You can modify the LeanSearch URL by setting the `LEANSEARCHCLIENT_LEANSEARCH_API_URL` environment variable.
  -/
LeanSearchClient.leansearch_search_cmd : Lean.ParserDescr
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.reflectsIsomorphisms_forget : ∀ {R : Type u} [inst : CommRing R], (CategoryTheory.forget (CommAlgCat R)).ReflectsIsomorphisms
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.withBotCoe : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.IsPredPrelimit x → Order.IsPredPrelimit ↑x
-- Mathlib.Algebra.Regular.Basic
/-- Any power of a right-regular element is right-regular.  -/
IsRightRegular.pow : ∀ {R : Type u_1} [inst : Monoid R] {a : R} (n : ℕ), IsRightRegular a → IsRightRegular (a ^ n)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.algebraMap_ofSubfield : ∀ {K : Type u} [inst : Field K] (s : Subfield K), algebraMap (↥s) K = s.subtype
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_pure : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''} {x : α}, f'' =o[pure x] g'' ↔ f'' x = 0
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableWithinAt.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {s : Set E} {f₂ : E → G},
  DifferentiableWithinAt 𝕜 f₁ s x →
    DifferentiableWithinAt 𝕜 f₂ s x → DifferentiableWithinAt 𝕜 (fun x => (f₁ x, f₂ x)) s x
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.natDegree_nodal : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [Nontrivial R],
  (Lagrange.nodal s v).natDegree = s.card
-- Mathlib.Data.Finset.NatDivisors
Finset.nat_divisors_prod : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → ℕ), (∏ i ∈ s, f i).divisors = ∏ i ∈ s, (f i).divisors
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.add_le_right_iff_mul_omega0_le : ∀ {a b : Ordinal.{u_1}}, a + b ≤ b ↔ a * Ordinal.omega0 ≤ b
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.isCoprime_X_sub_C_of_isUnit_sub : ∀ {R : Type u_1} [inst : CommRing R] {a b : R},
  IsUnit (a - b) → IsCoprime (Polynomial.X - Polynomial.C a) (Polynomial.X - Polynomial.C b)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.lineDifferentiableWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₀ f₁ : E → F}
  {s : Set E} {x v : E},
  f₀ =ᶠ[nhdsWithin x s] f₁ →
    f₀ x = f₁ x → (LineDifferentiableWithinAt 𝕜 f₀ s x v ↔ LineDifferentiableWithinAt 𝕜 f₁ s x v)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `!=` on `BitVec`s.  -/
BitVec.reduceBNe : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.instInhabited : {α : Type u_1} → Inhabited (FreeAddMonoid α)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {fallback : β} {f : Option β → Option β},
  (m.alter k f).getD k' fallback = if (k == k') = true then (f m[k]?).getD fallback else m.getD k' fallback
-- ProofWidgets.Data.Html
ProofWidgets.instRpcEncodableHtml : Lean.Server.RpcEncodable ProofWidgets.Html
-- Init.Data.UInt.Bitwise
UInt8.toUInt64_shiftRight : ∀ (a b : UInt8), (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 8)
-- Mathlib.Data.Num.ZNum
ZNum.cast_add : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (m n : ZNum), ↑(m + n) = ↑m + ↑n
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.coe_specialLinearGroup_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Algebra R ℝ] (g : Matrix.SpecialLinearGroup (Fin 2) R)
  (z : UpperHalfPlane),
  ↑(g • z) =
    (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) /
      (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1)))
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddCommGroup : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [AddCommGroup G] → AddCommGroup (l.Germ G)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_id : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  StarSubalgebra.map (StarAlgHom.id R A) S = S
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II_σ : ∀ {n : ℕ} (i : Fin (n + 1)), SimplexCategory.II.σ i = (SimplexCategory.δ i.succ.castSucc).op
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_inter_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.IndepFun.covariance_eq_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.MemLp X 2 μ → MeasureTheory.MemLp Y 2 μ → ProbabilityTheory.covariance X Y μ = 0
-- Mathlib.Data.W.Basic
WType.instIsEmpty : ∀ {α : Type u_1} {β : α → Type u_2} [hα : IsEmpty α], IsEmpty (WType β)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₂ → Std.DHashMap.Const.get? (m₁.diff m₂) k = none
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.coe_sdiff : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  [inst_3 : FaithfulSMul M X] (P Q : { P // IsLprojection X P }), ↑(P \ Q) = ↑P * (1 - ↑Q)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Whiskering a bicone with an equivalence between types preserves being a bilimit bicone.  -/
CategoryTheory.Limits.Bicone.whiskerIsBilimitIff : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {K : Type w'} →
          {f : J → C} → (c : CategoryTheory.Limits.Bicone f) → (g : K ≃ J) → (c.whisker g).IsBilimit ≃ c.IsBilimit
-- Init.Data.String.Lemmas.Basic
String.Pos.byte.congr_simp : ∀ {s : String} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.endPos), pos.byte h = pos_1.byte ⋯
-- Mathlib.Algebra.Group.Defs
/-- A Prop stating that the addition is commutative.  -/
IsAddCommutative : (M : Type u_2) → [Add M] → Prop
-- Aesop.Stats.Basic
Aesop.MonadStats : (Type → Type) → Type 1
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instToMessageDataSuggestion : Lean.ToMessageData Lean.Meta.Tactic.TryThis.Suggestion
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  (Std.HashMap.filter f m)[k]? = m[k]?.pfilter fun x_2 h' => f (m.getKey k ⋯) x_2
-- Init.Data.Array.Basic
/-- Applies the monadic predicate `p` to every element in the array, in order from left to right, and
returns the array of elements for which `p` returns `true`.

Only elements from `start` (inclusive) to `stop` (exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is checked.

Example:
```lean example
#eval #[1, 2, 5, 2, 7, 7].filterM fun x => do
  IO.println s!"Checking {x}"
  return x < 3
```
```output
Checking 1
Checking 2
Checking 5
Checking 2
Checking 7
Checking 7
```
```output
#[1, 2, 2]
```
 -/
Array.filterM : {m : Type → Type u_1} →
  {α : Type} → [Monad m] → (α → m Bool) → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m (Array α)
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
_private.Lean.Meta.Tactic.Grind.MarkNestedSubsingletons.0.Lean.Meta.Grind.markNestedSubsingletons.visit : Lean.Expr → Lean.Meta.Grind.M✝ Lean.Expr
-- Mathlib.Tactic.Sat.FromLRAT
/-- Constructs the proofs of `⊢ ctx.proof c` for each clause `c` in `ctx`.
The proofs are stashed in a `HashMap` keyed on the clause ID.  -/
Mathlib.Tactic.Sat.buildClauses : Array (Array ℤ) →
  Lean.Expr →
    ℕ →
      ℕ →
        Lean.Expr →
          Lean.Expr → ℕ × Std.HashMap ℕ Mathlib.Tactic.Sat.Clause → ℕ × Std.HashMap ℕ Mathlib.Tactic.Sat.Clause
-- Lean.Syntax
/-- Checks whether `sub` is contained in `super`.
`includeSuperStop` and `includeSubStop` control whether `super` and `sub` have
an inclusive upper bound.
 -/
Lean.Syntax.Range.includes : Lean.Syntax.Range → Lean.Syntax.Range → optParam Bool false → optParam Bool false → Bool
-- Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
_private.Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral.0.term𝓟 : Lean.ParserDescr
-- Init.Data.List.MinMaxIdx
List.minIdxOn_lt_length : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.minIdxOn f xs h < xs.length
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.mk_eq_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {v₁ v₂ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)},
  NumberField.FinitePlace.mk v₁ = NumberField.FinitePlace.mk v₂ ↔ v₁ = v₂
-- Mathlib.Data.Fin.Basic
Nat.exists_lt_iff_fin : ∀ {n : ℕ} {p : (k : ℕ) → k < n → Prop}, (∃ k, ∃ (hk : k < n), p k hk) ↔ ∃ k, p ↑k ⋯
-- Mathlib.GroupTheory.Exponent
/-- If there exists an injective, multiplication-preserving map from `G` to `H`,
then the exponent of `G` divides the exponent of `H`.
 -/
Monoid.exponent_dvd_of_monoidHom : ∀ {G : Type u} [inst : Monoid G] {H : Type u_1} [inst_1 : Monoid H] (e : G →* H),
  Function.Injective ⇑e → Monoid.exponent G ∣ Monoid.exponent H
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.mk.sizeOf_spec : ∀ (cmdName : String) (wrapper : Lean.Name) (requireProp isInstance : Bool),
  sizeOf { cmdName := cmdName, wrapper := wrapper, requireProp := requireProp, isInstance := isInstance } =
    1 + sizeOf cmdName + sizeOf wrapper + sizeOf requireProp + sizeOf isInstance
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.isoMk_inv_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  (h : A.A ≅ B.A)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a)
      CategoryTheory.Comonad.Coalgebra.isoMk._auto_1),
  (CategoryTheory.Comonad.Coalgebra.isoMk h w).inv.f = h.inv
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.response : Lean.JsonRpc.RequestID → Lean.JsonRpc.MessageMetaData
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF → ∀ {k a : α} {v : β k}, (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ k ∉ m then k else m.getKey! a
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.instUniqueElemVertsSingletonSubgraph : {V : Type u} → {G : SimpleGraph V} → (v : V) → Unique ↑(G.singletonSubgraph v).verts
-- Init.Data.BitVec.Lemmas
BitVec.ult_eq_decide : ∀ {w : ℕ} {x y : BitVec w}, x.ult y = decide (x.toNat < y.toNat)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_add_self : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  autoParam (IsSelfAdjoint a) CFC.abs_add_self._auto_1 → CFC.abs a + a = 2 • a⁺
-- Mathlib.Algebra.Module.LinearMap.End
/-- Each element of the monoid defines a module endomorphism.

This is a stronger version of `DistribMulAction.toAddMonoidEnd`.  -/
DistribMulAction.toModuleEnd : (R : Type u_1) →
  {S : Type u_3} →
    (M : Type u_4) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Monoid S] → [inst_4 : DistribMulAction S M] → [SMulCommClass S R M] → S →* Module.End R M
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- The flat sections of a functor into `ModuleCat R` form a submodule of all sections.
 -/
ModuleCat.sectionsSubmodule : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) → Submodule R ((j : J) → ↑(F.obj j))
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.repr.eq_1 : ∀ (n : ℕ), n.repr = String.ofList (Nat.toDigits 10 n)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_rightUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Mathlib.RingTheory.Jacobson.Radical
Ring.jacobson_le_of_isMaximal : ∀ {R : Type u_1} [inst : Ring R] (m : Ideal R) [m.IsMaximal], Ring.jacobson R ≤ m
-- Mathlib.CategoryTheory.Monoidal.Bimod
id_tensor_π_preserves_coequalizer_inv_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  {W X Y Z : C} (f g : X ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ W)
  (wh :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) h =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) h),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorLeft Z) f g).inv
        (CategoryTheory.Limits.coequalizer.desc h wh)) =
    h
-- Mathlib.Combinatorics.Additive.Corner.Roth
/-- The triangle indices for the proof of the corners theorem construction.  -/
_private.Mathlib.Combinatorics.Additive.Corner.Roth.0.Corners.triangleIndices : {G : Type u_1} → [AddCommGroup G] → Finset (G × G) → Finset (G × G × G)
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Ico_add_eq_sum_Ico_add_one : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {a b : α} [inst_1 : LinearOrder α]
  [inst_2 : LocallyFiniteOrder α] [inst_3 : AddMonoidWithOne α] [SuccAddOrder α] [NoMaxOrder α],
  a ≤ b → ∀ (f : α → M), ∑ x ∈ Finset.Ico a b, f x + f b = ∑ x ∈ Finset.Ico a (b + 1), f x
-- Init.Data.List.Lemmas
List.foldlM_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {l : List α} {f : β → α → m β} {b : β},
  List.foldlM f b l.reverse = List.foldrM (fun x y => f y x) b l
-- Mathlib.Data.List.DropRight
List.rdropWhile_nil : ∀ {α : Type u_1} (p : α → Bool), List.rdropWhile p [] = []
-- Mathlib.Topology.Algebra.Group.Basic
IsClosed.leftCoset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {U : Set G},
  IsClosed U → ∀ (x : G), IsClosed (x • U)
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- The series over `p^r` for primes `p` converges if and only if `r < -1`.  -/
Nat.Primes.summable_rpow : ∀ {r : ℝ}, (Summable fun p => ↑↑p ^ r) ↔ r < -1
-- Lean.Meta.Constructions.CtorIdx
Lean.mkCtorIdxName : Lean.Name → Lean.Name
-- Mathlib.RingTheory.Localization.BaseChange
instIsLocalizedModuleFinsuppLinearMap : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Submonoid R) (M : Type u_3) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_4} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  {α : Type u_7} [IsLocalizedModule S f], IsLocalizedModule S (Finsupp.mapRange.linearMap f)
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_iUnion : ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] [Finite ι] {s : ι → Set α},
  Bornology.IsBounded (⋃ i, s i) ↔ ∀ (i : ι), Bornology.IsBounded (s i)
-- Aesop.Tracing
Aesop.TraceOption.stats : Aesop.TraceOption
-- Mathlib.Data.Complex.Basic
Complex.ofReal_def : ∀ (r : ℝ), ↑r = { re := r, im := 0 }
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IsIndObject.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)},
  Nonempty (CategoryTheory.Limits.IndObjectPresentation A) → CategoryTheory.Limits.IsIndObject A
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.sum_eq_sum_add_sum : ∀ {K : Type u_1} [inst : Field K] {α : Type u_2} [inst_1 : AddCommMonoid α] [inst_2 : NumberField K]
  (f : NumberField.InfinitePlace K → α), ∑ w, f w = ∑ w, f ↑w + ∑ w, f ↑w
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Add G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffAdd I' n G] (f g : ContMDiffMap I I' N G n), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
the biproduct, see `preservesBinaryBiproduct_of_monoBiprodComparison`.  -/
CategoryTheory.Functor.biprodComparison'_comp_biprodComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms],
  CategoryTheory.CategoryStruct.comp (F.biprodComparison' X Y) (F.biprodComparison X Y) =
    CategoryTheory.CategoryStruct.id (F.obj X ⊞ F.obj Y)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The abscissa of absolute convergence of the L-series of the Möbius function is `1`.  -/
ArithmeticFunction.abscissaOfAbsConv_moebius : (LSeries.abscissaOfAbsConv fun n => ↑(ArithmeticFunction.moebius n)) = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_dblXYZ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblXYZ (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.ReaderT.wp_apply_eq : ∀ {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α ρ : Type u} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] (x : ReaderT ρ m α) (post : α → ρ → Pred) (epost : EPred) (r : ρ),
  Std.Internal.Do.wp x post epost r = Std.Internal.Do.wp (x.run r) (fun a => post a r) epost
-- Mathlib.Data.Nat.Nth
Nat.range_nth_subset : ∀ {p : ℕ → Prop}, Set.range (Nat.nth p) ⊆ insert 0 (Set.ofPred p)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.contains t.maxKey! = true
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.infinite_of_linearIndependent_coxeterWeight_four : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {i j : ι} [NeZero 2]
  [IsAddTorsionFree M], LinearIndependent R ![P.root i, P.root j] → P.coxeterWeight i j = 4 → Infinite ι
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- Geck's name for the "right" basis elements of `b.support ⊕ ι`.  -/
RootPairing.GeckConstruction.v : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} → (b : P.Base) → [DecidableEq ι] → ι → ↥b.support ⊕ ι → R
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₂_iff_isIso₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.Limits.IsZero T.obj₂ ↔ CategoryTheory.IsIso T.mor₃