mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_ofNat_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoDiv hp a (OfNat.ofNat m * p + b) = OfNat.ofNat m + toIcoDiv hp a b
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
IsRegular.mem_nonZeroDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r : M₀}, IsRegular r → r ∈ nonZeroDivisors M₀
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.quotientEquiv_apply_mk : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (x : E),
  (ZSpan.quotientEquiv b) (Submodule.Quotient.mk x) = ZSpan.fractRestrict b x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDeriv_fun_const_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜}, iteratedDeriv n (fun x => 0) x = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β} {kmi : α}, (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_compl_iff : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsCobounded sᶜ ↔ Bornology.IsBounded s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.instZeroHom : {D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D] → (M N : CategoryTheory.Mon D) → Zero (M ⟶ N)
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.mk.injEq : ∀ (description : Unit → Lean.MessageData) (m : Lean.Elab.Do.DoElabM Lean.Expr)
  (stM runInBase : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (restoreCont : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont)
  (description_1 : Unit → Lean.MessageData) (m_1 : Lean.Elab.Do.DoElabM Lean.Expr)
  (stM_1 runInBase_1 : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (restoreCont_1 : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont),
  ({ description := description, m := m, stM := stM, runInBase := runInBase, restoreCont := restoreCont } =
      { description := description_1, m := m_1, stM := stM_1, runInBase := runInBase_1,
        restoreCont := restoreCont_1 }) =
    (description = description_1 ∧ m = m_1 ∧ stM = stM_1 ∧ runInBase = runInBase_1 ∧ restoreCont = restoreCont_1)
-- Batteries.Tactic.Init
/-- `_` in tactic position acts like the `done` tactic: it fails and gives the list
of goals if there are any. It is useful as a placeholder after starting a tactic block
such as `by _` to make it syntactically correct and show the current goal.
 -/
Batteries.Tactic.tactic_ : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instDivisionMonoid : {α : Type u_1} → [DivisionMonoid α] → DivisionMonoid (WithZero α)
-- Mathlib.Data.Nat.Log
/-- `clog b n`, is the upper logarithm of natural number `n` in base `b`. It returns the smallest
`k : ℕ` such that `n ≤ b^k`, so if `b^k = n`, it returns exactly `k`.  -/
Nat.clog : ℕ → ℕ → ℕ
-- Mathlib.RingTheory.Valuation.Integers
Valuation.leSubmodule_zero : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] (K : Type u_1) [inst_1 : Field K] (v : Valuation K Γ₀),
  v.leSubmodule 0 = ⊥
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.instIsRightAdjointPushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [(PresheafOfModules.pushforward φ.hom).IsRightAdjoint] [CategoryTheory.HasWeakSheafify K AddCommGrpCat]
  [K.WEqualsLocallyBijective AddCommGrpCat], (SheafOfModules.pushforward φ).IsRightAdjoint
-- Init.Data.Array.OfFn
Array.idRun_ofFnM : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Id α}, (Array.ofFnM f).run = Array.ofFn fun i => (f i).run
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflQuiver.mk : {obj : Type u} → [toQuiver : Quiver obj] → ((X : obj) → X ⟶ X) → CategoryTheory.ReflQuiver obj
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_bijective : Function.Bijective Real.arsinh
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_strictMono_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, Function.Surjective ⇑f → StrictMono (Submonoid.comap f)
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.fourierMultiplierCLM_fourierMultiplierCLM_apply : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : NormedSpace ℂ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℂ 𝕜 F] [inst_7 : FiniteDimensional ℝ E] [inst_8 : MeasurableSpace E] [inst_9 : BorelSpace E]
  [CompleteSpace F] {g₁ g₂ : E → 𝕜},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      ∀ (f : SchwartzMap E F),
        (SchwartzMap.fourierMultiplierCLM F g₁) ((SchwartzMap.fourierMultiplierCLM F g₂) f) =
          (SchwartzMap.fourierMultiplierCLM F (g₁ * g₂)) f
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.op_symm_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (a : M),
  (AddMonoidHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.setLIntegral_trim_ae : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal},
  AEMeasurable f (μ.trim hm) →
    ∀ {s : Set α}, MeasurableSet s → ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (x : α) in s, f x ∂μ
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.visitExpr : Lean.Expr → Lean.CollectLevelParams.Visitor
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac).H = H
-- Lean.MonadEnv
Lean.withoutModifyingEnv : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [MonadFinally m] → {α : Type} → m α → m α
-- Mathlib.Order.CompleteLatticeIntervals
/-- The `sInf` function on a nonempty `OrdConnected` set `s` in a conditionally complete linear
order takes values within `s`, for all nonempty bounded-below subsets of `s`.  -/
sInf_within_of_ordConnected : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [hs : s.OrdConnected] ⦃t : Set ↑s⦄,
  t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_eq_pi_div_two : ∀ {x : ℝ}, Real.arccos x = Real.pi / 2 ↔ x = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.containsKey_filterMap : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)}
  {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      if h : Std.Internal.List.containsKey k l = true then
        (f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h)).isSome
      else false
