mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- The inclusion of right exact functors into functors is fully faithful.  -/
CategoryTheory.RightExactFunctor.fullyFaithful : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (CategoryTheory.RightExactFunctor.forget C D).FullyFaithful
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A filter `f` is totally bounded if for every entourage `d`, the `d`-neighborhood of some finite
set is in `f`.  -/
Filter.TotallyBounded : {α : Type u} → [uniformSpace : UniformSpace α] → Filter α → Prop
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.Subgroup.exists_generator_lt_one : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (H : Subgroup G) [Nontrivial ↥H]
  [hH : IsCyclic ↥H], ∃ a < 1, Subgroup.zpowers a = H
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minView.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l' r' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.View α β (l'.size + r'.size) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.View α β (l'.size + r'.size)) →
          ((dk : α) →
              (dv : β dk) →
                (dt : Std.DTreeMap.Internal.Impl α β) →
                  (hdt : dt.Balanced) →
                    (hdt' : dt.size = l'.size + r'.size) →
                      motive { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } }) →
            motive x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app_assoc : ∀ {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) (n : ℤ) (X : C) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.truncLTι n).app X)) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
MvPolynomial.irreducible_of_totalDegree_eq_one : ∀ {n : Type u_1} {R : Type u_2} [inst : CommRing R] [IsDomain R] {p : MvPolynomial n R},
  p.totalDegree = 1 → (∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ MvPolynomial.coeff i p) → IsUnit x) → Irreducible p
-- Mathlib.Data.Part
Part.inv_some : ∀ {α : Type u_1} [inst : Inv α] (a : α), (Part.some a)⁻¹ = Part.some a⁻¹
-- Mathlib.LinearAlgebra.Alternating.Curry
AlternatingMap.curryLeft_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f g : M [⋀^Fin n.succ]→ₗ[R] N),
  (f + g).curryLeft = f.curryLeft + g.curryLeft
-- Lean.Elab.DeclModifiers
Lean.Elab.RecKind.default : Lean.Elab.RecKind
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
WithZero.withZeroUnitsEquiv_symm_strictMono : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α], StrictMono ⇑WithZero.withZeroUnitsEquiv.symm
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ι_comp_lift : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A),
  ((TensorAlgebra.lift R) f).toLinearMap ∘ₗ TensorAlgebra.ι R = f
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupHomologyIsoOdd.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  [inst_3 : DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i),
  Rep.FiniteCyclicGroup.groupHomologyIsoOdd A g hg i hi = Rep.FiniteCyclicGroup.groupHomologyIsoOdd A g hg i hi
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_succ_right : ∀ (n k : ℕ), 0 < n → n.choose (k + 1) = (n - 1).choose k + (n - 1).choose (k + 1)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isOfFinOrder : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → k ≠ 0 → IsOfFinOrder ζ
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `b ≠ 0`. See `mul_inv_cancel_right`.  -/
le_mul_inv_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b : G₀}, a ≤ 0 → a ≤ a * b * b⁻¹
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fundamentalDomain.congr_simp : ∀ {ι : Type u_3} {s s_1 : Set (ι → ℕ)} (e_s : s = s_1) (hs : IsProperLinearSet s) [inst : Finite ι] (a a_1 : ι → ℕ),
  a = a_1 → IsProperLinearSet.fundamentalDomain✝ hs a = IsProperLinearSet.fundamentalDomain✝ ⋯ a_1
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffAt.pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_3 : NormedRing 𝔸]
  [inst_4 : NormedAlgebra 𝕜 𝔸] {f : E → 𝔸}, ContDiffAt 𝕜 n f x → ∀ (m : ℕ), ContDiffAt 𝕜 n (fun y => f y ^ m) x
