mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.leftZigzagIso_symm : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  (CategoryTheory.Bicategory.leftZigzagIso η ε).symm = CategoryTheory.Bicategory.rightZigzagIso ε.symm η.symm
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.toFun_eq_coe : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  (f : A →ₑ+[φ] B), f.toFun = ⇑f
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) {X : T} (Y : CategoryTheory.Over X)
  {X_1 Y_1 : CategoryTheory.CostructuredArrow F Y.left} (f : X_1 ⟶ Y_1),
  (CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse F Y).map f =
    CategoryTheory.CostructuredArrow.homMk (CategoryTheory.CostructuredArrow.homMk f.left ⋯) ⋯
-- Init.Data.Option.Lemmas
Option.mem_dite_none_left : ∀ {α : Type u_1} {p : Prop} {x : α} {x_1 : Decidable p} {l : ¬p → Option α},
  (x ∈ if h : p then none else l h) ↔ ∃ (h : ¬p), x ∈ l h
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.

This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
 -/
Std.IterM.Partial.toList : {α : Type w} →
  {m : Type w → Type w'} → [Monad m] → {β : Type w} → [Std.Iterator α m β] → Std.IterM.Partial m β → m (List β)
-- Mathlib.Order.CompleteLattice.Group
iSup₂_mul_le : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] [inst_1 : Mul α] [MulLeftMono α]
  [MulRightMono α] (u v : (i : ι) → κ i → α), ⨆ i, ⨆ j, u i j * v i j ≤ (⨆ i, ⨆ j, u i j) * ⨆ i, ⨆ j, v i j
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_def : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ),
  κ.compProd η =
    (((((ProbabilityTheory.Kernel.swap γ β).comp (η.parallelComp ProbabilityTheory.Kernel.id)).comp
                  (ProbabilityTheory.Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯)).comp
              (ProbabilityTheory.Kernel.id.parallelComp (ProbabilityTheory.Kernel.copy β))).comp
          (ProbabilityTheory.Kernel.id.parallelComp κ)).comp
      (ProbabilityTheory.Kernel.copy α)
-- Mathlib.LinearAlgebra.Trace
/-- The trace of a linear map corresponds to the contraction pairing under the isomorphism
`End(M) ≃ M* ⊗ M`  -/
LinearMap.trace_eq_contract_of_basis : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
  [Finite ι] (b : Module.Basis ι R M), LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
