mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Matrix.Normed
/-- The `L₁-L∞` norm preserves one on non-empty matrices. Note this is safe as an instance, as it
carries no data.  -/
Matrix.linfty_opNormOneClass : ∀ {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : SeminormedRing α] [NormOneClass α] [inst_3 : DecidableEq n]
  [Nonempty n], NormOneClass (Matrix n n α)
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- **Divergence theorem** for functions on the plane. It is formulated in terms of two functions
`f g : ℝ × ℝ → E` and iterated integral `∫ x in a₁..b₁, ∫ y in a₂..b₂, _`, where
`a₁ a₂ b₁ b₂ : ℝ`. When thinking of `f` and `g` as the two coordinates of a single function
`F : ℝ × ℝ → E × E` and when `E = ℝ`, this is the usual statement that the integral of the
divergence of `F` inside the rectangle with vertices `(aᵢ, bⱼ)`, `i, j =1,2`, equals the integral of
the normal derivative of `F` along the boundary.

See also `MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le`
for a version that uses an integral over `Icc a b`, where `a b : ℝ × ℝ`, `a ≤ b`.  -/
MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f g : ℝ × ℝ → E)
  (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ) (s : Set (ℝ × ℝ)),
  s.Countable →
    ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) →
      ContinuousOn g (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) →
          (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x) →
            MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)
                MeasureTheory.volume →
              ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
                  ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.brecOn.go : {motive_1 : Lean.Elab.Tactic.RCases.RCasesPatt → Sort u} →
  {motive_2 : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u} →
    (t : Lean.Elab.Tactic.RCases.RCasesPatt) →
      ((t : Lean.Elab.Tactic.RCases.RCasesPatt) → t.below → motive_1 t) →
        ((t : List Lean.Elab.Tactic.RCases.RCasesPatt) → Lean.Elab.Tactic.RCases.RCasesPatt.below_1 t → motive_2 t) →
          motive_1 t ×' t.below
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_finsetSum : ∀ {ι : Type u_1} {S : Type u_2} [inst : AddCommMonoid S] [inst_1 : Mul S] (t : RingCon S) (s : Finset ι) (f : ι → S),
  ↑(s.sum f) = ∑ i ∈ s, ↑(f i)
-- Mathlib.LinearAlgebra.Matrix.Permutation
Matrix.permMatrix_mulVec : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Fintype n] {v : n → R}
  [inst_2 : CommRing R], (Equiv.Perm.permMatrix R σ).mulVec v = v ∘ ⇑σ
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
/-- A morphism `q` satisfies `[InnerFibration q]` if it belongs to `innerFibrations`.  -/
SSet.InnerFibration : {X Y : SSet} → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Order.Field.Basic
div_le_div_of_nonpos_of_le : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c ≤ 0 → b ≤ a → a / c ≤ b / c
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.cons : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α × Bool},
  FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red.Step (x :: L₁) (x :: L₂)
-- Aesop.Util.Basic
Aesop.time' : {m : Type → Type u_1} → [Monad m] → [MonadLiftT BaseIO m] → m Unit → m Aesop.Nanos
-- Mathlib.Analysis.Meromorphic.Order
meromorphicOrderAt_of_not_meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, ¬MeromorphicAt f x → meromorphicOrderAt f x = 0
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- Given `c : F.CoconeTypes` and a map `φ : c.pt → T`, this is
the cocone for `F` obtained by postcomposition with `φ`.  -/
CategoryTheory.Functor.CoconeTypes.postcomp : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} → (c : F.CoconeTypes) → {T : Type w₂} → (c.pt → T) → F.CoconeTypes
-- Mathlib.Data.Finset.Sigma
Finset.pairwiseDisjoint_map_sigmaMk : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)},
  (↑s).PairwiseDisjoint fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)
-- Mathlib.Tactic.Ring.Common
/-- A total order on normalized expressions.
This is not an `Ord` instance because it is heterogeneous.
 -/
Mathlib.Tactic.Ring.Common.ExSum.cmp : Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {bt : Q(«$α») → Type} →
        {sα : Q(CommSemiring «$α»)} →
          Mathlib.Tactic.Ring.Common.RingCompare bt →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExSum bt sα a → Mathlib.Tactic.Ring.Common.ExSum bt sα b → Ordering
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_set_notMem : ∀ {α : Type u_1} (a : α), Measurable fun s => a ∉ s
-- Mathlib.Topology.Compactness.Lindelof
coLindelof_le_cofinite : ∀ {X : Type u} [inst : TopologicalSpace X], Filter.coLindelof X ≤ Filter.cofinite
-- Mathlib.Analysis.Calculus.Deriv.Star
deriv.star : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {x : 𝕜}
  [TrivialStar 𝕜], deriv (fun y => star (f y)) x = star (deriv f x)
