mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Basic
/-- Optimized version of `sigma`.  -/
List.sigmaTR : {α : Type u_1} → {σ : α → Type u_2} → List α → ((a : α) → List (σ a)) → List ((a : α) × σ a)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.fderivCLM_apply_of_gt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜]
  [inst_7 : IsScalarTower ℝ 𝕜 F], n < k + 1 → TestFunction.fderivCLM 𝕜 n k = 0
-- Mathlib.Topology.Semicontinuity.Basic
continuousOn_iff_lower_upperSemicontinuousOn : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ},
  ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edges_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).edges = s(u, v) :: p.edges
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzOnWith_iff_norm_sub_le`. -/
LipschitzOnWith.norm_sub_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {f : E → F}
  {C : NNReal} {s : Set E}, LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion_pos_iff : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G},
  K < 1 → S.Nonempty → (0 < Finset.expansion✝ K S A ↔ A.Nonempty)
-- Init.Data.SInt.Lemmas
Int8.toBitVec_ofBitVec : ∀ (b : BitVec 8), (Int8.ofBitVec b).toBitVec = b
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] (F : Ctop.Realizer α) (s : F.σ), IsOpen (F.F.f s)
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleData.unsafe_impl_2 : System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.discard_comp : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  μ.bind ⇑(ProbabilityTheory.Kernel.discard α) = μ Set.univ • MeasureTheory.Measure.dirac ()
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.findSomeM?_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__do_lift : Option γ) → (Unit → motive none) → ((fx : γ) → motive (some fx)) → motive __do_lift
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.left_mem_support : ∀ {V : Type u} (G : SimpleGraph V) {u v : V}, G.Adj u v → u ∈ G.support
-- Mathlib.Algebra.Notation.Prod
Prod.instMul.eq_1 : ∀ {M : Type u_8} {N : Type u_9} [inst : Mul M] [inst_1 : Mul N],
  Prod.instMul = { mul := fun p q => (p.1 * q.1, p.2 * q.2) }
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_indicator_comm : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Zero β] {s : Set Ω} (i : ι),
  MeasureTheory.stoppedProcess (fun i => s.indicator (u i)) τ i = s.indicator (MeasureTheory.stoppedProcess u τ i)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.prevn : ∀ {m₂ m₁ : List Char} {s : Substring.Raw},
  s.Valid →
    s.toString.toList = m₁.reverse ++ m₂ →
      ∀ (n : ℕ), s.prevn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len (List.drop n m₁) }
-- Mathlib.Data.ENNReal.Basic
ENNReal.one_le_coe_iff : ∀ {r : NNReal}, 1 ≤ ↑r ↔ 1 ≤ r
-- Mathlib.Topology.Covering.Basic
/-- A point `x : X` is evenly covered by `f : E → X` if `x` has an evenly covered neighborhood.

**Remark**: `DiscreteTopology I ∧ ∃ Trivialization I f, x ∈ t.baseSet` would be a simpler
definition, but unfortunately it does not work if `E` is nonempty but nonetheless `f` has empty
fibers over `s`. If `OpenPartialHomeomorph` could be refactored to work with an empty space and a
nonempty space while preserving the APIs, we could switch back to the definition.  -/
IsEvenlyCovered : {E : Type u_1} →
  {X : Type u_2} →
    [TopologicalSpace E] → [TopologicalSpace X] → (E → X) → X → (I : Type u_3) → [TopologicalSpace I] → Prop
-- Lean.Data.Lsp.Capabilities
/-- The client supports versioned document changes in `WorkspaceEdit`s.  -/
Lean.Lsp.WorkspaceEditClientCapabilities.documentChanges? : Lean.Lsp.WorkspaceEditClientCapabilities → Option Bool
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeEndWhile_eq_sliceFrom_skipSuffixWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  s.takeEndWhile pat = s.sliceFrom (s.skipSuffixWhile pat)
-- Mathlib.Data.ENNReal.Action
ENNReal.smulCommClass_left : ∀ {M : Type u_1} {N : Type u_2} [inst : MulAction ENNReal N] [inst_1 : SMul M N] [SMulCommClass ENNReal M N],
  SMulCommClass NNReal M N
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_toPartialEquiv : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y'),
  (eX.prod eY).toPartialEquiv = eX.prod eY.toPartialEquiv
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The diagonal `fun x ↦ f x x` of a polynomial function `f` is polynomial.  -/
WittVector.IsPoly₂.diag : ∀ {p : ℕ} {f : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R}
  [hf : WittVector.IsPoly₂ p f], WittVector.IsPoly p fun x _Rcr x_1 => f x_1 x_1
-- Mathlib.Probability.Process.LocalProperty
/-- If `p, q, r` are stable properties and `r` and `p` implies locally `q`, then `r` locally
and `p` locally imply `q` locally.  -/
ProbabilityTheory.IsStable.locally_induction₂ : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : ConditionallyCompleteLinearOrderBot ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} [SecondCountableTopology ι]
  [MeasureTheory.IsFiniteMeasure P] [DenselyOrdered ι] [NoMaxOrder ι] [inst_7 : Zero E] {r : (ι → Ω → E) → Prop}
  [𝓕.IsRightContinuous],
  (∀ (Y : ι → Ω → E), r Y → p Y → ProbabilityTheory.Locally q 𝓕 Y P) →
    ProbabilityTheory.IsStable 𝓕 r →
      ProbabilityTheory.IsStable 𝓕 p →
        ProbabilityTheory.IsStable 𝓕 q →
          ProbabilityTheory.Locally r 𝓕 X P → ProbabilityTheory.Locally p 𝓕 X P → ProbabilityTheory.Locally q 𝓕 X P
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.shape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m : ℤ),
  n + 1 ≠ m → h.d n m = 0
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquiv_refl : ∀ {A : Type u_8} {K : Type u_9} [inst : CommRing A] [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K], IsFractionRing.ringEquivOfRingEquiv (RingEquiv.refl A) = RingEquiv.refl K
-- Mathlib.Order.Interval.Finset.Box
_private.Mathlib.Order.Interval.Finset.Box.0.Finset.Icc_neg_mono : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : LocallyFiniteOrder α],
  Monotone fun n => Finset.Icc (-↑n) ↑n
-- Lean.Expr
_private.Lean.Expr.0.Lean.mkAppRangeAux.eq_def : ∀ (n : ℕ) (args : Array Lean.Expr) (i : ℕ) (e : Lean.Expr),
  Lean.mkAppRangeAux✝ n args i e = if i < n then Lean.mkAppRangeAux✝ n args (i + 1) (Lean.mkApp e args[i]!) else e
-- Mathlib.Data.Set.Function
/-- **Alias** of `Set.injOn_of_injective`. -/
Function.Injective.injOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ {s : Set α}, Set.InjOn f s
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.comp_functor : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₃ : CategoryTheory.MorphismProperty C₃} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (Ψ : CategoryTheory.LocalizerMorphism W₂ W₃), (Φ.comp Ψ).functor = Φ.functor.comp Ψ.functor
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_left_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).left.i = S.iCycles
-- Mathlib.LinearAlgebra.RootSystem.Reduced
/-- A root pairing is said to be reduced if any linearly dependent pair of roots is related by a
sign.

TODO Consider redefining this to make it perfectly symmetric between roots and coroots (i.e., so
that the same demand is made of coroots) and turning `RootPairing.instFlipIsReduced` into a
convenience constructor.  -/
RootPairing.IsReduced : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.eq : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (h : f.Homotopy g), f.homotopyClass = g.homotopyClass
-- Init.Data.UInt.Basic
instXorOpUSize : XorOp USize
-- Mathlib.Data.Sym.Basic
Sym.replicate_right_injective : ∀ {α : Type u_1} {n : ℕ}, n ≠ 0 → Function.Injective (Sym.replicate n)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.combine'.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  (match fuel.succ with
    | 0 => h_1 ()
    | fuel.succ => h_2 fuel) =
    h_2 fuel
-- Lean.Setup
Lean.Plugin.instCoeFilePath : Coe System.FilePath Lean.Plugin
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.const_mem_Lp : ∀ {E : Type u_4} {p : ENNReal} [inst : NormedAddCommGroup E] (α : Type u_6) {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (c : E) [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEEqFun.const α c ∈ MeasureTheory.Lp E p μ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSliceData : (α : Type u) → Type v → [Ord α] → Type (max u v)
-- Mathlib.Data.Complex.Basic
Complex.intCast_re : ∀ (n : ℤ), (↑n).re = ↑n
-- Mathlib.Data.Num.Lemmas
Num.castNum_and : ∀ (m n : Num), ↑(m &&& n) = ↑m &&& ↑n
-- Batteries.Data.Vector.Lemmas
Vector.get_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} (v : Vector α n) (f : α → β) (i : Fin n), (Vector.map f v).get i = f (v.get i)
-- Init.Data.List.Nat.Range
List.reverse_range' : ∀ {s n : ℕ}, (List.range' s n).reverse = List.map (fun x => s + n - 1 - x) (List.range n)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_smul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] {R : Type u_14} [inst_1 : Zero α]
  [inst_2 : SMulZeroClass R α] (x : R) (M : o → Matrix m n α), Matrix.blockDiagonal (x • M) = x • Matrix.blockDiagonal M
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The **Cauchy-Schwarz inequality** for positive semidefinite symmetric forms.  -/
LinearMap.BilinForm.apply_sq_le_of_symm : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (∀ (x : M), 0 ≤ (B x) x) → LinearMap.IsSymm B → ∀ (x y : M), (B x) y ^ 2 ≤ (B x) x * (B y) y
-- Mathlib.Data.Fintype.Powerset
Finset.powerset_univ : ∀ {α : Type u_1} [inst : Fintype α], Finset.univ.powerset = Finset.univ
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fg_iff_mul_fg : ∀ {M : Type u_3} [inst : AddMonoid M], AddMonoid.FG M ↔ Monoid.FG (Multiplicative M)
-- Mathlib.Order.CompleteLattice.Lemmas
/-- This is a weaker version of `inf_sSup_eq`  -/
iSup_inf_le_inf_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, ⨆ b ∈ s, a ⊓ b ≤ a ⊓ sSup s
-- Init.Data.String.Basic
String.Slice.replaceEnd : (s : String.Slice) → s.Pos → String.Slice
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Prokhorov theorem**: Given a sequence of compact sets `Kₙ` and a sequence `uₙ` tending
to zero, the finite measures of mass at most `C` giving mass at most `uₙ` to the complement of `Kₙ`
form a compact set.  -/
isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal),
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ (n : ℕ), IsCompact (K n)) → NormalSpace E ∨ Monotone K → IsCompact {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
-- Mathlib.Order.Heyting.Basic
/-- See `le_sdiff` for a stronger version in generalised Boolean algebras.  -/
Disjoint.le_sdiff_of_le_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, Disjoint a c → a ≤ b → a ≤ b \ c
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.existsProp.inj : ∀ {e e_1 : Lean.Expr}, Lean.Meta.Grind.SplitSource.existsProp e = Lean.Meta.Grind.SplitSource.existsProp e_1 → e = e_1
-- Mathlib.Data.UInt
UInt64.toBitVec_injective : Function.Injective UInt64.toBitVec
-- Init.Data.Int.DivMod.Lemmas
/-- If `n > 0` then `m` is not divisible by `n` iff it is between `n * k` and `n * (k + 1)`
for some `k`.  -/
Int.not_dvd_iff_lt_mul_succ : ∀ {n : ℤ} (m : ℤ), 0 < n → (¬n ∣ m ↔ ∃ k, n * k < m ∧ m < n * (k + 1))
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.insertMany : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type u_1} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  {t : Std.DTreeMap.Internal.Impl α β} {l : ρ} {h : t.Balanced}, t.WF → (↑(t.insertMany l h)).WF
-- Init.Data.Nat.Basic
Nat.le_add_left_of_le : ∀ {n m k : ℕ}, n ≤ m → n ≤ k + m
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.imp_to_or : ∀ (a b : Bool), (a = true → b = true) = ((!a || b) = true)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.SavedState.restore : Lean.Elab.Do.SavedState → optParam Bool false → Lean.Elab.Do.DoElabM Unit
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.versoSyntaxToString'.endBlock : ReaderT ℕ (StateM String) Unit
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.ltProp : LT Lean.JsonRpc.RequestID
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- `μ` is the Möbius function. If `n` is squarefree with an even number of distinct prime factors,
`μ n = 1`. If `n` is squarefree with an odd number of distinct prime factors, `μ n = -1`.
If `n` is not squarefree, `μ n = 0`.  -/
ArithmeticFunction.moebius : ArithmeticFunction ℤ
-- Mathlib.AlgebraicGeometry.Restrict
/-- If `U ≤ V` are opens of `X`, the restriction of `U` to `V` is isomorphic to `U`.  -/
AlgebraicGeometry.Scheme.Opens.isoOfLE : {X : AlgebraicGeometry.Scheme} → {U V : X.Opens} → U ≤ V → (↑((TopologicalSpace.Opens.map V.ι.base).obj U) ≅ ↑U)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_rio : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (bound : α),
      Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) =
        List.filter (fun e => (compare e.fst bound).isLT) t.toList
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.convs'Aux.eq_1 : ∀ {K : Type u_2} [inst : DivisionRing K] (x : Stream'.Seq (GenContFract.Pair K)), GenContFract.convs'Aux x 0 = 0
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.isIso_of_isIso_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} {X Y : CategoryTheory.GradedObject β C}
  (f : X ⟶ Y) [hf : ∀ (i : β), CategoryTheory.IsIso (f i)], CategoryTheory.IsIso f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- The continuous functional calculus commutes with integration.
For a version with stronger assumptions which in practice are often easier to verify, see
`cfc_setIntegral`.  -/
cfc_setIntegral' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [inst_6 : CompleteSpace A] {s : Set X} [inst_7 : NormedSpace ℝ A]
  (f : X → 𝕜 → 𝕜) (a : A),
  (∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)) →
    MeasureTheory.IntegrableOn (fun x => ContinuousMap.mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) s μ →
      autoParam (p a) cfc_setIntegral'._auto_1 →
        cfc (fun z => ∫ (x : X) in s, f x z ∂μ) a = ∫ (x : X) in s, cfc (f x) a ∂μ
-- Mathlib.FieldTheory.SeparableClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the preimage of
`separableClosure F K` under the map `i` is equal to `separableClosure F E`.  -/
separableClosure.comap_eq_of_algHom : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E →ₐ[F] K), IntermediateField.comap i (separableClosure F K) = separableClosure F E
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- `padicValInt p 0` is `0` for any `p`.  -/
padicValInt.zero : ∀ {p : ℕ}, padicValInt p 0 = 0
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.norm_def' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i),
  ‖f‖ = ↑(Finset.univ.sup fun b => ‖f b‖₊)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.map_adjoin_singleton : ∀ {F : Type u_1} (R : Type u) (A : Type v) {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] [inst_7 : IsScalarTower R A A] [inst_8 : SMulCommClass R A A]
  [inst_9 : IsScalarTower R B B] [inst_10 : SMulCommClass R B B] (f : F) (x : A),
  NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R {x}) = NonUnitalAlgebra.adjoin R {f x}
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.shiftFunctorZero_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) (X : t.Category),
  (CategoryTheory.shiftFunctorZero t.Category A).hom.app X =
    CategoryTheory.CategoryStruct.comp ((t.shiftIso 0).hom.app X) ((CategoryTheory.shiftFunctorZero C A).hom.app X)
-- Lean.Meta.Basic
/-- `forallTelescopeAuxAux lctx fvars j type`
Remarks:
- `lctx` is the `MetaM` local context extended with declarations for `fvars`.
- `type` is the type we are computing the telescope for. It contains only
  dangling bound variables in the range `[j, fvars.size)`
- if `reducing? == true` and `type` is not `forallE`, we use `whnf`.
- when `type` is not a `forallE` nor it can't be reduced to one, we
  execute the continuation `k`.

Here is an example that demonstrates the `reducing?`.
Suppose we have
```
abbrev StateM s a := s -> Prod a s
```
Now, assume we are trying to build the telescope for
```
forall (x : Nat), StateM Int Bool
```
if `reducing == true`, the function executes `k #[(x : Nat) (s : Int)] Bool`.
if `reducing == false`, the function executes `k #[(x : Nat)] (StateM Int Bool)`

