mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.eq_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N) {x : N} {y : M}, y = e.symm x ↔ e y = x
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zmultiples_zero_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.zmultiples 0 = ⊥
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- A function `f : G → A` satisfies the 1-coboundary condition if there's `x : A` such that
`g • x - x = f(g)` for all `g : G`.  -/
groupCohomology.IsCoboundary₁ : {G : Type u_1} → {A : Type u_2} → [AddCommGroup A] → [SMul G A] → (G → A) → Prop
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_div_left' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] [MulRightMono α] {a b : α},
  a ≤ b → ∀ (c : α), c / b ≤ c / a
-- Lean.Server.References
/-- Index that allows efficiently looking up the imports of a module by module name.
Since the same module can be imported multiple times with different attributes,
each module name maps to an array of imports.
 -/
Lean.Server.DirectImports.index : Lean.Server.DirectImports → Lean.Server.ModuleImportIndex
-- Mathlib.GroupTheory.NoncommCoprod
/-- Variant of `AddMonoidHom.noncommCoprod_apply` with the sum written in the other direction  -/
AddMonoidHom.noncommCoprod_apply' : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) (mn : M × N),
  (f.noncommCoprod g comm) mn = g mn.2 + f mn.1
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.mono_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting), CategoryTheory.Mono S.f
-- Lean.Data.Lsp.Internal
/-- Declarations of a file with associated position information.  -/
Lean.Lsp.Decls : Type
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.val_neg_addUnit : ∀ {M : Type u_6} [inst : AddMonoid M] {x : M} (hx : IsOfFinAddOrder x), ↑(-hx.addUnit) = (addOrderOf x - 1) • x
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_bot : ⊥.toENNReal = 0
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitAnchorRefInfo.mk.injEq : ∀ (numDigits : ℕ) (anchor : UInt64) (ordinal numDigits_1 : ℕ) (anchor_1 : UInt64) (ordinal_1 : ℕ),
  ({ numDigits := numDigits, anchor := anchor, ordinal := ordinal } =
      { numDigits := numDigits_1, anchor := anchor_1, ordinal := ordinal_1 }) =
    (numDigits = numDigits_1 ∧ anchor = anchor_1 ∧ ordinal = ordinal_1)
-- Mathlib.GroupTheory.Torsion
/-- Torsion additive groups are closed under extensions.  -/
IsAddTorsion.extension_closed : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : AddGroup H] {f : G →+ H},
  N = f.ker → IsAddTorsion H → IsAddTorsion ↥N → IsAddTorsion G
