mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- An arbitrary choice of local inverse of `f` near `x`.  -/
IsLocalDiffeomorphAt.localInverse : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} → IsLocalDiffeomorphAt I J n f x → PartialDiffeomorph J I N M n
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.instIsStableUnderShiftOppositeOpInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ], P.op.IsStableUnderShift ℤ
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryLE! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap.Raw α β cmp → α → α × β
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `homothety` as a multiplicative monoid homomorphism.  -/
AffineMap.homothetyHom : {k : Type u_2} →
  {V1 : Type u_3} →
    {P1 : Type u_4} →
      [inst : CommRing k] →
        [inst_1 : AddCommGroup V1] → [inst_2 : AddTorsor V1 P1] → [inst_3 : Module k V1] → P1 → k →* P1 →ᵃ[k] P1
-- Mathlib.Algebra.Module.Submodule.LinearMap
SMulMemClass.subtype_apply : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : SetLike A M] [inst_4 : AddSubmonoidClass A M] [inst_5 : SMulMemClass A R M] {S' : A} (x : ↥S'),
  (SMulMemClass.subtype S') x = ↑x
-- Mathlib.Order.SuccPred.Archimedean
/-- A `SuccOrder` is succ-archimedean if one can go from any two comparable elements by iterating
`succ`  -/
IsSuccArchimedean : (α : Type u_3) → [inst : Preorder α] → [SuccOrder α] → Prop
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.length_ne_zero_iff_eq_comp : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b),
  p.length ≠ 0 ↔ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1
-- Mathlib.Order.RelIso.Basic
/-- Two reflexive relations on a unique type are isomorphic.  -/
RelIso.ofUniqueOfRefl : {α : Type u_1} →
  {β : Type u_2} →
    (r : α → α → Prop) → (s : β → β → Prop) → [Std.Refl r] → [Std.Refl s] → [Unique α] → [Unique β] → r ≃r s
-- Mathlib.Analysis.Matrix.LDL
/-- The lower triangular matrix `L` of the LDL decomposition.  -/
LDL.lower : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : LinearOrder n] →
        [WellFoundedLT n] → [LocallyFiniteOrderBot n] → {S : Matrix n n 𝕜} → [Fintype n] → S.PosDef → Matrix n n 𝕜
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.ofNatThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.toByteArray_copy_ne_empty_iff : ∀ {s : String.Slice}, s.copy.toByteArray ≠ ByteArray.empty ↔ s.isEmpty = false
-- Init.Data.Slice.Array.Lemmas
Std.IterStep.mapIterator.eq_3 : ∀ {α : Type u} {β : Type w} {α' : Type u'} (f : α → α'),
  Std.IterStep.mapIterator f Std.IterStep.done = Std.IterStep.done
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- The constant Cauchy sequence  -/
_private.Mathlib.Algebra.Order.CauSeq.Basic.0.CauSeq.termConst_1 : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonRenameOptions : Lean.FromJson Lean.Lsp.RenameOptions
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_mul_natCast : ∀ {x : ℝ} (m : ℕ), Irrational (x * ↑m) → Irrational x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.Hom.addAction.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} [inst_3 : CategoryTheory.AddModObj M X] (Z : C),
  CategoryTheory.Hom.addAction Z = { toVAdd := CategoryTheory.Hom.instVAddHom Z, add_vadd := ⋯, zero_vadd := ⋯ }
