mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Prod
/-- This is the computation performed in the proof of [Halmos, §60 Th. A].  -/
MeasureTheory.measure_mul_lintegral_eq : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant]
  [ν.IsMulLeftInvariant],
  MeasurableSet s →
    ∀ (f : G → ENNReal), Measurable f → μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The identity equivalence between `FreeAddMonoid α` and `List α`.  -/
FreeAddMonoid.toList : {α : Type u_1} → FreeAddMonoid α ≃ List α
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
hasFTaylorSeriesUpToOn_top_iff : ∀ {𝕜 : 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] {s : Set E}
  {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  ↑⊤ ≤ N → (HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑n) f p s)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.maxValueSealed_def : Int16.maxValueSealed✝ = Int16.maxValue
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn_obj_zero : ∀ (n : ℕ) (i : Fin (n + 3)), (SSet.horn (n + 2) i).obj (Opposite.op { len := 0 }) = ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Infinite sums commute with scalar multiplication. Version for scalars living in a `Monoid`, but
requiring a summability hypothesis.  -/
Summable.tsum_const_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α]
  [inst_2 : DistribSMul γ α] [ContinuousConstSMul γ α] {f : β → α} {L : SummationFilter β} [T2Space α] [L.NeBot]
  (b : γ), Summable f L → ∑'[L] (i : β), b • f i = b • ∑'[L] (i : β), f i
-- Init.Prelude
XorOp.mk : {α : Type u} → (α → α → α) → XorOp α
-- Lean.Widget.Types
Lean.Widget.Module.mk.sizeOf_spec : ∀ (javascript : String) (javascriptHash : { x // x = hash javascript }),
  sizeOf { javascript := javascript, javascriptHash := javascriptHash } = 1 + sizeOf javascript + sizeOf javascriptHash
-- Mathlib.CategoryTheory.IsConnected
/-- **Alias** of `CategoryTheory.zag_symm`. -/
CategoryTheory.zag_symmetric : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], Std.Symm CategoryTheory.Zag
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonWorkspaceEdit : Lean.FromJson Lean.Lsp.WorkspaceEdit
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_symm : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∪ t \ s = t ∪ s \ t
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- The isomorphism `colimitFiberwiseColimitIso` induces an isomorphism of functors `(J ⥤ C) ⥤ C`
between `fiberwiseColim F H ⋙ colim` and `colim`.  -/
CategoryTheory.Limits.fiberwiseColimCompColimIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] →
            [inst_3 : CategoryTheory.Limits.HasColimitsOfShape C H] →
              (CategoryTheory.Limits.fiberwiseColim F H).comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim
-- Lean.Meta.Tactic.Generalize
/-- Telescopic `generalize` tactic. It can simultaneously generalize many terms.
It uses `kabstract` to occurrences of the terms that need to be generalized.
 -/
Lean.MVarId.generalize : Lean.MVarId →
  Array Lean.Meta.GeneralizeArg →
    optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.instances →
      Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES.map_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact)
  (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂), (DerivedCategory.triangleOfSES.map h₁ h₂ f).hom₁ = DerivedCategory.Q.map f.τ₁
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instAddZeroClass.eq_1 : ∀ {α : Type u} [inst : Add α],
  WithZero.instAddZeroClass = { toZero := WithZero.instZero, toAdd := WithZero.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.rootMultiplicity_comp_C_mul_X_add_C : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) (a b c : R),
  IsUnit a →
    Polynomial.rootMultiplicity c (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)) =
      Polynomial.rootMultiplicity (a * c + b) p
-- Mathlib.Tactic.ClickSuggestions
/-- `#click_suggestions` enables a widget in the infoview that gives tactic suggestions for
the expression in the tactic state that was (most recently) selected with shift-click.
Each suggestion has an insert button for pasting it into the editor, at the position of the cursor.

Theorems are searched for use in `apply`, `apply at`, `rw` and `grw`.
These suggestions are grouped and sorted by the pattern that the lemmas match with.
Rewrites that don't change the goal and rewrites that create the same goal as another rewrite
are filtered out, as well as suggestions that create new goal(s) with metavariables in them.
To see all suggestions, click on the filter button (▼) in the top right.
 -/
Mathlib.Tactic.ClickSuggestions.«command#click_suggestions» : Lean.ParserDescr
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Induction principle for `W`  -/
MvPFunctor.wInd : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} →
      {C : P.W α → Sort v} →
        ((a : P.A) →
            (f' : (P.drop.B a).Arrow α) → (f : P.last.B a → P.W α) → ((i : P.last.B a) → C (f i)) → C (P.wMk a f' f)) →
          (x : P.W α) → C x
