mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : (CategoryTheory.Limits.Cocone F)ᵒᵖ),
  CategoryTheory.Limits.coneRightOpOfCoconeEquiv.functor.obj c =
    CategoryTheory.Limits.coneRightOpOfCocone (Opposite.unop c)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_comap : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s : NonUnitalSubring S) (f : F),
  ↑(NonUnitalSubring.comap f s) = ⇑f ⁻¹' ↑s
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.symm : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple h e f → IsSl2Triple (-h) f e
-- Mathlib.Data.Quot
/-- A version of `Quotient.inductionOn₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit
arguments instead of instance arguments.  -/
Quotient.inductionOn₂' : ∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁ → Quotient s₂ → Prop}
  (q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → p q₁ q₂
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nnnorm_eq_add : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β],
  p ≠ ⊤ → ∀ (f : WithLp p (α × β)), ‖f‖₊ = (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_and : ∀ {w : ℕ} {x y : BitVec w} {start len : ℕ},
  BitVec.extractLsb' start len (x &&& y) = BitVec.extractLsb' start len x &&& BitVec.extractLsb' start len y
-- Mathlib.Data.Finsupp.Basic
/-- `Finsupp.filter p f` is the finitely supported function that is `f a` if `p a` is true and `0`
otherwise.  -/
Finsupp.filter : {α : Type u_1} → {M : Type u_5} → [inst : Zero M] → (p : α → Prop) → [DecidablePred p] → (α →₀ M) → α →₀ M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α}
  (h : k ∈ Std.ExtDHashMap.filterMap f m), (f (m.getKey k ⋯) (Std.ExtDHashMap.Const.get m k ⋯)).isSome = true
-- Mathlib.Order.Defs.LinearOrder
max_self : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α), max a a = a
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter.mk.inj : ∀ {fvar? type? : Option Lean.Expr} {idx : ℕ} {appearsInTypeProof : Bool} {fvar?_1 type?_1 : Option Lean.Expr}
  {idx_1 : ℕ} {appearsInTypeProof_1 : Bool},
  { fvar? := fvar?, type? := type?, idx := idx, appearsInTypeProof := appearsInTypeProof } =
      { fvar? := fvar?_1, type? := type?_1, idx := idx_1, appearsInTypeProof := appearsInTypeProof_1 } →
    fvar? = fvar?_1 ∧ type? = type?_1 ∧ idx = idx_1 ∧ appearsInTypeProof = appearsInTypeProof_1
-- Mathlib.Data.EReal.Basic
EReal.range_coe : Set.range Real.toEReal = {⊥, ⊤}ᶜ
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.ObjectProperty.HasInducedTStructure.mk : ∀ {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]
  {P : CategoryTheory.ObjectProperty C} {t : CategoryTheory.Triangulated.TStructure C} [inst_6 : P.IsTriangulated],
  (∀ (A : C),
      P A →
        ∃ X Y,
          ∃ (_ : t.IsLE X 0) (_ : t.IsGE Y 1),
            ∃ f g h,
              ∃ (_ :
                CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
                  CategoryTheory.Pretriangulated.distinguishedTriangles),
                P.isoClosure X ∧ P.isoClosure Y) →
    P.HasInducedTStructure t
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The map `ComposableArrows C m → ComposableArrows C n` obtained by precomposition with
a functor `Fin (n + 1) ⥤ Fin (m + 1)`.  -/
CategoryTheory.ComposableArrows.whiskerLeft : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n m : ℕ} →
      CategoryTheory.ComposableArrows C m →
        CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1)) → CategoryTheory.ComposableArrows C n
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.sylvesterMap.congr_simp : ∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f f_1 : Polynomial R) (e_f : f = f_1) (g g_1 : Polynomial R)
  (e_g : g = g_1) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n), f.sylvesterMap g hf hg = f_1.sylvesterMap g_1 ⋯ ⋯
-- Mathlib.Algebra.Group.Hom.Instances
instIsLeftCancelAddAddMonoidHom : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] [IsLeftCancelAdd N],
  IsLeftCancelAdd (M →+ N)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` has a finite
