mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSlice.instToIterator : {α : Type u_1} →
  {β : Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RciSliceData α β)) Id
        (Std.Iterators.Types.Map (Std.DTreeMap.Internal.Zipper α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
          pure (b.fst, b.snd))
        (α × β)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.compProd_toKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel ν]
  (hf : ProbabilityTheory.IsCondKernelCDF f κ ν), ν.compProd (ProbabilityTheory.IsCondKernelCDF.toKernel f hf) = κ
-- Mathlib.Probability.Distributions.Gaussian.CharFun
ProbabilityTheory.IsGaussian.charFunDual_eq' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : NormedSpace ℝ E]
  [ProbabilityTheory.IsGaussian μ] (L : StrongDual ℝ E),
  MeasureTheory.charFunDual μ L =
    Complex.exp (↑(L (∫ (x : E), id x ∂μ)) * Complex.I - ↑(((ProbabilityTheory.covarianceBilinDual μ) L) L) / 2)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.eq_boolKernel : ∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel Bool α),
  κ = ProbabilityTheory.Kernel.boolKernel (κ false) (κ true)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {f : α → β → Bool} {k k' : α},
  m.getKey? k = some k' → (Std.ExtHashMap.filter f m)[k]! = (Option.filter (f k') m[k]?).get!
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.coe_lt : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : Preorder β] {f g : α → β}, ↑f < ↑g ↔ ∀ᶠ (x : α) in ↑φ, f x < g x
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.subtype_bot_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α], ⟨∅, ⋯⟩ = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.nonempty_supp : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent), C.supp.Nonempty
-- Std.Time.DateTime.Timestamp
Std.Time.instTransOrdTimestamp : Std.TransOrd Std.Time.Timestamp
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.expMap =
    OpenPartialHomeomorph.pi fun w => NumberField.mixedEmbedding.fundamentalCone.expMap_single w
-- Init.Data.Range.Polymorphic.PRange
Std.Rcc.mk : {α : Type u} → α → α → Std.Rcc α
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.inclusion_self : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M),
  FirstOrder.Language.Substructure.inclusion ⋯ = FirstOrder.Language.Embedding.refl L ↥S
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- A morphism of Lie-Rinehart algebras, from `(A₁, L₁)` to `(A₂, L₂)`, consists of a pair of maps
`(σ, F)` where `σ : A₁ → A₂` is a morphism of algebras and `F` is a morphism of Lie algebras, which
respect the module structures.

Here we define the type of such morphisms with fixed `σ` (which can be regarded as functions
`L₁ → L₂`). In the future it may be useful to define the type of such morphisms with fixed `F`
(which can be regarded as functions `A₁ → A₂`) and the type of all such morphisms (which can be
regarded as functions `A₁ × L₁ → A₂ × L₂`).  -/
LieRinehartAlgebra.«term_→ₗ⁅_⁆_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The structure map `Proj A ⟶ Spec A₀`.  -/
AlgebraicGeometry.Proj.toSpecZero : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] → AlgebraicGeometry.Proj 𝒜 ⟶ AlgebraicGeometry.Spec (CommRingCat.of ↥(𝒜 0))
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.iSup_lt_lift : ∀ {ι : Type u} {f : ι → Cardinal.{max u v}} {c : Cardinal.{max u v}},
  Cardinal.lift.{v, u} (Cardinal.mk ι) < c.ord.cof → (∀ (i : ι), f i < c) → iSup f < c
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.range_map : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (c : f.Cell i) [inst_1 : P.IsProper], SSet.Subcomplex.range c.map = (↑(P.p c.s)).subcomplex
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonAssocRing : {R : Type u_1} →
  [inst : TopologicalSpace R] → [inst_1 : NonAssocRing R] → [IsTopologicalRing R] → NonAssocRing (SeparationQuotient R)
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.restrictNormalHom_continuous : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (L : IntermediateField k K)
  [inst_3 : Normal k ↥L], Continuous ⇑(AlgEquiv.restrictNormalHom ↥L)
