mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- Given functions `F i, f` which are continuous on a compact set `s`, `F` tends to `f`
uniformly on `s` if and only if the restrictions (as elements of `C(s, β)`) converge.  -/
ContinuousOn.tendsto_domRestrict_iff_tendstoUniformlyOn : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {s : Set α} [CompactSpace ↑s]
  {f : α → β} (hf : ContinuousOn f s) {ι : Type u_1} {p : Filter ι} {F : ι → α → β}
  (hF : ∀ (i : ι), ContinuousOn (F i) s),
  Filter.Tendsto (fun i => { toFun := s.domRestrict (F i), continuous_toFun := ⋯ }) p
      (nhds { toFun := s.domRestrict f, continuous_toFun := ⋯ }) ↔
    TendstoUniformlyOn F f p s
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLE.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (f : A ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X : CategoryTheory.Subobject B) (h : CategoryTheory.Subobject.mk f ≤ X),
  CategoryTheory.Subobject.ofMkLE f X h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).inv
      ((CategoryTheory.Subobject.mk f).ofLE X h)
-- Mathlib.Analysis.InnerProductSpace.Semisimple
/-- The orthogonal complement of an invariant submodule is invariant.  -/
LinearMap.IsSymmetric.orthogonalComplement_mem_invtSubmodule : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : Module.End 𝕜 E} {p : Submodule 𝕜 E}, LinearMap.IsSymmetric T → p ∈ T.invtSubmodule → pᗮ ∈ T.invtSubmodule
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.op_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (a : Mᵃᵒᵖ),
  (AddHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a
-- Init.Control.Except
/-- Sequences two actions that may throw exceptions. Typically used via `do`-notation or the `>>=`
operator.
 -/
ExceptT.bind : {ε : Type u} → {m : Type u → Type v} → [Monad m] → {α β : Type u} → ExceptT ε m α → (α → ExceptT ε m β) → ExceptT ε m β
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
commGroupAddCommGroupEquivalence_functor : commGroupAddCommGroupEquivalence.functor = CommGrpCat.toAddCommGrp
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α},
  a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (R₀ : Type u_5)
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀] [inst_9 : Fintype σ] [inst_10 : DecidableEq σ],
  (MvPolynomial.map (algebraMap R₀ R)) (P.jacobianOfHasCoeffs R₀) = P.jacobiMatrix.det
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- `MonoidAlgebra.mapDomain` as a linear equiv.  -/
MonoidAlgebra.mapDomainLinearEquiv : (R : Type u_1) →
  (S : Type u_2) →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] → [inst_2 : Module R S] → M ≃ N → MonoidAlgebra S M ≃ₗ[R] MonoidAlgebra S N
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_range_reflect : ∀ {δ : Type u_4} [inst : AddCommMonoid δ] (f : ℕ → δ) (n : ℕ),
  ∑ j ∈ Finset.range n, f (n - 1 - j) = ∑ j ∈ Finset.range n, f j