-- Mathlib.Order.Concept
Concept.copy.congr_simp : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c c_1 : Concept α β r) (e_c : c = c_1) (e e_1 : Set α)
  (e_e : e = e_1) (i i_1 : Set β) (e_i : i = i_1) (he : e = c.extent) (hi : i = c.intent),
  c.copy e i he hi = c_1.copy e_1 i_1 ⋯ ⋯
-- Init.Control.Lawful.Basic
LawfulFunctor.mk : ∀ {f : Type u → Type v} [inst : Functor f],
  (∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β) →
    (∀ {α : Type u} (x : f α), id <$> x = x) →
      (∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x) → LawfulFunctor f
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.norm_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], K ≠ ⊥ → ‖K.starProjection‖ = 1
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- When applied to `inr` and `inl` themselves, `lift` is the identity.  -/
TrivSqZeroExt.lift_inlAlgHom_inrHom : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M],
  TrivSqZeroExt.lift (TrivSqZeroExt.inlAlgHom S R M) (↑S (TrivSqZeroExt.inrHom R M)) ⋯ ⋯ ⋯ =
    AlgHom.id S (TrivSqZeroExt R M)
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.PulledChunk.mk.injEq : ∀ (final incomplete : Bool) (chunk : Std.Http.Chunk) (final_1 incomplete_1 : Bool) (chunk_1 : Std.Http.Chunk),
  ({ final := final, incomplete := incomplete, chunk := chunk } =
      { final := final_1, incomplete := incomplete_1, chunk := chunk_1 }) =
    (final = final_1 ∧ incomplete = incomplete_1 ∧ chunk = chunk_1)
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.naturality_2' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x : CategoryTheory.IsIso (α.app Y)},
  CategoryTheory.CategoryStruct.comp (α.app X)
      (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.inv (α.app Y))) =
    F.map f
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix_eq_toMatrix' : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  (Q : QuadraticForm R (n → R)), QuadraticForm.toMatrix (Pi.basisFun R n) Q = Q.toMatrix'
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.limitAuxiliaryCone_π_app : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) (X : J),
  (CategoryTheory.Comma.limitAuxiliaryCone F c₁).π.app X =
    CategoryTheory.CategoryStruct.comp (L.map (c₁.π.app X)) (F.obj X).hom
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is `charFunDual_eq_prod_iff` for `WithLp`.
See `charFun_eq_prod_iff` for the Hilbert space version.  -/
MeasureTheory.charFunDual_eq_prod_iff' : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E}
  {ν : MeasureTheory.Measure F} [BorelSpace E] [SecondCountableTopology E] (p : ENNReal) [inst_6 : Fact (1 ≤ p)]
  [BorelSpace F] [SecondCountableTopology F] [CompleteSpace E] [CompleteSpace F] {ξ : MeasureTheory.Measure (E × F)}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (L : StrongDual ℝ (WithLp p (E × F))),
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (WithLp.toLp p) ξ) L =
        MeasureTheory.charFunDual μ
            (L ∘SL ↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
          MeasureTheory.charFunDual ν
            (L ∘SL ↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F)) ↔
    ξ = μ.prod ν