limit `c` almost surely at `a`, then the derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-c`.  -/
intervalIntegral.deriv_integral_of_tendsto_ae_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        deriv (fun u => ∫ (x : ℝ) in u..b, f x) a = -c
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_ofReal_pow : ∀ {K : Type u_1} [inst : RCLike K] (a : ℝ) (n : ℕ), RCLike.im (↑a ^ n) = 0
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- The space of `E`-valued measures on `X`, i.e. continuous linear maps `C(X, R) → E`. (The case
`R = E` is the most important case.)

This is the same space `C(X, R) →L[R] E`, but we do not want it to inherit the default
(norm) topology, so we make a type synonym.
 -/
AbstractMeasure.«termD(_,_)» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.π_homologyMap_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂) {Z : C}
  (h : S₂.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.homologyπ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ)
        (CategoryTheory.CategoryStruct.comp S₂.homologyι h)) =
    CategoryTheory.CategoryStruct.comp S₁.iCycles
      (CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp S₂.pOpcycles h))
-- Mathlib.Order.Cover
toDual_wcovBy_toDual_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, OrderDual.toDual b ⩿ OrderDual.toDual a ↔ a ⩿ b
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Iso.toEquiv_apply : ∀ {X Y : Type u} (i : X ≅ Y) (a : X), i.toEquiv a = (CategoryTheory.ConcreteCategory.hom i.hom) a
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : Y ⟶ X) (S : CategoryTheory.Sieve X) (x : C)
  (sl : x ⟶ Y), (CategoryTheory.Sieve.pullback h S).arrows sl = S.arrows (CategoryTheory.CategoryStruct.comp sl h)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.Ordering.swap.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Mathlib.Data.ENNReal.BigOperators
/-- A sum is finite iff all summands are finite.  -/
ENNReal.sum_lt_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, ∑ a ∈ s, f a < ⊤ ↔ ∀ a ∈ s, f a < ⊤
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.toFun'.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj), ↑e = ↑e.toPartialEquiv
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- A function `f` is **Lipschitz continuous** with constant `K ≥ 0` **on `s`** if
for all `x, y` in `s` we have `dist (f x) (f y) ≤ K * dist x y`.  -/
LipschitzOnWith : {α : Type u} → {β : Type v} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → NNReal → (α → β) → Set α → Prop
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.doubleL.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rk : α) (rv : β rk) (rlk : α)
  (rlv : β rlk) (rll rlr rr : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.doubleL k v l rk rv rlk rlv rll rlr rr =
    Std.DTreeMap.Internal.Impl.bin rlk rlv (Std.DTreeMap.Internal.Impl.bin k v l rll)
      (Std.DTreeMap.Internal.Impl.bin rk rv rlr rr)
-- Std.Data.ExtTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.ExtTreeMap.entryAtIdx! : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtTreeMap α β cmp → ℕ → α × β
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ⟶ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
                        (θ.naturality f).hom =
                      CategoryTheory.CategoryStruct.comp (η.naturality f).hom
                        (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
                  CategoryTheory.Oplax.StrongTrans.Modification.naturality._autoParam →
                CategoryTheory.Oplax.StrongTrans.Modification η θ
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
/-- Auxiliary definition for `isLimit`.  -/
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {H : J.OneHypercoverFamily} →
            {P : CategoryTheory.Functor Cᵒᵖ A} →
              (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) →
                {X : C} →
                  {S : CategoryTheory.Sieve X} →
                    {E : J.OneHypercover X} →
                      H E →
                        (le : E.sieve₀ ≤ S) →
                          (F :
                              CategoryTheory.Limits.Multifork
                                (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) →
                            F.pt ⟶ P.obj (Opposite.op X)
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α} [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (choice : (x : β) → x ≤ l (u x) → α) (gc : GaloisConnection l u) (u_l_le : ∀ (x : α), u (l x) ≤ x)
  (choice_eq : ∀ (a : β) (h : a ≤ l (u a)), choice a h = u a),
  sizeOf { choice := choice, gc := gc, u_l_le := u_l_le, choice_eq := choice_eq } = 1
-- Init.Data.List.Nat.Basic
List.dropLast.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : List α) (h_1 : Unit → motive []) (h_2 : (head : α) → motive [head])
  (h_3 : (a : α) → (as : List α) → motive (a :: as)) (head : α),
  x = [head] →
    (match x with
      | [] => h_1 ()
      | [head] => h_2 head
      | a :: as => h_3 a as) ≍
      h_2 head
-- Mathlib.RingTheory.Ideal.Prime
/-- The complement of a prime ideal `P ⊆ R` is a submonoid of `R`.  -/
Ideal.primeCompl : {α : Type u} → [inst : Semiring α] → (P : Ideal α) → [hp : P.IsPrime] → Submonoid α
-- Mathlib.Order.Filter.Finite
Filter.iInf_sets_eq_finite' : ∀ {α : Type u} {ι : Sort x} (f : ι → Filter α), (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i.down).sets
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.sSup_ringCon : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] (S : Set (TwoSidedIdeal R)),
  (sSup S).ringCon = sSup (TwoSidedIdeal.ringCon '' S)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_not_measurableSet : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  ¬MeasurableSet s → ∫ᵛ (x : X) in s, f x ∂[B; μ] = 0
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.uSwitch_map_uSwitch_map : ∀ {X Y : FintypeCat} (f : X ⟶ Y),
  FintypeCat.uSwitch.map (FintypeCat.uSwitch.map f) =
    CategoryTheory.CategoryStruct.comp
      (FintypeCat.equivEquivIso ((FintypeCat.uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).hom
      (CategoryTheory.CategoryStruct.comp f
        (FintypeCat.equivEquivIso ((FintypeCat.uSwitch.obj Y).uSwitchEquiv.trans Y.uSwitchEquiv)).inv)
-- Mathlib.NumberTheory.PrimesCongruentOne
/-- For any positive `k : ℕ` there are infinitely many primes `p` such that `p ≡ 1 [MOD k]`.  -/
Nat.infinite_setOfPred_prime_modEq_one : ∀ {k : ℕ}, k ≠ 0 → {p | Nat.Prime p ∧ p ≡ 1 [MOD k]}.Infinite
-- Lean.Meta.IndPredBelow
/-- Records below proofs and motive proofs available. This is extended using `NewDecl`s while visiting
and rewriting match expressions.
 -/
Lean.Meta.IndPredBelow.RecursionContext : Type
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_bot_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (q : Submodule R N), Submodule.map₂ f ⊥ q = ⊥
-- Std.Time.Date.Unit.Month
_private.Std.Time.Date.Unit.Month.0.Std.Time.Month.Ordinal.clipDay.eq_1 : ∀ (leap : Bool) (month : Std.Time.Month.Ordinal) (day : Std.Time.Day.Ordinal),
  Std.Time.Month.Ordinal.clipDay leap month day =
    if ↑day > ↑(Std.Time.Month.Ordinal.days leap month) then Std.Time.Month.Ordinal.days leap month else day
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionItemCapabilities.mk.inj : ∀ {insertReplaceSupport? insertReplaceSupport?_1 : Option Bool},
  { insertReplaceSupport? := insertReplaceSupport? } = { insertReplaceSupport? := insertReplaceSupport?_1 } →
    insertReplaceSupport? = insertReplaceSupport?_1
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyLift_id_toSheafify_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) {Z : CategoryTheory.Functor Cᵒᵖ D}
  (h : CategoryTheory.sheafify J P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P) hP)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) h) =
    h
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.WithDensityᵥEq.congr_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f g : α → E}, f =ᵐ[μ] g → μ.withDensityᵥ f = μ.withDensityᵥ g
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat_7 : {α : Type u} → Std.Rio.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Std.Http.Data.URI.Basic
/-- Returns the URI scheme for a given port: `"https"` for 443, `"http"` otherwise.
 -/
Std.Http.URI.Scheme.ofPort : UInt16 → Std.Http.URI.Scheme
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.IsRightAdjoint.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {right : CategoryTheory.Functor D C}, (∃ left, Nonempty (left ⊣ right)) → right.IsRightAdjoint
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instOneValueGroupWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : ValuativeRel R] → One (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.Topology.MetricSpace.Basic
/-- A map between metric spaces is a uniform embedding if and only if the distance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y` and conversely.  -/
Metric.isUniformEmbedding_iff' : ∀ {β : Type v} {γ : Type w} [inst : MetricSpace γ] [inst_1 : PseudoMetricSpace β] {f : γ → β},
  IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.preservesLimitsOfShape_of_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_4 : CategoryTheory.Category.{v₄, u₄} B] (H : CategoryTheory.Functor E B)
  [CategoryTheory.Limits.PreservesLimitsOfShape C H], CategoryTheory.Limits.PreservesLimitsOfShape D H
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.vanishingIdeal_closure : ∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)),
  PrimeSpectrum.vanishingIdeal (closure t) = PrimeSpectrum.vanishingIdeal t