-- Mathlib.Topology.Algebra.Module.Cardinality
/-- In a topological vector space over a nontrivially normed field, any nonempty open set has
the same cardinality as the whole space.  -/
cardinal_eq_of_isOpen : ∀ {E : Type u_1} (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : AddGroup E]
  [inst_2 : MulActionWithZero 𝕜 E] [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E},
  IsOpen s → s.Nonempty → Cardinal.mk ↑s = Cardinal.mk E
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeffAddEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], MonoidAlgebra.coeffAddEquiv = MonoidAlgebra.coeffEquiv.addEquiv
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The vector from a vertex to its `faceOppositeCentroid` equals the average of reversed
displacements.  -/
Affine.Simplex.point_vsub_faceOppositeCentroid_eq_smul_sum_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.points i -ᵥ s.faceOppositeCentroid i = (↑n)⁻¹ • ∑ x, (s.points i -ᵥ s.points x)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roo_eq_some : ∀ {m n : ℤ} {i : ℕ}, i < (n - (m + 1)).toNat → (m<...n).toList[i]? = some (m + 1 + ↑i)
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.prod_rotate_eq_one_of_prod_eq_one : ∀ {G : Type u_7} [inst : Group G] {l : List G}, l.prod = 1 → ∀ (n : ℕ), (l.rotate n).prod = 1
-- Lean.Server.InfoUtils
Lean.Elab.Info.isSmaller : Lean.Elab.Info → Lean.Elab.Info → Bool
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `CostructuredArrow F d` is filtered for any `d : D`, then `F : C ⥤ D` is initial. This is
simply because cofiltered categories are connected. More profoundly, the converse is also true
if `C` is cofiltered, see `initial_iff_isCofiltered_costructuredArrow`.  -/
CategoryTheory.Functor.initial_of_isCofiltered_costructuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)],
  F.Initial
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_iff_isClosed_preimage : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] {f : α → γ},
  LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Set.Iic y)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- `C^n` constant functions as a `RingHom`.  -/
ContMDiffMap.C : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {N : Type u_6} →
                  [inst_4 : TopologicalSpace N] →
                    [inst_5 : ChartedSpace H N] →
                      {n : WithTop ℕ∞} →
                        {A : Type u_10} →
                          [inst_6 : NormedRing A] →
                            [inst_7 : NormedAlgebra 𝕜 A] →
                              [inst_8 : ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] →
                                𝕜 →+* ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A n
-- Init.ShareCommon
ShareCommon.State.mk : (σ : ShareCommon.StateFactory) → ShareCommon.State σ
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Reinterpret a `LinearIsometryEquiv` as a `LinearIsometry`.  -/
LinearIsometryEquiv.toLinearIsometry : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → (E ≃ₛₗᵢ[σ₁₂] E₂) → E →ₛₗᵢ[σ₁₂] E₂
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.eqIgnoreAsciiCase.go.eq_def : ∀ (s1 : String.Slice) (s1Curr : String.Pos.Raw) (s2 : String.Slice) (s2Curr : String.Pos.Raw),
  String.Slice.eqIgnoreAsciiCase.go✝ s1 s1Curr s2 s2Curr =
    if h : s1Curr < s1.rawEndPos ∧ s2Curr < s2.rawEndPos then
      have c1 := (s1.getUTF8Byte s1Curr ⋯).toAsciiLower;
      have c2 := (s2.getUTF8Byte s2Curr ⋯).toAsciiLower;
      if (c1 == c2) = true then String.Slice.eqIgnoreAsciiCase.go✝ s1 s1Curr.inc s2 s2Curr.inc else false
    else s1Curr == s1.rawEndPos && s2Curr == s2.rawEndPos
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelEpiComp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Epi f] [inst_3 : CategoryTheory.Limits.HasCokernel g],
  (CategoryTheory.Limits.cokernelEpiComp f g).hom =
    CategoryTheory.Limits.cokernel.desc (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.Limits.cokernel.π g) ⋯