if `maxFVars?` is `some max`, then we interrupt the telescope construction
when `fvars.size == max`


If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.

If `whnfIfReducing` is true, then in the `reducing == true` case, `k` is given the whnf of the type.
This does not have any performance cost.
 -/
_private.Lean.Meta.Basic.0.Lean.Meta.forallTelescopeReducingAuxAux : {α : Type} → Bool → Option ℕ → Lean.Expr → (Array Lean.Expr → Lean.Expr → Lean.MetaM α) → Bool → Bool → Lean.MetaM α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSymbolInformation : Lean.ToJson Lean.Lsp.SymbolInformation
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrRight_symm : ∀ {ι : Type u_7} {R : ι → Type u_8} {S : ι → Type u_9} [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (S i)] (e : (i : ι) → R i ≃+* S i),
  (RingEquiv.piCongrRight e).symm = RingEquiv.piCongrRight fun i => (e i).symm
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.instEvalExprConfig_1.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.DSimp.Config
-- Lean.Parser.Term
Lean.Parser.Term.char.formatter : Lean.PrettyPrinter.Formatter
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr),
  Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s =
    if hcurr : curr < w then
      let input := { discr := discr, lhs := lhs.get curr hcurr, rhs := rhs.get curr hcurr };
      let res := aig.mkIfCached input;
      let aig_1 := res.aig;
      have ref := res.ref;
      have this := ⋯;
      have discr_1 := discr.cast this;
      have lhs_1 := lhs.cast this;
      have rhs_1 := rhs.cast this;
      have s := s.cast this;
      have s := s.push ref;
      Std.Sat.AIG.RefVec.ite.go aig_1 (curr + 1) ⋯ discr_1 lhs_1 rhs_1 s
    else
      have this := ⋯;
      { aig := aig, vec := this ▸ s }
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (hd : CategoryTheory.Limits.IsColimit d),
  (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).functor = I.toSigmaCoforkFunctor hc hd
