mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.mk.injEq : ∀ (support : Finset ℕ) (prodPrimes : ℕ) (prodPrimes_squarefree : Squarefree prodPrimes) (weights : ℕ → ℝ)
  (weights_nonneg : ∀ (n : ℕ), 0 ≤ weights n) (totalMass : ℝ) (nu : ArithmeticFunction ℝ)
  (nu_mult : nu.IsMultiplicative) (nu_pos_of_prime : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → 0 < nu p)
  (nu_lt_one_of_prime : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → nu p < 1) (support_1 : Finset ℕ) (prodPrimes_1 : ℕ)
  (prodPrimes_squarefree_1 : Squarefree prodPrimes_1) (weights_1 : ℕ → ℝ)
  (weights_nonneg_1 : ∀ (n : ℕ), 0 ≤ weights_1 n) (totalMass_1 : ℝ) (nu_1 : ArithmeticFunction ℝ)
  (nu_mult_1 : nu_1.IsMultiplicative) (nu_pos_of_prime_1 : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes_1 → 0 < nu_1 p)
  (nu_lt_one_of_prime_1 : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes_1 → nu_1 p < 1),
  ({ support := support, prodPrimes := prodPrimes, prodPrimes_squarefree := prodPrimes_squarefree, weights := weights,
        weights_nonneg := weights_nonneg, totalMass := totalMass, nu := nu, nu_mult := nu_mult,
        nu_pos_of_prime := nu_pos_of_prime, nu_lt_one_of_prime := nu_lt_one_of_prime } =
      { support := support_1, prodPrimes := prodPrimes_1, prodPrimes_squarefree := prodPrimes_squarefree_1,
        weights := weights_1, weights_nonneg := weights_nonneg_1, totalMass := totalMass_1, nu := nu_1,
        nu_mult := nu_mult_1, nu_pos_of_prime := nu_pos_of_prime_1, nu_lt_one_of_prime := nu_lt_one_of_prime_1 }) =
    (support = support_1 ∧ prodPrimes = prodPrimes_1 ∧ weights = weights_1 ∧ totalMass = totalMass_1 ∧ nu = nu_1)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.zero_mul : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.Context.mk.inj : ∀ {offset offset_1 : ℕ}, { offset := offset } = { offset := offset_1 } → offset = offset_1
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instFourierInvSMul : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E],
  FourierInvSMul ℂ ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- An additive monoid object internal to a monoidal category.  -/
CategoryTheory.AddMon : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → Type (max u₁ v₁)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Ric.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Std.Rxc.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Ric α}, r.iter.toArray = r.toArray
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_sdiv : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec (a.sdiv b) = ISize.ofBitVec a / ISize.ofBitVec b
-- Mathlib.Computability.TuringMachine.Computable
/-- A Turing machine + a polynomial time function +
a proof it outputs `f` in at most `time(input.length)` steps.  -/
Turing.TM2ComputableInPolyTime : {α β αΓ βΓ : Type} → (α → List αΓ) → (β → List βΓ) → (α → β) → Type 1
-- Mathlib.Logic.Basic
Decidable.or_not_of_imp : ∀ {a b : Prop} [Decidable a], (a → b) → b ∨ ¬a
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.geometricallyConnected_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.GeometricallyConnected f ↔ AlgebraicGeometry.geometrically (fun x => ConnectedSpace ↥x) f
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- The underlying prelax functor.  -/
CategoryTheory.LaxFunctor.toPrelaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.LaxFunctor B C → CategoryTheory.PrelaxFunctor B C
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoord_symm_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (p : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℝ × ℝ)),
  ↑(NumberField.mixedEmbedding.polarCoord K).symm p = (p.1, Pi.map (fun i => ↑Complex.polarCoord.symm) p.2)
-- Mathlib.Algebra.Homology.Embedding.TruncLE
ComplexShape.Embedding.truncLE'Functor_obj : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncLE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c'),
  (e.truncLE'Functor C).obj K = K.truncLE' e
-- Mathlib.Order.Defs.PartialOrder
le_of_lt_or_eq' : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a ∨ a = b → b ≤ a
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.inner_assoc_assoc : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (x y : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G),
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) x) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 x y
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.matchExpr.injEq : ∀ (ref : Lean.Syntax) («meta» : Bool) (discr : Lean.Syntax)
  (alts : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) (elseBranch : Lean.Elab.Term.Do.Code)
  (ref_1 : Lean.Syntax) (meta_1 : Bool) (discr_1 : Lean.Syntax)
  (alts_1 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) (elseBranch_1 : Lean.Elab.Term.Do.Code),
  (Lean.Elab.Term.Do.Code.matchExpr ref «meta» discr alts elseBranch =
      Lean.Elab.Term.Do.Code.matchExpr ref_1 meta_1 discr_1 alts_1 elseBranch_1) =
    (ref = ref_1 ∧ «meta» = meta_1 ∧ discr = discr_1 ∧ alts = alts_1 ∧ elseBranch = elseBranch_1)