-- Std.Time.DateTime.Timestamp
Std.Time.instDecidableLtTimestamp : {x y : Std.Time.Timestamp} → Decidable (x < y)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.ne_zero : ∀ {ι : 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 : ι) [NeZero 2],
  P.root i ≠ 0
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x`. If the series converges at a
point, and all functions in the series are differentiable with a summable bound on the derivatives,
then the series is differentiable and its derivative is the sum of the derivatives.  -/
hasFDerivAt_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  {u : α → ℝ} [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {x₀ : E},
  Summable u →
    (∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) →
      (∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) →
        (Summable fun n => f n x₀) → ∀ (x : E), HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.mk : ∀ {V : Type u_1} {G : SimpleGraph V}, G.Connected → G.IsAcyclic → G.IsTree
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceOpcycles : ∀ {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 : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), CategoryTheory.Mono (X.kernelSequenceOpcycles f g fg h n).f
-- Mathlib.Data.Finset.Image
Finset.subtype_eq_empty : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s
-- Mathlib.Data.Finsupp.Indicator
Finsupp.eq_indicator_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) {g : ι → α},
  g = ⇑(Finsupp.indicator s f) ↔ Function.support g ⊆ ↑s ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.continuousOn_sqrt : ContinuousOn Complex.sqrt Complex.slitPlane
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.toList_take_zero : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite (Std.Iterators.Types.Take α Id) Id]
  {it : Std.Iter β}, (Std.Iter.take 0 it).toList = []
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
EuclideanGeometry.oangle_pointReflection_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  p₁ ≠ p₂ →
    p₃ ≠ p₂ →
      EuclideanGeometry.oangle p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) =
        EuclideanGeometry.oangle p₁ p₂ p₃ + ↑Real.pi
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.matrix_trace_commutator_zero : ∀ (n : Type u_1) (R : Type u₂) [inst : CommRing R] [inst_1 : Fintype n] (X Y : Matrix n n R), ⁅X, Y⁆.trace = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- **Alias** of `Real.exists_measure_rpow_eq_integral_rpowIntegrand₀₁`.

---

The integral representation of the function `x ↦ x ^ p` (where `p ∈ (0, 1)`) .  -/
Real.exists_measure_rpow_eq_integral : ∀ {p : ℝ},
  p ∈ Set.Ioo 0 1 →
    ∃ μ,
      ∀ x ∈ Set.Ici 0,
        MeasureTheory.IntegrableOn (fun t => p.rpowIntegrand₀₁ t x) (Set.Ioi 0) μ ∧
          x ^ p = ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t x ∂μ
-- Lean.Data.AssocList
Lean.AssocList.nil.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β], sizeOf Lean.AssocList.nil = 1
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_trans_assoc : ∀ {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] {G H K : CategoryTheory.Functor C D} (α : G ≅ H)
  (β : H ≅ K) (F : CategoryTheory.Functor D E) {Z : CategoryTheory.Functor C E} (h : K.comp F ≅ Z),
  CategoryTheory.Functor.isoWhiskerRight (α ≪≫ β) F ≪≫ h =
    CategoryTheory.Functor.isoWhiskerRight α F ≪≫ CategoryTheory.Functor.isoWhiskerRight β F ≪≫ h
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mk_le_mk : ∀ {M : Type u_1} [inst : Mul M] {s t : Set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s)
  (h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a * b ∈ t),
  { carrier := s, mul_mem' := h_mul } ≤ { carrier := t, mul_mem' := h_mul' } ↔ s ⊆ t
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.sum : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {α : Type u_1} {s : Finset α}
  {f : α → (ι → ℝ) → E} {g : α → F},
  (∀ i ∈ s, BoxIntegral.HasIntegral I l (f i) vol (g i)) →
    BoxIntegral.HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
-- Mathlib.Topology.Separation.Basic
nhdsSet_inj_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s t : Set X}, nhdsSet s = nhdsSet t ↔ s = t
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Refining each component of a pre-`0`-hypercover yields a refined pre-`0`-hypercover of the
base.  -/
CategoryTheory.PreZeroHypercover.bind : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : C} →
      (E : CategoryTheory.PreZeroHypercover T) →
        ((i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)) → CategoryTheory.PreZeroHypercover T
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.equivOfNatIso_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).unitIso =
    CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.symm ≪≫
      CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq ⋯ ≪≫
        CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α.hom α.inv
-- Mathlib.Data.Set.Sups
Set.iUnion_image_sup_right : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t : Set α), ⋃ b ∈ t, (fun x => x ⊔ b) '' s = s ⊻ t
-- Init.Data.List.Lemmas
List.dropLast_concat : ∀ {α : Type u_1} {l₁ : List α} {b : α}, (l₁ ++ [b]).dropLast = l₁
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.match_1.congr_eq_1 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  x = Ordering.lt →
    (match x with
      | Ordering.lt => h_1 ()
      | Ordering.eq => h_2 ()
      | Ordering.gt => h_3 ()) ≍
      h_1 ()
-- Init.Data.Array.Lemmas
Array.mem_iff_getElem : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs ↔ ∃ i, ∃ (h : i < xs.size), xs[i] = a
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instEssSurjKaroubiToKaroubiOfIsIdempotentComplete : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsIdempotentComplete C],
  (CategoryTheory.Idempotents.toKaroubi C).EssSurj
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsMinor.refl : ∀ {α : Type u_1} {M : Matroid α}, M ≤m M
-- Mathlib.Algebra.Algebra.Unitization
/-- **Alias** of the forward direction of `Unitization.isStarNormal_inr`. -/
IsStarNormal.of_inr : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarAddMonoid R] [inst_2 : Star A] {a : A}
  [inst_3 : AddCommMonoid A] [inst_4 : Mul A] [inst_5 : SMulWithZero R A], IsStarNormal ↑a → IsStarNormal a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.Cofan.op.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  (c : CategoryTheory.Limits.Cofan Z), c.op = CategoryTheory.Limits.Fan.mk (Opposite.op c.pt) fun a => (c.inj a).op
-- Mathlib.Order.Std
/-- Create a `LinearOrder` from a type satisfying `Std.IsLinearOrder`.

If an `LE` instance exists, either an `Std.IsLinearOrder` instance must exist, or there must be an
`Ord` instance together with `Std.LawfulOrderOrd`, `Std.LawfulEqOrd`, and `Std.TransOrd` instances.

If no `LE` instance exists, it can be generated from `Ord`, `Std.LawfulEqOrd`, and `Std.TransOrd`
instances.

If an `LT` instance exists, an `Std.LawfulOrderLT` instance must exist also; otherwise, a suitable
`LT` instance will be generated.

If a `DecidableLE` instance exists, it will be used. Otherwise, it can be generated from an `Ord`
instance.

If `DecidableEq` and `DecidableLT` instances exist, they will be used. Otherwise, they will be
generated from the `DecidableLE` instance.

If `Min` and `Max` instances exist, they will be used, in which case the user must provide
`Std.LawfulOrderLeftLeaningMin` or `Std.LawfulOrderLeftLeaningMax` respectively. Otherwise, they
will be generated.

If an `Ord` instance exists, it will be used, in which case the user must provide an
`Std.LawfulOrderOrd` instance. Otherwise, it will be generated.  -/
LinearOrder.ofStd : (α : Type u_1) → autoParam (LinearOrder.OfStdArgs α) LinearOrder.ofStd._auto_1 → LinearOrder α
-- Mathlib.Order.Filter.Bases.Finite
Filter.generate_eq_generate_inter : ∀ {α : Type u_1} (s : Set (Set α)), Filter.generate s = Filter.generate (Set.sInter '' {t | t.Finite ∧ t ⊆ s})
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.lift_normNoninc : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0),
  f.NormNoninc → (NormedAddGroupHom.lift S f hf).NormNoninc
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `AddHom.pi`.

---

A family of AddHom's `f a : γ → β a` defines an AddHom `AddHom.pi f : γ → Π a, β a` given by
`AddHom.pi f x b = f b x`.  -/
Pi.addHom : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → Add (f i)] → {γ : Type w} → [inst_1 : Add γ] → ((i : I) → γ →ₙ+ f i) → γ →ₙ+ (i : I) → f i
-- Mathlib.NumberTheory.Dioph
IsPoly.below.sub : ∀ {α : Type u_1} {motive : (a : (α → ℕ) → ℤ) → IsPoly a → Prop} {f g : (α → ℕ) → ℤ} (a : IsPoly f) (a_1 : IsPoly g),
  IsPoly.below a → motive f a → IsPoly.below a_1 → motive g a_1 → IsPoly.below ⋯
-- Mathlib.Order.BoundedOrder.Basic
Prod.fst_top : ∀ (α : Type u) (β : Type v) [inst : Top α] [inst_1 : Top β], ⊤.1 = ⊤
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.Rel'.inl_inr : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S),
  CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl ((CategoryTheory.ConcreteCategory.hom f) s))
    (Sum.inr ((CategoryTheory.ConcreteCategory.hom g) s))
-- Mathlib.Algebra.Star.Basic
/-- The opposite type carries the same star operation.  -/
MulOpposite.instStar : {R : Type u} → [Star R] → Star Rᵐᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_congr : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ} {W : Type u_4} {H : SimpleGraph W} (f : G ≃g H),
  G.Colorable n ↔ H.Colorable n
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.serreDerivative_add : ∀ (k : ℂ) (F G : UpperHalfPlane → ℂ),
  MDiff F →
    MDiff G → Derivative.serreDerivative k (F + G) = Derivative.serreDerivative k F + Derivative.serreDerivative k G
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Isomorphisms from identities in ℕ.  -/
CategoryTheory.CosimplicialObject.eqToIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.CosimplicialObject C) → {n m : ℕ} → n = m → (X.obj { len := n } ≅ X.obj { len := m })
-- Mathlib.Algebra.DirectSum.Module
DFinsupp.lsum.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] [inst_6 : Semiring S] [inst_7 : Module S N]
  [inst_8 : SMulCommClass R S N],
  DFinsupp.lsum S =
    { toFun := fun F => { toFun := ⇑(DFinsupp.sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯, invFun := fun F i => F ∘ₗ DFinsupp.lsingle i, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The subobject lattice of a subobject `Y` is order isomorphic to the interval `Set.Iic Y`.  -/
CategoryTheory.Subobject.subobjectOrderIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (Y : CategoryTheory.Subobject X) →
        CategoryTheory.Subobject (CategoryTheory.Subobject.underlying.obj Y) ≃o ↑(Set.Iic Y)
-- Init.Prelude
of_decide_eq_false : ∀ {p : Prop} [inst : Decidable p], decide p = false → ¬p
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.categoryObjects : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CategoryTheory.Cat} →
      {j : J} → CategoryTheory.SmallCategory ((F.comp CategoryTheory.Cat.objects).obj j)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_succ : ∀ (o : Ordinal.{u_1}), Cardinal.aleph (Order.succ o) = Order.succ (Cardinal.aleph o)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.foldlIdx.match_1.eq_1 : ∀ {β : Type u_1} (motive : List β → ℕ → Sort u_2) (x : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (b : β) → (l : List β) → (s : ℕ) → motive (b :: l) s),
  (match [], x with
    | [], x => h_1 x
    | b :: l, s => h_2 b l s) =
    h_1 x
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_pow_self : ∀ {p n : ℕ}, Nat.Prime p → (p ^ n).factorization p = n
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup_eq_sign_ker : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], alternatingGroup α = Equiv.Perm.sign.ker
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_self_apply_pow : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (n : ℕ) (x : α),
  f.cycleOf ((f ^ n) x) = f.cycleOf x
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.terminatedAt_iff_s_terminatedAt : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ}, g.TerminatedAt n ↔ g.s.TerminatedAt n
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_of_degree_eq_one : ∀ {p : Polynomial ℂ}, p.degree = 1 → p.mahlerMeasure = max ‖p.coeff 1‖ ‖p.coeff 0‖
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fdiv.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m.succ, Int.negSucc n with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_3 m n
-- Mathlib.Topology.Closure
/-- The closure of a set `s` is dense if and only if `s` is dense.  -/
dense_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense (closure s) ↔ Dense s
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_le_of_nhds_zero : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F}
  {C : ℝ}, 0 ≤ C → (∀ᶠ (x : E) in nhds 0, ‖f x‖ ≤ C * ‖x‖) → ‖f‖ ≤ C
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.center_toNonUnitalSubring : ∀ (R : Type u_3) (A : Type u_4) [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A],
  (NonUnitalSubalgebra.center R A).toNonUnitalSubring = NonUnitalSubring.center A
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.ins.match_3.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α)
  (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a y b))
  (h_3 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)),
  (match RBTree.RBNode.node RBTree.RBColor.red a y b with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node RBTree.RBColor.red a y b => h_2 a y b
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_3 a y b) =
    h_2 a y b
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The category of bipointed types.  -/
Bipointed : Type (u + 1)
-- Mathlib.RingTheory.Binomial
Ring.ascPochhammer_succ_succ : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Pow R ℕ] [NatPowAssoc R] [inst_3 : BinomialRing R] (r : R)
  (k : ℕ),
  (ascPochhammer ℕ (k + 1)).smeval (r + 1) =
    (k + 1).factorial • Ring.multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
_private.Mathlib.Algebra.Category.ModuleCat.Biproducts.0.lequivProdOfLeftSplitExact' : {R : Type u} →
  {A M B : Type v} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup A] →
        [inst_2 : Module R A] →
          [inst_3 : AddCommGroup B] →
            [inst_4 : Module R B] →
              [inst_5 : AddCommGroup M] →
                [inst_6 : Module R M] →
                  {j : A →ₗ[R] M} →
                    {g : M →ₗ[R] B} →
                      {f : M →ₗ[R] A} →
                        Function.Surjective ⇑g → j.range = g.ker → f ∘ₗ j = LinearMap.id → (A × B) ≃ₗ[R] M
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.hasStrictDerivAt_arctan : ∀ (x : ℝ), HasStrictDerivAt Real.arctan (1 / (1 + x ^ 2)) x
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.mk : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            (desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt) →
              autoParam
                  (∀ (s : CategoryTheory.Limits.Cocone F) (j : J),
                    CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc s) = s.ι.app j)
                  CategoryTheory.Limits.IsColimit.fac._autoParam →
                autoParam
                    (∀ (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
                      (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s)
                    CategoryTheory.Limits.IsColimit.uniq._autoParam →
                  CategoryTheory.Limits.IsColimit t
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- A version of `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric`
in terms of the value of the series.  -/
EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers : ∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →* F},
  Summable ⇑f → ∀ (N : ℕ), ∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' (m : ↑N.smoothNumbers), f ↑m
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_eq_card_iff : ∀ {V : Type u} {G : SimpleGraph V} [inst : Fintype V], G.chromaticNumber = ↑(Fintype.card V) ↔ G = ⊤