mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasColimit_inverse_equivalence_comp_iff : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (e : J ≌ K),
  CategoryTheory.Limits.HasColimit (e.inverse.comp F) ↔ CategoryTheory.Limits.HasColimit F
-- Mathlib.RingTheory.Flat.Localization
Module.flat_of_localized_span : ∀ (S : Type u_2) [inst : CommSemiring S] (M : Type u_3) [inst_1 : AddCommMonoid M] [inst_2 : Module S M] (s : Set S),
  Ideal.span s = ⊤ → (∀ (r : ↑s), Module.Flat S (LocalizedModule.Away (↑r) M)) → Module.Flat S M
-- Mathlib.Data.Matrix.Basic
Matrix.transpose_multiset_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : AddCommMonoid α] (s : Multiset (Matrix m n α)),
  s.sum.transpose = (Multiset.map Matrix.transpose s).sum
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instLinearMapClass : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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] [inst_6 : LieModule R L M],
  LinearMapClass (LieDerivation R L M) R L M
-- Mathlib.Algebra.Ring.BooleanRing
RingHom.asBoolAlg_id : ∀ {α : Type u_1} [inst : BooleanRing α], (RingHom.id α).asBoolAlg = BoundedLatticeHom.id (AsBoolAlg α)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_empty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n), s.exradius ∅ = s.inradius
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instFourierPair : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  [CompleteSpace E], FourierPair (SchwartzMap V E) (SchwartzMap V E)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isEmbedding_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α], Topology.IsEmbedding fun x => {x}
-- Mathlib.Topology.MetricSpace.Kuratowski
/-- A metric space can be embedded in `l^∞(ℝ)` via the distances to points in
a fixed countable set, if this set is dense. This map is given in `kuratowskiEmbedding`,
without density assumptions.  -/
KuratowskiEmbedding.embeddingOfSubset : {α : Type u} → [MetricSpace α] → (ℕ → α) → α → ↥(lp (fun x => ℝ) ⊤)
-- Mathlib.Testing.Plausible.Sampleable
Plausible.Rat.shrinkable : Plausible.Shrinkable ℚ
-- Lean.Meta.Basic
Lean.Meta.instInhabitedPostponedEntry.default : Lean.Meta.PostponedEntry
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_pred_assoc : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j) {Z : SSet} (h_1 : SSet.stdSimplex.obj { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE ⋯)
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso i).inv h_1) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.facePairComplIso i j h).inv
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (j.pred ⋯)) h_1)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.id : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n],
  modularCyclotomicCharacter.toFun n (RingEquiv.refl L) = 1
