mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of `Polynomial.Splits.of_degree_le_one_of_monic`. -/
Polynomial.splits_of_degree_le_one_of_monic : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.degree ≤ 1 → f.Monic → f.Splits
-- Std.Time.Time.Unit.Second
Std.Time.Second.instTransOrdOffset : Std.TransOrd Std.Time.Second.Offset
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mk : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      (toList : List ((i : ι) × M i)) →
        (∀ l ∈ toList, l.snd ≠ 1) → List.IsChain (fun l l' => l.fst ≠ l'.fst) toList → Monoid.CoprodI.Word M
-- Init.Data.Array.MinMax
Array.max?_mem : ∀ {α : Type u_1} {a : α} [inst : Max α] [Std.MaxEqOr α] (xs : Array α), xs.max? = some a → a ∈ xs
-- Mathlib.AlgebraicGeometry.Restrict
/-- The functor that restricts to open subschemes and then takes global section is
isomorphic to the structure sheaf.  -/
AlgebraicGeometry.Scheme.restrictFunctorΓ : {X : AlgebraicGeometry.Scheme} →
  X.restrictFunctor.op.comp ((CategoryTheory.Over.forget X).op.comp AlgebraicGeometry.Scheme.Γ) ≅ X.presheaf
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.instIsStrictlySupportedTruncLE_1 : ∀ {ι : 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 : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] {ι'' : Type u_4} {c'' : ComplexShape ι''} (e' : c''.Embedding c')
  [K.IsStrictlySupported e'], (K.truncLE e).IsStrictlySupported e'
-- Mathlib.Testing.Plausible.Functions
/-- The support of a zero default `TotalFunction`.  -/
Plausible.TotalFunction.zeroDefaultSupp : {α : Type u} → {β : Type v} → [DecidableEq α] → [Zero β] → [DecidableEq β] → Plausible.TotalFunction α β → Finset α
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.coe_sup : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  [inst_3 : FaithfulSMul M X] (P Q : { P // IsLprojection X P }), ↑(P ⊔ Q) = ↑P + ↑Q - ↑P * ↑Q
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.smul_equiv : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) {u : R}, IsUnit u → u • P ≈ P
-- Mathlib.GroupTheory.Exponent
AddGroup.exponent_dvd_iff_forall_zsmul_eq_zero : ∀ {G : Type u} [inst : AddGroup G] {n : ℤ}, ↑(AddMonoid.exponent G) ∣ n ↔ ∀ (g : G), n • g = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_iInter₂_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : SMul α β] (s : Set α)
  (t : (i : ι) → κ i → Set β), s • ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s • t i j
-- Mathlib.Algebra.Opposites
AddOpposite.rec'.eq_1 : ∀ {α : Type u_1} {F : αᵃᵒᵖ → Sort u_3} (h : (X : α) → F (AddOpposite.op X)) (X : αᵃᵒᵖ),
  AddOpposite.rec' h X = h (AddOpposite.unop X)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_const_top : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} [inst_1 : LinearOrder ι],
  (MeasureTheory.stoppedProcess u fun x => ⊤) = u
-- Mathlib.RingTheory.Ideal.Int
Int.liesOver_span_absNorm : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R), I.LiesOver (Ideal.span {↑(Ideal.absNorm (Ideal.under ℤ I))})
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_comap_eq_self_of_surjective : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ (t : Subsemiring S), Subsemiring.map f (Subsemiring.comap f t) = t
-- Mathlib.Analysis.Normed.Module.Ray
/-- The norms of two vectors on the same ray are equal if and only if they are equal.  -/
SameRay.norm_eq_iff : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F}, SameRay ℝ x y → (‖x‖ = ‖y‖ ↔ x = y)
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Polynomial.fiberEquivQuotient_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : Polynomial R →ₐ[R] S) (hf : Function.Surjective ⇑f) (p : Ideal R) [inst_3 : p.IsPrime] (a : p.ResidueField)
  (b : Polynomial R),
  (Polynomial.fiberEquivQuotient f hf p) (a ⊗ₜ[R] f b) =
    (Ideal.Quotient.mk (Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
      (Polynomial.C a * Polynomial.map (algebraMap R p.ResidueField) b)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.getElem?_toList_eq : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, r.toList[i]? = Std.PRange.succMany? (i + 1) r.lower
-- ImportGraph.Imports.ImportGraph
_private.ImportGraph.Imports.ImportGraph.0.Lean.Environment.importGraph.process : Lean.Environment → Lean.Name → Lean.NameMap (Array Lean.Name) → Lean.NameMap (Array Lean.Name)
-- Mathlib.GroupTheory.OrderOfElement
AddCommute.addOrderOf_add_eq_mul_addOrderOf_of_coprime : ∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
  AddCommute x y → (addOrderOf x).Coprime (addOrderOf y) → addOrderOf (x + y) = addOrderOf x * addOrderOf y
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.prod_nonneg : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f : ι → R} {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → 0 ≤ ∏ i ∈ s, f i
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsSubordinate.mono : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} [inst : Fintype ι]
  {π : BoxIntegral.TaggedPrepartition I},
  π.IsSubordinate r₁ → (∀ x ∈ BoxIntegral.Box.Icc I, r₁ x ≤ r₂ x) → π.IsSubordinate r₂
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_X_pow_left : ∀ {R : Type u_1} [inst : CommRing R] (g : Polynomial R) (m n : ℕ),
  g.natDegree ≤ n → (Polynomial.X ^ m).resultant g m n = g.coeff 0 ^ m
-- Init.Data.BitVec.Bitblast
BitVec.adcb.eq_1 : ∀ (x y c : Bool), BitVec.adcb x y c = (x.atLeastTwo y c, x ^^ (y ^^ c))
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.subset_union : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} [inst_1 : SetLike S G] [SubgroupClass S G] [inst : LE S]
  [IsConcreteLE S G] {H K L : S}, ↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.const.inj : ∀ {a : Lean.Name} {a_1 : ℕ} {a_2 : Lean.Name} {a_3 : ℕ},
  Lean.Meta.LazyDiscrTree.Key.const a a_1 = Lean.Meta.LazyDiscrTree.Key.const a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.commandCtx.injEq : ∀ (info info_1 : Lean.Elab.CommandContextInfo),
  (Lean.Elab.PartialContextInfo.commandCtx info = Lean.Elab.PartialContextInfo.commandCtx info_1) = (info = info_1)
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.neg_eq_self : ∀ {G : Type u_2} [inst : AddGroup G] {K : ℝ} {A : Set G}, IsApproximateAddSubgroup K A → -A = A
-- Mathlib.FieldTheory.Cardinality
Fintype.not_isField_of_card_not_prime_pow : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Ring α], ¬IsPrimePow (Fintype.card α) → ¬IsField α
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} {e : ↑(p ⁻¹' {x})}
  {γ : FundamentalGroup X x} {g : (Multiplicative G)ᵐᵒᵖ},
  (hp.fundamentalGroupToMulOpposite e) γ = g ↔ MulOpposite.unop g • ↑e = ↑(⋯.monodromy γ e)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The source of a 1-simplex in a path is identified with the source vertex.  -/
SSet.Truncated.Path.arrow_src : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} {m : ℕ} (f : X.Path m) (i : Fin m),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op))
      (f.arrow i) =
    f.vertex i.castSucc
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_subset_Ioo_left : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₁ ≤ a₂ → Set.Ioo a₂ b ⊆ Set.Ioo a₁ b
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearEquiv.analyticOnNhd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E ≃L[𝕜] F)
  (s : Set E), AnalyticOnNhd 𝕜 (⇑f) s