-- Init.Data.Vector.Lemmas
Vector.getElem_push_lt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α} {i : ℕ} (h : i < n), (xs.push x)[i] = xs[i]
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableAt_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I 1 M → ∀ {x : M}, x ∈ e.source → MDiffAt ↑e x
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_of_mem_dropn : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α} {n : ℕ}, a ∈ s.drop n → a ∈ s
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
/-- If `‖B x y‖ = ‖B · y‖ * ‖x‖` for all `x, y`, then the variation of a vector measure with
density `f` wrt `μ` is the measure with density `‖f‖ₑ` with respect to the variation of `μ`.

The condition on `B` is necessary: for a counterexample without it, let `B` be the scalar
product in `ℝ²` and `f x` everywhere horizontal and `μ s` everywhere vertical.
Then `μ.withDensity f B = 0` so its variation is zero, while the integral of `‖f‖ₑ` is not.

See also `variation_withDensity` under the very common condition `‖B x y‖ = ‖x‖ ‖y‖`.
 -/
MeasureTheory.VectorMeasure.variation_withDensity' : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {B : E →L[ℝ] F →L[ℝ] G}
  [CompleteSpace G],
  μ.Integrable f →
    (∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊) →
      (μ.withDensity f B).variation = (μ.transpose B).variation.withDensity fun x => ‖f x‖ₑ
-- Std.Time.Format.Modifier
Std.Time.Text.narrow.sizeOf_spec : sizeOf Std.Time.Text.narrow = 1
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.instInfSet.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M],
  Submonoid.instInfSet = { sInf := fun s => { carrier := ⋂ t ∈ s, ↑t, mul_mem' := ⋯, one_mem' := ⋯ } }
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.instInvOneClass : {σ : Type u_1} → {k : Type u_3} → [Field k] → InvOneClass (MvPowerSeries σ k)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.coeff_coeff_finSuccEquiv : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (p : MvPowerSeries (Fin (n + 1)) R) {k : ℕ} {x : Fin n →₀ ℕ},
  (MvPowerSeries.coeff x) ((PowerSeries.coeff k) ((MvPowerSeries.finSuccEquiv R n) p)) =
    (MvPowerSeries.coeff (Finsupp.cons k x)) p
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `mdifferentiableAt_iff_localFrameCoeff`.

---