-- Mathlib.Geometry.Manifold.HasGroupoid
_private.Mathlib.Geometry.Manifold.HasGroupoid.0.restr_mem_maximalAtlas_aux2 : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (G : StructureGroupoid H) [ClosedUnderRestriction G] {e e' : OpenPartialHomeomorph M H},
  e ∈ StructureGroupoid.maximalAtlas M G → e' ∈ atlas H M → ∀ {s : Set M}, IsOpen s → e'.symm.trans (e.restr s) ∈ G
-- Init.Data.Int.DivMod.Lemmas
Int.ofNat_fmod : ∀ (m n : ℕ), ↑(m % n) = (↑m).fmod ↑n
-- Mathlib.ModelTheory.Topology.Types
CompleteType.isClopen_typesWith : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} (φ : (L.withConstants α).Sentence), IsClopen (T.typesWith φ)
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.cast' : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} →
        {aig1 aig2 : Std.Sat.AIG α} →
          (s : aig1.RefVec len) →
            ((∀ {i : ℕ} (h : i < len), s.refs[i].gate < aig1.decls.size) →
                ∀ {i : ℕ} (h : i < len), s.refs[i].gate < aig2.decls.size) →
              aig2.RefVec len
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.List.take.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_1 x
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates the colimit of `K` and `F ≅ G`, then `G` creates the colimit of `K`.  -/
CategoryTheory.createsColimitOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F G : CategoryTheory.Functor C D} →
                (F ≅ G) → [CategoryTheory.CreatesColimit K F] → CategoryTheory.CreatesColimit K G
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The inverse has an inverse.  -/
SSet.Edge.InvStruct.invStructInv : {X : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} → {hom : SSet.Edge x₀ x₁} → (I : hom.InvStruct) → I.inv.InvStruct
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → Std.DHashMap.Raw.Const.get? (m₁ ∩ m₂) k = Std.DHashMap.Raw.Const.get? m₁ k
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_eq_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α], t.WF → ∀ {k : α}, t.contains k = true → t.getKey! k = k
-- Mathlib.Control.Fix
Pi.Part.hasFix : {α : Type u_1} → {β : Type u_3} → Fix (α → Part β)
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Copy of a `GenLoop` with a new map from the unit cube equal to the old one.
Useful to fix definitional equalities.  -/
GenLoop.copy : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} → (f : ↑(GenLoop N X x)) → (g : (N → ↑unitInterval) → X) → g = ⇑f → ↑(GenLoop N X x)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Init.Data.Float.Float32
instDivFloat32 : Div Float32
-- Mathlib.Topology.Order
/-- **Alias** of `setOfPred_isOpen_iSup`. -/
setOf_isOpen_iSup : ∀ {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α}, {s | IsOpen s} = ⋂ i, {s | IsOpen s}
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.coeff_mul_right_one_sub_of_lt_weightedOrder : ∀ {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [inst : Ring R] {f g : MvPowerSeries σ R} {d : σ →₀ ℕ},
  ↑((Finsupp.weight w) d) < MvPowerSeries.weightedOrder w g →
    (MvPowerSeries.coeff d) ((1 - g) * f) = (MvPowerSeries.coeff d) f
-- Mathlib.Algebra.Order.Group.Basic
zpow_le_zpow_iff_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {m n : ℤ} {a : α},
  1 < a → (a ^ m ≤ a ^ n ↔ m ≤ n)
-- Lean.Compiler.LCNF.Basic
/-- Low-level update `LetDecl` function. It does not update the local context.
Consider using `LetDecl.update : LetDecl → Expr → Expr → CompilerM LetDecl` if you want the local context
to be updated.
 -/
Lean.Compiler.LCNF.LetDecl.updateCore : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetDecl pu → Lean.Expr → Lean.Compiler.LCNF.LetValue pu → Lean.Compiler.LCNF.LetDecl pu
-- Mathlib.CategoryTheory.Sites.Limits
/-- If `E` is a cone which is a limit on the level of presheaves,
then the limit presheaf is again a sheaf.

This is used to show that the forgetful functor from sheaves to presheaves creates limits.
 -/
CategoryTheory.Sheaf.isSheaf_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {K : Type z} [inst_2 : CategoryTheory.Category.{z', z} K]
  [CategoryTheory.Limits.HasLimitsOfShape K D] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D))
  (E : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.sheafToPresheaf J D))) (hE : CategoryTheory.Limits.IsLimit E),
  CategoryTheory.Presheaf.IsSheaf J E.pt
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  a ∈ t.insert k ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.toPiLocalization_apply_apply : ∀ (R : Type u_1) [inst : CommSemiring R] {r : R} {I : MaximalSpectrum R},
  (MaximalSpectrum.toPiLocalization R) r I = (algebraMap R (Localization.AtPrime I.asIdeal)) r
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.card_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → (s ∩ t).card = k
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  P.epiModSerre f → P.isoModSerre f
-- Mathlib.Order.Hom.Basic
OrderHom.le_def : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f g : α →o β}, f ≤ g ↔ ∀ (x : α), f x ≤ g x
-- Mathlib.Data.Multiset.ZeroCons
Multiset.lt_cons_self : ∀ {α : Type u_1} (s : Multiset α) (a : α), s < a ::ₘ s
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l →
    (∀ a ∈ m, l.contains a = false) → (m.insertMany l).size = m.size + l.length
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix_of_matrix_vecMul : ∀ {κ : Type w} {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Fintype κ] (b : κ → B) (P : Matrix κ κ A),
  Algebra.traceMatrix A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.transpose * Algebra.traceMatrix A b * P
-- Std.Time.Date.PlainDate
/-- Creates a new `PlainDate` by adjusting the month to the given `month` value.
The day is rolled over to the next valid month if necessary.
 -/
