mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.neg_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (-φ).τ₃ = -φ.τ₃
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.expandDbgTrace : Lean.Macro
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ne_empty_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a : α}, a ∈ t → t ≠ ∅
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.coe_floorDiv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : AddCommMonoid β] [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] (f : ι →₀ β)
  (a : α), ⇑(f ⌊/⌋ a) = fun i => f i ⌊/⌋ a
-- Mathlib.Algebra.Group.Defs
/-- Auxiliary typeclass for types with an involutive `Inv`.  -/
InvolutiveInv : Type u_2 → Type u_2
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_mul_const : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι),
  s.indicator (fun x => f x * a) i = s.indicator f i * a
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsSeparator G ↔
    ∀ ⦃X Y : C⦄ (f g : X ⟶ Y),
      (∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) → f = g
-- Init.Data.List.Lemmas
List.length_reverse : ∀ {α : Type u_1} {as : List α}, as.reverse.length = as.length
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_top : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S],
  (Ideal.relNorm R) ⊤ = ⊤
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.instDiv : {R : Type u} → [inst : Field R] → Div (Polynomial R)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoMod hp a (b + m • p) = toIcoMod hp a b
-- Mathlib.RingTheory.Coalgebra.Hom
/-- Given `R`-modules `A, B` with comultiplication maps `Δ_A, Δ_B` and counit maps
`ε_A, ε_B`, an `R`-coalgebra homomorphism `A →ₗc[R] B` is an `R`-linear map `f` such that
`ε_B ∘ f = ε_A` and `(f ⊗ f) ∘ Δ_A = Δ_B ∘ f`.  -/
CoalgHom : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] →
            [inst_3 : AddCommMonoid B] →
              [inst_4 : Module R B] → [CoalgebraStruct R A] → [CoalgebraStruct R B] → Type (max u_2 u_3)
-- Std.Data.Internal.List.Associative
Std.Internal.List.beqModel_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : (k : α) → BEq (β k)]
  {l₁ l₂ l₃ l₄ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₂ →
    l₁.Perm l₃ → l₂.Perm l₄ → Std.Internal.List.beqModel l₁ l₂ = Std.Internal.List.beqModel l₃ l₄
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- The canonical morphism `cokernel S.f ⟶ Abelian.coimage S.g` for a short complex `S`
in an abelian category.  -/
CategoryTheory.ShortComplex.cokernelToAbelianCoimage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) → CategoryTheory.Limits.cokernel S.f ⟶ CategoryTheory.Abelian.coimage S.g
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.existsAddOfLE : ExistsAddOfLE Ordinal.{u_1}
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.pair_injective : Function.Injective2 ZFSet.pair
-- Mathlib.Order.Category.BddLat
bddLat_dual_comp_forget_to_lat : BddLat.dual.comp (CategoryTheory.forget₂ BddLat Lat) = (CategoryTheory.forget₂ BddLat Lat).comp Lat.dual
-- Std.Time.Date.Basic
/-- Convert `Hour.Offset` into `Week.Offset`.
 -/
Std.Time.Hour.Offset.toWeeks : Std.Time.Hour.Offset → Std.Time.Week.Offset
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_eq_zero_of_lt_two : ∀ {x : ℝ}, x < 2 → Chebyshev.theta x = 0
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The homology of the differentials on a page of the spectral sequence identifies
to the objects on the next page.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso : {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₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq' : κ) →
                            [X.HasSpectralSequence data] →
                              (CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r hr).homology pq' ≅
                                (CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r' ⋯).X pq'
-- Mathlib.Order.Interval.Finset.Defs
WithBot.Icc_bot_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α] (a : α),
  Finset.Icc ⊥ ↑a = Finset.insertNone (Finset.Iic a)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp_assoc_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h))
      (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h))
        (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h))
          (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)))
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.ext_isCircuit : ∀ {α : Type u_1} {M₁ M₂ : Matroid α},
  M₁.E = M₂.E → (∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)) → M₁ = M₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.div : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, s.Nonempty → t.Nonempty → (s / t).Nonempty