-- Mathlib.Algebra.Lie.Basic
LinearMap.instLieRingModule : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [inst_5 : LieRingModule L M] →
                    [LieModule R L M] →
                      [inst_7 : AddCommGroup N] →
                        [inst_8 : Module R N] →
                          [inst_9 : LieRingModule L N] → [LieModule R L N] → LieRingModule L (M →ₗ[R] N)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.toSubsemiring_eq_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  S.toSubsemiring = ⊤ ↔ S = ⊤
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compress_mem_compression_of_mem_compression : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α],
  a ∈ UV.compression u v s → UV.compress u v a ∈ UV.compression u v s
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.mctx : Lean.Meta.AbstractMVars.State → Lean.MetavarContext
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.erase_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α} {c : ℕ},
  (Std.HashMap.Raw.emptyWithCapacity c).erase k = Std.HashMap.Raw.emptyWithCapacity c
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.bInter : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set (Set Ω)}
  {s' : Set (Set Ω)} {u : Set ι},
  (∃ n ∈ u, ProbabilityTheory.IndepSets (s n) s' μ) → ProbabilityTheory.IndepSets (⋂ n ∈ u, s n) s' μ
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.quotientCompQhIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (f : K ⟶ L),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map f) ((DerivedCategory.quotientCompQhIso C).inv.app L) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C).inv.app K)
      (DerivedCategory.Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f))
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.Map.arrows_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (S : CategoryTheory.Subgroupoid C) {c d : D}
  (f : c ⟶ d),
  CategoryTheory.Subgroupoid.Map.Arrows φ hφ S c d f ↔
    ∃ a b g,
      ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
        f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))
