mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Basic
/-- Optional progress percentage to display (value 100 is considered 100%).
If not provided infinite progress is assumed.  -/
Lean.Lsp.WorkDoneProgressReport.percentage? : Lean.Lsp.WorkDoneProgressReport → Option ℕ
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State.mk.inj : ∀ {mvarId : Lean.MVarId} {xs eqs eqsNew : List Lean.FVarId} {mvarId_1 : Lean.MVarId}
  {xs_1 eqs_1 eqsNew_1 : List Lean.FVarId},
  { mvarId := mvarId, xs := xs, eqs := eqs, eqsNew := eqsNew } =
      { mvarId := mvarId_1, xs := xs_1, eqs := eqs_1, eqsNew := eqsNew_1 } →
    mvarId = mvarId_1 ∧ xs = xs_1 ∧ eqs = eqs_1 ∧ eqsNew = eqsNew_1
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C) {x : B}, F.toStrictlyUnitaryLaxFunctor.mapId x = (F.mapId x).inv
-- Mathlib.Data.Finsupp.Fintype
Fintype.card_finsupp : ∀ (ι : Type u_1) (α : Type u_2) [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Zero α] [inst_3 : Fintype α],
  Fintype.card (ι →₀ α) = Fintype.card α ^ Fintype.card ι
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.congr'_apply_right : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (x : N₁ ⋊[φ₁] G₁),
  ((SemidirectProduct.congr' fn fg) x).right = fg x.right
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_hom_app : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮)
  (X : ↑(F.obj { as := Opposite.op S })),
  (CategoryTheory.Pseudofunctor.CoGrothendieck.compIso F S).hom.app X = CategoryTheory.CategoryStruct.id S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_diff_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y), IsOpenMap ⇑h
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.forget₂_commRingCat_obj : ∀ {R : Type u} [inst : CommRing R] (A : CommAlgCat R),
  (CategoryTheory.forget₂ (CommAlgCat R) CommRingCat).obj A = CommRingCat.of ↑A