-- Init.Omega.Constraint
Lean.Omega.Constraint.combine_sat' : ∀ {s t : Lean.Omega.Constraint} {x y : Lean.Omega.Coeffs},
  s.sat' x y = true → t.sat' x y = true → (s.combine t).sat' x y = true
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.snd : ∀ {𝕜 : 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'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {f : N → M × M'} {s : Set N} {x : N}, MDiffAt[s] f x → (MDiffAt[s] fun x => (f x).2) x
-- Std.Async.Basic
Std.Async.EAsync.instFunctor : {ε : Type} → Functor (Std.Async.EAsync ε)
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `Rat.num a`,
such that `positivity` successfully recognises `a`.  -/
Mathlib.Meta.Positivity.evalRatNum : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_pos_neg_pos_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ},
  ↑(3 • A).card ≤ K * ↑A.card → ↑(A + -A + A).card ≤ K ^ 3 * ↑A.card
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.homAddEquiv_symm_apply_hom : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (f : ↑M →ₗ[R] ↑N),
  SemimoduleCat.Hom.hom (SemimoduleCat.homAddEquiv.symm f) = f
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.Walk.length.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (x : G.Walk u v),
  x.length =
    match v, x with
    | .(u), SimpleGraph.Walk.nil => 0
    | v, SimpleGraph.Walk.cons h q => q.length.succ
-- Mathlib.Computability.PartrecCode
/-- A function is partial recursive if and only if there is a code implementing it. Therefore,
`eval` is a **universal partial recursive function**.  -/
Nat.Partrec.Code.exists_code : ∀ {f : ℕ →. ℕ}, Nat.Partrec f ↔ ∃ c, c.eval = f
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.quasiIso_truncLEMap_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : CategoryTheory.Limits.HasZeroObject C],
  QuasiIso (HomologicalComplex.truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafification_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q),
  (CategoryTheory.sheafification J D).map η = CategoryTheory.sheafifyMap J η
-- Mathlib.Order.Filter.ENNReal
ENNReal.liminf_const_mul_of_ne_zero_of_ne_top : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal},
  a ≠ 0 → a ≠ ⊤ → Filter.liminf (fun x => a * u x) f = a * Filter.liminf u f
-- Mathlib.Topology.Filter
ContinuousAt.nhds : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X},
  ContinuousAt f x → ContinuousAt (nhds ∘ f) x
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
OrderIso.lift_cof_congr : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, v} (Order.cof β)
-- Lean.Message
Lean.MessageData.mkPPContext : Lean.NamingContext → Lean.MessageDataContext → Lean.PPContext
-- Mathlib.LinearAlgebra.Dimension.Constructions
finrank_span_finset_eq_card : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {s : Finset M}, LinearIndepOn R id ↑s → Module.finrank R ↥(Submodule.span R ↑s) = s.card
-- Std.Time.Format.Modifier
Std.Time.Modifier.d.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.d presentation = Std.Time.Modifier.d presentation_1) = (presentation = presentation_1)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isLimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C),
  (CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit F G).isLimit =
    CategoryTheory.Limits.evaluationJointlyReflectsLimits (CategoryTheory.Limits.pointwiseBinaryBicone F G).toCone
      fun d =>
      (CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
          (CategoryTheory.Limits.pairComp F G ((CategoryTheory.evaluation D C).obj d)).symm
          (CategoryTheory.Limits.BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone
          (((CategoryTheory.evaluation D C).obj d).mapCone (CategoryTheory.Limits.pointwiseBinaryBicone F G).toCone)
          (CategoryTheory.Limits.Cone.ext
            (CategoryTheory.Iso.refl
              ((CategoryTheory.Limits.Cone.postcompose
                      (CategoryTheory.Limits.pairComp F G ((CategoryTheory.evaluation D C).obj d)).symm.hom).obj
                  (CategoryTheory.Limits.BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt)
            ⋯))
        (CategoryTheory.Limits.BinaryBiproduct.isLimit (F.obj d) (G.obj d))
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandElaboratingSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {elabSnap : Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot}
  {resultSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandResultSnapshot}
  {infoTreeSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf}
  {reportSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotTree} {toSnapshot_1 : Lean.Language.Snapshot}
  {elabSnap_1 : Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot}
  {resultSnap_1 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandResultSnapshot}
  {infoTreeSnap_1 : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf}
  {reportSnap_1 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree},
  { toSnapshot := toSnapshot, elabSnap := elabSnap, resultSnap := resultSnap, infoTreeSnap := infoTreeSnap,
        reportSnap := reportSnap } =
      { toSnapshot := toSnapshot_1, elabSnap := elabSnap_1, resultSnap := resultSnap_1, infoTreeSnap := infoTreeSnap_1,
        reportSnap := reportSnap_1 } →
    toSnapshot = toSnapshot_1 ∧
      elabSnap = elabSnap_1 ∧ resultSnap = resultSnap_1 ∧ infoTreeSnap = infoTreeSnap_1 ∧ reportSnap = reportSnap_1
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- Given an indexed family `f : ι → E` of vectors in an inner product space `E`, for which the
size of the index set is the dimension of `E`, the matrix of coefficients of `f` with respect to the
orthonormal basis `gramSchmidtOrthonormalBasis` constructed from `f` is upper-triangular.  -/
InnerProductSpace.gramSchmidtOrthonormalBasis_inv_isUpperTriangular : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E),
  ((InnerProductSpace.gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).IsUpperTriangular
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The projection map to the second component of the product.  -/
CategoryTheory.Limits.prod.snd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] → X ⨯ Y ⟶ Y
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.comp_fst : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l : Filter α} (l' : Filter β), f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.discreteTopology_of_forall_lt : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {Γ₀ : Type u_3}
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀] [inst_3 : TopologicalSpace K] [IsValuativeTopology K] [MulArchimedean Γ₀]
  (v : Valuation K Γ₀) [v.Compatible] {r : Γ₀}, r ≠ 0 → (∀ (x : K), v x ≠ 0 → r < v x) → DiscreteTopology K
-- Mathlib.RingTheory.HahnSeries.PowerSeries
/-- Casts a power series as a Hahn series with coefficients from a strictly ordered semiring.  -/
HahnSeries.ofPowerSeries : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : Semiring Γ] →
        [inst_2 : PartialOrder Γ] → [inst_3 : IsStrictOrderedRing Γ] → PowerSeries R →+* HahnSeries Γ R
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2}
  (X : I → C) [inst_2 : CategoryTheory.Limits.HasCoproduct X] (i : I)
  [CategoryTheory.Limits.HasCoproduct fun k => X ↑k], CategoryTheory.Mono (CategoryTheory.Limits.Sigma.ι X i)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instIsRightCancelAdd : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α] [IsRightCancelAdd α], IsRightCancelAdd (Matrix m n α)