-- Lean.Parser.Syntax
Lean.Parser.Command.notationItem.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.normSq.eq_1 : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), InnerProductSpace.Core.normSq x = RCLike.re (inner 𝕜 x x)
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_univ : ∀ {α : Type u_2} [inst : Bornology α], Bornology.IsBounded Set.univ ↔ BoundedSpace α
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of `Cardinal.lt_one_iff`. -/
Cardinal.lt_one_iff_zero : ∀ {c : Cardinal.{u_1}}, c < 1 ↔ c = 0
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.instIteratorLoop.loop.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (acc : γ) (next : α)
  (h : LargeEnough next) (f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))),
  Std.Rxi.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl acc next h f =
    WellFounded.extrinsicFix₃
      (InvImage (Std.IteratorLoop.rel (Std.Rxi.Iterator α) Id Pl) fun x =>
        ({ internalState := { next := some x.fst } }, x.snd.fst))
      (fun next acc h G => do
        let __do_lift ← f next h acc
        match __do_lift with
          | ⟨ForInStep.yield acc', h'⟩ =>
            match hs : Std.PRange.succ? next with
            | some next' => G next' acc' ⋯ ⋯
            | none => pure acc'
          | ⟨ForInStep.done acc', property⟩ => pure acc')
      next acc h
-- Mathlib.RingTheory.Localization.Integer
/-- We can clear the denominators of a finite indexed family of fractions.  -/
IsLocalization.exist_integer_multiples_of_finite : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {ι : Type u_4} [Finite ι] (f : ι → S),
  ∃ b, ∀ (i : ι), IsLocalization.IsInteger R (↑b • f i)
-- Mathlib.Data.Set.List
_private.Mathlib.Data.Set.List.0.Option.getD.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
/-- For an additive functor `F : C ⥤ D` between abelian categories, the following are equivalent:
- `F` preserves short exact sequences, i.e. if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact then
  `0 ⟶ F(A) ⟶ F(B) ⟶ F(C) ⟶ 0` is exact.
- `F` preserves exact sequences, i.e. if `A ⟶ B ⟶ C` is exact then `F(A) ⟶ F(B) ⟶ F(C)` is exact.
- `F` preserves homology.
- `F` preserves both finite limits and finite colimits.
 -/