-- Mathlib.Topology.Order.Hom.Esakia
/-- The type of Esakia morphisms, aka continuous pseudo-epimorphisms, from `α` to `β`.  -/
EsakiaHom : (α : Type u_6) →
  (β : Type u_7) → [TopologicalSpace α] → [Preorder α] → [TopologicalSpace β] → [Preorder β] → Type (max u_6 u_7)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.toCycles_comp_isoCycles₂_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.toCycles A 3 2) (groupHomology.isoCycles₂ A).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₃ A).hom
      (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.f'
-- Mathlib.Algebra.Star.Unitary
IsUnit.mem_unitary_iff_mul_star_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {u : R}, IsUnit u → (u ∈ unitary R ↔ u * star u = 1)
-- Init.Data.Sum.Basic
Sum.isRight_inr : ∀ {α : Type u_1} {β : Type u_2} {x : β}, (Sum.inr x).isRight = true
-- Mathlib.Algebra.Free
FreeSemigroup.hom_ext_iff : ∀ {α : Type u} {β : Type v} [inst : Mul β] {f g : FreeSemigroup α →ₙ* β},
  f = g ↔ ⇑f ∘ FreeSemigroup.of = ⇑g ∘ FreeSemigroup.of
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation'.mk_app : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R}
  (d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X))
  (d_map :
    ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(R.obj X)),
      (d Y).d ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) =
        (CategoryTheory.ConcreteCategory.hom (M.map f)) ((d X).d x))
  (X : Dᵒᵖ), (PresheafOfModules.Derivation'.mk d d_map).app X = d X
-- Init.Data.Option.Lemmas
Option.isSome_bind : ∀ {α : Type u_1} {β : Type u_2} (x : Option α) (f : α → Option β),
  (x.bind f).isSome = Option.any (fun x => (f x).isSome) x
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize Int32
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentRegistrationOptions.mk : Option Lean.Lsp.DocumentSelector → Lean.Lsp.TextDocumentRegistrationOptions
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.sphere_eq_empty_of_neg : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, ε < 0 → Metric.sphere x ε = ∅
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.instModule.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S],
  MonoidAlgebra.instModule = { toDistribMulAction := MonoidAlgebra.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_intCast : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (z : ℤ), WithVal.toVal v ↑z = ↑z
-- Mathlib.Analysis.RCLike.Basic
/-- Conjugate as a linear isometry  -/
RCLike.conjLIE : {K : Type u_1} → [inst : RCLike K] → K ≃ₗᵢ[ℝ] K
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s₁ s₂ t : Finset α}, s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.eq_1 : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] (f : ℝ → ε) (μ : MeasureTheory.Measure ℝ)
  (a b : ℝ),
  IntervalIntegrable f μ a b =
    (MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ∧ MeasureTheory.IntegrableOn f (Set.Ioc b a) μ)
-- Mathlib.Tactic.Ring.Basic
/-- The core of `proveEq` takes expressions `e₁ e₂ : α` where `α` is a `CommSemiring`,
and returns a proof that they are equal (or fails).  -/
_private.Mathlib.Tactic.Ring.Basic.0.Mathlib.Tactic.Ring.proveEq.ringCore : {v : Lean.Level} → {α : Q(Type v)} → Q(CommSemiring «$α») → (e₁ e₂ : Q(«$α»)) → Mathlib.Tactic.AtomM Q(«$e₁» = «$e₂»)
-- Mathlib.Algebra.Ring.Parity
Nat.even_xor_odd : ∀ (n : ℕ), Xor (Even n) (Odd n)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C],
  CategoryTheory.Limits.HasColimitsOfShape J (AlgebraicGeometry.PresheafedSpace C)
-- Mathlib.Condensed.Solid
CondensedMod.IsSolid.isIso_solidification_map : ∀ {R : Type (u + 1)} {inst : Ring R} {A : CondensedMod R} [self : CondensedMod.IsSolid R A] (X : Profinite),
  CategoryTheory.IsIso ((CategoryTheory.yoneda.obj A).map ((Condensed.profiniteSolidification R).app X).op)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddCommSemigroup : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddCommSemigroup M] → AddCommSemigroup (l.Germ M)
-- Mathlib.Topology.Spectral.Hom
/-- function between topological spaces  -/
SpectralMap.toFun : {α : Type u_6} → {β : Type u_7} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → SpectralMap α β → α → β
-- Mathlib.Data.Finset.Sups
Finset.forall_disjSups_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t : Finset α} {p : α → Prop},
  (∀ c ∈ s.disjSups t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
-- Mathlib.Geometry.Manifold.Instances.Real
IccRightChart_symm_apply : ∀ (x y : ℝ) [h : Fact (x < y)] (z : EuclideanHalfSpace 1), ↑(IccRightChart x y).symm z = ⟨max (y - (↑z).ofLp 0) x, ⋯⟩
-- Mathlib.Data.Matrix.Diagonal
Matrix.one_apply_ne : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] {i j : n}, i ≠ j → 1 i j = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Supported binary predicates on `BVExpr`.
 -/