-- Mathlib.Dynamics.Newton
Polynomial.newtonMap_apply_of_isUnit : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  {x : S} (h : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))),
  P.newtonMap x = x - ↑h.unit⁻¹ * (Polynomial.aeval x) P
-- Batteries.Data.Array.Basic
/-- Fold a function `f` over the subarray from the left, returning the list of partial results.
 -/
Subarray.scanl : {β : Type u_1} → {α : Type u_2} → (β → α → β) → β → Subarray α → Array β
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.abs_cpow_inv_two_im : ∀ (x : ℂ), |(x ^ 2⁻¹).im| = √((‖x‖ - x.re) / 2)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.add_def : ∀ (α : Type u_2) (t₁ t₂ : FirstOrder.Language.ring.Term α), t₁ + t₂ = FirstOrder.Ring.addFunc.apply₂ t₁ t₂
-- Init.Data.ByteArray.Lemmas
_private.Init.Data.ByteArray.Lemmas.0.ByteArray.size.match_1.splitter : (motive : ByteArray → Sort u_1) → (x : ByteArray) → ((bs : Array UInt8) → motive { data := bs }) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.penultimate.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.penultimate = p.getVert (p.length - 1)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.eq_weierstrassDistinguished_mul_weierstrassUnit : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0),
  g = ↑(g.weierstrassDistinguished hg) * g.weierstrassUnit hg