-- Std.Do.SPred.Laws
Std.Do.SPred.bientails.refl : ∀ {σs : List (Type u)} (P : Std.Do.SPred σs), P ⊣⊢ₛ P
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α},
  k ∈ Std.ExtTreeMap.filterMap f t ↔ ∃ (h : k ∈ t), (f (t.getKey k h) t[k]).isSome = true
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic on an open set `U`, if `g` agrees with `f` on a codiscrete subset of `U`, then
`g` is also meromorphic on `U`.
 -/
MeromorphicOn.congr_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → f =ᶠ[Filter.codiscreteWithin U] g → IsOpen U → MeromorphicOn g U
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.eq_1 : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] (f : α → β),
  HasCompactMulSupport f = IsCompact (mulTSupport f)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.limitsOfShape_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W₁ W₂ : CategoryTheory.MorphismProperty C},
  W₁ ≤ W₂ → ∀ (J : Type u_2) [inst_1 : CategoryTheory.Category.{v_2, u_2} J], W₁.limitsOfShape J ≤ W₂.limitsOfShape J
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.add_nat : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (n : ℕ), LiouvilleWith p (x + ↑n)
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.unfoldAt : Lean.MVarId → Lean.FVarId → Array Lean.Name → Bool → Aesop.Script.TacticBuilder
-- Mathlib.Algebra.Group.Action.Faithful
instFaithfulSMulOfSubsingleton : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] [Subsingleton M], FaithfulSMul M α
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stmts₁ (Turing.TM2.Stmt.peek k a q) = insert (Turing.TM2.Stmt.peek k a q) (Turing.TM2.stmts₁ q)
-- Std.Data.Internal.List.Defs
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.values : {α : Type u} → {β : Type v} → List ((_ : α) × β) → List β
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for defining the element `0` of the ring of Witt vectors.  -/
WittVector.wittZero : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial (Fin 0 × ℕ) ℤ
-- Mathlib.Data.Int.WithZero
/-- `toNNReal` sends nonzero elements to positive elements.  -/
WithZeroMulInt.toNNReal_pos : ∀ {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : e ≠ 0), m ≠ 0 → 0 < (WithZeroMulInt.toNNReal he) m
-- Init.Data.BitVec.Bitblast
BitVec.mulRec.eq_2 : ∀ {w : ℕ} (x y : BitVec w) (s_2 : ℕ),
  x.mulRec y s_2.succ = x.mulRec y s_2 + if y.getLsbD s_2.succ = true then x <<< s_2.succ else 0