-- Mathlib.Order.Minimal
not_maximal_iff : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α], P x → (¬Maximal P x ↔ ∃ y, P y ∧ x ≤ y ∧ ¬y ≤ x)
-- Lean.Language.Basic
_private.Lean.Language.Basic.0.Lean.Language.SnapshotTree.waitAll.go : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → BaseIO (Task Unit)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftProp_inclusion : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) →
      ∀ {U V : TopologicalSpace.Opens M} (hUV : U ≤ V), ChartedSpace.LiftProp Q (TopologicalSpace.Opens.inclusion hUV)
-- Mathlib.Order.Atoms
Set.instIsAtomistic : ∀ {α : Type u_2}, IsAtomistic (Set α)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →+ N, k : P →+ U` for Submonoids `S, T` respectively, an
isomorphism `j : M ≃+ P` such that `j(S) = T` induces an isomorphism of localizations `N ≃+ U`.  -/
AddSubmonoid.LocalizationMap.addEquivOfAddEquiv : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          {P : Type u_3} →
            [inst_2 : AddCommMonoid P] →
              S.LocalizationMap N →
                {T : AddSubmonoid P} →
                  {Q : Type u_4} →
                    [inst_3 : AddCommMonoid Q] →
                      T.LocalizationMap Q → {j : M ≃+ P} → AddSubmonoid.map j.toAddMonoidHom S = T → N ≃+ Q
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List α} {k fallback : α},
      k ∉ t → l.contains k = false → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKeyD k fallback = fallback
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t.insert k).max! = t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.not_vgt_of_veq`. -/
ValuativeRel.veq.not_vgt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → ¬y <ᵥ x
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvalue_sub'_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ ρ : R}, (ρ • LinearMap.id - f).HasEigenvalue μ ↔ f.HasEigenvalue (ρ - μ)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.mkMethods : optParam (Option Lean.Meta.Grind.EvalTactic) none → Lean.CoreM Lean.Meta.Grind.Methods
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_notMem_range : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}), Ordinal.lsub f ∉ Set.range f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_inter_le_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ ∩ m₂).size ≤ m₁.size
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ \ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Algebra.Algebra.Hom.Rat
RingHom.toRatAlgHom_toRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R →+* S), ↑f.toRatAlgHom = f
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inl_aut_inv : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (g : G) (n : N),
  SemidirectProduct.inl ((φ g)⁻¹ n) = SemidirectProduct.inr g⁻¹ * SemidirectProduct.inl n * SemidirectProduct.inr g
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_add_one_le_iff : ∀ {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι], ⨆ i, f i + 1 ≤ a ↔ ∀ (i : ι), f i < a
-- Mathlib.Topology.Category.CompHaus.Basic
CompHaus.hasLimits : CategoryTheory.Limits.HasLimits CompHaus
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {he : t ≠ ∅} {km : α}, t.min he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_5 : L.Monoidal]
  (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_6 : CategoryTheory.Localization.Lifting L W G F],
  CategoryTheory.Localization.Lifting₂.iso L L W W (CategoryTheory.MonoidalCategory.curriedTensorPost G)
      (CategoryTheory.MonoidalCategory.curriedTensorPost F) =
    (CategoryTheory.Functor.postcompose₂.obj F).mapIso
        (CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost L) ≪≫
      CategoryTheory.MonoidalCategory.curriedTensorPostFunctor.mapIso (CategoryTheory.Localization.Lifting.iso L W G F)
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instSubsingletonOfIsEmpty : ∀ {α : Type u} [IsEmpty α], Subsingleton (WithOne α)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsFiniteMeasureForallVolume : ∀ {ι : Type u_1} [inst : Fintype ι] {α : ι → Type u_4} [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : ι), MeasureTheory.IsFiniteMeasure MeasureTheory.volume], MeasureTheory.IsFiniteMeasure MeasureTheory.volume
-- Mathlib.Analysis.Asymptotics.LinearGrowth
/-- Upper linear growth of a sequence.  -/
LinearGrowth.linearGrowthSup : {R : Type u_1} → [ConditionallyCompleteLattice R] → [Div R] → [NatCast R] → (ℕ → R) → R
-- Mathlib.Topology.MetricSpace.Holder
/-- A function `f : X → Y` between two `PseudoEMetricSpace`s is Hölder continuous with constant
`C : ℝ≥0` and exponent `r : ℝ≥0`, if `edist (f x) (f y) ≤ C * edist x y ^ r` for all `x y : X`.  -/
HolderWith : {X : Type u_1} → {Y : Type u_2} → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → NNReal → NNReal → (X → Y) → Prop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.replaceFun : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)} {f : ℝ → ℝ},
  ms.Sorted → (ms.replaceFun f).Sorted
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivAtFilter.neg` -/
HasFDerivAtFilter.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)}, HasFDerivAtFilter f f' L → HasFDerivAtFilter (fun i => -f i) (-f') L
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_inj : ∀ {a b : UInt8}, a.toBitVec = b.toBitVec ↔ a = b
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (PMF α)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isFiltered_of_semilatticeSup_nonempty : ∀ (α : Type u) [inst : SemilatticeSup α] [Nonempty α], CategoryTheory.IsFiltered α
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v).contains k = true
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBiproduct_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : F.PreservesZeroMorphisms] [inst_6 : CategoryTheory.Limits.PreservesBiproduct f F],
  (F.mapBiproduct f).hom = CategoryTheory.Limits.biproduct.lift fun j => F.map (CategoryTheory.Limits.biproduct.π f j)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_sub : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Ring R] [inst_1 : Ring S] (f : R →+ S) (x y : MonoidAlgebra R M),
  MonoidAlgebra.map f (x - y) = MonoidAlgebra.map f x - MonoidAlgebra.map f y