A section `s` of `V` is differentiable at `x ∈ e.baseSet` iff each of its
coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is  -/
mdifferentiableAt_iff_localFrame_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {x' : M}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜],
  x' ∈ e.baseSet →
    (MDiffAt (T% s) x' ↔ ∀ (i : ι), MDiffAt ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) x')
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.Pos.skipWhile.eq_1 : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- Any coreflective inclusion has a comonadic left adjoint.
cf Dual statement of Prop 5.3.3 of [Riehl][riehl2017]  -/
CategoryTheory.comonadicOfCoreflective : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {R : CategoryTheory.Functor D C} → [CategoryTheory.Coreflective R] → CategoryTheory.ComonadicLeftAdjoint R
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.uliftFunctor.eq_1 : AddMonCat.uliftFunctor =
  { obj := fun X => AddMonCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      AddMonCat.ofHom
        (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddMonCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.int : ℤ → Aesop.Frontend.Priority
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.pure : {m : Type w → Type w'} → [Pure m] → {α : Type w} → α → Std.Iterators.PostconditionT m α
-- Mathlib.Algebra.Lie.OfAssociative
AlgHom.instCoeLieHom : {A : Type v} →
  [inst : Ring A] →
    {R : Type u} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R A] → {B : Type w} → [inst_3 : Ring B] → [inst_4 : Algebra R B] → Coe (A →ₐ[R] B) (A →ₗ⁅R⁆ B)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.maxDegree.congr_simp : ∀ {V : Type u_1} (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ [inst : Fintype V] {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj], G.maxDegree = G_1.maxDegree
-- Init.Data.Order.Ord
Std.LawfulBEqOrd.compare_eq_iff_beq : ∀ {α : Type u} {x : Ord α} {x_1 : BEq α} [Std.LawfulBEqOrd α] {a b : α}, compare a b = Ordering.eq ↔ (a == b) = true
-- Mathlib.RingTheory.Algebraic.Integral
/-- **Alias** of the forward direction of `isAlgebraic_iff_isIntegral`.

---

An element of an algebra over a field is algebraic if and only if it is integral.  -/
IsAlgebraic.isIntegral : ∀ {K : Type u} {A : Type v} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A] {x : A},
  IsAlgebraic K x → IsIntegral K x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.unitOfArray_eq_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} (a : Array α),
  Std.DHashMap.Const.unitOfArray a = Std.DHashMap.Const.unitOfList a.toList
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Theorems : Type → Type
-- Mathlib.Topology.MetricSpace.Bounded
Metric.hasBasis_nhds_isOpen_isBounded : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α),
  (nhds x).HasBasis (fun a => x ∈ a ∧ IsOpen a ∧ Bornology.IsBounded a) id
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift_surjective : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑f → Function.Surjective ⇑(DividedPowerAlgebra.map R f)
-- Init.Data.String.Subslice
String.Slice.Subslice.extendLeft_extendLeft : ∀ {s : String.Slice} {sl : s.Subslice} (p₁ p₂ : s.Pos) (h₂ : p₂ ≤ sl.startInclusive)
  (h₁ : p₁ ≤ (sl.extendLeft p₂ h₂).startInclusive), (sl.extendLeft p₂ h₂).extendLeft p₁ h₁ = sl.extendLeft p₁ ⋯
-- Mathlib.Algebra.Order.Sub.Defs
/-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add_rev` assuming that `a = b + c` itself is
cancellable rather than `b`.  -/
AddLECancellable.tsub_eq_of_eq_add_rev' : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], AddLECancellable a → a = b + c → a - b = c
-- Mathlib.Logic.Denumerable
Denumerable.prod_ofNat_val : ∀ {α : Type u_1} {β : Type u_2} [inst : Denumerable α] [inst_1 : Denumerable β] (n : ℕ),
  Denumerable.ofNat (α × β) n = (Denumerable.ofNat α (Nat.unpair n).1, Denumerable.ofNat β (Nat.unpair n).2)
-- Mathlib.Dynamics.Ergodic.Action.Basic
ergodicVAdd_iff : ∀ (G : Type u_1) (α : Type u_2) [inst : VAdd G α] {x : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  ErgodicVAdd G α μ ↔
    MeasureTheory.VAddInvariantMeasure G α μ ∧
      ∀ {s : Set α},
        MeasurableSet s → (∀ (g : G), (fun x => g +ᵥ x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.AddConvolutionExists.distrib_add : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [T2Space F]
  [ContinuousAdd F] {f : M → E} {g g' : M → E'} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.AddConvolutionExists L f g →
    DiscreteConvolution.AddConvolutionExists L f g' →
      DiscreteConvolution.addConvolution L f (g + g') =
        DiscreteConvolution.addConvolution L f g + DiscreteConvolution.addConvolution L f g'
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_obj : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) (a : CategoryTheory.Pairwise ι),
  (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U).obj a =
    TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj U a
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_same_apply : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p : P1) (c : k), (AffineMap.lineMap p p) c = p
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β},
  m.WF →
    m.getKey? k = some k' →
      (Std.HashMap.Raw.filter f m).getD k fallback = (Option.filter (fun x => f k' x) m[k]?).getD fallback
-- Lean.Meta.Basic
/-- Execute `x` using approximate unification: `foApprox`, `ctxApprox` and `quasiPatternApprox`.   -/
Lean.Meta.approxDefEq : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.Trace.off.sizeOf_spec : sizeOf Lean.Lsp.Trace.off = 1
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGE.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, (compare a k).isGE = true) → Sort u_3)
  (size : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
  (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_2 size ky y l r ho he
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_neg : ∀ (a : BitVec System.Platform.numBits), ISize.ofBitVec (-a) = -ISize.ofBitVec a
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.mk.sizeOf_spec : ∀ {M : Type u_10} {N : Type u_11} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : SizeOf M] [inst_3 : SizeOf N]
  (toOneHom : OneHom M N) (map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y),
  sizeOf { toOneHom := toOneHom, map_mul' := map_mul' } = 1 + sizeOf toOneHom
-- Mathlib.Analysis.SpecificLimits.Normed
hasSum_geom_series_inverse : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (x : R),
  ‖x‖ < 1 → HasSum (fun i => x ^ i) (Ring.inverse (1 - x))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The equivalence `equivIoc` is measure preserving with respect to the natural volume measures.  -/
AddCircle.measurePreserving_equivIoc : ∀ (T : ℝ) [hT : Fact (0 < T)] {a : ℝ},
  MeasureTheory.MeasurePreserving (⇑(AddCircle.equivIoc T a)) MeasureTheory.volume
    (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_congr : ∀ {α : Type u_2} {P : α → Prop} (m : (s : α) → P s → ENNReal) {β : Type u_3} {Pb : β → Prop}
  {mb : (s : β) → Pb s → ENNReal} {sa : α} {sb : β},
  (P sa ↔ Pb sb) →
    (∀ (ha : P sa) (hb : Pb sb), m sa ha = mb sb hb) → MeasureTheory.extend m sa = MeasureTheory.extend mb sb
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of a measurable function is smaller than its mean.  -/
MeasureTheory.exists_le_setLAverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  μ s ≠ 0 → μ s ≠ ⊤ → AEMeasurable f (μ.restrict s) → ∃ x ∈ s, f x ≤ ⨍⁻ (a : α) in s, f a ∂μ
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.isUnit_iff_bijective : ∀ {f : CircleDeg1Lift}, IsUnit f ↔ Function.Bijective ⇑f
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_one_iff_eq : ∀ {α : Type u_2} [inst : One α] {s : Finset α}, s ⊆ 1 ↔ s = ∅ ∨ s = 1
-- Mathlib.Order.LiminfLimsup
Filter.liminf_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α},
  Filter.liminf u f = sSup {a | ∀ᶠ (n : β) in f, a ≤ u n}
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_2_comp_chainsIso₂_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : (Fin 2 → G) →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ B).hom)
      ((CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap f φ).f 2)) x) =
    Finsupp.mapRange ⇑(Rep.Hom.hom φ) ⋯
      (Finsupp.mapDomain (Prod.map ⇑f ⇑f) ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ A).hom) x))
-- Mathlib.CategoryTheory.Noetherian
CategoryTheory.Noetherian.toEssentiallySmall : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Noetherian C],
  CategoryTheory.EssentiallySmall.{u_2, v_1, u_1} C
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment.eq_1 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.addNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.rnDeriv_sub : ∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ] [hst : (s - t).HaveLebesgueDecomposition μ],
  (s - t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ - t.rnDeriv μ
-- Mathlib.CategoryTheory.Sites.MorphismProperty
/-- If `P` is stable under base change, it induces a Grothendieck topology: the one associated
to `coverage P`.  -/
CategoryTheory.MorphismProperty.grothendieckTopology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [P.IsStableUnderBaseChange] → [P.HasPullbacks] → CategoryTheory.GrothendieckTopology C
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.isCommMonObj_mk_pullbackSnd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [inst_2 : CategoryTheory.MonObj (CategoryTheory.Over.mk f)]
  [CategoryTheory.IsCommMonObj (CategoryTheory.Over.mk f)],
  CategoryTheory.IsCommMonObj (CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd f g))
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  {a : X} [inst_5 : LinearOrder X] [CompactIccSpace X] [NoMinOrder X] [OrderTopology X],
  MeasureTheory.IntegrableOn f (Set.Iio a) μ ↔
    MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧
      MeasureTheory.IntegrableAtFilter f (nhdsWithin a (Set.Iio a)) μ ∧
        MeasureTheory.LocallyIntegrableOn f (Set.Iio a) μ
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.seq.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ κ_1 : ProbabilityTheory.Kernel α β)
  (e_κ : κ = κ_1) [h : ProbabilityTheory.IsSFiniteKernel κ] (a a_1 : ℕ), a = a_1 → κ.seq a = κ_1.seq a_1
-- Aesop.Forward.SlotIndex
Aesop.SlotIndex : Type
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.iUnion : ∀ {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} [Countable ι] {s : ι → Set α},
  (∀ (i : ι), TopologicalSpace.IsSeparable (s i)) → TopologicalSpace.IsSeparable (⋃ i, s i)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_sub : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [inst_2 : IsTopologicalAddGroup M] (v w : MeasureTheory.VectorMeasure α M) (i : Set α),
  (v - w).restrict i = v.restrict i - w.restrict i