mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- If the derivatives within a set of `g` at `f x` are bounded by `C`, and the `i`-th derivative
within a set of `f` at `x` is bounded by `D^i` for all `1 ≤ i ≤ n`, then the `n`-th derivative
of `g ∘ f` is bounded by `n! * C * D^n`.  -/
norm_iteratedFDerivWithin_comp_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {n : ℕ} {s : Set E} {t : Set F}
  {x : E} {N : WithTop ℕ∞},
  ContDiffOn 𝕜 N g t →
    ContDiffOn 𝕜 N f s →
      ↑n ≤ N →
        UniqueDiffOn 𝕜 t →
          UniqueDiffOn 𝕜 s →
            Set.MapsTo f s t →
              x ∈ s →
                ∀ {C D : ℝ},
                  (∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
                    (∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
                      ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n.factorial * C * D ^ n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.comp_pow_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) {Z : C} (h_1 : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp (f ^ n) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f ^ n) h_1
-- Mathlib.GroupTheory.Transfer
/-- **Alias** of `MonoidHom.transferSylow_domRestrict_eq_pow`. -/
MonoidHom.transferSylow_restrict_eq_pow : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P)
  [Fact (Nat.Prime p)] [Finite (Sylow p G)] [inst_3 : (↑P).FiniteIndex],
  ⇑((MonoidHom.transferSylow P hP).domRestrict ↑P) = fun x => x ^ (↑P).index
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- If `f : ℂ → E` is continuous on a closed ball of positive radius and is differentiable at all
but countably many points of the corresponding open ball, then it is analytic on the open ball with
coefficients of the power series given by Cauchy integral formulas.  -/
Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : NNReal} {c : ℂ}
  {f : ℂ → E} {s : Set ℂ},
  s.Countable →
    ContinuousOn f (Metric.closedBall c ↑R) →
      (∀ z ∈ Metric.ball c ↑R \ s, DifferentiableAt ℂ f z) →
        0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.instReflectiveCpltSepUniformSpaceForget₂SubtypeForallαUniformContinuousForallCarrier : CategoryTheory.Reflective (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat)
-- Mathlib.Topology.ShrinkingLemma
/-- In a locally compact Hausdorff space `X`, if `s` is a compact set, `v` is a partial refinement,
and `i` is an index such that `i ∉ v.carrier`, then there exists a partial refinement that is
strictly greater than `v`.  -/
exists_gt_t2space : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [T2Space X]
  [LocallyCompactSpace X] (v : ShrinkingLemma.PartialRefinement u s fun w => IsCompact (closure w)),
  IsCompact s → ∀ i ∉ v.carrier, ∃ v', v < v' ∧ IsCompact (closure (v'.toFun i))
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.toFunLinear.eq_1 : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  MatrixEquivTensor.toFunLinear n R A = TensorProduct.lift (MatrixEquivTensor.toFunBilinear n R A)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequence_iso : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequence_iso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequence_iso._auto_3),
  (X.spectralSequence data).iso r r' pq' ⋯ ⋯ =
    ((X.spectralSequence data).page r ⋯).homologyIsoSc' pq pq' pq'' hpq hpq' ≪≫
      (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃
              hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).left.homologyIso ≪≫
        (X.spectralSequencePageXIso data r' ⋯ pq' i₀' i₁ i₂ i₃' hi₀' hi₁ hi₂ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).symm
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.ab_exact_iff_function_exact : ∀ (S : CategoryTheory.ShortComplex Ab),
  S.Exact ↔ Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodMulEquivOfGenerator_symm_apply_zpow : ∀ {G : Type u_2} [inst : Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n)
  (i : ℤ), (zmodMulEquivOfGenerator hg hn).symm (g ^ i) = Multiplicative.ofAdd ↑i
-- Mathlib.Analysis.CStarAlgebra.Spectrum
StarAlgEquivClass.toStarAlgEquiv.congr_simp : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Mul A] [inst_2 : SMul R A]
  [inst_3 : Star A] [inst_4 : Add B] [inst_5 : Mul B] [inst_6 : SMul R B] [inst_7 : Star B] [inst_8 : EquivLike F A B]
  [inst_9 : NonUnitalAlgEquivClass F R A B] [inst_10 : StarHomClass F A B] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Init.Data.Array.Set
/-- Set an element in an array, or panic if the index is out of bounds.

This will perform the update destructively provided that `a` has a reference
count of 1 when called.
 -/
Array.set! : {α : Type u_1} → Array α → ℕ → α → Array α
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Let `f : X ⟶ Y` be a relatively representable morphism in `D`. Then, for any
`g : F.obj a ⟶ Y`, `hf.pullback g` denotes the (choice of) a corresponding object in `C` such that
there is a pullback square of the following form
```
hf.pullback g --F.map snd--> F.obj a
    |                          |
   fst                         g
    |                          |
    v                          v
    X ---------- f ----------> Y
```  -/
CategoryTheory.Functor.relativelyRepresentable.pullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {X Y : D} → {f : X ⟶ Y} → F.relativelyRepresentable f → {a : C} → (F.obj a ⟶ Y) → C
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- The lift (in `C`) obtained from the universal property of `F.obj (hf.pullback g)`, in the
case when the cone point is in the image of `F.obj`.  -/
CategoryTheory.Functor.relativelyRepresentable.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {X Y : D} →
            {f : X ⟶ Y} →
              (hf : F.relativelyRepresentable f) →
                {a : C} →
                  {g : F.obj a ⟶ Y} →
                    {c : C} →
                      (i : F.obj c ⟶ X) →
                        (h : c ⟶ a) →
                          CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g →
                            [F.Full] → c ⟶ hf.pullback g
-- Lean.Syntax
/-- Adds the given trailing substring to a `Syntax`' existing trailing substring if they are adjacent.
 -/
Lean.Syntax.addTrailing : Lean.Syntax → Substring.Raw → Lean.Syntax
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instIsLeftCancelVAddSubtypeMem : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  [IsLeftCancelVAdd R M], IsLeftCancelVAdd R ↥s
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqLhs.sizeOf_spec : ∀ (gen : Bool), sizeOf (Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen) = 1 + sizeOf gen
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.isoMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g g_1 : f.right ≅ f'.right)
  (e_g : g = g_1) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom),
  CategoryTheory.StructuredArrow.isoMk g w = CategoryTheory.StructuredArrow.isoMk g_1 ⋯