-- Mathlib.Analysis.LocallyConvex.Barrelled
/-- The **Banach-Steinhaus** theorem, or **Uniform Boundedness Principle**, for maps from a
barrelled space to any space whose topology is generated by a family of seminorms. Use
`WithSeminorms.equicontinuous_TFAE` and `Seminorm.bound_of_continuous` to get explicit bounds on
the seminorms from equicontinuity.  -/
WithSeminorms.banach_steinhaus : ∀ {ι : Type u_2} {κ : Type u_3} {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} {E : Type u_6} {F : Type u_7}
  [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂} [RingHomIsometric σ₁₂]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₁ E] [inst_6 : Module 𝕜₂ F]
  [inst_7 : UniformSpace E] [inst_8 : UniformSpace F] [IsUniformAddGroup E] [IsUniformAddGroup F] [ContinuousSMul 𝕜₁ E]
  [BarrelledSpace 𝕜₁ E] {𝓕 : ι → E →SL[σ₁₂] F} {q : SeminormFamily 𝕜₂ F κ},
  WithSeminorms q →
    (∀ (k : κ) (x : E), BddAbove (Set.range fun i => (q k) ((𝓕 i) x))) → UniformEquicontinuous (DFunLike.coe ∘ 𝓕)
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The counit of the adjunction `lightCondSetToTopCat ⊣ topCatToLightCondSet` is always bijective,
but not an isomorphism in general (the inverse isn't continuous unless `X` is sequential).
 -/
LightCondSet.topCatAdjunctionCounitEquiv : (X : TopCat) → ↑X.toLightCondSet.toTopCat ≃ ↑X
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.map_comp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms E] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_6 : F.PreservesZeroMorphisms] (G : CategoryTheory.Functor D E)
  [inst_7 : G.PreservesZeroMorphisms], S.map (F.comp G) = (S.map F).map G
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast : ∀ (n : ℕ) [NeZero n] (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [IsFractionRing A K] [IsDomain A] [NeZero ↑n], IsFractionRing (CyclotomicRing n A K) (CyclotomicField n K)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rci.toArray_iter : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rci α}, r.iter.toArray = r.toArray
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePosAssignment.eq_1 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.removePosAssignment =
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- The ideal of `A ⊗[R] B` generated by `I` is the image of `I ⊗[R] B`  -/
Ideal.map_includeLeft_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} {B : Type u_3} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal A),
  Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeLeft I) =
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instLieAddGroupOfSomeENatTopOfLEInfty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {a : WithTop ℕ∞}
  [LieAddGroup I (↑⊤) G] [h : ENat.LEInfty a], LieAddGroup I a G
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.get? (t.maxD fallback) = some (t.maxD fallback)
-- Init.Data.Range.Polymorphic.Fin
Fin.instHasSize_1 : {n : ℕ} → Std.Rxo.HasSize (Fin n)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- the intermediate object in the factorization  -/
CategoryTheory.MorphismProperty.MapFactorizationData.Z : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} → {X Y : C} → {f : X ⟶ Y} → W₁.MapFactorizationData W₂ f → C
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.copy_eq : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (f : A →⋆ₙ+* B) (f' : A → B) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.of_restrictScalars : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] {A : Type u_5}
  [inst_2 : CommSemiring A] [inst_3 : Algebra R A] [inst_4 : Module R M] (S : Submonoid R) {N : Type u_6}
  [inst_5 : AddCommMonoid N] [inst_6 : Module R N] [inst_7 : Module A M] [inst_8 : Module A N]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R A N] (f : M →ₗ[A] N) [IsLocalizedModule S (↑R f)],
  IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncLT : ∀ {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) (X : C) (n : ℤ) [t.IsLE X n] (i : EInt),
  t.IsLE ((t.eTruncLT.obj i).obj X) n
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_symmDiff : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : AsBoolAlg α), ofBoolAlg (symmDiff a b) = ofBoolAlg a + ofBoolAlg b
-- Init.Data.SInt.Lemmas
Int64.add_eq_right : ∀ {a b : Int64}, a + b = b ↔ a = 0
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- If a set `s` separates the absolutely continuous part of `μ` with respect to `ν`
from the singular part, then the singular part equals the restriction of `μ` to `s`.  -/
MeasureTheory.Measure.singularPart_eq_restrict' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α} [μ.HaveLebesgueDecomposition ν],
  (μ.singularPart ν) sᶜ = 0 → (ν.withDensity (μ.rnDeriv ν)) s = 0 → μ.singularPart ν = μ.restrict s
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.toFormula.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ),
  FirstOrder.Language.BoundedFormula.falsum.toFormula = FirstOrder.Language.BoundedFormula.falsum
-- Mathlib.Tactic.ComputeDegree
/-- `tryRfl mvs` takes as input a list of `MVarId`s, scans them partitioning them into two
lists: the goals containing some metavariables and the goals not containing any metavariable.

If a goal containing a metavariable has the form `?_ = x`, `x = ?_`, where `?_` is a metavariable
and `x` is an expression that does not involve metavariables, then it closes this goal using `rfl`,
effectively assigning the metavariable to `x`.

If a goal does not contain metavariables, it tries `rfl` on it.

It returns the list of `MVarId`s, beginning with the ones that initially involved (`Expr`)
metavariables followed by the rest.
 -/
Mathlib.Tactic.ComputeDegree.tryRfl : List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.Group.Submonoid.Finsupp
AddSubmonoid.mem_closure_range_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {ι : Type u_2} {f : ι → M} {x : M},
  x ∈ AddSubmonoid.closure (Set.range f) ↔ ∃ a, x = a.sum fun x1 x2 => x2 • f x1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_diff_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.top_rpow_of_pos : ∀ {y : ℝ}, 0 < y → ⊤ ^ y = ⊤
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.string : Lean.Lsp.SymbolKind
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.unique_zpow_zmod : ∀ {α : Type u_1} {a : α} [inst : Group α] [inst_1 : Fintype α],
  (∀ (x : α), x ∈ Subgroup.zpowers a) → ∀ (x : α), ∃! n, x = a ^ n.val
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isRat_zpow_neg : ∀ {α : Type u_1} [inst : DivisionRing α] {a : α} {b : ℤ} {nb : ℕ} {num : ℤ} {den : ℕ},
  Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb) →
    Mathlib.Meta.NormNum.IsRat (a ^ nb)⁻¹ num den → Mathlib.Meta.NormNum.IsRat (a ^ b) num den
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- If `F : A ⥤ B` is fully faithful, then `sheafCompose J F` is fully faithful.  -/
CategoryTheory.fullyFaithfulSheafCompose : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {B : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} B] →
            (J : CategoryTheory.GrothendieckTopology C) →
              {F : CategoryTheory.Functor A B} →
                [inst_3 : J.HasSheafCompose F] → F.FullyFaithful → (CategoryTheory.sheafCompose J F).FullyFaithful