-- Mathlib.Data.ZMod.Basic
/-- In `ZMod (p ^ d)` with `0 < d`, a natural number is a unit iff `p` does not divide it.  -/
ZMod.isUnit_natCast_iff_not_dvd_pow : ∀ {p d a : ℕ}, Nat.Prime p → 0 < d → (IsUnit ↑a ↔ ¬p ∣ a)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_mk : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {toEquiv : A₁ ≃ A₂}
  {map_mul : ∀ (x y : A₁), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y}
  {map_add : ∀ (x y : A₁), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y}
  {commutes : ∀ (r : R), toEquiv.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r},
  ⇑{ toEquiv := toEquiv, map_mul' := map_mul, map_add' := map_add, commutes' := commutes } = ⇑toEquiv
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.deriv_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {R : Type u_1} [inst_1 : CommSemiring R]
  [inst_2 : Algebra R 𝕜] (q : Polynomial R),
  deriv (fun x => (Polynomial.aeval x) q) x = (Polynomial.aeval x) (Polynomial.derivative q)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.of_subsingleton : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [Subsingleton E]
  [MeasureTheory.IsProbabilityMeasure P], ProbabilityTheory.HasGaussianLaw X P
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.instAddEquivClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β],
  AddEquivClass (α ≃+o β) α β
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.Monic.isUnit_leadingCoeff_of_dvd : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {a p : Polynomial R}, p.Monic → a ∣ p → IsUnit a.leadingCoeff
-- Init.Data.SInt.IntToBitVec
USize.toBitVec32_toISize : ∀ (n : USize) (h : System.Platform.numBits = 32), n.toISize.toBitVec32 h = n.toBitVec32 h
-- Init.Grind.Config
Lean.Grind.LinarithConfig.mk.sizeOf_spec : ∀ (toNoopConfig : Lean.Grind.NoopConfig), sizeOf { toNoopConfig := toNoopConfig } = 1 + sizeOf toNoopConfig
-- Mathlib.Topology.MetricSpace.HausdorffDimension
IsometryEquiv.dimH_image : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] (e : X ≃ᵢ Y) (s : Set X),
  dimH (⇑e '' s) = dimH s
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant additive monoid homomorphisms.  -/
«DistribMulActionHomIdLocal≺» : Lean.TrailingParserDescr
-- Mathlib.Topology.Specialization
topToPreord_obj_coe : ∀ (X : TopCat), ↑(topToPreord.obj X) = Specialization ↑X
-- Mathlib.Topology.Category.Sequential
/-- The equivalence between isomorphisms in `Sequential` and homeomorphisms
of topological spaces.  -/
Sequential.isoEquivHomeo : {X Y : Sequential} → (X ≅ Y) ≃ (↑X.toTop ≃ₜ ↑Y.toTop)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} [inst_4 : Inhabited β] {f : Option β → Option β},
  m.WF → (m.alter k f)[k']! = if (k == k') = true then (f m[k]?).get! else m[k']!
-- Mathlib.Order.BooleanAlgebra.Set
/-- `ite` for sets: `Set.ite t s s' ∩ t = s ∩ t`, `Set.ite t s s' ∩ tᶜ = s' ∩ tᶜ`.
Defined as `s ∩ t ∪ s' \ t`.  -/
Set.ite : {α : Type u_1} → Set α → Set α → Set α → Set α
-- Mathlib.CategoryTheory.DifferentialObject
/-- The shift functor on `DifferentialObject S C` is additive.  -/
CategoryTheory.DifferentialObject.shiftFunctorAdd : {S : Type u_1} →
  [inst : AddCommGroupWithOne S] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            (m n : S) →
              CategoryTheory.DifferentialObject.shiftFunctor C (m + n) ≅
                (CategoryTheory.DifferentialObject.shiftFunctor C m).comp
                  (CategoryTheory.DifferentialObject.shiftFunctor C n)
-- Mathlib.Computability.Partrec
Nat.Partrec.below.left : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop}, Nat.Partrec.below Nat.Partrec.left
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- Sum of a multiset of elements in an `AddSubgroup` of an `AddCommGroup` is in
the `AddSubgroup`.  -/
AddSubgroup.multiset_sum_mem : ∀ {G : Type u_3} [inst : AddCommGroup G] (K : AddSubgroup G) (g : Multiset G), (∀ a ∈ g, a ∈ K) → g.sum ∈ K
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.nest_insidePart_add_outsidePart : ∀ {p : DyckWord}, p ≠ 0 → p.insidePart.nest + p.outsidePart = p
-- Mathlib.Control.Functor.Multivariate
MvFunctor.id_map' : ∀ {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] [LawfulMvFunctor F] (x : F α),
  MvFunctor.map (fun _i a => a) x = x
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- If `ps` is cospherical, then any of its isometric images is cospherical.  -/
Isometry.cospherical : ∀ {E : Type u_3} {F : Type u_4} [inst : MetricSpace E] [inst_1 : MetricSpace F] {f : E → F},
  Isometry f → ∀ {ps : Set E}, EuclideanGeometry.Cospherical ps → EuclideanGeometry.Cospherical (f '' ps)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- If a function is continuous outside of a countable set, then it is measurable.  -/
measurable_of_countable_not_continuousAt : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] [MeasurableSingletonClass α] {f : α → γ},
  {x | ¬ContinuousAt f x}.Countable → Measurable f
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_eq_iSup : ∀ {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [inst : IsWellOrder ι r] [inst_1 : IsWellOrder ι' r']
  {o : Ordinal.{u}} (ho : Ordinal.type r = o) (ho' : Ordinal.type r' = o)
  (f : (a : Ordinal.{u}) → a < o → Ordinal.{u_3}),
  iSup (Ordinal.familyOfBFamily' r ho f) = iSup (Ordinal.familyOfBFamily' r' ho' f)
-- Mathlib.Data.Num.Bitwise
Num.land_eq_and : ∀ (p q : Num), p.land q = p &&& q
-- Mathlib.Analysis.Analytic.Composition
/-- If two functions `g` and `f` are continuously polynomial respectively at `f x` and `x`,
then `g ∘ f` is continuously polynomial at `x`.  -/
CPolynomialAt.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E},
  CPolynomialAt 𝕜 g (f x) → CPolynomialAt 𝕜 f x → CPolynomialAt 𝕜 (g ∘ f) x
-- Mathlib.CategoryTheory.Elements
/-- The forward direction of the equivalence `F.Elements ≅ (*, F)`.  -/
CategoryTheory.CategoryOfElements.toStructuredArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) →
      CategoryTheory.Functor F.Elements (CategoryTheory.StructuredArrow PUnit.{w + 1} F)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- A sequence `φ` of subsets of `α` is a `MeasureTheory.AECover` w.r.t. a measure `μ` and a filter