-- Mathlib.Data.Fin.Tuple.Basic
Fin.repeat_rev : ∀ {m n : ℕ} {α : Sort u_1} (a : Fin n → α) (k : Fin (m * n)), Fin.repeat m a k.rev = Fin.repeat m (a ∘ Fin.rev) k
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_hom_rightUnitor : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X : Rep.{u, u, v} k G},
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = ↑(Representation.TensorProduct.rid k X.ρ)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.denote : Nat.Internal.Linear.Context → Nat.Internal.Linear.PolyCnstr → Prop
-- Mathlib.Order.Antichain
Set.Subsingleton.isAntichain : ∀ {α : Type u_1} {s : Set α}, s.Subsingleton → ∀ (r : α → α → Prop), IsAntichain r s
-- Mathlib.Analysis.Calculus.ParametricIntegral
/-- Differentiation under integral of `x ↦ ∫ F x a` at a given point `x₀`, assuming `F x₀` is
integrable, `‖F x a - F x₀ a‖ ≤ bound a * ‖x - x₀‖` for `x` in a neighborhood of `x₀` for ae `a`
integrable Lipschitz bound `bound` (with a neighborhood independent of `a`), and `F x` is
ae-measurable for `x` in the same ball. See `hasFDerivAt_integral_of_dominated_loc_of_lip` for a
slightly less general but usually more useful version.  -/
hasFDerivAt_integral_of_dominated_loc_of_lip' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E] {H : Type u_4}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {s : Set H}
  {F' : α → H →L[𝕜] E},
  s ∈ nhds x₀ →
    (∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (F x) μ) →
      MeasureTheory.Integrable (F x₀) μ →
        MeasureTheory.AEStronglyMeasurable F' μ →
          (∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F x a - F x₀ a‖ ≤ bound a * ‖x - x₀‖) →
            MeasureTheory.Integrable bound μ →
              (∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) →
                MeasureTheory.Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
-- Mathlib.GroupTheory.Congruence.Defs
/-- Definition of the function on the quotient by a congruence relation `c` induced by a function
that is constant on `c`'s equivalence classes.  -/
Con.liftOn_coe : ∀ {M : Type u_1} [inst : Mul M] {β : Sort u_4} (c : Con M) (f : M → β) (h : ∀ (a b : M), c a b → f a = f b) (x : M),
  Con.liftOn (↑x) f h = f x
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a right absorbing element for multiplication  -/
MulZeroOneClass.mul_zero : ∀ {M₀ : Type u} [self : MulZeroOneClass M₀] (a : M₀), a * 0 = 0
-- Std.Do.WP.SimpLemmas
Std.Do.WP.withReader_MonadWithReaderOf : ∀ {m : Type u → Type v} {ρ : Type u} {n : Type u → Type v} {nsh : Std.Do.PostShape} {α : Type u}
  {Q : Std.Do.PostCond α nsh} [inst : MonadWithReaderOf ρ m] [inst_1 : Std.Do.WP n nsh] [inst_2 : MonadFunctor m n]
  (f : ρ → ρ) (x : n α),
  (Std.Do.wp (MonadWithReaderOf.withReader f x)).apply Q =
    (Std.Do.wp (MonadFunctor.monadMap (fun {β} => MonadWithReaderOf.withReader f) x)).apply Q
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.apply_skipWhile_bool_eq_false : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} {h : pos.skipWhile p ≠ s.endPos},
  p ((pos.skipWhile p).get h) = false
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator.mk : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Zipper α β → α → Std.DTreeMap.Internal.RxcIterator α β
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.presheaf_mono_of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.MorphismProperty C}
  {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
  P ≤ CategoryTheory.MorphismProperty.monomorphisms C →
    ∀ {X : C} {f : CategoryTheory.yoneda.obj X ⟶ G}, P.presheaf f → CategoryTheory.Mono f
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.d_d : ∀ {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₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d_d._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d_d._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d_d._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.d_d._auto_7),
  CategoryTheory.CategoryStruct.comp (X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
      (X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄) =
    0
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.instIsTopologicalSemiringSubtypeMem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A] [IsTopologicalSemiring A]
  (s : StarSubalgebra R A), IsTopologicalSemiring ↥s
-- Mathlib.GroupTheory.Complement
AddSubgroup.instInhabitedRightTransversal.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  AddSubgroup.instInhabitedRightTransversal = { default := ⟨Set.range Quotient.out, ⋯⟩ }
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- A group `G` acts properly on a topological space `X` if and only if for all ultrafilters
`𝒰` on `X × G`, if `𝒰` converges to `(x₁, x₂)` along the map `(g, x) ↦ (g • x, x)`,
then there exists `g : G` such that `g • x₂ = x₁` and `𝒰.fst` converges to `g`.  -/
properSMul_iff_continuousSMul_ultrafilter_tendsto : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X],
  ProperSMul G X ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) →
          ∃ g, g • x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)