-- Mathlib.Tactic.DefEqTransformations
/-- `refold_let x y z at loc` looks for the bodies of local definitions `x`, `y`, and `z` at the given
location and replaces them with `x`, `y`, or `z`. This is the inverse of "zeta reduction."
This also exists as a `conv`-mode tactic.
 -/
Mathlib.Tactic.refoldLetStx : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_eq_div_of_div_eq_div : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b c d : G₀}, c ≠ 0 → d ≠ 0 → a / b = c / d → a / c = b / d
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddLeftCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddRightCancelMonoid α],
  AddOpposite.instAddLeftCancelMonoid = { toAddMonoid := AddOpposite.instAddMonoid, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Algebra.Group.Finsupp
/-- `Finsupp.single` as an `AddMonoidHom`.

See `Finsupp.lsingle` in `Mathlib/LinearAlgebra/Finsupp/Defs.lean` for the stronger version as a
linear map.  -/
Finsupp.singleAddHom : {ι : Type u_1} → {M : Type u_3} → [inst : AddZeroClass M] → ι → M →+ ι →₀ M
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Given a power series `P = u • X + O(X²)` with `u` invertible,
this is the construction of a power series `Q` such that `P(Q(X)) = X`.  -/
PowerSeries.substInvFun : {R : Type u_2} → [inst : CommRing R] → (P : PowerSeries R) → [Invertible ((PowerSeries.coeff 1) P)] → ℕ → R
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lmulEquiv_eq_lidOfCompatibleSMul : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : TensorProduct.CompatibleSMul R S S S],
  Algebra.TensorProduct.lmulEquiv R S = Algebra.TensorProduct.lidOfCompatibleSMul R S S
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameParams.newName : Lean.Lsp.RenameParams → String
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_map_eval : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [inst_3 : DecidableEq ι]
  (i : ι),
  MeasureTheory.Measure.map (Function.eval i) (MeasureTheory.Measure.pi μ) =
    (∏ j ∈ Finset.univ.erase i, (μ j) Set.univ) • μ i
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pullback a distributive multiplicative action along an injective additive monoid
homomorphism.
See note [reducible non-instances].  -/
Function.Injective.distribMulAction : {M : Type u_1} →
  {A : Type u_7} →
    {B : Type u_9} →
      [inst : Monoid M] →
        [inst_1 : AddMonoid A] →
          [inst_2 : DistribMulAction M A] →
            [inst_3 : AddMonoid B] →
              [inst_4 : SMul M B] →
                (f : B →+ A) → Function.Injective ⇑f → (∀ (c : M) (x : B), f (c • x) = c • f x) → DistribMulAction M B
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.insertMany_append : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {l₁ l₂ : List ((a : α) × β a)},
  m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.prod_toFun : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddMonoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (f : A →ₜ+ B) (g : A →ₜ+ C)
  (i : A), (f.prod g) i = (f i, g i)
-- Mathlib.Algebra.Regular.SMul
isSMulRegular_iff_right_eq_zero_of_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : AddGroup M] [inst_1 : DistribSMul R M] {r : R},
  IsSMulRegular M r ↔ ∀ (m : M), r • m = 0 → m = 0
