mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.coeff_select : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (P : ℕ → Prop) (x : WittVector p R) (n : ℕ),
  (WittVector.select P x).coeff n = (MvPolynomial.aeval x.coeff) (WittVector.selectPoly P n)
-- Mathlib.Tactic.Algebra.Basic
/-- Frontend of `algebra`: attempt to close a goal `g`, assuming it is an equation of semirings.  -/
Mathlib.Tactic.Algebra.proveEq : Option ((u : Lean.Level) × Q(Type u)) → Lean.MVarId → Mathlib.Tactic.AtomM Unit
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.MonObj.ofRepresentableBy M (CategoryTheory.yonedaMonObj M)
      (CategoryTheory.yonedaMonObjRepresentableBy M) =
    inst_2
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_eq_singleton_iff : ∀ {k n : ℕ}, (*...=n).toArray = #[k] ↔ n = 0 ∧ 0 = k
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The inclusion map from the second component of the coproduct.  -/
CategoryTheory.Limits.coprod.inr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] → Y ⟶ X ⨿ Y
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- The (colimit) cocone with cocone point `A`.  -/
CategoryTheory.Limits.IndObjectPresentation.cocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (P : CategoryTheory.Limits.IndObjectPresentation A) →
        CategoryTheory.Limits.Cocone (P.F.comp CategoryTheory.yoneda)
-- Mathlib.Topology.Defs.Basic
/-- A map `f : X → Y` is said to be an *open map*,
if the image of any open `U : Set X` is open in `Y`.  -/
IsOpenMap : {X : Type u} → {Y : Type v} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.refl_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (a : A), (ContinuousAlgEquiv.refl R A) a = a
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : SizeOf C] [inst_6 : SizeOf D] (X : D)
  [addMod : CategoryTheory.AddModObj A X], sizeOf { X := X, addMod := addMod } = 1 + sizeOf X + sizeOf addMod
-- Mathlib.Tactic.SplitIfs
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.SplitPosition.target.sizeOf_spec : sizeOf Mathlib.Tactic.SplitPosition.target✝ = 1
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.div_def : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Div (G i)] (f g : (i : ι) → G i), f / g = fun i => f i / g i
-- Mathlib.Analysis.Convex.Slope
/-- If for any three points `x < y < z`, the slope of the secant line of `f : 𝕜 → 𝕜` on `[x, y]` is
strictly less than the slope of the secant line of `f` on `[y, z]`, then `f` is strictly convex.  -/
strictConvexOn_of_slope_strict_mono_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  Convex 𝕜 s →
    (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)) →
      StrictConvexOn 𝕜 s f
-- Mathlib.Geometry.Euclidean.NinePointCircle
/-- Euler points are a set of points that the `ninePointCircle` passes through. They are defined as
being $1/n$th of the way from the Monge point to a vertex. Specifically for triangles, these are
the midpoints between the orthocenter and a given vertex
(`Affine.Triangle.eulerPoint_eq_midpoint`).  -/
Affine.Simplex.eulerPoint : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex ℝ P n → Fin (n + 1) → P
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.op_boundaryLE_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {j : ι},
  e.op.BoundaryLE j ↔ e.BoundaryGE j
-- Batteries.Data.MLList.Basic
/-- Convert a `List` of values inside the monad into a `MLList`.  -/
MLList.ofListM : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → List (m α) → MLList m α
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.go.eq_1 : ∀ {α : Type u_1} (l : List α) (a : α) (a_1 : ℕ) (a_2 : Array α), List.setTR.go✝ l a [] a_1 a_2 = l
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.List.compareLex.match_1.eq_4 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : α) (xs : List α) (y : α) (ys : List α)
  (h_1 : Unit → motive [] []) (h_2 : (x : List α) → motive [] x) (h_3 : (x : List α) → motive x [])
  (h_4 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match x :: xs, y :: ys with
    | [], [] => h_1 ()
    | [], x => h_2 x
    | x, [] => h_3 x
    | x :: xs, y :: ys => h_4 x xs y ys) =
    h_4 x xs y ys
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.Hom.ext_iff : ∀ {A B : AddCommMonCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.isBoundedAt_iff_exists_SL2Z : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ},
  IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range →
    (c.IsBoundedAt f k ↔
      ∃ γ,
        (Matrix.SpecialLinearGroup.mapGL ℝ) γ • OnePoint.infty = c ∧
          UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k γ f))