`l` if almost every point (w.r.t. `μ`) of `α` eventually belongs to `φ n` (w.r.t. `l`), and if
each `φ n` is measurable.  This definition is a technical way to avoid duplicating a lot of
proofs.  It should be thought of as a sufficient condition for being able to interpret
`∫ x, f x ∂μ` (if it exists) as the limit of `∫ x in φ n, f x ∂μ` as `n` tends to `l`.
See for example `MeasureTheory.AECover.lintegral_tendsto_of_countably_generated`,
`MeasureTheory.AECover.integrable_of_integral_norm_tendsto` and
`MeasureTheory.AECover.integral_tendsto_of_countably_generated`.  -/
MeasureTheory.AECover : {α : Type u_1} → {ι : Type u_2} → [inst : MeasurableSpace α] → MeasureTheory.Measure α → Filter ι → (ι → Set α) → Prop
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.hasSmallLocalizedHom_of_isLocalization : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [L.IsLocalization W] {X Y : C},
  CategoryTheory.Localization.HasSmallLocalizedHom W X Y
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.whiskerRight_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C)
  [inst_2 : CategoryTheory.MonoidalCoherence X Y],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCategory.whiskerRightIso CategoryTheory.MonoidalCoherence.iso Z
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substInvFun.eq_def : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)] (x : ℕ),
  P.substInvFun x =
    match x with
    | 0 => 0
    | 1 => ⅟((PowerSeries.coeff 1) P)
    | n.succ =>
      -⅟((PowerSeries.coeff 1) P) *
        (PowerSeries.coeff (n + 1)) (PowerSeries.subst (∑ i, PowerSeries.C (P.substInvFun ↑i) * PowerSeries.X ^ ↑i) P)
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.emptyQuiver : (V : Type u) → Quiver (Quiver.Empty V)
-- Init.Data.UInt.Lemmas
UInt8.ofNat_sub : ∀ {a b : ℕ}, b ≤ a → UInt8.ofNat (a - b) = UInt8.ofNat a - UInt8.ofNat b
-- Mathlib.Order.Disjoint
Disjoint.inf_left : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α} (c : α), Disjoint a b → Disjoint (a ⊓ c) b
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.InfiniteNeg.neg : ∀ {x : ℝ*}, x.InfiniteNeg → (-x).InfinitePos
-- Init.Data.Array.MinMax
Array.max?_toList : ∀ {α : Type u_1} [inst : Max α] {xs : Array α}, xs.toList.max? = xs.max?
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.connectedComponentEquiv_symm_apply : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G'.ConnectedComponent),
  φ.connectedComponentEquiv.symm C = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ.symm).toRelHom C
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.id_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id X.toComma
-- Mathlib.Data.Nat.Factorization.Basic
Nat.Ico_filter_pow_dvd_eq : ∀ {n p b : ℕ}, Nat.Prime p → n ≠ 0 → n ≤ p ^ b → {i ∈ Finset.Ico 1 n | p ^ i ∣ n} = {i ∈ Finset.Icc 1 b | p ^ i ∣ n}
-- Lean.Parser.Extension
Lean.Parser.ParserAttributeHook.mk.sizeOf_spec : ∀ (postAdd : Lean.Name → Lean.Name → Bool → Lean.AttrM Unit), sizeOf { postAdd := postAdd } = 1
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly.instInhabitedId : (p : ℕ) → Inhabited (WittVector.IsPoly p fun x x_1 => id)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- A `C^n` vector bundle `E` is naturally a `C^n` manifold.  -/
Bundle.TotalSpace.isManifold : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] [IsManifold IB n B],
  IsManifold (IB.prod (modelWithCornersSelf 𝕜 F)) n (Bundle.TotalSpace F E)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof) →
      ((t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof) → t.below → motive_2 t) → motive_2 t ×' t.below
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P]
  (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (d.pullbackGluedIso i).inv.left
      (CategoryTheory.Limits.pullback.fst d.glued.hom (𝒰.f i)) =
    CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i
-- Init.Data.BitVec.Lemmas
BitVec.getElem_shiftLeftZeroExtend : ∀ {m i : ℕ} {x : BitVec m} {n : ℕ} (h : i < m + n),
  (x.shiftLeftZeroExtend n)[i] = if h' : i < n then false else x[i - n]
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.ext_iff : ∀ {𝕜 : 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'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  {h h' : Diffeomorph I I' M M' n}, h = h' ↔ ∀ (x : M), h x = h' x
-- Mathlib.Algebra.Star.TensorProduct
starLinearEquiv_tensor : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : AddCommMonoid B]
  [inst_7 : StarAddMonoid B] [inst_8 : Module R B] [inst_9 : StarModule R B],
  starLinearEquiv R = TensorProduct.congr (starLinearEquiv R) (starLinearEquiv R)