-- Mathlib.Analysis.ODE.ExistUnique
/-- If a vector field `f : E → E` is continuously differentiable at `x₀ : E`, then it admits an
integral curve `α : ℝ → E` defined on an open interval, with initial condition `α t₀ = x₀`.  -/
ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E},
  ContDiffAt ℝ 1 f x₀ → ∀ (t₀ : ℝ), ∃ α, α t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.epsilon_zero_lt_gamma : ∀ (o : Ordinal.{u_1}), Ordinal.epsilon 0 < o.gamma
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.isMeasurablyGenerated_bot : ∀ {α : Type u_1} [inst : MeasurableSpace α], ⊥.IsMeasurablyGenerated
-- Lean.Parser.Basic
Lean.Parser.OrElseOnAntiquotBehavior.acceptLhs.sizeOf_spec : sizeOf Lean.Parser.OrElseOnAntiquotBehavior.acceptLhs = 1
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
continuous_const_cpow : ∀ (z : ℂ) [NeZero z], Continuous fun s => z ^ s
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_eq_self_of_superset : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s t : Set α} {f : α → M}, s.indicator f = f → s ⊆ t → t.indicator f = f
-- Mathlib.Order.WithBot
WithTop.ge_of_forall_gt_iff_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : WithTop α} [DenselyOrdered α] [NoMaxOrder α],
  (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.atEnd.sizeOf_spec : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToForwardSearcher pat σ] [inst_1 : (a : String.Slice) → SizeOf (σ a)]
  [inst_2 : SizeOf ρ], sizeOf String.Slice.SplitInclusiveIterator.atEnd = 1
-- Mathlib.Data.Sum.Order
/-- The linear/lexicographical `≤` on a sum.  -/
Sum.Lex.LE : {α : Type u_1} → {β : Type u_2} → [LE α] → [LE β] → LE (α ⊕ₗ β)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂CommMon_obj_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Init.Data.Array.GetLit
Array.toListLitAux.eq_def : ∀ {α : Type u_1} (xs : Array α) (n : ℕ) (hsz : xs.size = n) (x : ℕ) (x_1 : x ≤ xs.size) (x_2 : List α),
  xs.toListLitAux n hsz x x_1 x_2 =
    match x, x_1, x_2 with
    | 0, x, acc => acc
    | i.succ, hi, acc => xs.toListLitAux n hsz i ⋯ (xs.getLit i hsz ⋯ :: acc)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A version of `WithBot.map` for `OneHom`s.  -/
OneHom.withBotMap : {M : Type u_1} → {N : Type u_2} → [inst : One M] → [inst_1 : One N] → OneHom M N → OneHom (WithBot M) (WithBot N)
-- Mathlib.Algebra.Lie.Weights.Basic
/-- The family of eigenvalues corresponding to a weight.  -/
LieModule.Weight.toFun : {R : Type u_2} →
  {L : Type u_3} →
    {M : Type u_4} →
      [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 : LieRing.IsNilpotent L] → LieModule.Weight R L M → L → R
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredLimit_iff : ∀ {α : Type u_1} {a : α} [inst : Preorder α], ¬Order.IsPredLimit a ↔ IsMax a ∨ ¬Order.IsPredPrelimit a
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (base : X.base ⟶ Y.base) (fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber)
  (base_1 : X.base ⟶ Y.base) (fiber_1 : (F.map base_1).toFunctor.obj X.fiber ⟶ Y.fiber),
  ({ base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 }) = (base = base_1 ∧ fiber ≍ fiber_1)
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- The regular coverage on a regular category `C`.
 -/
CategoryTheory.regularCoverage : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Preregular C] → CategoryTheory.Coverage C
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Submonoid.subsemiringClosure_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (M : Submonoid R) {x : R},
  x ∈ M.subsemiringClosure ↔ x ∈ AddSubmonoid.closure ↑M
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instAddCommMonoid : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] → [ContinuousAdd M] → AddCommMonoid (MeasureTheory.VectorMeasure α M)
-- Mathlib.Logic.Equiv.Basic
Equiv.piOptionEquivProd_symm_apply : ∀ {α : Type u_10} {β : Option α → Type u_9} (x : β none × ((a : α) → β (some a))) (a : Option α),
  Equiv.piOptionEquivProd.symm x a = Option.casesOn a x.1 x.2
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.prettyParam : Array Lean.Expr → ℕ → Lean.MetaM Lean.MessageData
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_append : ∀ {n m i : ℕ} {x : BitVec n} {y : BitVec m}, (x ++ y).getMsbD i = if n ≤ i then y.getMsbD (i - n) else x.getMsbD i
-- Mathlib.RingTheory.Smooth.Fiber
/-- [Stacks Tag 00TF](https://stacks.math.columbia.edu/tag/00TF) (We require the whole fiber to be smooth instead) -/
Algebra.IsSmoothAt.of_formallySmooth_fiber : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Algebra.FinitePresentation R S] (p : Ideal R) (q : Ideal S) [inst_5 : p.IsPrime] [inst_6 : q.IsPrime] [q.LiesOver p]
  [Algebra.FormallySmooth p.ResidueField (p.Fiber S)], Algebra.IsSmoothAt R q