CategoryTheory.Functor.exact_tfae : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).ShortExact,
      ∀ (S : CategoryTheory.ShortComplex C), S.Exact → (S.map F).Exact, F.PreservesHomology,
      CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F].TFAE
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.symm_apply_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N) {x : N} {y : M}, e.symm x = y ↔ x = e y
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instSupSet : (ι : Type u_1) → SupSet (PreAbstractSimplicialComplex ι)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.step_intermediateDropWhile : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → Bool} {dropping : Bool},
  (Std.IterM.Intermediate.dropWhile P dropping it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        if h' : dropping = true then
          match hP : P out with
          | true =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhile P true it') ⋯))
          | false =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhile P false it') out ⋯))
        else
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhile P false it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhile P dropping it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Order.Interval.Set.ProjIcc
/-- Extend a function `(-∞, b] → β` to a map `α → β`.  -/
Set.IicExtend : {α : Type u_1} → {β : Type u_2} → [inst : LinearOrder α] → {b : α} → (↑(Set.Iic b) → β) → α → β
-- Mathlib.Data.LawfulXor.Basic
LawfulXor.xor_zero : ∀ {α : Type u_1} {inst : XorOp α} {inst_1 : Zero α} [self : LawfulXor α] (a : α), a ^^^ 0 = a
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.preimage_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ℝ), f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
-- Mathlib.Topology.EMetricSpace.Basic
/-- ε-δ characterization of Cauchy sequences on pseudoemetric spaces  -/
EMetric.cauchy_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : Filter α},
  Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.comp_smul' : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : CommRing k] [inst_2 : Monoid G] (A B C : TopRep k G)
  (f : A ⟶ B) (r : k) (g : B ⟶ C),
  CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigOWith_const_one : ∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] [inst_2 : One F] [NormOneClass F]
  (c : E) (l : Filter α), Asymptotics.IsBigOWith ‖c‖ l (fun _x => c) fun _x => 1
-- Mathlib.Order.WithBot
WithBot.noMaxOrder : ∀ {α : Type u_1} [inst : LT α] [NoMaxOrder α] [Nonempty α], NoMaxOrder (WithBot α)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Value of Riemann zeta at `-ℕ` in terms of `bernoulli'`.  -/
riemannZeta_neg_nat_eq_bernoulli' : ∀ (k : ℕ), riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)
-- Init.Grind.Offset
Lean.Grind.Nat.le_lo : ∀ (u w v k : ℕ), u ≤ w → w + k ≤ v → u + k ≤ v
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly.eval₂' : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F), Polynomial.eval₂ (FixedPoints.subfield G F).subtype x (FixedPoints.minpoly G F x) = 0
-- Mathlib.Tactic.DefEqAbuse
/-- A return value for functions called by traversals of `MessageData`. May either descend into
children or ascend immediately (skipping children), optionally including a value accumulated by the
traversal in both cases.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep : Type u_1 → Type u_1
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.sat_relabel : ∀ {α : Type u_1} {β : Type u_2} {r1 : β → Bool} {r2 : α → β} {f : Std.Sat.CNF α},
  Std.Sat.CNF.Sat (r1 ∘ r2) f → Std.Sat.CNF.Sat r1 (Std.Sat.CNF.relabel r2 f)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.truncateToReal.eq_1 : ∀ (t x : ENNReal), t.truncateToReal x = (min t x).toReal
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.iInf_normalizer_le_normalizer_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_6} (H : ι → AddSubgroup G),
  ⨅ i, AddSubgroup.normalizer ↑(H i) ≤ AddSubgroup.normalizer ↑(⨅ i, H i)
-- Mathlib.Data.Set.Countable
/-- **Alias** of `Set.Countable.ofPred_finite`.

---

