mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.mapIso_refl : ∀ {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 : C), F.mapIso (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl (F.obj X)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsCocircuit.of_contract : ∀ {α : Type u_1} {M : Matroid α} {K C : Set α}, (M.contract C).IsCocircuit K → M.IsCocircuit K
-- Init.Data.SInt.Lemmas
USize.toISize_sub : ∀ (a b : USize), (a - b).toISize = a.toISize - b.toISize
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.isInjectiveTheorem : Lean.Meta.Grind.Extension → Lean.Name → Lean.CoreM Bool
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
_private.Mathlib.FieldTheory.IntermediateField.Adjoin.Defs.0.IntermediateField.mkInsertTerm.run : {m : Type → Type} → [Monad m] → [Lean.MonadQuotation m] → Lean.TSyntaxArray `term → ℕ → m Lean.Term
-- Mathlib.Data.Matrix.Block
/-- `Matrix.blockDiag` as an `AddMonoidHom`.  -/
Matrix.blockDiagAddMonoidHom : (m : Type u_2) →
  (n : Type u_3) →
    (o : Type u_4) → (α : Type u_12) → [inst : AddZeroClass α] → Matrix (m × o) (n × o) α →+ o → Matrix m n α
-- Mathlib.Tactic.Ring.Common
/-- The main case of exponentiation of ring expressions is when `va` is a polynomial and `n` is a
nonzero literal expression, like `(x + y)^5`. In this case we work out the polynomial completely
into a sum of monomials.

* `x ^ 1 = x`
* `x ^ (2*n) = x ^ n * x ^ n`
* `x ^ (2*n+1) = x ^ n * x ^ n * x`
 -/
Mathlib.Tactic.Ring.Common.evalPowNat : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                (n : Q(ℕ)) →
                  Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» ^ «$n»))
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FormallyUnramified) →
    AlgebraicGeometry.FormallyUnramified f
-- Mathlib.Data.Matrix.Basis
Matrix.single_mul_single_same : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq l] [inst_1 : DecidableEq m]
  [inst_2 : DecidableEq n] [inst_3 : Fintype m] [inst_4 : NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (k : n)
  (d : α), Matrix.single i j c * Matrix.single j k d = Matrix.single i k (c * d)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_roots_map_of_injective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Semiring S] {p : Polynomial S}
  {f : S →+* R},
  Function.Injective ⇑f → ∀ {x : R}, p ≠ 0 → (x ∈ (Polynomial.map f p).roots ↔ Polynomial.eval₂ f x p = 0)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.Flat
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.forget_createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat),
  MonCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c t =>
      have this := ⋯;
      {
        liftedCone :=
          { pt := MonCat.of (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt,
            π := { app := fun j => MonCat.ofHom (MonCat.limitπMonoidHom F j), naturality := ⋯ } },
        validLift :=
          CategoryTheory.Limits.Cone.ext
            ((CategoryTheory.Limits.Types.isLimitEquivSections t).trans
                  (equivShrink ↑(F.comp (CategoryTheory.forget MonCat)).sections)).symm.toIso
            ⋯,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget MonCat)
            (CategoryTheory.Limits.Types.Small.limitConeIsLimit (F.comp (CategoryTheory.forget MonCat)))
            (fun s =>
              MonCat.ofHom
                {
                  toFun :=
                    ⇑(CategoryTheory.ConcreteCategory.hom
                        ((CategoryTheory.Limits.Types.Small.limitConeIsLimit
                              (F.comp (CategoryTheory.forget MonCat))).lift
                          ((CategoryTheory.forget MonCat).mapCone s))),
                  map_one' := ⋯, map_mul' := ⋯ })
            ⋯ }
-- Init.Grind.Norm
Lean.Grind.Int.subNatNat_eq : ∀ (a b : ℕ), Int.subNatNat a b = ↑a - ↑b
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_of_image : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'},
  ⇑f '' ↑I = ↑J → LieIdeal.map f I = J
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (hf : Function.HasFiniteSupport f),
  ∑ᶠ (i : α), f i = ∑ i ∈ Set.Finite.toFinset hf, f i
-- Mathlib.Topology.Semicontinuity.Basic
continuousWithinAt_iff_lower_upperSemicontinuousWithinAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ},
  ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.isoOfIsoLift_hom : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [inst_2 : p.IsHomLift f φ.hom],
  (CategoryTheory.IsHomLift.isoOfIsoLift p f φ).hom = f
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.Nat.xgcdAux.match_1.eq_2 : ∀ (motive : (n : ℕ) → ((m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → Sort u_1) (k : ℕ)
  (ih : (m : ℕ) → m < k.succ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
  (h_1 : (ih : (m : ℕ) → m < 0 → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive 0 ih)
  (h_2 : (k : ℕ) → (ih : (m : ℕ) → m < k.succ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive k.succ ih),
  (match k.succ, ih with
    | 0, ih => h_1 ih
    | k.succ, ih => h_2 k ih) =
    h_2 k ih
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, panicking if the map is empty.
 -/
Std.ExtDTreeMap.minKey! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtDTreeMap α β cmp → α
-- Mathlib.Tactic.Widget.StringDiagram
/-- The identifier of the variable.  -/
Mathlib.Tactic.Widget.StringDiagram.PenroseVar.ident : Mathlib.Tactic.Widget.StringDiagram.PenroseVar → String
-- Lean.Declaration
Lean.QuotVal : Type
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Module.End.ker_pow_eq_ker_pow_finrank_of_le : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {f : Module.End K V} {m : ℕ},
  Module.finrank K V ≤ m → LinearMap.ker (f ^ m) = LinearMap.ker (f ^ Module.finrank K V)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.finSuccEquiv_eq : ∀ (R : Type u) [inst : CommSemiring R] (n : ℕ),
  ↑(MvPolynomial.finSuccEquiv R n) =
    MvPolynomial.eval₂Hom (Polynomial.C.comp MvPolynomial.C) fun i =>
      Fin.cases Polynomial.X (fun k => Polynomial.C (MvPolynomial.X k)) i
-- Mathlib.Analysis.Normed.Group.Uniform
norm_map' : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) (x : E), ‖f x‖ = ‖x‖
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.IsUniversal.uniq : ∀ {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 g : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (η : f ⟶ g),
  η = CategoryTheory.Limits.IsInitial.to h g
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.Equiv.impl : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.Equiv m₂ → (Std.DHashMap.Internal.toListModel m₁.buckets).Perm (Std.DHashMap.Internal.toListModel m₂.buckets)
-- Mathlib.Combinatorics.SimpleGraph.Dart
/-- The dart with reversed orientation from a given dart.  -/
SimpleGraph.Dart.symm : {V : Type u_1} → {G : SimpleGraph V} → G.Dart → G.Dart
-- Mathlib.Topology.Constructions
continuousAt_apply : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (i : ι) (x : (i : ι) → A i),
  ContinuousAt (fun p => p i) x
-- Lean.Data.Lsp.Internal
/-- Result for a single module query.
Identifiers in the response are sorted descendingly by how well they match the query.
 -/
Lean.Lsp.LeanQueriedModule : Type
-- Init.Data.List.Lemmas
List.head?_insert : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List α} {a : α},
  (List.insert a l).head? = some (if h : a ∈ l then l.head ⋯ else a)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_lt_of_le : ∀ {a b c : Ordinal.{u_4}}, b ≤ a → (a - b < c ↔ a < b + c)
-- Mathlib.Order.Filter.Prod
Filter.map_snd_prod : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [f.NeBot], Filter.map Prod.snd (f ×ˢ g) = g
-- Init.Data.Nat.Lemmas
Nat.mul_le_of_le_div : ∀ (k x y : ℕ), x ≤ y / k → x * k ≤ y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.comp_zpow_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g ^ n) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g ^ n) h
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Coerce continuous affine equivalences to affine equivalences.  -/
ContinuousAffineEquiv.coe : {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₂] → Coe (P₁ ≃ᴬ[k] P₂) (P₁ ≃ᵃ[k] P₂)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'.match_1.eq_1 : ∀ {β : Type u_3} (γ : Type u_1) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (acc : γ) (out : β)
  (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) (c : γ)
  (h' : PlausibleForInStep out acc (ForInStep.yield c))
  (h_1 : (c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩)
  (h_2 : (c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩),
  (match ⟨ForInStep.yield c, h'⟩ with
    | ⟨ForInStep.yield c, h'⟩ => h_1 c h'
    | ⟨ForInStep.done c, h⟩ => h_2 c h) =
    h_1 c h'
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instAdditiveKaroubiToKaroubi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (CategoryTheory.Idempotents.toKaroubi C).Additive
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.IsOrdering.toIsPrime : ∀ {R : Type u_1} {inst : CommRing R} {P : RingPreordering R} [self : P.IsOrdering], P.support.IsPrime
-- Mathlib.Data.Finsupp.ToDFinsupp
/-- Interpret a `Finsupp` as a homogeneous `DFinsupp`.  -/
Finsupp.toDFinsupp : {ι : Type u_1} → {M : Type u_3} → [inst : Zero M] → (ι →₀ M) → Π₀ (x : ι), M
-- Mathlib.GroupTheory.IndexNSmul
/-- If `A ≤ B` are subgroups of an additive group `M` such that `A` has finite relative index
in `B`, where `B` is finitely generated and torsion-free as a `ℤ`-module, then `A` and `B`
have the same rank.  -/
AddSubgroup.finrank_eq_of_isFiniteRelIndex : ∀ {M : Type u_1} [inst : AddCommGroup M] {A B : AddSubgroup M} [Module.Finite ℤ ↥B] [Module.IsTorsionFree ℤ ↥B],
  A ≤ B → ∀ [A.IsFiniteRelIndex B], Module.finrank ℤ ↥A = Module.finrank ℤ ↥B
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Any morphism `k : Y ⟶ W` satisfying `∀ j₁ j₂, f j₁ ≫ k = f j₂ ≫ k` induces a morphism
`l : wideCoequalizer f ⟶ W` satisfying `wideCoequalizer.π ≫ g = l`.  -/
CategoryTheory.Limits.wideCoequalizer.desc' : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] →
            [Nonempty J] →
              {W : C} →
                (k : Y ⟶ W) →
                  (∀ (j₁ j₂ : J),
                      CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) →
                    { l // CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) l = k }
-- Mathlib.Data.NNReal.Defs
NNReal.sSup_of_not_bddAbove : ∀ {s : Set NNReal}, ¬BddAbove s → sSup s = 0
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.norm.go.eq_1 : ∀ (r : Nat.Internal.Linear.Poly), Nat.Internal.Linear.Poly.norm.go [] r = r
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_op : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C), P.op.unop = P
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.mul_iSup : ∀ (o : Ordinal.{u_1}) {ι : Sort u_2} (f : ι → Ordinal.{u_1}), o * ⨆ i, f i = ⨆ i, o * f i
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.SkeletalFunctor.isEquivalence : SimplexCategory.skeletalFunctor.IsEquivalence
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- Asymptotically, the characteristic function for the zeros of `f * g` is less than or equal to the
sum of the characteristic functions for the zeros of `f` and `g`, respectively.
 -/
ValueDistribution.characteristic_mul_zero_eventuallyLE : ∀ {f₁ f₂ : ℂ → ℂ},
  Meromorphic f₁ →
    (∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) →
      Meromorphic f₂ →
        (∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) →
          ValueDistribution.characteristic (f₁ * f₂) 0 ≤ᶠ[Filter.atTop]
            ValueDistribution.characteristic f₁ 0 + ValueDistribution.characteristic f₂ 0
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.refl_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X], (OpenPartialHomeomorph.refl X).symm = OpenPartialHomeomorph.refl X
-- Mathlib.Computability.RegularExpressions
RegularExpression.instMul : {α : Type u_1} → Mul (RegularExpression α)
-- Mathlib.RingTheory.Etale.Finite
/-- The object property of finite étale `R`-algebras.  -/
CommAlgCat.finiteEtale : (R : Type u) → [inst : CommRing R] → CategoryTheory.ObjectProperty (CommAlgCat R)
-- Mathlib.Data.Real.Basic
Real.cauchy_one : Real.cauchy 1 = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.unitOfList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α},
  Std.DTreeMap.Raw.Const.unitOfList (hd :: tl) cmp = Std.DTreeMap.Raw.Const.insertManyIfNewUnit (∅.insertIfNew hd ()) tl
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.subConst_empty_right : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A : Finset G), A.subConst ∅ = 0
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.pair.injEq : ∀ {ι : Type v} (a a_1 a_2 a_3 : ι),
  (CategoryTheory.Pairwise.pair a a_1 = CategoryTheory.Pairwise.pair a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousCore.gc : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜],
  GaloisConnection HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] {I J : Ideal R₁} {z : K},
  FractionalIdeal.spanSingleton (nonZeroDivisors R₁) z * ↑I = ↑J ↔
    Ideal.span {(IsLocalization.sec (nonZeroDivisors R₁) z).1} * I =
      Ideal.span {↑(IsLocalization.sec (nonZeroDivisors R₁) z).2} * J
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorphOfImageEq_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (t : Set Y) (h : ⇑e '' s = t), (e.toPartialHomeomorphOfImageEq s t h).toPartialEquiv = e.toPartialEquivOfImageEq s t h
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeResult.capabilities : Lean.Lsp.InitializeResult → Lean.Lsp.ServerCapabilities
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.t_smul_eq_unitsSMul : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (w : HNNExtension.NormalWord d), HNNExtension.t • w = HNNExtension.NormalWord.unitsSMul φ 1 w
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
hasMFDerivWithinAt_sdiff_singleton : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)} (y : M), HasMFDerivAt[s \ {y}] f x f' ↔ HasMFDerivAt[s] f x f'
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- An analogue of `Filter.HasBasis.tendsto_right_iff` for `TendstoUniformlyOnFilter`.  -/
Filter.HasBasis.tendstoUniformlyOnFilter_iff_of_uniformity : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {X : Type u_5} {ιβ : Type u_8} {F : X → α → β} {f : α → β}
  {l : Filter X} {l' : Filter α} {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)},
  (uniformity β).HasBasis pβ sβ →
    (TendstoUniformlyOnFilter F f l l' ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i)
-- Init.Data.SInt.Basic
/-- Non-strict inequality of word-sized signed integers, defined as inequality of the corresponding
integers. Usually accessed via the `≤` operator.
 -/
ISize.le : ISize → ISize → Prop
-- Mathlib.CategoryTheory.Abelian.Transfer
/-- If `C` is an additive category, `D` is an abelian category,
we have `F : C ⥤ D` `G : D ⥤ C` (with `G` preserving zero morphisms),
`G` is left exact (that is, preserves finite limits),
and further we have `adj : G ⊣ F` and `i : F ⋙ G ≅ 𝟭 C`,
then `C` is also abelian.  -/
CategoryTheory.abelianOfAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteProducts C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) →
                (G : CategoryTheory.Functor D C) →
                  [G.PreservesZeroMorphisms] →
                    [CategoryTheory.Limits.PreservesFiniteLimits G] →
                      (F.comp G ≅ CategoryTheory.Functor.id C) → (G ⊣ F) → CategoryTheory.Abelian C
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.continuous_integral_integral : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E], Continuous fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- A version of `contract_delete_contract_delete` without the disjointness hypothesis,
and hence a less simple RHS.  -/
Matroid.contract_delete_contract_delete' : ∀ {α : Type u_1} (M : Matroid α) (C D C' D' : Set α),
  (((M.contract C).delete D).contract C').delete D' = (M.contract (C ∪ C' \ D)).delete (D ∪ D')
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.mk.injEq : ∀ {α : Type u} (as as_1 : α), ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceCofibrantObjectWeakEquivalencesιCofibrantObjectLocalizerMorphism : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphism C).IsLocalizedEquivalence
-- Init.Data.List.Lemmas
/-- Variant of `all_bne` with `!=` reversed.  -/
List.all_bne' : ∀ {α : Type u_1} {a : α} [inst : BEq α] [PartialEquivBEq α] {l : List α}, (l.all fun x => x != a) = !l.contains a
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.zero_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Std.Data.DTreeMap.Lemmas
/-- Simpler variant of `get!_filter` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Const.get!_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited β] {f : α → β → Bool} {k : α},
  Std.DTreeMap.Const.get! (Std.DTreeMap.filter f t) k = (Option.filter (f k) (Std.DTreeMap.Const.get? t k)).get!
-- Init.Prelude
/-- Returns a value without modifying the state or throwing an exception.
 -/
EStateM.pure : {ε σ α : Type u} → α → EStateM ε σ α
-- Mathlib.Topology.FiberBundle.Basic
/-- Topology on the total space that will make the prebundle into a bundle.  -/
FiberPrebundle.totalSpaceTopology : {B : Type u_2} →
  {F : Type u_3} →
    {E : B → Type u_5} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] → FiberPrebundle F E → TopologicalSpace (Bundle.TotalSpace F E)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.forget₂_map : ∀ (R : Type u) [inst : Semiring R] (X Y : SemimoduleCat R) (f : X ⟶ Y),
  (CategoryTheory.forget₂ (SemimoduleCat R) AddCommMonCat).map f = AddCommMonCat.ofHom ↑(SemimoduleCat.Hom.hom f)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.inl_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.snd X Y) = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 = 0 → WeierstrassCurve.Jacobian.Point.toAffine W P = 0