mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Monadic
/-- This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
List.foldlM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {p : α → Prop} {l : List { x // p x }}
  {f : β → { x // p x } → m β} {g : β → α → m β} {x : β},
  (∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) → List.foldlM f x l = List.foldlM g x l.unattach
-- Mathlib.Analysis.Calculus.Implicit
/-- `HasStrictFDerivAt.implicitFunction` sends `(z, y)` to a point in `f ⁻¹' z`.  -/
HasStrictFDerivAt.map_implicitFunction_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤),
  ∀ᶠ (p : F × ↥(↑f').ker) in nhds (f a, 0), f (HasStrictFDerivAt.implicitFunction f f' hf hf' p.1 p.2) = p.1
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.IsCardinalAccessible.preservesColimitOfShape : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} (κ : Cardinal.{w}) {inst_2 : Fact κ.IsRegular} [self : F.IsCardinalAccessible κ]
  (J : Type w) [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ],
  CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Data.List.Lattice
List.forall_mem_of_forall_mem_union_right : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Prop} [inst : DecidableEq α], (∀ x ∈ l₁ ∪ l₂, p x) → ∀ x ∈ l₂, p x
-- Mathlib.Data.Set.Subsingleton
Set.eq_empty_or_singleton_of_subsingleton : ∀ {α : Type u} [Subsingleton α] (s : Set α), s = ∅ ∨ ∃ a, s = {a}
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.sum_add_tsum_nat_add : ∀ {f : ℕ → NNReal} (k : ℕ), Summable f → ∑' (i : ℕ), f i = ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k)
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIoi.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
  Set.instFintypeIoi a = Fintype.ofFinset (Finset.Ioi a) ⋯
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.μ_def : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y : Action (Type u) G},
  CategoryTheory.Functor.LaxMonoidal.μ (Rep.linearization k G) X Y = Rep.ofHom (Representation.LinearizeMonoidal.μ X Y)
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isNat_zpow_pos : ∀ {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : ℤ} {nb ne : ℕ},
  Mathlib.Meta.NormNum.IsNat b nb → Mathlib.Meta.NormNum.IsNat (a ^ nb) ne → Mathlib.Meta.NormNum.IsNat (a ^ b) ne
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.netMaxcard_monotone_subset : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X) (n : ℕ), Monotone fun F => Dynamics.netMaxcard T F U n
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.StrongCore.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G}
  {naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (η.app b) ≅ CategoryTheory.CategoryStruct.comp (η.app a) (G.map f)}
  {naturality_hom :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
      CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom._autoParam}
  {naturality_1 :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (η.app b) ≅ CategoryTheory.CategoryStruct.comp (η.app a) (G.map f)}
  {naturality_hom_1 :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality_1 f).hom = η.naturality f)
      CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom._autoParam},
  { naturality := naturality, naturality_hom := naturality_hom } =
      { naturality := naturality_1, naturality_hom := naturality_hom_1 } →
    naturality = naturality_1
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_compl_eq_mk_compl_infinite : ∀ {α : Type u_1} [Infinite α] {s t : Set α},
  Cardinal.mk ↑s < Cardinal.mk α → Cardinal.mk ↑t < Cardinal.mk α → Cardinal.mk ↑sᶜ = Cardinal.mk ↑tᶜ