-- Lean.Meta.Basic
Lean.Meta.instInhabitedExprParamInfo : Inhabited Lean.Meta.ExprParamInfo
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.inhabitedσ : (tm : Turing.FinTM2) → Inhabited tm.σ
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddAction.is_zero_pretransitive' : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α], AddAction.IsMultiplyPretransitive G α 0
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.brecOn.go : {α : Type u} →
  {β : Type v} →
    {motive : Lean.PersistentHashMap.Zipper α β → Sort u_1} →
      (t : Lean.PersistentHashMap.Zipper α β) →
        ((t : Lean.PersistentHashMap.Zipper α β) → Lean.PersistentHashMap.Zipper.below t → motive t) →
          motive t ×' Lean.PersistentHashMap.Zipper.below t
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.liftAux.eq_1 : ∀ (R : Type u) {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (f : X → CommutatorRing L), FreeLieAlgebra.liftAux R f = (FreeNonUnitalNonAssocAlgebra.lift R) f
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- Weak version of the main theorem on differentiation of measures: given a Vitali family `v`
for a locally finite measure `μ`, and another locally finite measure `ρ`, then for `μ`-almost
every `x` the ratio `ρ a / μ a` converges, when `a` shrinks to `x` along the Vitali family,
towards the Radon-Nikodym derivative of `ρ` with respect to `μ`.

This version assumes that `ρ` is absolutely continuous with respect to `μ`. The general version
without this superfluous assumption is `VitaliFamily.ae_tendsto_rnDeriv`.
 -/
VitaliFamily.ae_tendsto_rnDeriv_of_absolutelyContinuous : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ρ.AbsolutelyContinuous μ → ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (nhds (ρ.rnDeriv μ x))
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_whiskerRight : ∀ {C : Type u} {X₁ X₂ : CategoryTheory.FreeMonoidalCategory C} (f : X₁.Hom X₂)
  (Y : CategoryTheory.FreeMonoidalCategory C),
  ⟦f.whiskerRight Y⟧ = CategoryTheory.MonoidalCategoryStruct.whiskerRight ⟦f⟧ Y
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective : ∀ {𝕜 : 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' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → ∀ {x : M}, x ∈ e.source → Function.Bijective ⇑(mfderiv% ↑e x)
-- Init.Data.String.PosRaw
String.Pos.Raw.eq_zero_iff : ∀ {p : String.Pos.Raw}, p = 0 ↔ p.byteIdx = 0
-- Init.Data.SInt.Lemmas
Int8.eq_iff_ofBitVec_eq : ∀ {a b : BitVec 8}, a = b ↔ Int8.ofBitVec a = Int8.ofBitVec b
-- Mathlib.Topology.Closure
IsClosed.closure_interior_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → closure (interior s) ⊆ s
-- Mathlib.Topology.Order.DenselyOrdered
left_nhdsWithin_Ioo_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a < b → (nhdsWithin a (Set.Ioo a b)).NeBot
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instModuleReal : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    {α : Type u_2} →
      [inst : Semiring α] →
        [inst_1 : Module α ℝ] → [inst_2 : Module α ℂ] → [IsScalarTower α ℝ ℂ] → Module α (SlashInvariantForm Γ k)
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.instDecidablePredShatters : {α : Type u_1} → [inst : DecidableEq α] → {𝒜 : Finset (Finset α)} → DecidablePred 𝒜.Shatters
-- Mathlib.Data.Matrix.Basis
Matrix.subringCenter_eq_scalar_map : ∀ {n : Type u_3} (R : Type u_5) [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Ring R],
  Subring.center (Matrix n n R) = Subring.map (Matrix.scalar n) (Subring.center R)
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.instInhabited : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      (X : (i : I) × C i) → Inhabited (CategoryTheory.Sigma.SigmaHom X X)
-- Mathlib.Data.ENNReal.Basic
ENNReal.min_eq_zero_iff : ∀ {a b : ENNReal}, min a b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.Order.Hom.Basic
/-- Any type satisfying `OrderIsoClass` can be cast into `OrderIso` via
`OrderIsoClass.toOrderIso`.  -/
instCoeTCOrderIsoOfOrderIsoClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : LE α] → [inst_1 : LE β] → [inst_2 : EquivLike F α β] → [OrderIsoClass F α β] → CoeTC F (α ≃o β)
-- Mathlib.NumberTheory.SelbergSieve
/-- The Selberg upper bound sieve in particular introduces a parameter called the `level` which
gives the user control over the size of the error term.  -/
SelbergSieve : Type
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.CasesPattern.elab : Lean.Syntax → Lean.Elab.TermElabM Aesop.CasesPattern
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.instSMulCommClass : ∀ {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Zero A] [inst_1 : Zero B]
  [inst_2 : SMulZeroClass M B] [inst_3 : SMulZeroClass N B] [SMulCommClass M N B], SMulCommClass M N (ZeroHom A B)
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
Stream'.Seq.head.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α), s.head = s.get? 0
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {ι : Sort u_7} (f : G →+ N)
  (s : ι → AddSubgroup N), AddSubgroup.comap f (iInf s) = ⨅ i, AddSubgroup.comap f (s i)
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the forward direction of `mdifferentiableWithinAt_iff_differentiableWithinAt`.

---

For maps between vector spaces, `MDifferentiableWithinAt` and `DifferentiableWithinAt`
coincide  -/
MDifferentiableWithinAt.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E} {x : E}, MDiffAt[s] f x → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instStarMul : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : Mul β] → [StarMul β] → StarMul (MeasureTheory.SimpleFunc α β)
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.instInhabitedBuiltinPropagators : Inhabited Lean.Meta.Grind.BuiltinPropagators
-- Mathlib.Algebra.Star.Unitary
Unitary.toMonoidHom_mapEquiv : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R ≃⋆* S), (Unitary.mapEquiv f).toStarMonoidHom = Unitary.map f.toStarMonoidHom
-- Init.Data.ByteArray.Lemmas
_private.Init.Data.ByteArray.Lemmas.0.ByteArray.getElem!_eq_data_getElem! : ∀ (data : ByteArray) (i : ℕ), data[i]! = data.data[i]!
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryCoproductIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.FunctorToTypes.binaryCoproductIso F G =
    CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.FunctorToTypes.binaryCoproductColimitCocone F G)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastArithShiftRightConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (target : aig.ShiftTarget w)
  (assign : α → Bool) (idx : ℕ) (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst aig target).vec.get idx hidx }⟧ =
    if hidx : target.distance + idx < w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance + idx) hidx }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (w - 1) ⋯ }⟧
-- Init.Internal.Order.Basic
Lean.Order.instCCPOESTOfNonempty : {ε σ α : Type} → [Nonempty ε] → Lean.Order.CCPO (EST ε σ α)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- A measurable set `s` is a *fundamental domain* for an action of a group `G` on a measurable
space `α` with respect to a measure `μ` if the sets `g • s`, `g : G`, are pairwise a.e. disjoint and
cover the whole space.  -/
MeasureTheory.IsFundamentalDomain : (G : Type u_1) →
  {α : Type u_2} →
    [One G] →
      [SMul G α] →
        [inst : MeasurableSpace α] →
          Set α → autoParam (MeasureTheory.Measure α) MeasureTheory.IsFundamentalDomain._auto_1 → Prop