-- Batteries.Data.List.Basic
/-- Quaternary version of `List.zipWith`.  -/
List.zipWith₄ : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {δ : Type u_4} → {ε : Type u_5} → (α → β → γ → δ → ε) → List α → List β → List γ → List δ → List ε
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.separatelyContinuousAdd : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [SeparatelyContinuousAdd M] (S : AddSubmonoid M),
  SeparatelyContinuousAdd ↥S
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {fallback : β},
  (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Mathlib.Geometry.Euclidean.PerpBisector
Isometry.mapsTo_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V' : Type u_3} {P' : Type u_4} [inst_4 : NormedAddCommGroup V']
  [inst_5 : InnerProductSpace ℝ V'] [inst_6 : MetricSpace P'] [inst_7 : NormedAddTorsor V' P'] {f : P → P'},
  Isometry f →
    ∀ (p₁ p₂ : P), Set.MapsTo f ↑(AffineSubspace.perpBisector p₁ p₂) ↑(AffineSubspace.perpBisector (f p₁) (f p₂))
-- Mathlib.Data.Set.Card
Set.ncard_singleton : ∀ {α : Type u_1} (a : α), {a}.ncard = 1
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc_coe_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜},
  x ∈ Set.Ioc a (a + p) → AddCircle.liftIoc p a f ↑x = f x
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Multilinear maps over the ring `R`, from `∀ i, M₁ i` to `M₂` where `M₁ i` and `M₂` are modules
over `R`.  -/
MultilinearMap : (R : Type uR) →
  {ι : Type uι} →
    (M₁ : ι → Type v₁) →
      (M₂ : Type v₂) →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] → [(i : ι) → Module R (M₁ i)] → [Module R M₂] → Type (max (max uι v₁) v₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          W.addX P Q =
            ((P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) ^ 2 +
                      W.a₁ * (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) * P 2 * Q 2 * WeierstrassCurve.Jacobian.addZ P Q -
                    W.a₂ * P 2 ^ 2 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 -
                  P 0 * Q 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 -
                Q 0 * P 2 ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) /
              (P 2 * Q 2) ^ 2
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.untilToken.better : Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Server.FileWorker.AbsoluteLspSemanticToken → Bool
-- Mathlib.Order.NonemptyFiniteChains
PartOrd.nonemptyFiniteChainsFunctor_map : ∀ {X Y : PartOrd} (f : X ⟶ Y),
  PartOrd.nonemptyFiniteChainsFunctor.map f =
    PartOrd.ofHom (PartialOrder.NonemptyFiniteChains.orderHomMap (PartOrd.Hom.hom f))
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- The weighted cone `W.weightedLimCone F` is a limit.  -/
CategoryTheory.Functor.isLimitWeightedLimCone : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (W : CategoryTheory.Functor J (Type w)) →
          (F : CategoryTheory.Functor J C) →
            [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] → (W.weightedLimCone F).IsLimit
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.restrictVar.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    {β : Type u_5} →
      [inst : DecidableEq α] →
        (motive : (x : L.Term α) → (↥x.varFinset → β) → Sort u_4) →
          (x : L.Term α) →
            (x_1 : ↥x.varFinset → β) →
              ((a : α) → (f : ↥(FirstOrder.Language.var a).varFinset → β) → motive (FirstOrder.Language.var a) f) →
                ((l : ℕ) →
                    (F : L.Functions l) →
                      (ts : Fin l → L.Term α) →
                        (f : ↥(FirstOrder.Language.func F ts).varFinset → β) →
                          motive (FirstOrder.Language.func F ts) f) →
                  motive x x_1
-- Mathlib.Analysis.Normed.Group.Basic
mem_eball_one_iff : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E} {r : ENNReal}, a ∈ Metric.eball 1 r ↔ ‖a‖ₑ < r
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedAddGroup.toContinuousENorm.eq_1 : ∀ {E : Type u_4} [inst : SeminormedAddGroup E],
  SeminormedAddGroup.toContinuousENorm = { toENorm := NNNorm.toENorm, continuous_enorm := ⋯ }
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
TensorProduct.AlgebraTensorModule.range_lTensor_idealMap : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) {B : Type u_3} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (S : Type u_4) [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (I : Ideal B),
  ((TensorProduct.AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range =
    Submodule.restrictScalars S (Ideal.map Algebra.TensorProduct.includeRight I)
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.range_fst_of_isPullback : ∀ {P X Y Z : Type u} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom fst) =
      ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)
-- Mathlib.Order.DirectedInverseSystem
/-- A copy of `DirectedSystem.map_self` specialized to FunLike, as otherwise the
`fun i j h ↦ f i j h` can confuse the simplifier.  -/
DirectedSystem.map_self' : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] ⦃i : ι⦄ (x : F i), (f i i ⋯) x = x
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.ZoneRules.mk.injEq : ∀ (initialLocalTimeType : Std.Time.TimeZone.LocalTimeType) (transitions : Array Std.Time.TimeZone.Transition)
  (transitionRule : Option Std.Time.TimeZone.RecurringRule) (initialLocalTimeType_1 : Std.Time.TimeZone.LocalTimeType)
  (transitions_1 : Array Std.Time.TimeZone.Transition) (transitionRule_1 : Option Std.Time.TimeZone.RecurringRule),
  ({ initialLocalTimeType := initialLocalTimeType, transitions := transitions, transitionRule := transitionRule } =
      { initialLocalTimeType := initialLocalTimeType_1, transitions := transitions_1,
        transitionRule := transitionRule_1 }) =
    (initialLocalTimeType = initialLocalTimeType_1 ∧ transitions = transitions_1 ∧ transitionRule = transitionRule_1)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parent.eq_1 : ∀ (self : Batteries.UnionFind) (i : ℕ), self.parent i = Batteries.UnionFind.parentD self.arr i
-- Mathlib.Analysis.Normed.Group.Int
nnnorm_zpow_le_mul_norm : ∀ {α : Type u_1} [inst : SeminormedCommGroup α] (n : ℤ) (a : α), ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
/-- `(Subfunctor.equalizer f g).toFunctor` is the equalizer of `f` and `g`.  -/
CategoryTheory.Subfunctor.equalizer.forkIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₁ F₂ : CategoryTheory.Functor C (Type w)} →
      {A : CategoryTheory.Subfunctor F₁} →
        (f g : A.toFunctor ⟶ F₂) → CategoryTheory.Limits.IsLimit (CategoryTheory.Subfunctor.equalizer.fork f g)