Std.Time.PlainDate.withMonthRollOver : Std.Time.PlainDate → Std.Time.Month.Ordinal → Std.Time.PlainDate
-- Init.Prelude
/-- Increments the macro scope counter so that inside the body of `x` the macro
scope is fresh.
 -/
Lean.Macro.withFreshMacroScope : {α : Type} → Lean.MacroM α → Lean.MacroM α
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {Y : CategoryTheory.Abelian.SpectralObject C EInt},
  (∀ (i j : EInt) (hij : i ≤ j),
      WithBotTop.coe 0 < i →
        ∀ (n : ℤ),
          CategoryTheory.Limits.IsZero
            ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))) →
    (∀ (i j : EInt) (hij : i ≤ j) (n : ℤ),
        j ≤ WithBotTop.coe n →
          CategoryTheory.Limits.IsZero
            ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))) →
      Y.IsThirdQuadrant
-- Lean.Declaration
Lean.instInhabitedInductiveVal : Inhabited Lean.InductiveVal
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isIntegral_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsIntegral Y]
  [Nonempty ↥X], AlgebraicGeometry.IsIntegral X
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpArgs.fvarIds : Lean.Elab.Tactic.Grind.DSimpArgs → Array Lean.FVarId
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctor_η : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] (F : M →* N),
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Discrete.monoidalFunctor F) = CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.compSubConstCLM_zero : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F],
  SchwartzMap.compSubConstCLM 𝕜 0 = ContinuousLinearMap.id 𝕜 (SchwartzMap E F)
-- Std.Time.Format.Basic
Std.Time.FormatConfig.mk.inj : ∀ {allowLeapSeconds : Bool} {dateformat : Std.Time.DateFormat} {allowLeapSeconds_1 : Bool}
  {dateformat_1 : Std.Time.DateFormat},
  { allowLeapSeconds := allowLeapSeconds, dateformat := dateformat } =
      { allowLeapSeconds := allowLeapSeconds_1, dateformat := dateformat_1 } →
    allowLeapSeconds = allowLeapSeconds_1 ∧ dateformat = dateformat_1
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.le_iff_forall_le : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α], Order.IsPredLimit a → (b ≤ a ↔ ∀ (c : α), a < c → b ≤ c)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List α} {k : α},
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l) k =
        if k ∈ t ∨ l.contains k = true then some () else none
-- Mathlib.Algebra.Star.StarAlgHom
instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B]
  [inst_5 : EquivLike F A B] [NonUnitalAlgEquivClass F R A B], NonUnitalAlgHomClass F R A B
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalConvConvSeq : Lean.Elab.Tactic.Tactic
-- Mathlib.Order.Hom.Lattice
InfHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β],
  InfHom.instFunLike = { coe := InfHom.toFun, coe_injective := ⋯ }