Std.Tactic.BVDecide.BVBinPred : Type
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
Module.End.finite_hasEigenvalue : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  [IsDomain R] [Module.Finite R M] [Module.IsTorsionFree R M], {μ | f.HasEigenvalue μ}.Finite
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∈ m₂ → (m₁ ∩ m₂)[k]! = m₁[k]!
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.instIsStrictCutFlipOrderingSwap : ∀ {α : Type u_1} (cmp : α → α → Ordering) (cut : α → Ordering) [RBTree.RBNode.IsStrictCut cmp cut],
  RBTree.RBNode.IsStrictCut (flip cmp) fun x => (cut x).swap
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerRight_whiskerLeft : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} (D : Type u_4) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor A B) {G H : CategoryTheory.Functor B C}
  (η : G ⟶ H),
  CategoryTheory.Join.mapWhiskerRight (F.whiskerLeft η) (CategoryTheory.Functor.id D) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft D F G).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id D)).whiskerLeft
          (CategoryTheory.Join.mapWhiskerRight η (CategoryTheory.Functor.id D)))
        (CategoryTheory.Join.mapCompLeft D F H).inv)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal)
  {s : Set α}, MeasurableSet s → (f.restrict s).lintegral μ = ∑ r ∈ f.range, r * μ (⇑f ⁻¹' {r} ∩ s)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] {f g : InfTopHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Control.Fold
Monoid.Foldr.mk : {α : Type u} → (α → α) → Monoid.Foldr α
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_succ_le : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k : ℕ), LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I ≤ LieAlgebra.derivedSeriesOfIdeal R L k I
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion : ∀ (v : NumberField.InfinitePlace ℚ) (x : ℚ), ‖↑x‖ = ↑|x|
-- Init.Omega.IntList
Lean.Omega.IntList.sub_def : ∀ (xs ys : Lean.Omega.IntList), xs - ys = List.zipWithAll (fun x y => x.getD 0 - y.getD 0) xs ys
-- Mathlib.Data.List.DropRight
List.rdrop_append_length_add : ∀ {α : Type u_1} {l₁ l₂ : List α} (k : ℕ), (l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k
-- Mathlib.Topology.UniformSpace.Defs
/-- If `s ∈ uniformity`, then `Prod.swap ⁻¹' s ∈ uniformity`.  -/
UniformSpace.Core.symm : ∀ {α : Type u} (self : UniformSpace.Core α), Filter.Tendsto Prod.swap self.uniformity self.uniformity
-- Mathlib.Topology.Category.CompHaus.Limits
CompHaus.instHasExplicitFiniteCoproductsTrue : CompHausLike.HasExplicitFiniteCoproducts fun x => True
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InsertReplaceEdit.newText : Lean.Lsp.InsertReplaceEdit → String
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₃ : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_3),
  (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₃)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] (a : α),
  Std.DHashMap.Internal.AssocList.get! a Std.DHashMap.Internal.AssocList.nil =
    panicWithPosWithDecl "Std.Data.DHashMap.Internal.AssocList.Basic" "Std.DHashMap.Internal.AssocList.get!" 163 11
      "key is not present in hash table"
-- Mathlib.CategoryTheory.Filtered.FinallySmall
/-- If `C` is a locally small cofiltered initially small category,
this is an initial functor from a small cofiltered category.  -/
CategoryTheory.InitiallySmall.fromCofilteredInitialModel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofiltered C] →
      [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_3 : CategoryTheory.InitiallySmall C] →
          CategoryTheory.Functor (CategoryTheory.InitiallySmall.CofilteredInitialModel C) C
-- Mathlib.GroupTheory.QuotientGroup.Finite
/-- If `F` and `coker(F →* G)` are finite, then `G` is finite.  -/
Group.fintypeOfDomOfCoker : {F : Type u_1} →
  {G : Type u_2} →
    [inst : Group F] →
      [inst_1 : Group G] → [Fintype F] → (f : F →* G) → [f.range.Normal] → [Fintype (G ⧸ f.range)] → Fintype G
-- Mathlib.Order.Hom.Basic
disjoint_map_orderIso_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderBot β] {a b : α} (f : α ≃o β), Disjoint (f a) (f b) ↔ Disjoint a b
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pushoutMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : S ⟶ X} {g : S ⟶ Y} {f' : S ⟶ X'}
  {g' : S ⟶ Y'} {i₁ : X ⟶ X'} [inst_3 : CategoryTheory.Limits.HasPushoutsAlong f]
  [inst_4 : CategoryTheory.Limits.HasPushoutsAlong g'] {i₂ : Y ⟶ Y'},
  P i₁ →
    P i₂ →
      ∀ (e₁ : f' = CategoryTheory.CategoryStruct.comp f i₁) (e₂ : g' = CategoryTheory.CategoryStruct.comp g i₂),
        P (CategoryTheory.Limits.pushout.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
constFormalMultilinearSeries_apply_of_nonzero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {c : F} {n : ℕ},
  n ≠ 0 → constFormalMultilinearSeries 𝕜 E c n = 0
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentSpace.fiberBundle : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_6} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → [inst_6 : IsManifold I 1 M] → FiberBundle E (TangentSpace I)