-- Mathlib.RingTheory.Idempotents
/-- If `e` and `f` are idempotent elements such that `e + f = 1` and `e * f = 0`,
`S` is isomorphic as an `R`-algebra to `S ⧸ (e) × S ⧸ (f)`.  -/
AlgEquiv.prodQuotientOfIsIdempotentElem : (R : Type u_1) →
  [inst : CommRing R] →
    {S : Type u_4} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {e f : S} →
            IsIdempotentElem e →
              IsIdempotentElem f → e + f = 1 → e * f = 0 → S ≃ₐ[R] (S ⧸ Ideal.span {e}) × S ⧸ Ideal.span {f}
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
MeasureTheory.measure_unitBall_eq_integral_div_gamma : ∀ {E : Type u_1} {p : ℝ} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  0 < p →
    μ (Metric.ball 0 1) =
      ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(Module.finrank ℝ E) / p + 1))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β} {he : Std.ExtDTreeMap.Const.alter t k f ≠ ∅},
  (Std.ExtDTreeMap.Const.alter t k f).maxKey he = k ↔
    (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `NoNatZeroDivisors` instance for `type` if available.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.noZeroDivInst? : Lean.Meta.Grind.Arith.CommRing.CommRing → Option Lean.Expr
-- Mathlib.Data.Set.Prod
Set.prod_eq_iff_eq : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β}, t.Nonempty → (s ×ˢ t = s₁ ×ˢ t ↔ s = s₁)
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.S'_compactSpace : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} [inst : TopologicalSpace S] [T2Space S] [inst_2 : TopologicalSpace T]
  [CompactSpace T] [inst_4 : TopologicalSpace X] [T1Space (OnePoint X)] (π : T → S × OnePoint X),
  Continuous π → CompactSpace ↑(InternalProjectivityProof.S'✝ π)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insert_inductive_case : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n)
  (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))),
  (∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]) →
    ∀ (idx : Fin units.size) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
      f.ClearInsertInductionMotive f_assignments_size units (↑idx) assignments →
        f.ClearInsertInductionMotive f_assignments_size units (↑idx + 1)
          (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments units[idx])
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- `symm` is `true` when rewriting from right to left  -/
Mathlib.Tactic.ClickSuggestions.RwLemma.symm : Mathlib.Tactic.ClickSuggestions.RwLemma → Bool
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a normal subgroup `S ≤ G`, this sends `A : Rep k G` to the `n`th "coinflation" map
`Hₙ(G, A) ⟶ Hₙ(G ⧸ S, A_S)` induced by the quotient maps `G →* G ⧸ S` and `A →ₗ A_S`.  -/
groupHomology.coinfNatTrans : (k : Type u) →
  {G : Type u} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) →
          [inst_2 : S.Normal] →
            (n : ℕ) →
              groupHomology.functor k G n ⟶
                (Rep.quotientToCoinvariantsFunctor k S).comp (groupHomology.functor k (G ⧸ S) n)
-- Lean.Environment
Lean.Kernel.Exception.declHasMVars.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name) (expr : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.declHasMVars env name expr) = 1 + sizeOf env + sizeOf name + sizeOf expr
-- Mathlib.Data.PNat.Defs
PNat.mk_coe : ∀ (n : ℕ) (h : 0 < n), ↑⟨n, h⟩ = n
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instMonoid : {R : Type u_1} →
  [inst : Monoid R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → Monoid (OreLocalization S R)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasSumLocallyUniformly_iff_tendstoLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasSumLocallyUniformly f g ↔ TendstoLocallyUniformly (fun x1 x2 => ∑ i ∈ x1, f i x2) g Filter.atTop
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.truncLT_mem_range_sSupFun : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {c : Set (HahnEmbedding.Partial seed)},
  c.Nonempty →
    ∀ (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c) (x : ↥(HahnEmbedding.Partial.sSupFun hc).domain)
      (c_1 : FiniteArchimedeanClass M),
      toLex ((HahnSeries.truncLTLinearMap K c_1) (ofLex (↑(HahnEmbedding.Partial.sSupFun hc) x))) ∈
        (HahnEmbedding.Partial.sSupFun hc).toFun.range
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  5 ≤ Nat.card α → ∀ {g : ↥(alternatingGroup α)}, (↑g).IsThreeCycle → g ∈ commutatorSet ↥(alternatingGroup α)
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all `n : ℕ`,
`|X| ^ n * exp (v * X)` is integrable.  -/
ProbabilityTheory.integrable_pow_abs_mul_exp_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp ((v + t) * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp ((v - t) * X ω)) μ →
        ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => |X ω| ^ n * Real.exp (v * X ω)) μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.TypeDefinitionParams : Type