-- Mathlib.FieldTheory.Galois.GaloisClosure
/-- The minimal (finite) Galois intermediate field containing a finite set `s : Set K` in a
Galois extension `K/k` defined as the normal closure of the field obtained by adjoining
the set `s : Set K` to `k`.  -/
FiniteGaloisIntermediateField.adjoin : (k : Type u_1) →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] → [IsGalois k K] → (s : Set K) → [Finite ↑s] → FiniteGaloisIntermediateField k K
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.hle : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} {w : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput old w), old.decls.size ≤ self.aig.decls.size
-- Mathlib.Algebra.Module.LocalizedModule.Exact
/-- Localization of modules is an exact functor.  -/
IsLocalizedModule.map_exact : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M₀ : Type u_2} {M₀' : Type u_5} [inst_1 : AddCommMonoid M₀]
  [inst_2 : AddCommMonoid M₀'] [inst_3 : Module R M₀] [inst_4 : Module R M₀'] (f₀ : M₀ →ₗ[R] M₀')
  [inst_5 : IsLocalizedModule S f₀] {M₁ : Type u_3} {M₁' : Type u_6} [inst_6 : AddCommMonoid M₁]
  [inst_7 : AddCommMonoid M₁'] [inst_8 : Module R M₁] [inst_9 : Module R M₁'] (f₁ : M₁ →ₗ[R] M₁')
  [inst_10 : IsLocalizedModule S f₁] {M₂ : Type u_4} {M₂' : Type u_7} [inst_11 : AddCommMonoid M₂]
  [inst_12 : AddCommMonoid M₂'] [inst_13 : Module R M₂] [inst_14 : Module R M₂'] (f₂ : M₂ →ₗ[R] M₂')
  [inst_15 : IsLocalizedModule S f₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂),
  Function.Exact ⇑g ⇑h → Function.Exact ⇑((IsLocalizedModule.map S f₀ f₁) g) ⇑((IsLocalizedModule.map S f₁ f₂) h)
-- Aesop.Rule.Name
Aesop.DisplayRuleName.ruleName.inj : ∀ {n n_1 : Aesop.RuleName}, Aesop.DisplayRuleName.ruleName n = Aesop.DisplayRuleName.ruleName n_1 → n = n_1
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_antitone_kernel_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν ν' : ProbabilityTheory.Kernel α γ},
  ν ≤ ν' → κ.fst ≤ ν → ∀ (n : ℕ) (a : α) (x : γ) (s : Set β), κ.densityProcess ν' n a x s ≤ κ.densityProcess ν n a x s
-- Batteries.Util.ProofWanted
/-- The carried value. Reference the declaration via `❰…❱` rather than projecting this
directly.  -/
DerivedWanted.val : {α : Sort u} → DerivedWanted α → α
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.toIsCancelMulZero : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : UniqueFactorizationMonoid α], IsCancelMulZero α
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.IsGE.ge : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.Limits.HasZeroObject C} {inst_3 : CategoryTheory.HasShift C ℤ}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {t : CategoryTheory.Triangulated.TStructure C} {X : C} {n : ℤ} [self : t.IsGE X n], t.ge n X
-- Mathlib.Combinatorics.Pigeonhole
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.  Given a function `f`
between finite types `α` and `β` and a number `b` such that `card β • b ≤ card α`, there exists an
element `y : β` such that its preimage has at least `b` elements.
See also `Fintype.exists_lt_card_fiber_of_nsmul_lt_card` for a stronger statement.  -/
Fintype.exists_le_card_fiber_of_nsmul_le_card : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {b : M} [inst_3 : CommSemiring M] [inst_4 : LinearOrder M] [IsStrictOrderedRing M] [Nonempty β],
  Fintype.card β • b ≤ ↑(Fintype.card α) → ∃ y, b ≤ ↑{x | f x = y}.card
-- Init.Data.Option.Basic
Option.map_some : ∀ {α : Type u_1} {β : Type u_2} (a : α) (f : α → β), Option.map f (some a) = some (f a)
-- Mathlib.Data.List.Basic
/-- A single `List.map` of a composition of functions is equal to
composing a `List.map` with another `List.map`, fully applied.
This is the reverse direction of `List.map_map`.
 -/
List.comp_map : ∀ {α : Type u} {β : Type v} {γ : Type w} (h : β → γ) (g : α → β) (l : List α),
  List.map (h ∘ g) l = List.map h (List.map g l)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y : C} [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] {m : M},
  CategoryTheory.Localization.SmallShiftedHom.equiv W L = CategoryTheory.Localization.SmallShiftedHom.equiv W L
-- Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
/-- First part of the First Main Theorem, quantitative version: If `f` is meromorphic on the complex
plane, then the difference between the characteristic functions of `f` and `f⁻¹` is bounded by an
explicit constant.
 -/
ValueDistribution.characteristic_sub_characteristic_inv_le : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    |ValueDistribution.characteristic f ⊤ R - ValueDistribution.characteristic f⁻¹ ⊤ R| ≤
      max |Real.log ‖f 0‖| |Real.log ‖meromorphicTrailingCoeffAt f 0‖|
-- Batteries.Data.List.Lemmas
List.getElem?_set_of_lt' : ∀ {α : Type u_1} (a : α) {m n : ℕ} (l : List α), m < l.length → (l.set m a)[n]? = if m = n then some a else l[n]?
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousWithinAt_univ : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α) (x₀ : X),
  EquicontinuousWithinAt F Set.univ x₀ ↔ EquicontinuousAt F x₀
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finrank_of_not_finite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R], ¬Module.Finite R M → Module.finrank R M = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.all_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {p : α → β → Bool}, t₁.Equiv t₂ → t₁.all p = t₂.all p
-- Mathlib.Algebra.Lie.Prod
LieHom.ker_snd : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂],
  LieIdeal.toLieSubalgebra R (L₁ × L₂) (LieHom.snd R L₁ L₂).ker = (LieHom.inl R L₁ L₂).range
