mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.MeanInequalities
Real.Lr_le_Lp_mul_Lq_tsum_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p q r : ℝ},
  p.HolderTriple q r →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) →
          (Summable fun i => g i ^ q) →
            (∑' (i : ι), (f i * g i) ^ r) ^ (1 / r) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
-- Lean.Data.Lsp.Extra
/-- `$/lean/rpc/connect` client->server request.

Starts an RPC session at the given file's worker, replying with the new session ID.
Multiple sessions may be started and operating concurrently.

A session may be destroyed by the server at any time (e.g. due to a crash), in which case further
RPC requests for that session will reply with `RpcNeedsReconnect` errors. The client should discard
references held from that session and `connect` again.  -/
Lean.Lsp.RpcConnectParams : Type
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.iff_exists : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (I : Ideal A), Ideal.IsHomogeneous 𝒜 I ↔ ∃ S, I = Ideal.span (Subtype.val '' S)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_mul_rpow_one_add_sq : ∀ {a b t : ℝ},
  t ≠ -1 →
    ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t =
      (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))
-- Mathlib.Algebra.Order.SuccPred
Order.lt_one_iff_nonpos : ∀ {α : Type u_1} {x : α} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero 1]
  [SuccAddOrder α], x < 1 ↔ x ≤ 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.tactic.injEq : ∀ (tacticCode : Lean.Syntax) (ctx : Lean.Elab.Term.SavedContext) (kind : Lean.Elab.Term.TacticMVarKind)
  (delayOnMVars : Bool) (tacticCode_1 : Lean.Syntax) (ctx_1 : Lean.Elab.Term.SavedContext)
  (kind_1 : Lean.Elab.Term.TacticMVarKind) (delayOnMVars_1 : Bool),
  (Lean.Elab.Term.SyntheticMVarKind.tactic tacticCode ctx kind delayOnMVars =
      Lean.Elab.Term.SyntheticMVarKind.tactic tacticCode_1 ctx_1 kind_1 delayOnMVars_1) =
    (tacticCode = tacticCode_1 ∧ ctx = ctx_1 ∧ kind = kind_1 ∧ delayOnMVars = delayOnMVars_1)
-- Init.Data.Array.Count
Array.countP_flatten : ∀ {α : Type u_1} {p : α → Bool} {xss : Array (Array α)},
  Array.countP p xss.flatten = (Array.map (Array.countP p) xss).sum
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.mk' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {r : ENNReal},
  (∀ (m : ℕ), n ≤ m → p m = 0) →
    0 < r →
      (∀ y ∈ Metric.eball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)) →
        HasFiniteFPowerSeriesOnBall f p x n r
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.infinite : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} [M.RankInfinite], M.IsBase B → B.Infinite
-- Mathlib.Data.Nat.MaxPowDiv
Nat.padicValNat_le_self : ∀ {p : ℕ} (n : ℕ), padicValNat p n ≤ n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRciSlice : {α : Type u} →
  [inst : Ord α] →
    Std.Rci.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RciSlice α)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalSubsemiring_inj : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {s t : NonUnitalSubalgebra R A}, s.toNonUnitalSubsemiring = t.toNonUnitalSubsemiring ↔ s = t
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_smul_le_range : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (c : R₂), (c • f).range ≤ f.range
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Function.Embedding.codRestrict.congr_simp : ∀ {α : Sort u_1} {β : Type u_2} (p : Set β) (f f_1 : α ↪ β) (e_f : f = f_1) (H : ∀ (a : α), f a ∈ p),
  Function.Embedding.codRestrict p f H = Function.Embedding.codRestrict p f_1 ⋯