-- Aesop.Tree.Data
Aesop.RappData : Type → Type → Type
-- Mathlib.Analysis.RCLike.Basic
RCLike.one_im : ∀ {K : Type u_1} [inst : RCLike K], RCLike.im 1 = 0
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommMagma : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : CommMagma M] → [ContinuousMul M] → CommMagma (SeparationQuotient M)
-- Mathlib.Order.Std
/-- Create a `Preorder` from a type satisfying `Std.IsPreorder`.

If an `LE` instance exists, either an `Std.IsPreorder` instance must exist, or there must be an
`Ord` instance together with `Std.LawfulOrderOrd` and `Std.TransOrd` instances.

If no `LE` instance exists, it can be generated from `Ord` and `Std.TransOrd` instances.

If an `LT` instance exists, an `Std.LawfulOrderLT` instance must exist also; otherwise, a suitable
`LT` instance will be generated.  -/
Preorder.ofStd : (α : Type u_1) → autoParam (Preorder.OfStdArgs α) Preorder.ofStd._auto_1 → Preorder α
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.exp_artanh : ∀ {x : ℝ}, x ∈ Set.Ioo (-1) 1 → Real.exp (Real.artanh x) = √((1 + x) / (1 - x))
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `s` is differentiable at `x`, so is its coefficient `b.localFrameCoeff e i` in the local
frame near `x` induced by `e` and `b`  -/
mdifferentiableAt_localFrameCoeff : ∀ {𝕜 : 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
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuousOn.comp : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β} {s : Set α} {g : β → γ} {t : Set β},
  UniformContinuousOn g t → UniformContinuousOn f s → Set.MapsTo f s t → UniformContinuousOn (g ∘ f) s
-- Mathlib.Algebra.AffineMonoid.Basic
IsAffineMonoid.mk : ∀ {M : Type u_1} [inst : CommMonoid M] [toIsCancelMul : IsCancelMul M] [toFG : Monoid.FG M]
  [toIsMulTorsionFree : IsMulTorsionFree M], IsAffineMonoid M
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.peek.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Turing.TM2.Stmt Γ Λ σ),
  sizeOf (Turing.TM2.Stmt.peek k a a_1) = 1 + sizeOf k + sizeOf a_1
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.coe_symm_addEquiv : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V], ⇑(WithLp.addEquiv p V).symm = WithLp.toLp p
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_smulFamily : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid V] [inst_3 : SMulWithZero R V] (f : α → R) (s : HahnSeries.SummableFamily Γ V α) (g : Γ),
  (HahnSeries.SummableFamily.smulFamily f s).hsum.coeff g = ∑ᶠ (i : α), f i • (s i).coeff g
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_truncGEπ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ),
  b ≤ a → ∀ (X : C), CategoryTheory.IsIso ((t.truncGE a).map ((t.truncGEπ b).app X))
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) [inst_9 : Module.Finite R L] [inst_10 : Module.Free R L] (x : L),
  φ.IsNilRegular x ↔ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
-- Mathlib.Util.Export
Lean.Export.Entry.expr.sizeOf_spec : ∀ (n : Lean.Expr), sizeOf (Lean.Export.Entry.expr n) = 1 + sizeOf n
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpackSign_packComponents : ∀ {spec : Float.Model.Format} (s : Float.Model.UnpackedFloat.Sign) (e : BitVec spec.exponentBits)
  (m : BitVec spec.mantissaBitsWithoutImplicit),
  Float.Model.UnpackedFloat.unpackSign (Float.Model.UnpackedFloat.packComponents spec s e m) = s.toBitVec
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLE_reverse`. -/
List.SortedGE.reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGE → l.reverse.SortedLE
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsAddMonHom.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M' N' : C}
  [inst_2 : CategoryTheory.AddMonObj M'] [inst_3 : CategoryTheory.AddMonObj N'] {f : M' ⟶ N'},
  autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero)
      CategoryTheory.IsAddMonHom.zero_hom._autoParam →
    autoParam
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
            CategoryTheory.AddMonObj.add)
        CategoryTheory.IsAddMonHom.add_hom._autoParam →
      CategoryTheory.IsAddMonHom f