-- Mathlib.Topology.Algebra.InfiniteSum.Real
dist_le_tsum_dist_of_tendsto₀ : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α} {a : α},
  (Summable fun n => dist (f n) (f n.succ)) →
    Filter.Tendsto f Filter.atTop (nhds a) → dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {km : α}, t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.ker_le_ker_iff_range_le_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {T U : E →L[𝕜] E},
  (↑T).IsSymmetric → (↑U).IsSymmetric → ((↑U).ker ≤ (↑T).ker ↔ (↑T).range ≤ (↑U).range)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closedCell_zero_injective : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D],
  Function.Injective (Topology.RelCWComplex.closedCell 0)
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
_private.Mathlib.AlgebraicTopology.DoldKan.NCompGamma.0.Fin.succ.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin n → Sort u_1) (i : ℕ) (h : i < n) (h_1 : (i : ℕ) → (h : i < n) → motive ⟨i, h⟩),
  (match ⟨i, h⟩ with
    | ⟨i, h⟩ => h_1 i h) =
    h_1 i h
-- Mathlib.RingTheory.PowerSeries.Catalan
PowerSeries.catalanSeries.eq_1 : PowerSeries.catalanSeries = PowerSeries.mk catalan
-- Mathlib.Logic.Function.Basic
/-- Non-dependent version of `Function.update_comp_eq_of_injective'`  -/
Function.update_comp_eq_of_injective : ∀ {α : Sort u} {α' : Sort w} [inst : DecidableEq α] [inst_1 : DecidableEq α'] {β : Sort u_1} (g : α' → β) {f : α → α'},
  Function.Injective f → ∀ (i : α) (a : β), Function.update g (f i) a ∘ f = Function.update (g ∘ f) i a
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAgainst.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.MorphismProperty C},
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), P' f → P.IsStableUnderBaseChangeAlong f) → P.IsStableUnderBaseChangeAgainst P'
-- Std.Sync.Notify
Std.Notify.State.mk.sizeOf_spec : ∀ (consumers : Std.Queue (Std.Notify.Consumer Unit)), sizeOf { consumers := consumers } = 1 + sizeOf consumers
-- Mathlib.Algebra.Lie.Abelian
Function.Injective.isLieAbelian : ∀ {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₂},
  Function.Injective ⇑f → IsLieAbelian L₂ → IsLieAbelian L₁
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.declName : Lean.Elab.PartialFixpoint.EqnInfo → Lean.Name
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The type of morphisms in `Semigrp R`.  -/
Semigrp.Hom : Semigrp → Semigrp → Type u
-- Mathlib.Data.List.DropRight
/-- Take `n` elements from the tail end of a list.  -/
List.rtake : {α : Type u_1} → List α → ℕ → List α
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The sum of two elements of an additive subsemigroup belongs to the subsemigroup.  -/
AddSubsemigroup.add_mem' : ∀ {M : Type u_3} [inst : Add M] (self : AddSubsemigroup M) {a b : M},
  a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
/-- If `f` has derivative `f'` at `a` in the strict sense and `c > 0`, then `f` approximates `f'`
with constant `c` on some neighborhood of `a`.  -/
HasStrictFDerivAt.approximates_deriv_on_nhds : ∀ {𝕜 : 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 → F}
  {f' : E →L[𝕜] F} {a : E},
  HasStrictFDerivAt f f' a → ∀ {c : NNReal}, Subsingleton E ∨ 0 < c → ∃ s ∈ nhds a, ApproximatesLinearOn f f' s c
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.refl_trans : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  (DilationEquiv.refl X).trans e = e
-- Mathlib.Algebra.Order.CauSeq.Basic
rat_add_continuous_lemma : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Ring β]
  (abv : β → α) [IsAbsoluteValue abv] {ε : α},
  0 < ε → ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ + a₂ - (b₁ + b₂)) < ε
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp},
  t.WF → t.isEmpty = (t.size == 0)
-- Init.System.IOError
IO.Error.alreadyExists.inj : ∀ {filename : Option String} {osCode : UInt32} {details : String} {filename_1 : Option String} {osCode_1 : UInt32}
  {details_1 : String},
  IO.Error.alreadyExists filename osCode details = IO.Error.alreadyExists filename_1 osCode_1 details_1 →
    filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1