-- Mathlib.Algebra.Order.Group.Indicator
Function.support_iSup : ∀ {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : ConditionallyCompleteLattice M] [Nonempty ι]
  (f : ι → α → M), (Function.support fun x => ⨆ i, f i x) ⊆ ⋃ i, Function.support (f i)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zsmul_mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] (g : G) (k : ℤ), k • g ∈ AddSubgroup.zmultiples g
-- Mathlib.Order.WithBot
/-- **Alias** of the reverse direction of `WithBot.strictMono_map_iff`. -/
StrictMono.withBot_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → StrictMono (WithBot.map f)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atBot_principal : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {f : α → β} {s : Set β},
  Filter.Tendsto f Filter.atBot (Filter.principal s) ↔ ∃ N, ∀ n ≤ N, f n ∈ s
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.subgroupOfPrimitiveMapToOne.eq_1 : ∀ (R : Type u_1) [inst : CommMonoidWithZero R] (n : ℕ) [inst_1 : NeZero n] (p : ℕ) [hp : Fact (Nat.Prime p)],
  DirichletCharacter.subgroupOfPrimitiveMapToOne R n p =
    Subgroup.map (DirichletCharacter.changeLevel ⋯) (DirichletCharacter.annihilator R {ZMod.unitOfCoprime p ⋯})