-- Init.Data.Int.Order
Int.sub_right_lt_of_lt_add : ∀ {a b c : ℤ}, a < b + c → a - c < b
-- Mathlib.Condensed.Discrete.Basic
Condensed.underlying_obj : ∀ (C : Type w) [inst : CategoryTheory.Category.{u + 1, w} C]
  (j : CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) C),
  (Condensed.underlying C).obj j = j.obj.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_naturality_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z Z' : C} (f : Z ⟶ Z') {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z') ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f)) h)
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin_insert : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α},
  t ∈ nhdsWithin a (insert a s) ↔ a ∈ t ∧ t ∈ nhdsWithin a s
-- Init.Data.Iterators.Consumers.Access
_private.Init.Data.Iterators.Consumers.Access.0.Std.Iter.atIdxSlow?.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    (it : Std.Iter β) →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) →
                  motive ⟨Std.IterStep.yield it' out, property⟩) →
            ((it' : Std.Iter β) →
                (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩) →
              ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.eventually_isPartition : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι),
  ∀ᶠ (π : BoxIntegral.TaggedPrepartition I) in BoxIntegral.IntegrationParams.toFilteriUnion I ⊤, π.IsPartition
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGT_eq_next : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p < s.rawEndPos} (h' : String.Pos.Raw.IsValidForSlice s p),
  s.posGT p h = (s.pos p h').next ⋯
-- Std.Data.DHashMap.Basic
/-- Creates a hash map from an array of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.DHashMap.Const.unitOfArray : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Std.DHashMap α fun x => Unit
-- Mathlib.Analysis.CStarAlgebra.Unitization
/-- The minimal unitization (over `ℂ`) of a C⋆-algebra, equipped with the C⋆-norm. When `A` is
unital, `A⁺¹ ≃⋆ₐ[ℂ] (ℂ × A)`.  -/
CStarAlgebra.«term_⁺¹» : Lean.TrailingParserDescr
-- Mathlib.Data.Fintype.Defs
/-- `univ` is the universal finite set of type `Finset α` implied from
the assumption `Fintype α`.  -/
Finset.univ : {α : Type u_1} → [Fintype α] → Finset α
-- Lean.Meta.LitValues
/-- Return `some ⟨n, v⟩` if `e` is an `OfNat.ofNat` application encoding a `Fin n` with value `v`  -/
Lean.Meta.getFinValue? : Lean.Expr → Lean.MetaM (Option ((n : ℕ) × Fin n))
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_ι_top : ∀ {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), t.eTruncLTι ⊤ = CategoryTheory.CategoryStruct.id (t.eTruncLT.obj ⊤)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.ematch.inj : ∀ {thm thm_1 : Lean.Meta.Grind.EMatchTheorem},
  Lean.Meta.Grind.Entry.ematch thm = Lean.Meta.Grind.Entry.ematch thm_1 → thm = thm_1
-- Mathlib.RingTheory.Localization.Finiteness
Submodule.of_localizationSpan' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  (s : Set R),
  Ideal.span s = ⊤ →
    ∀ {Mₚ : ↑s → Type u_1} [inst_3 : (g : ↑s) → AddCommMonoid (Mₚ g)] [inst_4 : (g : ↑s) → Module R (Mₚ g)]
      {Rₚ : ↑s → Type u_2} [inst_5 : (g : ↑s) → CommSemiring (Rₚ g)] [inst_6 : (g : ↑s) → Algebra R (Rₚ g)]
      [inst_7 : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)] [inst_8 : (g : ↑s) → Module (Rₚ g) (Mₚ g)]
      [inst_9 : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)] (ϕ : (g : ↑s) → M →ₗ[R] Mₚ g)
      [inst_10 : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)],
      (∀ (g : ↑s), (Submodule.localized' (Rₚ g) (Submonoid.powers ↑g) (ϕ g) N).FG) → N.FG
-- Mathlib.Data.Holor
Holor.cprankMax_upper_bound : ∀ {α : Type} [inst : Semiring α] {ds : List ℕ} (x : Holor α ds), Holor.CPRankMax ds.prod x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The natural transformation `S.cycles ⟶ S.X₂` for all short complexes `S`.  -/
CategoryTheory.ShortComplex.iCyclesNatTrans : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          CategoryTheory.ShortComplex.cyclesFunctor C ⟶ CategoryTheory.ShortComplex.π₂
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.Model.0.Lean.Meta.Grind.Arith.Cutsat.getCutsatAssignment? : Lean.Meta.Grind.Goal → Lean.Meta.Grind.ENode → IO (Option ℚ)
-- Mathlib.CategoryTheory.Monad.Coequalizer
/-- The Beck cofork is a split coequalizer.  -/
CategoryTheory.Monad.beckSplitCoequalizer : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → (X : T.Algebra) → CategoryTheory.IsSplitCoequalizer (T.map X.a) (T.μ.app X.A) X.a
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExcept.eq_1 : ∀ (L : PeriodPair) (l₀ z : ℂ),
  L.weierstrassPExcept l₀ z = ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.IsStableUnderBaseChange.mem_coverings_of_isPullback : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C}
  [self : J.IsStableUnderBaseChange] {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S →
    ∀ {Y : C} (g : Y ⟶ S) {P : ι → C} (p₁ : (i : ι) → P i ⟶ Y) (p₂ : (i : ι) → P i ⟶ X i),
      (∀ (i : ι), CategoryTheory.IsPullback (p₁ i) (p₂ i) g (f i)) →
        CategoryTheory.Presieve.ofArrows P p₁ ∈ J.coverings Y
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Submodule.mem_span_iff_exists_finset_subset : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {x : M}, x ∈ Submodule.span R s ↔ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_hom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasCokernel f]
  [inst_7 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_8 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_9 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_10 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_11 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_12 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_13 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))]
  [inst_14 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  (CategoryTheory.Abelian.PreservesCoimageImageComparison.iso F f).hom.right =
    (CategoryTheory.Abelian.PreservesImage.iso F f).hom
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.martingale_zero : ∀ {Ω : Type u_1} (E : Type u_2) {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] (ℱ : MeasureTheory.Filtration ι m0)
  (μ : MeasureTheory.Measure Ω), MeasureTheory.Martingale 0 ℱ μ
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_comap : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {s : Subsemiring S} {f : R →+* S}
  {x : R}, x ∈ Subsemiring.comap f s ↔ f x ∈ s
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.Units.complexConj_eq_self_iff : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (u : (NumberField.RingOfIntegers K)ˣ),
  (NumberField.IsCMField.complexConj K) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u) =
      (algebraMap (NumberField.RingOfIntegers K) K) ↑u ↔
    ∃ v,
      (algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)) K) ↑v =
        (algebraMap (NumberField.RingOfIntegers K) K) ↑u
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_erase!_eq_of_not_compare_minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k fallback : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ¬compare k (t.minKeyD fallback) = Ordering.eq →
          (Std.DTreeMap.Internal.Impl.erase! k t).minKeyD fallback = t.minKeyD fallback
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.bound : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G},
  IsBoundedBilinearMap 𝕜 f → ∃ C > 0, ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