-- Mathlib.RingTheory.Multiplicity
emultiplicity_add_eq_min : ∀ {α : Type u_1} [inst : Ring α] {p a b : α},
  emultiplicity p a ≠ emultiplicity p b → emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.symm_trans_self : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), e.symm.trans e = ContinuousAffineEquiv.refl k P₂
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.instRankOneAdicCompletion`. -/
NumberField.instRankOneAdicCompletion : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsDedekindDomain R] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) → [Module.Finite ℤ R] → [Module.Free ℤ R] → Valued.v.RankOne
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- `canonicalEquiv f f'` is the canonical equivalence between the fractional
ideals in `P` and in `P'`, which are both localizations of `R` at `S`.  -/
FractionalIdeal.canonicalEquiv : {R : Type u_5} →
  [inst : CommRing R] →
    (S : Submonoid R) →
      (P : Type u_6) →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            (P' : Type u_7) →
              [inst_3 : CommRing P'] →
                [inst_4 : Algebra R P'] →
                  [IsLocalization S P] → [IsLocalization S P'] → FractionalIdeal S P ≃+* FractionalIdeal S P'
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.inv_logb_mul_base : ∀ {a b : ℝ}, a ≠ 0 → b ≠ 0 → ∀ (c : ℝ), (Real.logb (a * b) c)⁻¹ = (Real.logb a c)⁻¹ + (Real.logb b c)⁻¹
-- Mathlib.Algebra.GroupWithZero.Units.Basic
zpow_ne_zero_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} {n : ℤ}, n ≠ 0 → (a ^ n ≠ 0 ↔ a ≠ 0)
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.volume_apply' : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι),
  (MeasureTheory.volume ↑I).toReal = ∏ i, (I.upper i - I.lower i)
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isConnected_closedEBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  IsConnected (Metric.closedEBall x r)
-- Lean.Elab.Command.Scope
/-- True if a `public section` is in scope.  -/
Lean.Elab.Command.Scope.isPublic : Lean.Elab.Command.Scope → Bool
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mapIso_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (e : A ≅ B),
  (CategoryTheory.MonoOver.mapIso e).inverse = CategoryTheory.MonoOver.map e.inv
-- Std.Http.Test.Helpers
/-- Assert `needle` appears anywhere in the response.
 -/
Std.Http.Internal.Test.assertContains : ByteArray → String → IO Unit
-- Lean.Meta.HaveTelescope
Lean.Meta.HaveInfo.mk.sizeOf_spec : ∀ (typeBackDeps valueBackDeps : Std.HashSet ℕ) (decl : Lean.LocalDecl) (level : Lean.Level),
  sizeOf { typeBackDeps := typeBackDeps, valueBackDeps := valueBackDeps, decl := decl, level := level } =
    1 + sizeOf typeBackDeps + sizeOf valueBackDeps + sizeOf decl + sizeOf level
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.zero_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Injective 0
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Binary entropy has derivative `log (1 - p) - log p`.  -/
Real.hasDerivAt_binEntropy : ∀ {p : ℝ}, p ≠ 0 → p ≠ 1 → HasDerivAt Real.binEntropy (Real.log (1 - p) - Real.log p) p
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.alterKey_cons_perm.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} {k : α} (motive : Option (β k) → Sort u_2) (v : β k) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- The condition `f = O[𝓝[≠] a] 1` is equivalent to `f = O[𝓝 a] 1`.  -/
Asymptotics.isBigO_one_nhds_ne_iff : ∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] {f : α → E} [inst_2 : One F]
  [NormOneClass F] [inst_4 : TopologicalSpace α] {a : α}, (f =O[nhdsWithin a {a}ᶜ] fun x => 1) ↔ f =O[nhds a] fun x => 1
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- `QuotientAddGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
given that `e` maps `G` to `H`.  -/
QuotientAddGroup.congr : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup H] →
        (G' : AddSubgroup G) →
          (H' : AddSubgroup H) →
            [inst_2 : G'.Normal] → [inst_3 : H'.Normal] → (e : G ≃+ H) → AddSubgroup.map (↑e) G' = H' → G ⧸ G' ≃+ H ⧸ H'
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A homology data for a short complex `S` in the opposite category
induces a homology data for `S.unop`.  -/
CategoryTheory.ShortComplex.HomologyData.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex Cᵒᵖ} → S.HomologyData → S.unop.HomologyData
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.alter : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.OrientedOrd α] →
        [Std.LawfulEqOrd α] →
          {k : α} →
            (Option (β k) → Option (β k)) →
              Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k)
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- If R has Krull dimension ≤ 0, then `piLocalizationToIsMaximal R` is an isomorphism.  -/
PrimeSpectrum.piLocalizationToMaximalEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    (∀ (I : Ideal R), I.IsPrime → I.IsMaximal) → PrimeSpectrum.PiLocalization R ≃+* MaximalSpectrum.PiLocalization R
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
      S.cokernelToAbelianCoimage =
    0
-- Aesop.Index.Forward
/-- Index for forward rules.  -/
Aesop.ForwardIndex : Type
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.Prod.continuous_inv_fun : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)],
  ContinuousOn (Bundle.Trivialization.Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ)
-- Mathlib.Algebra.Notation.Support
/-- `support` of a function is the set of points `x` such that `f x ≠ 0`.  -/
Function.support : {ι : Type u_1} → {M : Type u_3} → [Zero M] → (ι → M) → Set ι
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.orderTop_one : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : Zero R] [inst_3 : One R] [NeZero 1],
  HahnSeries.orderTop 1 = 0
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'Map_comp_assoc : ∀ {ι : 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]
  {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : ∀ (i' : ι'), M.HasHomology i'] {Z : HomologicalComplex C c} (h : M.truncGE' e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map (CategoryTheory.CategoryStruct.comp φ φ') e) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map φ e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map φ' e) h)
-- Mathlib.Topology.Order
induced_top : ∀ {α : Type u_1} {β : Type u_2} {g : β → α}, TopologicalSpace.induced g ⊤ = ⊤
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- [Stacks Tag 01KE](https://stacks.math.columbia.edu/tag/01KE) -/
AlgebraicGeometry.ValuativeCriterion.Existence.eq : AlgebraicGeometry.ValuativeCriterion.Existence = (AlgebraicGeometry.topologically @SpecializingMap).universally
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.const_smul : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β}
  [inst : TopologicalSpace β] {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : Zero β]
  [inst_3 : SMulZeroClass 𝕜 β] [ContinuousSMul 𝕜 β],
  MeasureTheory.FinStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.FinStronglyMeasurable (c • f) μ
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Cardinal.iSup_lt_of_lt_cof_ord : ∀ {α : Type u} {f : α → Cardinal.{u}} {a : Cardinal.{u}},
  Cardinal.mk α < a.ord.cof → (∀ (i : α), f i < a) → ⨆ i, f i < a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapFunctor_obj : ∀ (T : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} T] (X : Tᵒᵖ),
  (CategoryTheory.Under.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Under (Opposite.unop X))
-- Mathlib.Data.Nat.Factorization.Root
Nat.factorization_floorRoot : ∀ (n a : ℕ), (n.floorRoot a).factorization = a.factorization ⌊/⌋ n
-- Mathlib.Tactic.Order.Graph.Tarjan
Mathlib.Tactic.Order.Graph.TarjanState.mk.sizeOf_spec : ∀ (toDFSState : Mathlib.Tactic.Order.Graph.DFSState) (id lowlink : Std.HashMap ℕ ℕ) (stack : Array ℕ)
  (onStack : Std.HashSet ℕ) (time : ℕ),
  sizeOf { toDFSState := toDFSState, id := id, lowlink := lowlink, stack := stack, onStack := onStack, time := time } =
    1 + sizeOf toDFSState + sizeOf id + sizeOf lowlink + sizeOf stack + sizeOf onStack + sizeOf time
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_of_pos_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulStrictMono α],
  b < c → 0 < a → a * b < a * c
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.hasNeg.eq_1 : ∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M), c.hasNeg = { neg := Quotient.map' Neg.neg ⋯ }
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- If `B : BoxIntegral.Box` has integral vertices and contains the point `x`, then the index of
`x` is admissible for `B`.  -/
BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] {B : BoxIntegral.Box ι},
  BoxIntegral.hasIntegralVertices B →
    ∀ {x : ι → ℝ}, x ∈ B → BoxIntegral.unitPartition.index n x ∈ BoxIntegral.unitPartition.admissibleIndex n B
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `Finsupp.single` as a `MonoidHom` from the product type into the additive monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of
`Finsupp.single`.
 -/
AddMonoidAlgebra.singleHom : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddZeroClass M] → R × Multiplicative M →* AddMonoidAlgebra R M
-- Mathlib.Algebra.Group.Pi.Units
MulEquiv.val_piUnits_symm_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (f : (i : ι) → (M i)ˣ) (x : ι),
  ↑(MulEquiv.piUnits.symm f) x = ↑(f x)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.coeff_sub_eq_neg_right_of_lt : ∀ {R : Type u} {n : ℕ} [inst : Ring R] {p q : Polynomial R}, p.natDegree < n → (p - q).coeff n = -q.coeff n
-- Batteries.Classes.Order
Std.LawfulBCmp.toLawfulLTCmp : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [inst_2 : BEq α] {cmp : α → α → Ordering} [self : Std.LawfulBCmp cmp],
  Std.LawfulLTCmp cmp
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_comp_lift : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = 0),
  ((ExteriorAlgebra.lift R) ⟨f, cond⟩).toLinearMap ∘ₗ ExteriorAlgebra.ι R = f