The set of finite sets in a countable type is countable.  -/
Set.Countable.setOf_finite : ∀ {α : Type u} [Countable α], {s | s.Finite}.Countable
-- Lean.Exception
/-- Returns `true` if the exception is an interrupt generated by `checkInterrupted`.  -/
Lean.Exception.isInterrupt : Lean.Exception → Bool
-- Init.Grind.Offset
Lean.Grind.isLE : ℕ → ℕ → Bool
-- Mathlib.Order.Category.FinBddDistLat
/-- The type of morphisms in `FinBddDistLat R`.  -/
FinBddDistLat.Hom : FinBddDistLat → FinBddDistLat → Type u
-- Mathlib.Tactic.Translate.Reorder
/-- Determine how many forall binders should be introduced to get a non-dependent conclusion.  -/
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.depForallDepth : Lean.Expr → ℕ
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] (X : D) (f : CategoryTheory.CostructuredArrow L X),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left)
      (CategoryTheory.CategoryStruct.comp ((L.leftKanExtension F).map f.hom)
        (L.leftKanExtensionObjIsoColimit F X).hom) =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso'_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C}
  (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' X i).hom.right =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W X.right)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr : Type
-- Std.Http.Protocol.H1.Writer
/-- The outgoing message that will be written to the output.
 -/
Std.Http.Protocol.H1.Writer.messageHead : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Message.Head dir.swap
-- Batteries.Data.Fin.Coding
Fin.encodeOrdering_decodeOrdering : ∀ (x : Fin 3), Fin.encodeOrdering (Fin.decodeOrdering x) = x
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The canonical right distributivity isomorphism  -/
CategoryTheory.rightDistrib : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        [CategoryTheory.IsMonoidalRightDistrib C] →
          (X Y Z : C) →
            CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ≅
              CategoryTheory.MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instTop : {α : Type u} → [inst : Group α] → Top (GroupTopology α)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.add_subset_add`.  -/
Set.list_sum_subset_list_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : List ι) (f₁ f₂ : ι → Set α),
  (∀ i ∈ t, f₁ i ⊆ f₂ i) → (List.map f₁ t).sum ⊆ (List.map f₂ t).sum
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.le_one : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (i : ι) (x : X),
  (f i) x ≤ 1
-- Init.Data.UInt.Lemmas
UInt64.add_comm : ∀ (a b : UInt64), a + b = b + a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_ext : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} {f g : A ⟶ B},
  Rep.Hom.hom f = Rep.Hom.hom g → f = g
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.norm_rpow_div : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.MemLp f p μ → ∀ (q : ENNReal), MeasureTheory.MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_gamma_zero : ∀ (o : Ordinal.{u_1}), Ordinal.veblen o.gamma 0 = o.gamma
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The embedding of the coerced subgroupoid to its parent  -/
CategoryTheory.Subgroupoid.hom : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] → (S : CategoryTheory.Subgroupoid C) → CategoryTheory.Functor (↑S.objs) C
-- Std.Data.Iterators.Lemmas.Combinators.Drop
Std.Iter.toList_drop : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.drop n it).toList = List.drop n it.toList
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedInClass.instContinuousMapClass : ∀ (B : Type u_5) (E : outParam (Type u_6)) (F : outParam (Type u_7)) [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace ℝ F] (n : outParam ℕ∞)
  (K : outParam (TopologicalSpace.Compacts E)) [inst_4 : ContDiffMapSupportedInClass B E F n K],
  ContinuousMapClass B E F
-- Lean.Meta.AppBuilder
/-- Returns `a - b` using a heterogeneous `-`. This method assumes `a` and `b` have the same type.  -/
Lean.Meta.mkSub : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tsum_setProd_singleton_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  (t : Set γ) (f : β × γ → α), ∑' (x : ↑({b} ×ˢ t)), f ↑x = ∑' (c : ↑t), f (b, ↑c)
-- Mathlib.Algebra.Group.Center
Set.centralizer_centralizer_centralizer : ∀ {M : Type u_1} [inst : Mul M] (S : Set M), S.centralizer.centralizer.centralizer = S.centralizer
-- Mathlib.RingTheory.Adjoin.Singleton
/-- Ring homomorphism between `A[b]` and `A[↑b]`.  -/
Algebra.RingHom.adjoinAlgebraMap : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : CommSemiring B] →
          [inst_2 : CommSemiring C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra B C] →
                [inst_5 : Algebra A C] → [IsScalarTower A B C] → (b : B) → ↥A[b] →+* ↥A[(algebraMap B C) b]