-- Mathlib.Data.WSeq.Defs
/-- Get the weak sequence of initial segments of the input sequence  -/
Stream'.WSeq.inits : {α : Type u} → Stream'.WSeq α → Stream'.WSeq (List α)
-- Mathlib.Data.Finset.Defs
Finset.eq_of_veq : ∀ {α : Type u_1} {s t : Finset α}, s.val = t.val → s = t
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.add_mem' : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (self : ConvexCone R M) ⦃x : M⦄,
  x ∈ self.carrier → ∀ ⦃y : M⦄, y ∈ self.carrier → x + y ∈ self.carrier
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The second projection of the pullback of `f` and `g`.  -/
CategoryTheory.Limits.pullback.snd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) → [inst_1 : CategoryTheory.Limits.HasPullback f g] → CategoryTheory.Limits.pullback f g ⟶ Y
-- Init.Data.UInt.Lemmas
USize.neg_zero : -0 = 0
-- Mathlib.Data.Finset.Image
Finset.image_toFinset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} [inst_1 : DecidableEq α] {s : Multiset α},
  Finset.image f s.toFinset = (Multiset.map f s).toFinset
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instReprFanin.repr : Std.Sat.AIG.Fanin → ℕ → Std.Format
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.inner_toL2_toL2_eq : ∀ {H : Type u_8} {V : Type u_9} [inst : NormedAddCommGroup H] [inst_1 : NormedSpace ℝ H]
  [inst_2 : FiniteDimensional ℝ H] [inst_3 : MeasurableSpace H] [inst_4 : BorelSpace H] [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℂ V] (f g : SchwartzMap H V)
  (μ : autoParam (MeasureTheory.Measure H) SchwartzMap.inner_toL2_toL2_eq._auto_1) [inst_7 : μ.HasTemperateGrowth],
  inner ℂ (f.toLp 2 μ) (g.toLp 2 μ) = ∫ (x : H), inner ℂ (f x) (g x) ∂μ
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.trivial_X_mon_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The proposition that elements of `target` are mapped to elements of `source`.  -/
PartialEquiv.map_target' : ∀ {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : β⦄, x ∈ self.target → self.invFun x ∈ self.source
-- Mathlib.GroupTheory.Sylow
Sylow.iSup_of_normal : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {ι : Type u_2} (H : ι → Subgroup G) [∀ (i : ι), (H i).Normal],
  (∀ (i : ι), IsPGroup p ↥(H i)) → IsPGroup p ↥(⨆ i, H i)
-- Mathlib.Order.Cover
/-- **Alias** of the forward direction of `covBy_iff_le_iff_lt_right`. -/
CovBy.le_iff_lt_right : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, y ⋖ x → ∀ {z : α}, x ≤ z ↔ y < z
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Contraction.0.CliffordAlgebra.«term_⌊__1» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- The cocone over the proposed colimit module.  -/
ModuleCat.FilteredColimits.colimitCocone : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J (ModuleCat R)) → CategoryTheory.Limits.Cocone F
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
tendsto_smoothingFun_comp : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 →
    ∀ (x : R) {ψ : ℕ → ℕ},
      StrictMono ψ → Filter.Tendsto (fun n => μ (x ^ ψ n) ^ (1 / ↑(ψ n))) Filter.atTop (nhds (smoothingFun μ x))
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.fst : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F], IsBoundedLinearMap 𝕜 fun x => x.1
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.pow_p_dvd_int_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (a : ℤ), ↑p ^ n ∣ ↑a ↔ ↑p ^ n ∣ a
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_lt_self : ∀ {a b : ENNReal}, a ≠ ⊤ → a ≠ 0 → b ≠ 0 → a - b < a
-- Init.Data.Nat.Lemmas
Nat.add_sub_cancel' : ∀ {n m : ℕ}, m ≤ n → m + (n - m) = n
-- Mathlib.Order.PiLex
Pi.ofLex_apply : ∀ {ι : Type u_1} {β : ι → Type u_2} (x : Lex ((i : ι) → β i)) (i : ι), ofLex x i = x i
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_comap : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N] (f : M →ₗ[R] N) (C : ConvexCone R N),
  ↑(ConvexCone.comap f C) = ⇑f ⁻¹' ↑C
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holder_smul_right : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (c : 𝕜)
  (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ContinuousLinearMap.holder r B f (c • g) = c • ContinuousLinearMap.holder r B f g
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.comul_counit_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.ComonObj M] {Z : C} (f : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.ComonObj.counit) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).inv
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.darts_drop : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.drop n).darts = List.drop n p.darts