-- Init.Notation
/-- `a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. -/
«term_/_» : Lean.TrailingParserDescr
-- Lean.Elab.App
Lean.Elab.Term.instInhabitedElabElimInfo.default : Lean.Elab.Term.ElabElimInfo
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.strictLimitsOfShape.limit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasLimit F],
  (∀ (j : J), P (F.obj j)) → P.strictLimitsOfShape J (CategoryTheory.Limits.limit F)
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.nu_mult : ∀ (self : BoundingSieve), self.nu.IsMultiplicative
-- Mathlib.Data.Finset.Sups
Finset.image_subset_infs_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α} {a : α},
  a ∈ s → Finset.image (fun x => a ⊓ x) t ⊆ s ⊼ t
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_uIoo_castLE : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.uIoo (Fin.castLE h i) (Fin.castLE h j) = Set.uIoo i j
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- **Alias** of `Metric.Snowflaking.image_ofSnowflaking_eball`. -/
Metric.Snowflaking.image_ofSnowflaking_emetricBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  (d : ENNReal),
  ⇑Metric.Snowflaking.ofSnowflaking '' Metric.eball x d = Metric.eball (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.forM_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : α × β → m PUnit.{w + 1}},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → forM t₁ f = forM t₂ f
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.eq_zero_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  {m : M}, f m = 0 ↔ ∃ s', s' • m = 0
-- Init.Data.Array.Monadic
Array.filterMapM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → Prop}
  {xs : Array { x // p x }} {f : { x // p x } → m (Option β)} {g : α → m (Option β)},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → stop = xs.size → Array.filterMapM f xs 0 stop = Array.filterMapM g xs.unattach
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey? t.maxKey! = some t.maxKey!
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_inv : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (x : ↥s), ↑x⁻¹ = (↑x)⁻¹
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.id_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) (n : ι), (Algebra.Generators.Hom.id P).val n = MvPolynomial.X n
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.Precoverage.preZeroHypercoverFamily_property : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C) (X : C)
  (E : CategoryTheory.PreZeroHypercover X), K.preZeroHypercoverFamily.property E = (E.presieve₀ ∈ K.coverings X)
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.prodFan.eq_1 : ∀ (A B : CommRingCat),
  A.prodFan B =
    CategoryTheory.Limits.BinaryFan.mk (CommRingCat.ofHom (RingHom.fst ↑A ↑B)) (CommRingCat.ofHom (RingHom.snd ↑A ↑B))
-- Mathlib.Order.DirectedInverseSystem
/-- "Nullary map" to construct an element in the direct limit.  -/
DirectLimit.map₀ : {ι : Type u_1} →
  [inst : Preorder ι] →
    {F : ι → Type u_4} →
      {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} →
        (f : (i j : ι) → (h : i ≤ j) → T h) →
          [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] →
            [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] → [Nonempty ι] → ((i : ι) → F i) → DirectLimit F f
-- Mathlib.Data.Multiset.MapFold
Multiset.forall_mem_map_iff : ∀ {α : Type u_1} {β : Type v} {f : α → β} {p : β → Prop} {s : Multiset α},
  (∀ y ∈ Multiset.map f s, p y) ↔ ∀ x ∈ s, p (f x)
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- **Alias** of `MeasureTheory.Measure.AbsolutelyContinuous.rfl`. -/
MeasureTheory.Measure.absolutelyContinuous_rfl : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.AbsolutelyContinuous μ
-- Mathlib.Order.LiminfLimsup
Filter.exists_forall_mem_of_hasBasis_mem_blimsup' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : Filter β} {b : ι → Set β},
  l.HasBasis (fun x => True) b →
    ∀ {u : β → Set α} {p : β → Prop} {x : α},
      x ∈ Filter.blimsup u l p → ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.injective_ofFn : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] (n : ℕ), Function.Injective ⇑(Polynomial.ofFn n)
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
/-- A generic monic polynomial of degree `n` as an element of the
free commutative ring in `n + 1` variables, with a variable for each
of the `n` non-leading coefficients of the polynomial and one variable (`Fin.last n`)
for `X`.  -/
FirstOrder.Field.genericMonicPoly : (n : ℕ) → FreeCommRing (Fin (n + 1))
-- Mathlib.NumberTheory.Bernoulli
bernoulli'PowerSeries_mul_exp_sub_one : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : Algebra ℚ A],
  bernoulli'PowerSeries A * (PowerSeries.exp A - 1) = PowerSeries.X * PowerSeries.exp A
-- Mathlib.Dynamics.Ergodic.Action.Regular
instErgodicSMulMulOppositeOfIsMulRightInvariant : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsMulRightInvariant], ErgodicSMul Gᵐᵒᵖ G μ
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instBot : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → Bot (CategoryTheory.Precoverage C)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
      CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f)
          (J.isoRightDerivedToHomotopyCategoryObj F).hom =
        CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom
          (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ)
-- Mathlib.RepresentationTheory.Rep.Res
Rep.instPreservesLimitsResFunctor : ∀ {G : Type v1} {H : Type v2} [inst : Monoid G] [inst_1 : Monoid H] (f : H →* G) {k : Type u} [inst_2 : Ring k],
  CategoryTheory.Limits.PreservesLimits (Rep.resFunctor f)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- Any rank-at-most-one valuation has a mul-archimedean value group.
The converse (for any compatible valuation) is `ValuativeRel.isRankLeOne_iff_mulArchimedean`
which is in a later file since it requires a larger theory of reals.  -/
ValuativeRel.instMulArchimedeanValueGroupWithZeroOfIsRankLeOne : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [ValuativeRel.IsRankLeOne R],
  MulArchimedean (ValuativeRel.ValueGroupWithZero R)