-- Mathlib.Data.Multiset.NatAntidiagonal
/-- The antidiagonal of `n` does not contain duplicate entries.  -/
Multiset.Nat.nodup_antidiagonal : ∀ (n : ℕ), (Multiset.Nat.antidiagonal n).Nodup
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_D₃_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : 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_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄)
  (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) {Z : C₄}
  (h_1 : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h_1) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h_1
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_iff_superpolynomialDecay_norm : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [inst : NormedField β],
  Asymptotics.SuperpolynomialDecay l k f ↔ Asymptotics.SuperpolynomialDecay l (fun a => ‖k a‖) fun a => ‖f a‖
-- Mathlib.Order.CompleteLattice.Defs
/-- Every set has a greatest lower bound.  -/
CompleteLattice.isGLB_sInf : ∀ {α : Type u_8} [self : CompleteLattice α] (s : Set α), IsGLB s (sInf s)
-- Mathlib.RingTheory.Ideal.Operations
Associates.mk_ne_zero' : ∀ {R : Type u_1} [inst : CommSemiring R] {r : R}, Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheafCocone_ι_app : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C] (y : ↑X)
  (x : (TopologicalSpace.OpenNhds y)ᵒᵖ),
  (skyscraperPresheafCocone p₀ A y).ι.app x =
    CategoryTheory.Limits.terminal.from
      (((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A)).obj x)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.mapBaseChange_tmul : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B] (x : B)
  (y : Ω[A⁄R]), (KaehlerDifferential.mapBaseChange R A B) (x ⊗ₜ[A] y) = x • (KaehlerDifferential.map R R A B) y
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.not_isUnit_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]}, ¬IsUnit z ↔ ‖z‖ < 1
-- Mathlib.Algebra.Order.WithTop.Untop0
/-- Conversion from `WithTop α` to `α`, mapping `⊤` to zero.  -/
WithTop.untop₀ : {α : Type u_1} → [Zero α] → WithTop α → α
-- Batteries.Data.UnionFind.Basic
/-- Find root of a union-find node, updating the structure using path compression.
Panics if index is out of bounds.  -/
Batteries.UnionFind.find! : Batteries.UnionFind → ℕ → Batteries.UnionFind × ℕ
-- Mathlib.Data.Fintype.Prod
Set.toFinset_prod : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) [inst : Fintype ↑s] [inst_1 : Fintype ↑t]
  [inst_2 : Fintype ↑(s ×ˢ t)], (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset
-- Mathlib.Data.Option.NAry
/-- `Option.map₂` in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism.  -/
Option.map₂_def : ∀ {α β γ : Type u} (f : α → β → γ) (a : Option α) (b : Option β), Option.map₂ f a b = f <$> a <*> b
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
/-- If a function vanishes on `sᶜ`, then its integral on `s` coincides with its integral on the
whole space.  -/
MeasureTheory.VectorMeasure.setIntegral_eq_integral_of_forall_compl_eq_zero : ∀ {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}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s → (∀ x ∉ s, f x = 0) → ∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_coe_eq_self_iff_mem_Ioc : ∀ {θ : ℝ}, (↑θ).toReal = θ ↔ θ ∈ Set.Ioc (-Real.pi) Real.pi
-- Lean.Data.LBool
Lean.LBool.noConfusionType : Sort v✝ → Lean.LBool → Lean.LBool → Sort v✝
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_3),
  (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₁ =
    CategoryTheory.CategoryStruct.id (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology
-- Mathlib.Topology.EMetricSpace.Defs
/-- The extended pseudodistance on a subset of a pseudoemetric space is the restriction of
the original pseudodistance, by definition.  -/
Subtype.edist_eq : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (x y : Subtype p), edist x y = edist ↑x ↑y
-- Mathlib.RingTheory.Ideal.CotangentBaseChange
Ideal.tensorCotangentHom_surjective : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (I : Ideal S), Function.Surjective ⇑(Ideal.tensorCotangentHom R T I)
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_coe : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5}
  [inst : FunLike F α β] [inst_1 : RingHomClass F α β] (f : F), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Hom.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.StrongTrans.Hom η θ},
  x.as = y.as → x = y
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.mk.injEq : ∀ (carrier : Type u) [str : AddSemigroup carrier] (carrier_1 : Type u) (str_1 : AddSemigroup carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_obj : ∀ (x : CategoryTheory.Limits.WalkingParallelPair),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.obj x =
    CategoryTheory.Limits.parallelPair.parallelPairObj CategoryTheory.Limits.WalkingParallelFamily.zero
      CategoryTheory.Limits.WalkingParallelFamily.one x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.typeParameter.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.typeParameter = 1
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.coeff_preHilbertPoly_self : ∀ (F : Type u_1) [inst : Field F] [CharZero F] (d k : ℕ), (Polynomial.preHilbertPoly F d k).coeff d = (↑d.factorial)⁻¹
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.reduceBinPred : Lean.Name → ℕ → (ℕ → ℕ → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.toReal_of_ne_top : ∀ {p q : ENNReal}, p ≠ ⊤ → q ≠ ⊤ → ∀ [p.HolderConjugate q], p.toReal.HolderConjugate q.toReal
-- Mathlib.Algebra.Polynomial.Sequence
/-- The `i`-th element in the sequence has degree `i`. Use `S.degree_eq` instead.  -/
Polynomial.Sequence.degree_eq' : ∀ {R : Type u_1} [inst : Semiring R] (self : Polynomial.Sequence R) (i : ℕ), (↑self i).degree = ↑i
-- Mathlib.Combinatorics.Digraph.Basic
/-- The supremum of two digraphs `x ⊔ y` has edges where either `x` or `y` have edges.  -/
Digraph.instMax : {V : Type u_2} → Max (Digraph V)
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_smul : ∀ {S : Type u_1} {R : Type u_3} [inst : CommRing R] (a : Quaternion R) [inst_1 : SMul S R] (s : S),
  (s • a).imJ = s • a.imJ
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.mk.injEq : ∀ {α : Type u_8} {β : Type u_9} [inst : SupSet α] [inst_1 : SupSet β] (toFun : α → β)
  (map_sSup' : ∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s)) (toFun_1 : α → β)
  (map_sSup'_1 : ∀ (s : Set α), toFun_1 (sSup s) = sSup (toFun_1 '' s)),
  ({ toFun := toFun, map_sSup' := map_sSup' } = { toFun := toFun_1, map_sSup' := map_sSup'_1 }) = (toFun = toFun_1)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
uniformContinuous_rangeFactorization_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous (Set.rangeFactorization f) ↔ UniformContinuous f
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `CommMonoid.Torsion.ofTorsion`.

---

Torsion submonoids of a torsion submonoid are isomorphic to the submonoid.  -/
Torsion.ofTorsion : (G : Type u_1) → [inst : CommMonoid G] → ↥(CommMonoid.torsion ↥(CommMonoid.torsion G)) ≃* ↥(CommMonoid.torsion G)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_inclusion : ∀ {R : Type u} [inst : NonAssocRing R] {S T : Subring R} (h : S ≤ T) (x : ↥S), ↑((Subring.inclusion h) x) = ↑x
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution of the zero measure with a measure μ returns
the zero measure.  -/
MeasureTheory.Measure.zero_conv : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] (μ : MeasureTheory.Measure M),
  MeasureTheory.Measure.conv 0 μ = 0
-- Std.Time.Time.HourMarker
Std.Time.HourMarker.ofNat_ctorIdx : ∀ (x : Std.Time.HourMarker), Std.Time.HourMarker.ofNat x.ctorIdx = x
-- Aesop.Script.Step
Aesop.Script.Step.postGoals : Aesop.Script.Step → Array Aesop.GoalWithMVars
-- Aesop.BuiltinRules.ApplyHyps
Aesop.BuiltinRules.applyHyp : Lean.FVarId → Lean.MVarId → Lean.Meta.TransparencyMode → Aesop.BaseM Aesop.RuleApplication
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesToE_map : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁')
  (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (f₁₂' : i₀' ⟶ i₂') (h₁₂' : CategoryTheory.CategoryStruct.comp f₁' f₂' = f₁₂')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₂ f₁₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁₂' f₃') (n₀ n₁ n₂ : ℤ),
  autoParam (β.app 0 = α.app 0) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_1 →
    autoParam (β.app 1 = α.app 2) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_3 →
      ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_5)
        (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_7),
        CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
            (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (X.opcyclesMap f₁₂ f₃ f₁₂' f₃' β n₁)
            (X.opcyclesToE f₁' f₂' f₃' f₁₂' h₁₂' n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.associator_hom_toNatTrans : ∀ {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E),
  (CategoryTheory.Bicategory.associator F G H).hom.toNatTrans = (F.toFunctor.associator G.toFunctor H.toFunctor).hom
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin.mono : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S T : Set E),
  S ⊆ T → IntermediateField.adjoin F S ≤ IntermediateField.adjoin F T
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Variant of `Scheme.exists_isOpenCover_and_isAffine_of_finite` in terms of `Scheme.OpenCover`.  -/
AlgebraicGeometry.Scheme.OpenCover.exists_of_isCofiltered_of_finite : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)]
  [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] (𝒰 : c.pt.OpenCover) [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)]
  [Finite 𝒰.I₀],
  ∃ i R f,
    ∃ (_ :
      CategoryTheory.Presieve.ofArrows (fun i => AlgebraicGeometry.Spec (R i)) f ∈
        AlgebraicGeometry.Scheme.zariskiPrecoverage.coverings (D.obj i)),
      ∃ g, ∀ (j : 𝒰.I₀), CategoryTheory.IsPullback (g j) (𝒰.f j) (f j) (c.π.app i)
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.brecOn_2.go : {motive_1 : Mathlib.Tactic.Translate.ArgReorder → Sort u} →
  {motive_2 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u} →
    {motive_3 : List (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u} →
      {motive_4 : ℕ × Mathlib.Tactic.Translate.ArgReorder → Sort u} →
        (t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
          ((t : Mathlib.Tactic.Translate.ArgReorder) → t.below → motive_1 t) →
            ((t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
                Mathlib.Tactic.Translate.ArgReorder.below_1 t → motive_2 t) →
              ((t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
                  Mathlib.Tactic.Translate.ArgReorder.below_2 t → motive_3 t) →
                ((t : ℕ × Mathlib.Tactic.Translate.ArgReorder) →
                    Mathlib.Tactic.Translate.ArgReorder.below_3 t → motive_4 t) →
                  motive_3 t ×' Mathlib.Tactic.Translate.ArgReorder.below_2 t
-- Std.Http.Internal.IndexMultiMap
Std.Internal.instReprIndexMultiMap : {α : Type u_1} →
  {β : Type u_2} → {inst : BEq α} → {inst_1 : Hashable α} → [Repr α] → [Repr β] → Repr (Std.Internal.IndexMultiMap α β)
-- Mathlib.Data.Set.Sigma
/-- Indexed sum of sets. `s.sigma t` is the set of dependent pairs `⟨i, a⟩` such that `i ∈ s` and
`a ∈ t i`.  -/
Set.sigma : {ι : Type u_1} → {α : ι → Type u_3} → Set ι → ((i : ι) → Set (α i)) → Set ((i : ι) × α i)
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_preimage : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {s : Set β} {f : α → β},
  Filter.EventuallyConst (f ⁻¹' s) l ↔ Filter.EventuallyConst s (Filter.map f l)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.val_assemble₁_le : ∀ {w : UInt8} {h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done} {c : Char},
  ByteArray.utf8DecodeChar?.assemble₁ w h = some c → c.val ≤ 127
-- Lean.Parser.Term
Lean.Parser.Term.letPatDecl.formatter : optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.sum_PrimePow_eq_sum_sum : ∀ {R : Type u_1} [inst : AddCommMonoid R] (f : ℕ → R) {x : ℝ},
  0 ≤ x →
    ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n =
      ∑ k ∈ Finset.Icc 1 ⌊Real.log x / Real.log 2⌋₊, ∑ p ∈ Finset.Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃_map_app_app_app_app_app_app : ∀ {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] {X Y : CategoryTheory.Functor C₁ D₁} (τ₁ : X ⟶ Y)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X_1 : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (c : C₁) (X_2 : C₂)
  (X_3 : C₃),
  (((((((CategoryTheory.Functor.whiskeringLeft₃ E).map τ₁).app F₂).app F₃).app X_1).app c).app X_2).app X_3 =
    ((X_1.map (τ₁.app c)).app (F₂.obj X_2)).app (F₃.obj X_3)
-- Batteries.Lean.PersistentHashSet
Lean.PersistentHashSet.instBEq_batteries : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → BEq (Lean.PersistentHashSet α)
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.idxOf_eq_getD_idxOf?`. -/
List.idxOf_eq_idxOf? : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), List.idxOf a l = (List.idxOf? a l).getD l.length
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.numLeaves`.  -/
Tree.numLeaves : {α : Type u_1} → Tree α → ℕ