-- Init.Data.Array.Range
Array.pop_range' : ∀ {s n step : ℕ}, (Array.range' s n step).pop = Array.range' s (n - 1) step
-- Mathlib.Topology.UniformSpace.Ultra.Constructions
IsUltraUniformity.bot : ∀ {X : Type u_1} [inst : UniformSpace X] [DiscreteUniformity X], IsUltraUniformity X
-- Lean.Environment
Lean.Kernel.Environment.resetDiag : Lean.Kernel.Environment → Lean.Kernel.Environment
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.apply_of_skipSuffixWhile_le_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos},
  s.skipSuffixWhile P ≤ pos → ∀ (h' : pos < s.endPos), P (pos.get ⋯)
-- Mathlib.Data.Complex.Basic
Complex.instZero : Zero ℂ
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- Any finite group is finitely presented.  -/
Group.IsFinitelyPresented.instOfFinite : ∀ (G : Type u_1) [inst : Group G] [Finite G], Group.IsFinitelyPresented G
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- A morphism of bimodule objects.  -/
Bimod.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {A B : CategoryTheory.Mon C} → Bimod A B → Bimod A B → Type v₁
-- Mathlib.Order.WithBot
WithTop.forall : ∀ {α : Type u_1} {p : WithTop α → Prop}, (∀ (x : WithTop α), p x) ↔ p ⊤ ∧ ∀ (x : α), p ↑x
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.getHaveTelescopeInfo.collect : Lean.Expr →
  ℕ → Lean.Meta.HaveTelescopeInfo → Lean.LocalContext → Array Lean.Expr → Lean.MetaM Lean.Meta.HaveTelescopeInfo
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k k' : α}, cmp k k' = Ordering.eq → t.get! k = t.get! k'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
CStarAlgebra.instNonnegSpectrumClass' : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A], NonnegSpectrumClass ℝ A
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Presentation.directSum_G : ∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {M : ι → Type v}
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  (pres : (i : ι) → Module.Presentation A (M i)), (Module.Presentation.directSum pres).G = ((i : ι) × (pres i).G)
-- Mathlib.Order.BoundedOrder.Basic
IsTop.rec.eq_1 : ∀ {α : Type u} [inst : LE α] {motive : (x : α) → IsTop x → Sort u_1} (top : [inst_1 : OrderTop α] → motive ⊤ ⋯) (x : α)
  (hx : IsTop x), IsTop.rec top x hx = top
-- Mathlib.Order.Defs.Unbundled
Equivalence.isEquiv : ∀ {α : Sort u_1} (r : α → α → Prop), Equivalence r → IsEquiv α r
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instCommSemiring : {d : ℤ} → CommSemiring (ℤ√d)
-- Mathlib.Data.PNat.Basic
/-- Subtraction a - b is defined in the obvious way when
a > b, and by a - b = 1 if a ≤ b.
 -/
PNat.instSub : Sub ℕ+
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.toSubring_injective : ∀ {K : Type u} [inst : Field K], Function.Injective ValuationSubring.toSubring
-- Mathlib.Algebra.Order.Module.Defs
/-- Typeclass for monotonicity of scalar multiplication by nonnegative elements on the left,
namely `b₁ ≤ b₂ → a • b₁ ≤ a • b₂` if `0 ≤ a`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedModule`.  -/
PosSMulMono : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero α] → Prop
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- objects  -/
CategoryTheory.CoreSmallCategoryOfSet.obj : {Ω : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.CoreSmallCategoryOfSet Ω C → Set Ω
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₁ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true}, (m₁.union m₂ ⋯ ⋯).getKey k h' = m₂.getKey k ⋯
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [inst_1 : Ring R] (v : Valuation R Γ)
  [hv : v.IsRankOneDiscrete] (k : ℤ),
  (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v) (↑(Valuation.IsRankOneDiscrete.generator' v) ^ k) =
    WithZero.exp (-k)
-- Mathlib.Data.Nat.Factorization.PrimePow
IsPrimePow.exists_ordCompl_eq_one : ∀ {n : ℕ}, IsPrimePow n → ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.hlift : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} (self : D.IsTerminal e) {j : J}
  (hj : D.P j), D.W (self.lift hj)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- The recognition theorem for ind-objects: `A : Cᵒᵖ ⥤ Type v` is an ind-object if and only if
`CostructuredArrow yoneda A` is filtered and finally `v`-small.
Theorem 6.1.5 of [Kashiwara2006]  -/
CategoryTheory.Limits.isIndObject_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)),
  CategoryTheory.Limits.IsIndObject A ↔
    CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) ∧
      CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- A functor is said to preserve finite limits, if it preserves all limits of shape `J`,
where `J : Type` is a finite category.
 -/
CategoryTheory.Limits.PreservesFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.volume (NumberField.mixedEmbedding.fundamentalCone.normLeOne K) =
    2 ^ NumberField.InfinitePlace.nrRealPlaces K * ↑NNReal.pi ^ NumberField.InfinitePlace.nrComplexPlaces K *
      ENNReal.ofReal (NumberField.Units.regulator K)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- There is no established mathematical convention
for the operator precedence of big operators like `∏` and `∑`.
We will have to make a choice.

Online discussions, such as https://math.stackexchange.com/q/185538/30839
seem to suggest that `∏` and `∑` should have the same precedence,
and that this should be somewhere between `*` and `+`.
The latter have precedence levels `70` and `65` respectively,
and we therefore choose the level `67`.

In practice, this means that parentheses should be placed as follows:
```lean
∑ k ∈ K, (a k + b k) = ∑ k ∈ K, a k + ∑ k ∈ K, b k →
  ∏ k ∈ K, a k * b k = (∏ k ∈ K, a k) * (∏ k ∈ K, b k)
```
(Example taken from page 490 of Knuth's *Concrete Mathematics*.)
 -/
LibraryNote.operator_precedence_of_big_operators : Batteries.Util.LibraryNote
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsLocalizationCompιWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)],
  (HomotopicalAlgebra.FibrantObject.ι.comp L).IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject C))
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_piCongrLeft : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} [inst : Fintype ι] {m : (i : ι) → MeasurableSpace (α i)}
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [inst_2 : Fintype ι']
  (f : ι' ≃ ι),
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piCongrLeft α f)) (MeasureTheory.Measure.pi fun i' => μ (f i'))
    (MeasureTheory.Measure.pi μ)
-- Init.Data.List.Control
List.instForMOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → [Monad m] → ForM m (List α) α
-- Mathlib.Data.LawfulXor.Basic
xor_eq_zero_iff : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] {a b : α}, a ^^^ b = 0 ↔ a = b
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.GaloisCategory.toPreGaloisCategory : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.GaloisCategory C],
  CategoryTheory.PreGaloisCategory C
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Every monomorphism is a regular monomorphism  -/
CategoryTheory.IsRegularMonoCategory.regularMonoOfMono : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.IsRegularMonoCategory C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.IsRegularMono f
-- Mathlib.Data.Prod.TProd
_private.Mathlib.Data.Prod.TProd.0.List.TProd.elim.match_1.splitter : {ι : Type u_1} →
  {α : ι → Type u_2} →
    (motive : (x : List ι) → List.TProd α x → (x_2 : ι) → x_2 ∈ x → Sort u_3) →
      (x : List ι) →
        (x_1 : List.TProd α x) →
          (x_2 : ι) →
            (x_3 : x_2 ∈ x) →
              ((i : ι) →
                  (is : List ι) →
                    (v : List.TProd α (i :: is)) → (j : ι) → (hj : j ∈ i :: is) → motive (i :: is) v j hj) →
                motive x x_1 x_2 x_3
-- Init.Data.UInt.BasicAux
instLTUSize : LT USize
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.coe_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β]
  (f g : InfTopHom α β), ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.Algebra.Algebra.Operations
Submodule.equivOpposite_apply : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Submodule R Aᵐᵒᵖ),
  Submodule.equivOpposite p = MulOpposite.op (Submodule.comap (↑(MulOpposite.opLinearEquiv R)) p)
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsArtinianRing R] (I : MaximalSpectrum R),
  (IsArtinianRing.primeSpectrumEquivMaximalSpectrum.symm I).asIdeal = I.asIdeal
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_toNonUnitalSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A), ↑S.toNonUnitalSubsemiring = ↑S
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instAddCommMonoid : AddCommMonoid ℕ
-- Mathlib.Computability.Reduce
/-- `p` and `q` are many-one equivalent if each one is many-one reducible to the other.  -/
ManyOneEquiv : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → (α → Prop) → (β → Prop) → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂)[k]? = none
-- Mathlib.CategoryTheory.Abelian.Subobject
CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C)
  (a : (CategoryTheory.Subobject (Opposite.op X))ᵒᵈ),
  (RelIso.symm (CategoryTheory.Abelian.subobjectIsoSubobjectOp X)) a =
    CategoryTheory.Subobject.lift (fun x f x_1 => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) ⋯
      a
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tendsto_cofinite_zero_of_tsum_ne_top : ∀ {α : Type u_4} {f : α → ENNReal}, ∑' (x : α), f x ≠ ⊤ → Filter.Tendsto f Filter.cofinite (nhds 0)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).minKey? = some k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
/-- A typeclass carrying a choice of monoidal structural isomorphism between two objects.
Used by the `⊗≫` monoidal composition operator, and the `coherence` tactic.
 -/
CategoryTheory.MonoidalCoherence : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Type v
-- Lean.Parser.Term
Lean.Parser.Term.forInMacro' : Lean.Parser.Parser
-- Mathlib.Topology.EMetricSpace.Defs
AddOpposite.instPseudoEMetricSpace.eq_1 : ∀ {α : Type u_2} [inst : PseudoEMetricSpace α],
  AddOpposite.instPseudoEMetricSpace = PseudoEMetricSpace.induced AddOpposite.unop inst
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_mul_go : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ acc : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      acc.NonnegCoeffs →
        Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.mul.go p₂ p₁ acc) =
          Lean.Grind.CommRing.Poly.denoteS ctx acc +
            Lean.Grind.CommRing.Poly.denoteS ctx p₁ * Lean.Grind.CommRing.Poly.denoteS ctx p₂
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.comap_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M → N),
  Function.Surjective f → ∀ (hf' : ∀ (x y : M), f (x + y) = f x + f y), Function.Injective (AddCon.comap f hf')
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair
`(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)`  -/
CovariantClass.elim : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.subgroup_mul_singleton : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G} {h : G}, h ∈ H → ↑H * {h} = ↑H
-- Init.Data.Order.FactoriesExtra
Std.compare_eq_eq : ∀ {α : Type u} [inst : Ord α] [inst_1 : BEq α] [inst_2 : LE α] [Std.LawfulOrderOrd α] [Std.LawfulOrderBEq α] {a b : α},
  compare a b = Ordering.eq ↔ (a == b) = true
-- Mathlib.CategoryTheory.Retract
CategoryTheory.NatTrans.retractArrowApp_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) {X Y : C} (h : CategoryTheory.Retract X Y),
  (CategoryTheory.NatTrans.retractArrowApp τ h).r = CategoryTheory.Arrow.homMk (F.map h.r) (G.map h.r) ⋯
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.localizedModule.eq_1 : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (M : ModuleCat R) (S : Submonoid R),
  M.localizedModule S = ModuleCat.of (Localization S) (Shrink.{v, max v u} (LocalizedModule S ↑M))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {fallback : Unit},
  Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.unitOfList l cmp) k fallback = ()
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.zsmul : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x ≡ y [SMOD U] → ∀ (n : ℤ), n • x ≡ n • y [SMOD U]
-- Mathlib.Algebra.Notation.Support
Function.support_extend_zero_subset : ∀ {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [inst : Zero N] {f : ι → κ} {g : ι → N},
  Function.support (Function.extend f g 0) ⊆ f '' Function.support g
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I],
  Profinite.NobelingProof.GoodProducts C = {l | Profinite.NobelingProof.Products.isGood C l}
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.instNormedSpaceComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              (h : Manifold.IsSubmersionAt I J n f x) → NormedSpace 𝕜 h.complement