mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Control
List.forIn'_eq_forIn' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m], List.forIn' = forIn'
-- Lean.Elab.Term.TermElabM
/-- Use coercion to synthesize value for the metavariable.
If synthesis fails, then throws an error.
- If `mkErrorMsg?` is provided, then the error `mkErrorMsg expectedType e` is thrown.
  The `mkErrorMsg` function is allowed to throw an error itself.
- Otherwise, throws a default type mismatch error message.
  If `header?` is not provided, the default header is "type mismatch".
  If `f?` is provided, then throws an application type mismatch error.
 -/
Lean.Elab.Term.SyntheticMVarKind.coe : Option String →
  Lean.Expr →
    Lean.Expr →
      Option Lean.Expr →
        Option (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData) → Lean.Elab.Term.SyntheticMVarKind
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_eq_zero_of_lt_orderTop : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} {i : Γ},
  ↑i < x.orderTop → x.coeff i = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The underlying presheaf of abelian groups of a presheaf of modules.  -/
PresheafOfModules.presheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → PresheafOfModules R → CategoryTheory.Functor Cᵒᵖ Ab
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.Semaphore.lock : Std.Semaphore → Std.Mutex Std.SemaphoreState✝
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_mul : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x₁ x₂ : M) (y₁ y₂ : ↥S), f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] {P : Ideal R} [inst_5 : P.IsPrime] [inst_6 : FaithfulSMul R S],
  IsScalarTower (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (FractionRing S)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivAt.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {f' g' : StrongDual ℂ E}
  {x : E},
  HasFDerivAt f f' x →
    HasFDerivAt g g' x →
      f x ∈ Complex.slitPlane →
        HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.triangle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C))
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom
      (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X)
        (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) =
    CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ
      (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom
      (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Algebra.Order.Round
round_intCast_add : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α)
  (y : ℤ), round (↑y + x) = y + round x
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- A global declaration in the environment.  -/
Lean.Meta.Origin.decl : Lean.Name → optParam Bool true → optParam Bool false → Lean.Meta.Origin
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.ofRepr.sizeOf_spec : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : SizeOf ι] [inst_5 : SizeOf 𝕜] [inst_6 : SizeOf E]
  (repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι), sizeOf { repr := repr } = 1 + sizeOf repr
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.llp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [self : W₁.IsWeakFactorizationSystem W₂], W₂.llp = W₁
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.π_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (W : C)
  (k : (b : J.R) → I.right b ⟶ W)
  (h :
    ∀ (a : J.L),
      CategoryTheory.CategoryStruct.comp (I.fst a) (k (J.fst a)) =
        CategoryTheory.CategoryStruct.comp (I.snd a) (k (J.snd a)))
  (b : J.R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b)
      (CategoryTheory.Limits.Multicoequalizer.desc I W k h) =
    k b
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_prod_left : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_3} (s : Finset ι) (f : ι → Polynomial R) (g : Polynomial R) (n : ℕ),
  ∏ i ∈ s, (f i).leadingCoeff ≠ 0 →
    g.natDegree ≤ n →
      (∏ i ∈ s, f i).resultant g (∏ i ∈ s, f i).natDegree n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n
-- Mathlib.Data.Vector.Zip
List.Vector.zipWith_get : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : List.Vector α n) (y : List.Vector β n)
  (i : Fin n), (List.Vector.zipWith f x y).get i = f (x.get i) (y.get i)
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.simpHaveTelescopeAux : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        [Lean.Meta.MonadSimp m] →
          Lean.Meta.HaveTelescopeInfo →
            Array Bool → Array Bool → Lean.Expr → ℕ → Array Lean.Expr → m Lean.Meta.SimpHaveResult✝
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_insert_iff : ∀ {α : Type u_1} {s t : Set α} {a : α}, s ⊆ insert a t ↔ s ⊆ t ∨ a ∈ s ∧ s \ {a} ⊆ t
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  {f g : β → α}, UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x * g x
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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), t.eTruncLT.obj ⊥ = 0
-- Mathlib.Algebra.Homology.Opposite
/-- Auxiliary definition for `unopEquivalence`.  -/
HomologicalComplex.unopCounitIso : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          (HomologicalComplex.unopInverse V c).comp (HomologicalComplex.unopFunctor V c) ≅
            CategoryTheory.Functor.id (HomologicalComplex V c.symm)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipPrefixWhile_eq_startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String}, s.startsWith pat = false → s.skipPrefixWhile pat = s.startPos