-- Mathlib.Control.Fold
Traversable.foldrm.ofFreeMonoid_comp_of : ∀ {α β : Type u} {m : Type u → Type u} [inst : Monad m] [inst_1 : LawfulMonad m] (f : β → α → m α),
  ⇑(Monoid.foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.foldrM.mk ∘ f
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation from a metric space is a uniform inducing map  -/
Dilation.isUniformInducing : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [DilationClass F α β] (f : F), IsUniformInducing ⇑f
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.ofNat_toNat : ∀ {a : ℤ}, a ≥ 0 → Int.ofNat a.toNat = a
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_3.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.Data.NNReal.Defs
NNReal.coe_div : ∀ (r₁ r₂ : NNReal), ↑(r₁ / r₂) = ↑r₁ / ↑r₂
-- Mathlib.Analysis.BoxIntegral.Basic
/-- If `f` is integrable on `I` along `l`, then for two sufficiently fine tagged prepartitions
(in the sense of the filter `BoxIntegral.IntegrationParams.toFilter l I`) such that they cover
the same part of `I`, the integral sums of `f` over `π₁` and `π₂` are very close to each other.  -/
BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol →
    Filter.Tendsto (fun π => (BoxIntegral.integralSum f vol π.1, BoxIntegral.integralSum f vol π.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓ Filter.principal {π | π.1.iUnion = π.2.iUnion}) (uniformity F)
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.toCanonicallyOrderedAdd : ∀ {α : Type u_1} [inst : IdemSemiring α], CanonicallyOrderedAdd α
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM.go.match_1.splitter : {β : Type u_2} →
  {α : Type u_1} →
    (motive : List α → β → List β → Sort u_3) →
      (x : List α) →
        (x_1 : β) →
          (x_2 : List β) →
            ((last : β) → (acc : List β) → motive [] last acc) →
              ((x : α) → (xs : List α) → (last : β) → (acc : List β) → motive (x :: xs) last acc) → motive x x_1 x_2
-- Mathlib.Algebra.Category.MonCat.Yoneda
/-- The `AddCommMonCat`-valued coyoneda embedding composed with the forgetful functor is the usual
coyoneda embedding.  -/
AddCommMonCat.coyonedaForget : AddCommMonCat.coyoneda.comp
    ((CategoryTheory.Functor.whiskeringRight AddCommMonCat AddCommMonCat (Type u_1)).obj
      (CategoryTheory.forget AddCommMonCat)) ≅
  CategoryTheory.coyoneda
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.MorphismProperty.nonempty_kernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (W : CategoryTheory.MorphismProperty C) {X₁ X₂ : C} (f : X₁ ⟶ X₂),
  W f → ∀ [CategoryTheory.Limits.HasKernel f], W.kernels.Nonempty
-- Lean.Declaration
Lean.instBEqRecursorVal.beq : Lean.RecursorVal → Lean.RecursorVal → Bool
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for a left-open right-closed range `lo<...=hi`.
This is an internal function.
Use `Roc.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Roc.Internal.iter : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Roc α → Std.Iter α
-- Mathlib.RingTheory.Congruence.Basic
RingCon.toCon_eq_bot : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {c : RingCon R}, c.toCon = ⊥ ↔ c = ⊥
-- Init.Meta.Defs
Lean.Meta.ApplyNewGoals.all : Lean.Meta.ApplyNewGoals
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_comp_of_finrank_eq : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} {W : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] [inst_6 : NormedAddCommGroup W] [inst_7 : InnerProductSpace 𝕜 W]
  [inst_8 : FiniteDimensional 𝕜 V] (f : U →ₗ[𝕜] V) (g : V →ₗ[𝕜] W),
  Module.finrank 𝕜 U = Module.finrank 𝕜 V → (g ∘ₗ f).normDet = g.normDet * f.normDet
-- Init.Data.SInt.Lemmas
Int16.lt_of_le_of_ne : ∀ {a b : Int16}, a ≤ b → a ≠ b → a < b
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.aleph_omega0_le : ∀ {c : Cardinal.{u_1}}, c.IsSingular → Cardinal.aleph Ordinal.omega0 ≤ c
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.FinValue : Type
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.orderHom_zero : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [inst_5 : IsStrictOrderedRing S] (f : S →+o R),
  (ArchimedeanClass.orderHom f) 0 = ArchimedeanClass.mk (f 1)
-- Mathlib.Topology.Separation.Basic
/-- The neighbourhoods filter of `x` within `s`, under the discrete topology, is equal to
the pure `x` filter (which is the principal filter at the singleton `{x}`.)  -/
nhdsWithin_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → ∀ {x : X}, x ∈ s → nhdsWithin x s = pure x
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_injOn_pos_of_base_lt_one : ∀ {b : ℝ}, 0 < b → b < 1 → Set.InjOn (Real.logb b) (Set.Ioi 0)
-- Mathlib.Analysis.Convex.Basic
/-- The translation of a convex set is also convex.  -/
Convex.translate_preimage_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 ((fun x => z + x) ⁻¹' s)
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for finite measure sets with respect to compact sets
and is locally finite in an R₁ space,
then any compact set can be approximated from outside by open sets.  -/
IsCompact.measure_eq_iInf_isOpen : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α},
  IsCompact K → μ K = ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.id_mapId : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : B),
  (CategoryTheory.LaxFunctor.id B).mapId a = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
-- Mathlib.Order.UpperLower.Closure
UpperSet.erase_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {a : α}, s.erase a = s ↔ a ∉ s
-- Mathlib.CategoryTheory.RegularCategory.Basic
/-- Given a morphism `f : A ⟶ B` and subobjects `A' ⟶ A` and `B' ⟶ B`, the `frobeniusMorphism`
gives a `StrongEpiMonoFactorisation` of `(A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f` through
`((«exists» f).obj A' ⊓ B').arrow`.
This is an auxiliary definition to show `frobenius_reciprocity`.
 -/
CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Regular C] →
      {A B : C} →
        (f : A ⟶ B) →
          (A' : CategoryTheory.Subobject A) →
            (B' : CategoryTheory.Subobject B) →
              CategoryTheory.Limits.StrongEpiMonoFactorisation
                (CategoryTheory.CategoryStruct.comp (A' ⊓ (CategoryTheory.Subobject.pullback f).obj B').arrow f)
-- Init.Data.Int.Gcd
Int.gcd_self_add_right : ∀ (m n : ℤ), m.gcd (m + n) = m.gcd n
-- Init.Data.Int.Order
Int.add_lt_of_lt_neg_add : ∀ {a b c : ℤ}, b < -a + c → a + b < c
-- Mathlib.Algebra.Group.Action.Sum
Sum.FaithfulVAddLeft : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β] [FaithfulVAdd M α],
  FaithfulVAdd M (α ⊕ β)
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The binary coproduct in the category of a `SemilatticeSup` with `OrderBot` is the same as the
supremum.
 -/
CategoryTheory.Limits.CompleteLattice.coprod_eq_sup : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (x y : α), (x ⨿ y) = x ⊔ y
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two functions agree in a neighborhood, then so do their Taylor series.  -/
Filter.EventuallyEq.ftaylorSeries : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F}
  {x : E}, f₁ =ᶠ[nhds x] f → ftaylorSeries 𝕜 f₁ =ᶠ[nhds x] ftaylorSeries 𝕜 f
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.rccIterator.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound upperBound : α),
  Std.DTreeMap.Internal.rccIterator t lowerBound upperBound =
    {
      internalState :=
        { iter := Std.DTreeMap.Internal.Zipper.prependMapGE t lowerBound Std.DTreeMap.Internal.Zipper.done,
          upper := upperBound } }
-- Mathlib.Order.RelClasses
/-- **Alias** of `subset_antisymm`.

---

Set notation form of `le_antisymm` -/
HasSubset.Subset.antisymm : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → b ⊆ a → a = b
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Config.mk.sizeOf_spec : ∀ (maxTransitionDepth maxSteps : ℕ),
  sizeOf { maxTransitionDepth := maxTransitionDepth, maxSteps := maxSteps } =
    1 + sizeOf maxTransitionDepth + sizeOf maxSteps
-- Mathlib.Order.Sublattice
Sublattice.notMem_bot : ∀ {α : Type u_2} [inst : Lattice α] (a : α), a ∉ ⊥
-- Mathlib.Topology.Algebra.Algebra
/-- The topological closure of a subalgebra  -/
Subalgebra.topologicalClosure : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : Algebra R A] → [IsSemitopologicalSemiring A] → Subalgebra R A → Subalgebra R A
-- Init.Prelude
/-- The universe-polymorphic empty type, with no constructors.

`PEmpty` can be used in any universe, but this flexibility can lead to worse error messages and more
challenges with universe level unification. Prefer the type `Empty` or the proposition `False` when
possible.
 -/
PEmpty : Sort u
-- Std.Internal.UV.Timer
_private.Std.Internal.UV.Timer.0.Std.Internal.UV.TimerImpl : NonemptyType
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.counit_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (self : A →ₗc[R] B), CoalgebraStruct.counit ∘ₗ self.toLinearMap = CoalgebraStruct.counit
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C]
  [inst_4 : CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)],
  W.isLocal.isLocal (CategoryTheory.OrthogonalReflection.toSucc W Z)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.cyclesMap'_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.cyclesMap' (φ + φ') h₁ h₂ =
    CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ + CategoryTheory.ShortComplex.cyclesMap' φ' h₁ h₂
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_toSnowflaking_closedBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : X) {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.toSnowflaking '' Metric.closedBall x r =
      Metric.closedBall (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- Construct a valuative relation on a ring using a valuation.  -/
ValuativeRel.ofValuation : {S : Type u_3} →
  {Γ : Type u_4} → [inst : Ring S] → [inst_1 : LinearOrderedCommGroupWithZero Γ] → Valuation S Γ → ValuativeRel S
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_π_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) (j : J),
  ((CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).π.app j).f = c.π.app j
-- Mathlib.RingTheory.Etale.Field
Algebra.FormallyEtale.of_formallyUnramified_of_field : ∀ (K : Type u_1) (A : Type u) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A] [Algebra.EssFiniteType K A]
  [Algebra.FormallyUnramified K A], Algebra.FormallyEtale K A
-- Mathlib.Algebra.Group.Opposite
MulOpposite.op_div : ∀ {α : Type u_1} [inst : DivInvMonoid α] (x y : α), MulOpposite.op (x / y) = (MulOpposite.op y)⁻¹ * MulOpposite.op x
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.VersionedHtml.mk.injEq : ∀ (html : ProofWidgets.Html) (idx : ℕ) (html_1 : ProofWidgets.Html) (idx_1 : ℕ),
  ({ html := html, idx := idx } = { html := html_1, idx := idx_1 }) = (html = html_1 ∧ idx = idx_1)
-- Lean.Elab.Command
Lean.Elab.Command.instMonadRefCommandElabM : Lean.MonadRef Lean.Elab.Command.CommandElabM
-- Mathlib.Topology.Neighborhoods
nhdsWithin_mono : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) {s t : Set X}, s ⊆ t → nhdsWithin x s ≤ nhdsWithin x t
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.intCast_zero : ∀ {R : Type u_2} [inst : CommRing R], ↑0 = 0