-- Init.Grind.Norm
Nat.lt.eq_1 : ∀ (n m : ℕ), n.lt m = n.succ.le m
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm : Lean.Meta.Grind.Arith.Linear.IneqCnstr → ℕ → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
LinearMap.isometryOfOrthonormal_toLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E')
  {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)),
  (f.isometryOfOrthonormal hv hf).toLinearMap = f
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- The Euler product for the Riemann ζ function, valid for `s.re > 1`.
This version is stated in terms of `HasProd`.  -/
riemannZeta_eulerProduct_hasProd : ∀ {s : ℂ}, 1 < s.re → HasProd (fun p => (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- An ideal is principal if a power coprime to the class number is principal.  -/
Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDedekindDomain R] [inst_3 : Fintype (ClassGroup R)]
  {n : ℕ},
  n.Coprime (Fintype.card (ClassGroup R)) → ∀ {I : Ideal R}, Submodule.IsPrincipal (I ^ n) → Submodule.IsPrincipal I
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_one' : ∀ {E : Type u_5} [inst : SeminormedGroup E], ‖1‖₊ = 0
-- Mathlib.RingTheory.Congruence.Hom
/-- The algebra homomorphism on the quotient of an algebra by a
congruence relation `c` induced by an algebra homomorphism
constant on the equivalence classes of `c`.  -/
RingCon.liftₐ : {M : Type u_1} →
  {P : Type u_3} →
    {R : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring M] →
          [inst_2 : Algebra R M] →
            [inst_3 : Semiring P] →
              [inst_4 : Algebra R P] →
                (c : RingCon M) → (f : M →ₐ[R] P) → c ≤ RingCon.ker f.toRingHom → c.Quotient →ₐ[R] P
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ` and `f''` is strictly negative on `D`,
then `f` is strictly concave on `D`.
Note that we don't require twice differentiability explicitly as it is already implied by the second
derivative being strictly negative, except at at most one point.  -/
strictConcaveOn_of_deriv2_neg' : ∀ {D : Set ℝ}, Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ D, deriv^[2] f x < 0) → StrictConcaveOn ℝ D f
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.neg_congr : ∀ {R : Type u_2} [inst : CommRing R] {a a' b : R}, a = a' → -a' = b → -a = b
-- Mathlib.Topology.Order.NhdsSet
Ioc_mem_nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a ≤ b → c < d → Set.Ioc a d ∈ nhdsSet (Set.Ioc b c)
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
/-- Predicate for when the gaussNorm is achieved by an index.  -/
MvPowerSeries.AchievesGaussNorm : {R : Type u_1} → {σ : Type u_2} → (R → ℝ) → (σ → ℝ) → MvPowerSeries σ R → [Ring R] → (σ →₀ ℕ) → Prop
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.isClosable_iff_exists_closed_extension : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F}, f.IsClosable ↔ ∃ g, g.IsClosed ∧ f ≤ g
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- **Alias** of `MulChar.domRestrict_ofUnitHom`. -/
MulChar.restrict_ofUnitHom : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_3} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ)
  (S : Submonoid R),
  MulChar.domRestrict S (MulChar.ofUnitHom f) =
    MulChar.ofUnitHom ((f.domRestrict S.units).comp ↑S.unitsEquivUnitsType.symm)
-- Aesop.Rule
Aesop.SafeRuleInfo.mk : ℤ → Aesop.Safety → Aesop.SafeRuleInfo
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformlyOn_of_seq_tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {l : Filter ι} [l.IsCountablyGenerated],
  (∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun n => F (u n)) f Filter.atTop s) →
    TendstoUniformlyOn F f l s
-- Mathlib.Data.List.Intervals
List.Ico.pred_singleton : ∀ {m : ℕ}, 0 < m → List.Ico (m - 1) m = [m - 1]
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_strongAssignmentsInvariant : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : ℕ),
  f.StrongAssignmentsInvariant → (f.deleteOne id).StrongAssignmentsInvariant
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffOn_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {n : WithTop ℕ∞}, ContMDiffOn I I n id s
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.zpow₀ : ∀ {R : Type u_1} [inst : GroupWithZero R] [inst_1 : StarMul R] {x : R},
  IsSelfAdjoint x → ∀ (n : ℤ), IsSelfAdjoint (x ^ n)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
isClosedEmbedding_cfcₙAux : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁],
  Topology.IsClosedEmbedding ⇑(cfcₙAux ⋯ a ha)
-- Mathlib.Algebra.Free
FreeAddSemigroup.traverse_pure : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : α), traverse F (pure x) = pure <$> F x
-- Mathlib.Analysis.MellinTransform
/-- If `f` is locally integrable, decays exponentially at infinity, and is `O(x ^ (-b))` at 0, then
its Mellin transform is holomorphic on `b < s.re`.  -/
mellin_differentiableAt_of_isBigO_rpow_exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ},
  0 < a →
    ∀ {f : ℝ → E} {s : ℂ},
      MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
        (f =O[Filter.atTop] fun t => Real.exp (-a * t)) →
          (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → b < s.re → DifferentiableAt ℂ (mellin f) s
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity.coe_injective : ∀ {M : Type u_1} [inst : CommMonoid M] {n : ℕ}, Function.Injective fun x => ↑↑x
-- Mathlib.Data.EReal.Inv
EReal.sign_mul : ∀ (x y : EReal), SignType.sign (x * y) = SignType.sign x * SignType.sign y
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.not_limZero_const_of_nonzero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {q : ℚ}, q ≠ 0 → ¬(CauSeq.const (padicNorm p) q).LimZero
-- Mathlib.Data.Fintype.Powerset
Set.instFinite : ∀ {α : Type u_1} [Finite α], Finite (Set α)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.injective : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → Function.Injective ⇑f
-- Mathlib.Data.Set.Image
Set.preimage_subset_image_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse g f → ∀ (s : Set β), f ⁻¹' s ⊆ g '' s
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R],
  CanLift (Set R) (NonUnitalStarSubsemiring R) SetLike.coe fun s =>
    0 ∈ s ∧
      (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧
        (∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : R}, x ∈ s → star x ∈ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List ((a : α) × β a)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.ExtDTreeMap.ofList l cmp).getKey? k' = some k