-- Lean.LocalContext
Lean.LocalDecl.toExpr : Lean.LocalDecl → Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesMap_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i],
  HomologicalComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (HomologicalComplex.opcyclesMap ψ i)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.visitApp : Lean.Expr → Lean.Name → Array Lean.Expr → Lean.Meta.Try.Collector.M Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.map_map_equiv : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} {δ : α → Type w'}
  {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a},
  (Std.DHashMap.map g (Std.DHashMap.map f m)).Equiv (Std.DHashMap.map (fun k v => g k (f k v)) m)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- Typecheck an `AlgHom` as a morphism in `CommAlgCat`.  -/
CommAlgCat.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : CommRing X] →
        [inst_2 : Algebra R X] →
          [inst_3 : CommRing Y] → [inst_4 : Algebra R Y] → (X →ₐ[R] Y) → (CommAlgCat.of R X ⟶ CommAlgCat.of R Y)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The canonical morphism `A →ₐ[R₁] I.quotient` is surjective.  -/
Ideal.Quotient.mkₐ_surjective : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] (I : Ideal A)
  [inst_3 : I.IsTwoSided], Function.Surjective ⇑(Ideal.Quotient.mkₐ R₁ I)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {outWidth w len : ℕ} →
          aig.RefVec (len * w) →
            outWidth = (len + 1) / 2 * w →
              0 < len → Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget aig outWidth
-- Lean.Level
/-- A total order on level expressions that has the following properties
 - `succ l` is an immediate successor of `l`.
 - `zero` is the minimal element.
This total order is used in the normalization procedure.  -/
Lean.Level.normLt : Lean.Level → Lean.Level → Bool
-- Mathlib.Algebra.Ring.NonZeroDivisors
mul_cancel_left_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] {x y r : R}, r ∈ nonZeroDivisors R → (r * x = r * y ↔ x = y)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : Zero α] [inst_1 : Zero β] (f : α → β),
  f 0 = 0 → Matrix.map 0 f = 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.setImportedEntries.unsafe_1 : Array Lean.ModuleData →
  Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState →
    Array Lean.EnvExtensionState → Array Lean.EnvExtensionState
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.mkHomToSingle.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} (φ φ_1 : K.X j ⟶ A) (e_φ : φ = φ_1)
  (hφ : ∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0),
  HomologicalComplex.mkHomToSingle φ hφ = HomologicalComplex.mkHomToSingle φ_1 ⋯
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Define a `Kernel α (γ × β)` from a `Kernel α (β × γ)` by taking the map of `Prod.swap`.
We use `mapOfMeasurable` in the definition for better defeqs.  -/
ProbabilityTheory.Kernel.swapRight : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} → ProbabilityTheory.Kernel α (β × γ) → ProbabilityTheory.Kernel α (γ × β)
-- Lean.Elab.Tactic.Induction
/-- Separate out the optional `with` tactics from the rest of the alternates
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getOptPreTacOfOptInductionAlts : Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles._auto_1) {Z : C}
  (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
      (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁) h) =
    CategoryTheory.CategoryStruct.comp (X.iCycles f₂ f₃ n₀)
      (CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) h)
-- Lean.Meta.AppBuilder
/-- Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, returns
term `@id expectedType e`.  -/
Lean.Meta.mkExpectedTypeHint : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- **Alias** of `AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange`.

---