-- Mathlib.Order.Hom.Basic
/-- `Prod.map` of two `OrderHom`s as an `OrderHom`  -/
OrderHom.prodMap : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      {δ : Type u_5} →
        [inst : Preorder α] →
          [inst_1 : Preorder β] → [inst_2 : Preorder γ] → [inst_3 : Preorder δ] → (α →o β) → (γ →o δ) → α × γ →o β × δ
-- Batteries.Recycling.RBTree.Depth
_private.Batteries.Recycling.RBTree.Depth.0.RBTree.RBNode.depthLB.match_1.eq_1 : ∀ (motive : RBTree.RBColor → ℕ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive RBTree.RBColor.red n)
  (h_2 : (n : ℕ) → motive RBTree.RBColor.black n),
  (match RBTree.RBColor.red, n with
    | RBTree.RBColor.red, n => h_1 n
    | RBTree.RBColor.black, n => h_2 n) =
    h_1 n
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.ByteArray.validateUTF8.go.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : true = false → motive false) (h_2 : true = true → motive true),
  (match h : true with
    | false => h_1 h
    | true => h_2 h) =
    h_2 ⋯
-- Init.PropLemmas
and_rotate : ∀ {a b c : Prop}, a ∧ b ∧ c ↔ b ∧ c ∧ a
-- Std.Time.Duration
Std.Time.Duration.instHSub : HSub Std.Time.Duration Std.Time.Duration Std.Time.Duration
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_id : ∀ {α : Type u_1} {m : MeasurableSpace α}, MeasurableSpace.map id m = m
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorδ_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ W X Y Z)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.SemiCartesianMonoidalCategory.snd W Y)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X Z)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommSemigroupOfMulHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → CommSemigroup (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)],
  DirectLimit.instCommSemigroupOfMulHomClass = { toSemigroup := DirectLimit.instSemigroupOfMulHomClass, mul_comm := ⋯ }
-- Lean.ProjFns
Lean.Environment.getProjectionFnInfo? : Lean.Environment → Lean.Name → Option Lean.ProjectionFunctionInfo
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  (Std.DHashMap.filterMap f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), (f k (m.get k h)).isSome = true
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasCoproducts_of_colimit_cofans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (cf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Cofan f)
  (cf_isColimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsColimit (cf f)),
  CategoryTheory.Limits.HasCoproducts C
-- Mathlib.Algebra.Group.Basic
eq_iff_eq_of_div_eq_div : ∀ {G : Type u_3} [inst : Group G] {a b c d : G}, a / b = c / d → (a = b ↔ c = d)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_add_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {β : Type u_5} [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] {s t : Finset α} {f : α → β} {a : β}, (s + t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x + y) ≤ a
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.all : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → φ.all.IsPrenex
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) [Inhabited α] {k k' : α} {f : β k → β k}
  (hc : (m.modify k f).contains k' = true), (m.modify k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (r : R), (Polynomial.X - Polynomial.C r).roots = {r}