-- Init.Data.SInt.IntToBitVec
Bool.toBitVec32_toISize : ∀ {b : Bool} (h : System.Platform.numBits = 32), b.toISize.toBitVec32 h = BitVec.setWidth 32 (BitVec.ofBool b)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFDerivAt.continuousMultilinearMap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] {G : Type u_4} [inst_6 : NormedAddCommGroup G]
  [inst_7 : NormedSpace 𝕜 G] [inst_8 : DecidableEq ι] {x : G} {f : G → ContinuousMultilinearMap 𝕜 E F}
  {g : (i : ι) → G → E i} {f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F} {g' : (i : ι) → G →L[𝕜] E i},
  HasFDerivAt f f' x →
    (∀ (i : ι), HasFDerivAt (g i) (g' i) x) →
      HasFDerivAt (fun x => (f x) fun x_1 => g x_1 x)
        ((ContinuousMultilinearMap.apply 𝕜 E F fun x_1 => g x_1 x) ∘SL f' +
          ∑ i, (f x).toContinuousLinearMap (fun x_1 => g x_1 x) i ∘SL g' i)
        x
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.isCoverDense : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D)
  [CategoryTheory.Functor.IsDenseSubsite J K G], G.IsCoverDense K
-- Mathlib.Analysis.Normed.MulAction
nndist_smul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β]
  [NormSMulClass α β] (s : α) (x y : β), nndist (s • x) (s • y) = ‖s‖₊ * nndist x y
-- Mathlib.Data.ENat.Basic
ENat.lt_two_iff : ∀ {n : ℕ∞}, n < 2 ↔ n ≤ 1
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Exactness of `J`-shaped limits stated as `lim : (J ⥤ C) ⥤ C` preserving finite colimits.  -/
CategoryTheory.HasExactLimitsOfShape.preservesFiniteColimits : ∀ {J : Type u'} {inst : CategoryTheory.Category.{v', u'} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C} [self : CategoryTheory.HasExactLimitsOfShape J C],
  CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.divRight.eq_1 : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulRightMono α] (a : α),
  OrderIso.divRight a = { toEquiv := Equiv.divRight a, map_rel_iff' := ⋯ }
-- Mathlib.Combinatorics.Quiver.Symmetric
_private.Mathlib.Combinatorics.Quiver.Symmetric.0.Quiver.Symmetrify.lift.match_1.eq_1 : ∀ {V : Type u_2} [inst : Quiver V] {X Y : Quiver.Symmetrify V} (motive : (X ⟶ Y) → Sort u_3) (g : X ⟶ Y)
  (h_1 : (g : X ⟶ Y) → motive (Sum.inl g)) (h_2 : (g : Y ⟶ X) → motive (Sum.inr g)),
  (match Sum.inl g with
    | Sum.inl g => h_1 g
    | Sum.inr g => h_2 g) =
    h_1 g
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.is_descending_rev_series_of_is_ascending`. -/
is_descending_rev_series_of_is_ascending : ∀ (G : Type u_1) [inst : Group G] {H : ℕ → Subgroup G} {n : ℕ},
  H n = ⊤ → Subgroup.IsAscendingCentralSeries H → Subgroup.IsDescendingCentralSeries fun m => H (n - m)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.comp_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {R S T : CategoryTheory.Grp C} (f : R ⟶ S) (g : S ⟶ T),
  (CategoryTheory.CategoryStruct.comp f g).hom.hom = CategoryTheory.CategoryStruct.comp f.hom.hom g.hom.hom
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Suppose `a : X → Set A` is continuous and `a x` satisfies the predicate `p` for all `x`.
Suppose further that `s : X → Set 𝕜` is a family of compact sets `s x₀` contains the spectrum of
`a x` for all sufficiently close `x`. If `f : 𝕜 → 𝕜` is continuous on each `s x`, then
`fun x ↦ cfc f (a x)` is continuous.  -/
Continuous.cfc : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [inst_6 : TopologicalSpace X] {s : X → Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A},
  Continuous a →
    (∀ (x : X), IsCompact (s x)) →
      (∀ (x₀ : X), ∀ᶠ (x : X) in nhds x₀, spectrum 𝕜 (a x) ⊆ s x₀) →
        autoParam (∀ (x : X), ContinuousOn f (s x)) Continuous.cfc._auto_1 →
          autoParam (∀ (x : X), p (a x)) Continuous.cfc._auto_3 → Continuous fun x => cfc f (a x)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inl_comp_tensorHom_assoc : ∀ {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) {Z : AugmentedSimplexCategory}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj y₁ y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (x₁.inl x₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) h) =
    CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.CategoryStruct.comp (y₁.inl y₂) h)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.anyM.eq_def : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool) (x : List α),
  List.anyM p x =
    match x with
    | [] => pure false
    | a :: as => do
      let __do_lift ← p a
      match __do_lift with
        | true => pure true
        | false => List.anyM p as
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Bridge between the auto-derived graded-monoid power `GradedMonoid.GMonoid.gnpow` and the
bespoke `ModularForm.pow`: as elements of `GradedMonoid (ModularForm Γ)`, the pair
`⟨n • k, gnpow n f⟩` agrees with `⟨n * k, f.pow n⟩`.  -/
ModularForm.gnpow_eq_pow : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k : ℤ} (f : ModularForm Γ k) (n : ℕ),
  ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
Homeomorph.transOpenPartialHomeomorph_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z),
  ↑(e.transOpenPartialHomeomorph f').symm = ⇑e.symm ∘ ↑f'.symm
-- Mathlib.NumberTheory.HeckeRing.Defs
HeckeCosetModule.instAddCommGroup : {G : Type u_1} →
  [inst : Group G] →
    (Δ : Submonoid G) →
      (H₁ H₂ : Subgroup G) → (Z : Type u_2) → [inst_1 : AddCommGroup Z] → AddCommGroup (HeckeCosetModule Δ H₁ H₂ Z)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.min_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (fun a => min (f a) 0) μ
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.inductiveStepRealization.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] (n : ℕ)
  (X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C))
  (a a_1 : CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝ n X),
  a = a_1 →
    CategoryTheory.IsFiltered.FilteredClosureSmall.inductiveStepRealization✝ n X a =
      CategoryTheory.IsFiltered.FilteredClosureSmall.inductiveStepRealization✝ n X a_1
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.insertPerm.match_1.eq_4 : ∀ (motive : (x : ℕ) → Fin2 x → Fin2 x → Sort u_1) (a : ℕ) (i : Fin2 a.succ) (j : Fin2 (a + 1))
  (h_1 : (n : ℕ) → motive (n + 1) Fin2.fz Fin2.fz) (h_2 : (n : ℕ) → (j : Fin2 n) → motive (n + 1) Fin2.fz j.fs)
  (h_3 : (a : ℕ) → (a_1 : Fin2 a.succ) → motive (a.succ + 1) a_1.fs Fin2.fz)
  (h_4 : (a : ℕ) → (i : Fin2 a.succ) → (j : Fin2 (a + 1)) → motive (a.succ + 1) i.fs j.fs),
  (match a.succ + 1, i.fs, j.fs with
    | .(n + 1), Fin2.fz, Fin2.fz => h_1 n
    | .(n + 1), Fin2.fz, j.fs => h_2 n j
    | .(a.succ + 1), a_1.fs, Fin2.fz => h_3 a a_1
    | .(a.succ + 1), i.fs, j.fs => h_4 a i j) =
    h_4 a i j
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.isDenseEmbedding_coe : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α], IsDenseEmbedding UniformSpace.Completion.coe'
-- Mathlib.Data.Rel
SetRel.mem_cod : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {b : β}, b ∈ R.cod ↔ ∃ a, (a, b) ∈ R
-- Mathlib.Analysis.Convex.Topology
Convex.nontrivial_iff_nonempty_interior : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜}, Convex 𝕜 s → (s.Nontrivial ↔ (interior s).Nonempty)
-- Init.Data.SInt.Lemmas
ISize.toBitVec_ofInt : ∀ (i : ℤ), (ISize.ofInt i).toBitVec = BitVec.ofInt System.Platform.numBits i
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.ext_iff : ∀ {μ : YoungDiagram} {T T' : SemistandardYoungTableau μ}, T = T' ↔ ∀ (i j : ℕ), T i j = T' i j
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_le_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {n : ℕ∞},
  G.vertexCoverNum ≤ n ↔ ∀ (m : ℕ∞), (∀ (s : Set V), G.IsVertexCover s → m ≤ s.encard) → m ≤ n
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrableOn_rpow_mul_exp_neg_rpow : ∀ {p s : ℝ},
  -1 < s → 0 < p → MeasureTheory.IntegrableOn (fun x => x ^ s * Real.exp (-x ^ p)) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Order.Interval.Finset.Fin
Fin.Ici_add_one_eq_Ioi : ∀ {n : ℕ} {a : Fin n}, ↑a + 1 < n → Finset.Ici (a + 1) = Finset.Ioi a
-- Mathlib.Order.Sublattice
Sublattice.LatticeHom.range_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {f : LatticeHom α β},
  ↑(Sublattice.LatticeHom.range f) = Set.range ⇑f
-- Aesop.Util.Tactic.Ext
Aesop.ExtResult.mk.sizeOf_spec : ∀ (depth : ℕ) (commonFVarIds : Array Lean.FVarId) (goals : Array (Lean.MVarId × Array Lean.FVarId)),
  sizeOf { depth := depth, commonFVarIds := commonFVarIds, goals := goals } =
    1 + sizeOf depth + sizeOf commonFVarIds + sizeOf goals
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Any change of coordinates with empty source belongs to `continuousGroupoid`.  -/
ContinuousGroupoid.mem_of_source_eq_empty : ∀ {𝕜 : 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}
  (f : OpenPartialHomeomorph H H), f.source = ∅ → f ∈ continuousGroupoid H
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.mconv_absolutelyContinuous : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] {μ ν ρ : MeasureTheory.Measure M}
  [ρ.IsMulLeftInvariant] [MeasureTheory.SFinite ν], ν.AbsolutelyContinuous ρ → (μ.mconv ν).AbsolutelyContinuous ρ
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- An `apply at` suggestion section.  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.appAt : Array Mathlib.Tactic.ClickSuggestions.ApplyAtLemma → Mathlib.Tactic.ClickSuggestions.Candidates✝
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Matrix.det_eq_prod_roots_charpoly : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {K : Type u_3} [inst_2 : Field K] (A : Matrix n n K)
  [IsAlgClosed K], A.det = A.charpoly.roots.prod
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.codExtend_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s}
  (e : Bundle.Trivialization F proj),
  (Bundle.Trivialization.codExtend hs nonempty e).source = e.toPretrivialization.source
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.subsingleton_cotangentSpace_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  Subsingleton (IsLocalRing.CotangentSpace R) ↔ IsField R
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.containsInOrderLower : String → String → Bool
-- Std.Time.Date.Unit.Month
Std.Time.Month.instDecidableEqQuarter : DecidableEq Std.Time.Month.Quarter
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.map : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j j' : J)
  (f : j ⟶ j') (x : ↑(F.obj j)),
  CommRingCat.Colimits.Relation F
    (CommRingCat.Colimits.Prequotient.of j' ((CategoryTheory.ConcreteCategory.hom (F.map f)) x))
    (CommRingCat.Colimits.Prequotient.of j x)
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable within `S` at `x ∈ S`, then the
slope of any secant line with left endpoint at `x` is strictly greater than the derivative of `f`
within `S` at `x`.

This is fractionally weaker than `StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi` but simpler to
apply under a `DifferentiableOn S` hypothesis.  -/
StrictConvexOn.lt_slope_of_hasDerivWithinAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S x → f' < slope f x y
-- Mathlib.Analysis.Convex.AmpleSet
/-- The empty set in a vector space is ample.  -/
ampleSet_empty : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F], AmpleSet ∅
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Finite.lt_ciInf_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {a : α} {s : Set ι} {f : ι → α},
  s.Finite → (∃ x ∈ s, f x ≤ sInf ∅) → (a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.compRightId_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f : u ⟶ u}
  (h : CategoryTheory.Arrow.RightHomotopy f (CategoryTheory.CategoryStruct.id u)) (g : u ⟶ v),
  (h.compRightId g).hom = CategoryTheory.CategoryStruct.comp h.hom (CategoryTheory.Arrow.Hom.left g)
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The same-universe version of `lift_rank_le_of_injective_injective`.  -/
rank_le_of_injective_injective : ∀ {R : Type u} {R' : Type u'} {M M₁ : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Ring R'] [inst_4 : AddCommGroup M₁] [inst_5 : Module R' M₁] (i : R' → R) (j : M →+ M₁),
  (∀ (r : R'), i r = 0 → r = 0) →
    Function.Injective ⇑j → (∀ (r : R') (m : M), j (i r • m) = r • j m) → Module.rank R M ≤ Module.rank R' M₁
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_lt_mul_iff_left : ∀ {a b c : ENNReal}, c ≠ 0 → c ≠ ⊤ → (a * c < b * c ↔ a < b)
-- Mathlib.CategoryTheory.InducedCategory
/-- `InducedCategory D F`, where `F : C → D`, is a typeclass synonym for `C`,
which provides a category structure so that the morphisms `X ⟶ Y` are the morphisms
in `D` from `F X` to `F Y`.
 -/
CategoryTheory.InducedCategory : {C : Type u₁} → (D : Type u₂) → (C → D) → Type u₁
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  Multiset.toFinsupp (s ∪ t) = Multiset.toFinsupp s ⊔ Multiset.toFinsupp t
-- Mathlib.FieldTheory.LinearDisjoint
/-- If there are `F`-bases `{ u_i }`, `{ v_j }` of `A`, `L`, such that the products
`{ u_i * v_j }` are linearly independent over `F`, then `A` and `L` are linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_basis_mul' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E]
  {κ : Type u_1} {ι : Type u_2} (a : Module.Basis κ F ↥A) (b : Module.Basis ι F L),
  (LinearIndependent F fun i => ↑(a i.1) * (algebraMap L E) (b i.2)) → A.LinearDisjoint L
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendCyclesIso_hom_iCycles : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (K.iCycles j) =
    CategoryTheory.CategoryStruct.comp ((K.extend e).iCycles j') (K.extendXIso e hj').hom
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
log_riemannZeta_add_log_sub_isLittleO_ofReal : (fun s => Real.log (riemannZeta ↑s).re + Real.log (s - 1)) =o[nhdsWithin 1 (Set.Ioi 1)] fun x => 1
-- Mathlib.Topology.Separation.Regular
/-- The `SeparationQuotient` of a regular space is a T₃ space.  -/
instT3SpaceSeparationQuotientOfRegularSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X], T3Space (SeparationQuotient X)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.natCast_eq_top : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, n ≠ 0 → ↑n = ⊤
-- Init.Data.Nat.Gcd
Nat.dvd_gcd_iff : ∀ {k : ℕ} {m n : ℕ}, k ∣ m.gcd n ↔ k ∣ m ∧ k ∣ n
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : ↑X.affineOpens),
  ↑↑((AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv f) U) = (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ↑U
-- Mathlib.RingTheory.Congruence.Hom
/-- The first isomorphism theorem for semirings in the case of a homomorphism with right inverse.  -/
RingCon.quotientKerEquivOfRightInverse : {M : Type u_1} →
  {P : Type u_3} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring P] →
        (f : M →+* P) → (g : P → M) → Function.RightInverse g ⇑f → (RingCon.ker f).Quotient ≃+* P
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A group is commutative if the quotient by the center is cyclic.
Also see `commGroupOfCyclicCenterQuotient` for the `CommGroup` instance.  -/
MonoidHom.isMulCommutative_of_isCyclic_of_ker_le_center : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] [IsCyclic G'] (f : G →* G'),
  f.ker ≤ Subgroup.center G → IsMulCommutative G
-- Mathlib.SetTheory.Ordinal.Principal
/-- The main characterization theorem for additive principal ordinals.  -/
Ordinal.isPrincipal_add_iff_zero_or_omega0_opow : ∀ {o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun x => Ordinal.omega0 ^ x
-- Mathlib.Order.Heyting.Hom
CoheytingHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] (f : CoheytingHom α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_mul_univ : ∀ {α : Type u_2} [inst : Monoid α], Set.univ * Set.univ = Set.univ
-- Mathlib.Data.Sigma.Basic
Prod.fst_comp_toSigma : ∀ {α : Type u_7} {β : Type u_8}, Sigma.fst ∘ Prod.toSigma = Prod.fst
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_diff!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff! m₂).getKey? k = m₁.getKey? k