Smooth of relative dimension `n` is stable under base change.  -/
AlgebraicGeometry.isSmoothOfRelativeDimension_isStableUnderBaseChange : ∀ (n : ℕ), CategoryTheory.MorphismProperty.IsStableUnderBaseChange (@AlgebraicGeometry.SmoothOfRelativeDimension n)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Equal maps of arrows are right homotopic.  -/
CategoryTheory.Arrow.RightHomotopy.ofEq : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} → {f g : u ⟶ v} → f = g → CategoryTheory.Arrow.RightHomotopy f g
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.unop_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor Eᵒᵖ Cᵒᵖ} (α : F ⟶ G),
  CategoryTheory.NatTrans.unop (H.whiskerLeft α) =
    CategoryTheory.CategoryStruct.comp (H.unopComp G).hom
      (CategoryTheory.CategoryStruct.comp (H.unop.whiskerLeft (CategoryTheory.NatTrans.unop α)) (H.unopComp F).inv)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hf_int : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (self : WeakFEPair E),
  MeasureTheory.LocallyIntegrableOn self.f (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_nsmul_interval : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s : NonemptyInterval α)
  (n : ℕ), ↑(n • s) = n • ↑s
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.glue.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (sz : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced →
        Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size r.size →
          Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
      Std.DTreeMap.Internal.Impl.leaf.size)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
            Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hr hlr)
  (h_2 :
    (sz' : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                    (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size) →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') hr hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hr, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hr, hlr => h_1 hr hlr
    | Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'', hr, hlr => h_2 sz' k' v' l'' r'' hr hlr) =
    h_1 hr hlr
-- Mathlib.Analysis.InnerProductSpace.SingularValues
/-- If `T : E →ₗ[𝕜] F` is a linear map between finite dimensional inner product spaces, then
`T.singularValues` is the infinite sequence where the first dim(E) elements are the square roots of
eigenvalues of `T.adjoint ∘ₗ T` (which are guaranteed to be nonnegative real numbers), arranged
in descending order and repeated according to their multiplicity, and the rest of the elements in
the infinite sequence are zero. Please see the module docstring of
`Mathlib/Analysis/InnerProductSpace/SingularValues.lean` for an explanation of this design decision.

The singular values are zero-indexed, so `T.singularValues 0` refers to the first singular value.
This means the positive singular values occur at `0 ≤ i < rank(T)` and not `1 ≤ i ≤ rank(T)`.
 -/
LinearMap.singularValues : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          [FiniteDimensional 𝕜 E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : InnerProductSpace 𝕜 F] → [FiniteDimensional 𝕜 F] → (E →ₗ[𝕜] F) → ℕ →₀ ℝ
-- Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
/-- In a linearly ordered additive group with the order topology, the multiples of a
single element form a discrete subgroup.  -/
AddSubgroup.instDiscreteTopologyZMultiples : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] (g : G), DiscreteTopology ↥(AddSubgroup.zmultiples g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_inv_app : ∀ (X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ),
  CategoryTheory.Limits.walkingCospanOpEquiv.unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_le_neg_norm_iff_eq_neg_norm : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, RCLike.re z ≤ -‖z‖ ↔ z = -↑‖z‖
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α}, k ∈ Std.ExtDTreeMap.map f t ↔ k ∈ t
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.eventually_mem_or_not_mem : ∀ {β : Type u_2} (L : SummationFilter β) [L.HasSupport] (b : β),
  (∀ᶠ (s : Finset β) in L.filter, b ∈ s) ∨ ∀ᶠ (s : Finset β) in L.filter, b ∉ s