-- Lean.Meta.Sym.Arith.Types
/-- `Semiring` instance for `type`  -/
Lean.Meta.Sym.Arith.Semiring.semiringInst : Lean.Meta.Sym.Arith.Semiring → Lean.Expr
-- Mathlib.Data.ENat.Basic
ENat.lt_add_one_iff : ∀ {m n : ℕ∞}, n ≠ ⊤ → (m < n + 1 ↔ m ≤ n)
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (P : C),
  CategoryTheory.Projective P ↔ (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op P)).PreservesEpimorphisms
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_add_neg_nhds_zero : ∀ (Gᵣ : Type u_3) [inst : UniformSpace Gᵣ] [inst_1 : AddGroup Gᵣ] [IsRightUniformAddGroup Gᵣ],
  uniformity Gᵣ = Filter.comap (fun x => x.2 + -x.1) (nhds 0)
-- Lean.Meta.Tactic.Grind.Types
/-- `grind_pattern` guard  -/
Lean.Meta.Grind.SplitSource.guard : Lean.Meta.Grind.Origin → Lean.Meta.Grind.SplitSource
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoLocallyConstantOfIsColimit_inv : ∀ (X : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts X]
  (hX :
    (S : LightProfinite) →
      CategoryTheory.Limits.IsColimit (X.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))),
  (LightCondensed.isoLocallyConstantOfIsColimit X hX).inv = CompHausLike.LocallyConstant.counitApp X
-- Mathlib.Geometry.Manifold.HasGroupoid
Structomorph.mk : {H : Type u} →
  [inst : TopologicalSpace H] →
    {G : StructureGroupoid H} →
      {M : Type u_5} →
        {M' : Type u_6} →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : TopologicalSpace M'] →
              [inst_3 : ChartedSpace H M] →
                [inst_4 : ChartedSpace H M'] →
                  (toHomeomorph : M ≃ₜ M') →
                    (∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
                        c ∈ atlas H M →
                          c' ∈ atlas H M' → c.symm.trans (toHomeomorph.toOpenPartialHomeomorph.trans c') ∈ G) →
                      Structomorph G M M'
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.splitter : (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) →
  (op : Std.Tactic.BVDecide.BVBinOp) →
    (Unit → motive Std.Tactic.BVDecide.BVBinOp.and) →
      (Unit → motive Std.Tactic.BVDecide.BVBinOp.or) →
        (Unit → motive Std.Tactic.BVDecide.BVBinOp.xor) →
          (Unit → motive Std.Tactic.BVDecide.BVBinOp.add) →
            (Unit → motive Std.Tactic.BVDecide.BVBinOp.mul) →
              (Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) →
                (Unit → motive Std.Tactic.BVDecide.BVBinOp.umod) → motive op
-- Init.Data.BitVec.Lemmas
BitVec.sdiv_self : ∀ {w : ℕ} {x : BitVec w}, x.sdiv x = if (x == 0#w) = true then 0#w else 1#w
-- ProofWidgets.Component.Basic
ProofWidgets.instToModuleComponent : {Props : Type} → Lean.Widget.ToModule (ProofWidgets.Component Props)
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Constructor for morphisms to the end of a functor.  -/
CategoryTheory.Limits.end_.lift : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          [inst_2 : CategoryTheory.Limits.HasEnd F] →
            {X : C} →
              (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) →
                (∀ ⦃i j : J⦄ (g : i ⟶ j),
                    CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
                      CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) →
                  (X ⟶ CategoryTheory.Limits.end_ F)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (↑(m.insertMany l)).get? k' = some (cast ⋯ v)
-- Init.Data.Array.MapIdx
List.mapIdxM.go.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : ℕ → α → m β) (a : Array β) (a_1 : α)
  (as : List α),
  List.mapIdxM.go f (a_1 :: as) a = do
    let __do_lift ← f a.size a_1
    List.mapIdxM.go f as (a.push __do_lift)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f},
  (m.alter k f)[k'] = if heq : (k == k') = true then (f m[k]?).get ⋯ else m[k']
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.enumList_nodup : Turing.PartrecToTM2.Γ'.enumList.Nodup
-- Mathlib.Algebra.DirectSum.Ring
/-- The `Semiring` structure derived from `GSemiring A`.  -/
DirectSum.instSemiringOfNat : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommMonoid (A i)] → [inst_1 : AddMonoid ι] → [DirectSum.GSemiring A] → Semiring (A 0)
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
AddMonoidAlgebra.counit_single : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] {X : Type u_3} [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (x : X) (a : A),
  CoalgebraStruct.counit (AddMonoidAlgebra.single x a) = CoalgebraStruct.counit a
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_image`.

---

The infimum edistance is invariant under isometries  -/
EMetric.infEdist_image : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {x : α} {t : Set α}
  {Φ : α → β}, Isometry Φ → Metric.infEDist (Φ x) (Φ '' t) = Metric.infEDist x t
-- Std.Data.DTreeMap.Raw.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.
 -/
Std.DTreeMap.Raw.insert : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → (a : α) → β a → Std.DTreeMap.Raw α β cmp