-- Lean.Server.GoTo
_private.Lean.Server.GoTo.0.Lean.Server.getInstanceProjectionArg?.reduceToProjection? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.ProjectionFunctionInfo))
-- Mathlib.Algebra.Lie.Abelian
LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (f : M →ₗ⁅R,L⁆ N), ⇑↑(LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = ⇑f
-- Lean.Elab.BindersUtil
_private.Lean.Elab.BindersUtil.0.Lean.Elab.Term.expandMatchAlts?.expand : Array (Lean.TSyntax `Lean.Parser.Term.matchAlt) → Lean.MacroM (Option (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt)))
-- Aesop.RuleTac.Forward.Basic
Aesop.ForwardHypData.mk.injEq : ∀ (depths depths_1 : Std.HashMap Lean.FVarId ℕ), ({ depths := depths } = { depths := depths_1 }) = (depths = depths_1)
-- Mathlib.Topology.MetricSpace.Holder
/-- For fixed `f : X → Y`, `A : Set X` and `C : ℝ≥0`, the set of all parameters `r : ℝ≥0` such that
`f` is `(C, r)`-Hölder on `A` is convex.  -/
convex_setOfPred_holderOnWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (f : X → Y) (C : NNReal)
  (A : Set X), Convex NNReal {r | HolderOnWith C r f A}
-- Init.Data.Int.Basic
/-- Decides whether an integer is negative.

```
#eval (7 : Int).decNonneg.decide -- true
#eval (0 : Int).decNonneg.decide -- true
#eval ¬ (-7 : Int).decNonneg.decide -- true
```

Implemented by efficient native code.  -/
Int.decNonneg : (m : ℤ) → Decidable m.NonNeg
-- Batteries.Data.List.Lemmas
List.isChain_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ}, List.IsChain (fun x1 x2 => x1 < x2) (List.findIdxs p xs s)
-- Mathlib.NumberTheory.AbelSummation
/-- Abel's summation formula.  -/
sum_mul_eq_sub_sub_integral_mul : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {a b : ℝ},
  0 ≤ a →
    a ≤ b →
      (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) →
        MeasureTheory.IntegrableOn (deriv f) (Set.Icc a b) MeasureTheory.volume →
          ∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
            f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Finset.Icc 0 ⌊a⌋₊, c k -
              ∫ (t : ℝ) in Set.Ioc a b, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff_congr_ae : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  {f g : AddCircle T → E}, f =ᵐ[AddCircle.haarAddCircle] g → fourierCoeff f = fourierCoeff g
-- Init.Data.ByteArray.Basic
ByteArray.Iterator.mk.inj : ∀ {array : ByteArray} {idx : ℕ} {array_1 : ByteArray} {idx_1 : ℕ},
  { array := array, idx := idx } = { array := array_1, idx := idx_1 } → array = array_1 ∧ idx = idx_1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.forgetToScheme_map : ∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.Scheme CategoryTheory.ObjectProperty.FullSubcategory.obj}
  (f : X ⟶ Y), AlgebraicGeometry.AffineScheme.forgetToScheme.map f = f.hom
-- Mathlib.RingTheory.Localization.Ideal
/-- `IsLocalization.map_inf` as an `FrameHom`.  -/
IsLocalization.mapFrameHom : {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] → FrameHom (Ideal R) (Ideal S)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.BaseIO.bindTaskCheap : {α : Type u_1} →
  {β : Type} → Lean.Server.ServerTask α → (α → BaseIO (Lean.Server.ServerTask β)) → BaseIO (Lean.Server.ServerTask β)
-- Mathlib.Topology.Homotopy.Equiv
Homeomorph.trans_toHomotopyEquiv : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z),
  (h₀.trans h₁).toHomotopyEquiv = h₀.toHomotopyEquiv.trans h₁.toHomotopyEquiv
-- Batteries.Data.String.Matcher
String.Matcher.toMatcher : String.Matcher → Array.Matcher Char
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.ker_prod : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] (f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃), (↑(f.prod g)).ker = (↑f).ker ⊓ (↑g).ker
-- Lean.Elab.MutualInductive
/-- Auxiliary function for `inferResultingUniverse`.
Consider the constraint `u ≤ ?r + rOffset`.
This function simplifies the constraints in an attempt to find a minimal solution
of the form `?r := max l₁ ... lₙ` where each `lᵢ` is normalized and not a `max`/`imax`.

In the calculation, we allow negative values of `rOffset`. For example, `u ≤ ?r - 4` means `u + 4 ≤ ?r`.

The `typeLMVarIds` array is all the level mvars that appear in all the type formers in an inductive family.
All other level mvars are ignored — the idea is that type former level mvars can become level parameters,
but constructor level mvars need to be inferred separately.

Positive values of `rOffset` tend to correspond to "too big" of an inferred universe.
Consider `u ≤ ?r + 1`, which is a constraint that comes from the example
```lean
inductive I (α : Sort u) : Type _ where
  | mk (x : α)
```
This is likely a mistake. The best solution would be `Sort (max u 1)` rather than `Type (u + 1)`,
but by this point in elaboration it is impossible to rectify.
So, for `u ≤ ?r + 1` we record both `u` and `1`
to be able to inform the user what they should have probably used instead.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.accLevel : Lean.Level →
  Lean.Level → ℕ → Array Lean.LMVarId → ExceptT Lean.MessageData (StateT Lean.Elab.Command.AccLevelState✝ Id) Unit
-- Mathlib.Order.ULift
ULift.instSDiff_mathlib : {α : Type u} → [SDiff α] → SDiff (ULift.{v, u} α)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- Two paths are equal in the fundamental groupoid if and only if they are homotopic.  -/
FundamentalGroupoid.fromPath_eq_iff_homotopic : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (f g : Path x₀ x₁),
  FundamentalGroupoid.fromPath (Path.Homotopic.Quotient.mk f) =
      FundamentalGroupoid.fromPath (Path.Homotopic.Quotient.mk g) ↔
    f.Homotopic g
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a monoid inherits a monoid structure.  -/
SubmonoidClass.toMonoid : {M : Type u_4} →
  [inst : Monoid M] → {A : Type u_5} → [inst_1 : SetLike A M] → [SubmonoidClass A M] → (S : A) → Monoid ↥S
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.coe_real_preimage_closedBall_inter_eq : ∀ (p : ℝ) {x ε : ℝ},
  ∀ s ⊆ Metric.closedBall x (|p| / 2),
    QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε ∩ s = if ε < |p| / 2 then Metric.closedBall x ε ∩ s else s
-- Lean.Elab.MutualDef
/-- Snapshot for incremental processing of top-level tactic block, if any.

Invariant: if the bundle's `old?` is set, then the state *up to the start* of the tactic block is
unchanged, i.e. reuse is possible.
 -/
Lean.Elab.DefViewElabHeader.tacSnap? : Lean.Elab.DefViewElabHeader → Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- Given a pullback in `C`, construct a binary product in `C/B`.  -/
CategoryTheory.Over.ConstructProducts.over_binaryProduct_of_pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {B : C},
  CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over B)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesIsoH.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1) (n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁), X.opcyclesIsoH f n₀ n₁ hn₁ = X.opcyclesIsoH f n₀_1 n₁ ⋯
-- Mathlib.Data.Int.Init
_private.Mathlib.Data.Int.Init.0.Int.inductionOn'.pos.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Injective affine maps preserve affine independence.  -/
AffineMap.affineIndependent_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂),
  Function.Injective ⇑f → (AffineIndependent k (⇑f ∘ p) ↔ AffineIndependent k p)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq.inj : ∀ {lhs : ℕ} {rhs : Lean.Meta.Grind.CnstrRHS} {lhs_1 : ℕ} {rhs_1 : Lean.Meta.Grind.CnstrRHS},
  Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq lhs rhs =
      Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq lhs_1 rhs_1 →
    lhs = lhs_1 ∧ rhs = rhs_1
-- Init.Data.SInt.Lemmas
Int32.ofNat_int8ToNatClampNeg : ∀ (x : Int8), 0 ≤ x → Int32.ofNat x.toNatClampNeg = x.toInt32
-- Mathlib.Analysis.Convex.Function
ConvexOn.lt_right_of_left_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ openSegment 𝕜 x y → f x < f z → f z < f y
-- Lean.Util.LeanOptions
Lean.instReprLeanOption.repr : Lean.LeanOption → ℕ → Std.Format
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.nonneg_iff_isSelfAdjoint_and_negPart_eq_zero : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A]
  [T2Space A] {a : A}, 0 ≤ a ↔ IsSelfAdjoint a ∧ a⁻ = 0
-- Init.Data.BitVec.Lemmas
BitVec.clz_le : ∀ {w : ℕ} {x : BitVec w}, x.clz ≤ ↑w
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.IsFiltered.initial_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofiltered C], (CategoryTheory.Prod.snd C D).Initial
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.matchesAt_iff_splits : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt c pos ↔ ∃ t₁ t₂, pos.Splits t₁ (String.singleton c ++ t₂)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ),
  Set.EqOn (deriv (L.weierstrassPExcept l₀)) (L.derivWeierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h))
      (X.toCycles f g fg h n) =
    0
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_mod_eq_head! : ∀ (b : ℕ) (l : List ℕ), Nat.ofDigits b l % b = l.head! % b
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.sInf_toNonUnitalSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)),
  (sInf S).toNonUnitalSubsemiring = sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S)
-- Init.Data.Int.ToString
_private.Init.Data.Int.ToString.0.Int.repr.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (m : ℕ) (h_1 : (m : ℕ) → motive (Int.ofNat m)) (h_2 : (m : ℕ) → motive (Int.negSucc m)),
  (match Int.ofNat m with
    | Int.ofNat m => h_1 m
    | Int.negSucc m => h_2 m) =
    h_1 m
-- Init.Data.Option.Lemmas
Option.join_le : ∀ {α : Type u_1} [inst : LE α] {o : Option (Option α)} {o' : Option α}, o.join ≤ o' ↔ o ≤ some o'
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.normal : IO.Promise Unit → Std.CancellationToken.Consumer