-- Mathlib.Algebra.Order.Monovary
Monovary.nsmul_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β}, Monovary f g → ∀ (n : ℕ), Monovary f (n • g)
-- Mathlib.CategoryTheory.MorphismProperty.IsSmall
CategoryTheory.MorphismProperty.isSmall_ofHoms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} [Small.{w, t} ι] {A B : ι → C}
  (f : (i : ι) → A i ⟶ B i),
  CategoryTheory.MorphismProperty.IsSmall.{w, v, u} (CategoryTheory.MorphismProperty.ofHoms f)
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel_k.eq_1 : ∀ (fuel : ℕ),
  Lean.Grind.AC.Seq.unionFuel_k fuel =
    Nat.rec (motive := fun x => Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq) Lean.Grind.AC.Seq.concat
      (fun x ih s₁ s₂ =>
        Lean.Grind.AC.Seq.rec
          (fun x₁ =>
            Lean.Grind.AC.Seq.rec
              (fun x₂ =>
                Bool.rec (Lean.Grind.AC.Seq.cons x₂ (Lean.Grind.AC.Seq.var x₁))
                  (Lean.Grind.AC.Seq.cons x₁ (Lean.Grind.AC.Seq.var x₂)) (Nat.blt x₁ x₂))
              (fun x x_1 x_2 => Lean.Grind.AC.Seq.insert x₁ s₂) s₂)
          (fun x₁ s₁' x =>
            Lean.Grind.AC.Seq.rec (fun x₂ => Lean.Grind.AC.Seq.insert x₂ s₁)
              (fun x₂ s₂' x =>
                Bool.rec (Lean.Grind.AC.Seq.cons x₂ (ih s₁ s₂')) (Lean.Grind.AC.Seq.cons x₁ (ih s₁' s₂))
                  (Nat.blt x₁ x₂))
              s₂)
          s₁)
      fuel
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.instBraiding : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory Cᴹᵒᵖ
-- Mathlib.Order.Antisymmetrization
le_of_antisymmRel_of_le : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → b ≤ c → a ≤ c
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.equiv_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P₁ : Algebra.Extension R S} {P₂ : Algebra.Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁)
  (c : ↥P₁.cotangentComplex.ker),
  (Algebra.Extension.H1Cotangent.equiv f₁ f₂) c = ⟨(Algebra.Extension.Cotangent.map f₁) ↑c, ⋯⟩
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.mk : {R : Type u} →
  [toIntCast : IntCast R] →
    [toAddMonoidWithOne : AddMonoidWithOne R] →
      [toNeg : Neg R] →
        [toSub : Sub R] →
          [toZSMul : ZSMul R] →
            autoParam (∀ (a b : R), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam →
              autoParam (∀ (a : R), 0 • a = 0) SubNegMonoid.zsmul_zero'._autoParam →
                autoParam (∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a) SubNegMonoid.zsmul_succ'._autoParam →
                  autoParam (∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)) SubNegMonoid.zsmul_neg'._autoParam →
                    (∀ (a : R), -a + a = 0) →
                      autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) AddGroupWithOne.intCast_ofNat._autoParam →
                        autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1))
                            AddGroupWithOne.intCast_negSucc._autoParam →
                          AddGroupWithOne R
-- Batteries.Data.Fin.Coding
Fin.decodeOption.eq_2 : ∀ {n : ℕ} (i : ℕ) (h : i + 1 < n + 1), Fin.decodeOption ⟨i.succ, h⟩ = some ⟨i, ⋯⟩
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- Removing an edge from `H` for each subgraph isomorphic to `G` means that the number of edges
we've removed is at most the number of copies of `G` in `H`.  -/
SimpleGraph.le_card_edgeFinset_killCopies_add_copyCount : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype ↑G.edgeSet]
  [inst_1 : Fintype V], G.edgeFinset.card ≤ (G.killCopies H).edgeFinset.card + G.copyCount H
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitAuxAuxAux_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (X : C),
  (CategoryTheory.OverPresheafAux.unitAuxAuxAux η X).inv =
    TypeCat.ofHom (CategoryTheory.OverPresheafAux.unitBackward η X)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonFoldingRange.toJson : Lean.Lsp.FoldingRange → Lean.Json
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.instTopologicalSpace : {X : Type u_1} → [TopologicalSpace X] → TopologicalSpace (OnePoint X)