-- Mathlib.Data.ULift
PLift.map_bijective : ∀ {α : Sort u} {β : Sort v} {f : α → β}, Function.Bijective (PLift.map f) ↔ Function.Bijective f
-- Batteries.Data.UnionFind.Basic
/-- Find root of a union-find node, updating the structure using path compression.  -/
Batteries.UnionFind.findN : {n : ℕ} → (self : Batteries.UnionFind) → Fin n → n = self.size → Batteries.UnionFind × Fin n
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Affine equivalence between two equal affine subspace.

This is the affine version of `LinearEquiv.ofEq`.  -/
AffineEquiv.ofEq : {k : Type u_1} →
  {V₁ : Type u_2} →
    {P₁ : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] →
            [inst_3 : AddTorsor V₁ P₁] →
              (S₁ S₂ : AffineSubspace k P₁) →
                [inst_4 : Nonempty ↥S₁] → [inst_5 : Nonempty ↥S₂] → S₁ = S₂ → ↥S₁ ≃ᵃ[k] ↥S₂
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.eval₂_unique : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} {a : S}
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R]
  [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ →
    PowerSeries.HasEval a →
      ∀ {ε : PowerSeries R → S},
        Continuous ε → (∀ (p : Polynomial R), ε ↑p = Polynomial.eval₂ φ a p) → ε = PowerSeries.eval₂ φ a