mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Options
Lean.Option.Decl.mk.inj : ∀ {α : Type} {defValue : α} {descr : String} {deprecation? : Option Lean.OptionDeprecation} {defValue_1 : α}
  {descr_1 : String} {deprecation?_1 : Option Lean.OptionDeprecation},
  { defValue := defValue, descr := descr, deprecation? := deprecation? } =
      { defValue := defValue_1, descr := descr_1, deprecation? := deprecation?_1 } →
    defValue = defValue_1 ∧ descr = descr_1 ∧ deprecation? = deprecation?_1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.instAlgebraSubtypeMemMin_1 : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → (K₁ K₂ : IntermediateField F E) → Algebra ↥(K₁ ⊓ K₂) ↥K₂
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasLimit_iff_of_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G), CategoryTheory.Limits.HasLimit F ↔ CategoryTheory.Limits.HasLimit G
-- Mathlib.Topology.Algebra.Star
continuousAt_star : ∀ {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R] {x : R}, ContinuousAt star x
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNormal.match_1.eq_6 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (f g : Turing.ToPartrec.Code)
  (k : Turing.PartrecToTM2.Cont') (h_1 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match f.case g, k with
    | Turing.ToPartrec.Code.zero', k => h_1 k
    | Turing.ToPartrec.Code.succ, k => h_2 k
    | Turing.ToPartrec.Code.tail, k => h_3 k
    | f.cons fs, k => h_4 f fs k
    | f.comp g, k => h_5 f g k
    | f.case g, k => h_6 f g k
    | f.fix, k => h_7 f k) =
    h_6 f g k
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mem_carrier : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : AddSubmonoid M} {x : M}, x ∈ s.carrier ↔ x ∈ s
-- Lean.Elab.Do.Basic
/-- If `x` is a `mut` variable, record that its current binding aliases the original `let mut` binding,
so that go-to-definition and find-references treat both as the same variable.
 -/
Lean.Elab.Do.registerMutVarAlias : Lean.Name → Lean.Elab.Do.DoElabM Unit
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice.fun_cases_unfolding : ∀ (s : String.Slice) (p : String.Pos.Raw) (motive : Bool → Prop),
  (∀ (h : p < s.rawEndPos), motive (decide (s.getUTF8Byte p h).IsUTF8FirstByte)) →
    (¬p < s.rawEndPos → motive (decide (p = s.rawEndPos))) → motive (String.Pos.Raw.isValidForSlice s p)
-- Mathlib.Algebra.Notation
NegPart.mk : {α : Type u_1} → (α → α) → NegPart α
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.reverse = Polynomial.reflect f.natDegree f
-- Mathlib.Algebra.Quaternion
_private.Mathlib.Algebra.Quaternion.0.Cardinal.pow_four : ∀ {R : Type u_1} [Infinite R], Cardinal.mk R ^ 4 = Cardinal.mk R
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.addMonoidOf.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M),
  AddLocalization.addMonoidOf S = { toFun := fun x => AddLocalization.mk x 0, map_add' := ⋯, isLocalizationMap := ⋯ }
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (a : α), addRothNumber {a} = 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Init.Data.ByteArray.Bootstrap
ByteArray.toList_data_append' : ∀ {a b : ByteArray}, (a.append b).data.toList = a.data.toList ++ b.data.toList
-- Mathlib.Data.Set.Lattice.Image
Set.singleton_seq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set α}, {f}.seq t = f '' t
-- Init.Data.SInt.Lemmas
Int32.toInt8_toInt16 : ∀ (n : Int32), n.toInt16.toInt8 = n.toInt8
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  (F.map f).toFunctor.map ((F.mapId a).hom.toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv.toNatTrans.app X)
      ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X)
-- Mathlib.Algebra.Group.Basic
sub_right_inj : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a - b = a - c ↔ b = c
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.path_apply : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u v : ↥(unitary A)) (huv : ‖↑v - ↑u‖ < 2) (t : ↑unitInterval),
  (Unitary.path u v huv) t = selfAdjoint.expUnitary (↑t • Unitary.argSelfAdjoint (v * star u)) * u
-- Mathlib.RingTheory.EuclideanDomain
/-- This is a version of `isCoprime_div_gcd_div_gcd` which replaces the `q ≠ 0` assumption with
`gcd p q ≠ 0`.  -/
isCoprime_div_gcd_div_gcd_of_gcd_ne_zero : ∀ {R : Type u_1} [inst : EuclideanDomain R] [inst_1 : GCDMonoid R] {p q : R},
  gcd p q ≠ 0 → IsCoprime (p / gcd p q) (q / gcd p q)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The map `K.homology i ⟶ L.homology i` induced by a morphism in `HomologicalComplex`.  -/
HomologicalComplex.homologyMap : {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 : HomologicalComplex C c} →
            (K ⟶ L) → (i : ι) → [inst_2 : K.HasHomology i] → [inst_3 : L.HasHomology i] → K.homology i ⟶ L.homology i
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Hom.ext : ∀ {X Y : Type u} {x y : TypeCat.Hom X Y}, x.hom' = y.hom' → x = y
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.rootForm_apply_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (x y : M), (P.RootForm x) y = ∑ i, (P.coroot' i) x * (P.coroot' i) y
-- Lean.Expr
Lean.PersistentExprSet : Type
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.LaxTrans.Modification.id η).app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharType.upper : Lean.FuzzyMatching.CharType
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanIsoMk_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (z : F.obj CategoryTheory.Limits.WalkingCospan.one ≅ G.obj CategoryTheory.Limits.WalkingCospan.one)
  (l : F.obj CategoryTheory.Limits.WalkingCospan.left ≅ G.obj CategoryTheory.Limits.WalkingCospan.left)
  (r : F.obj CategoryTheory.Limits.WalkingCospan.right ≅ G.obj CategoryTheory.Limits.WalkingCospan.right)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z.hom =
        CategoryTheory.CategoryStruct.comp l.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl))
      CategoryTheory.Limits.cospanIsoMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z.hom =
        CategoryTheory.CategoryStruct.comp r.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
      CategoryTheory.Limits.cospanIsoMk._auto_3)
  (X : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospanIsoMk z l r hl hr).inv.app X =
    (Option.rec z (fun val => CategoryTheory.Limits.WalkingPair.rec l r val) X).inv
-- Mathlib.GroupTheory.Complement
AddSubgroup.vadd_toLeftFun : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {F : Type u_2} [inst_1 : AddGroup F] [inst_2 : AddAction F G]
  [inst_3 : AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (g : G),
  f +ᵥ ↑(⋯.toLeftFun g) = ↑(⋯.toLeftFun (f +ᵥ g))
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] (e : R ≃+* S)
  (s : NonUnitalSubsemiring R) (y : ↑(⇑↑e.toAddEquiv '' ↑s.toAddSubmonoid)),
  ↑((e.nonUnitalSubsemiringMap s).symm y) = e.symm ↑y
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instIsTorsionFreeInteger : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {ΓR : Type u_6}
  {ΓA : Type u_7} [inst_3 : LinearOrderedCommGroupWithZero ΓR] [inst_4 : LinearOrderedCommGroupWithZero ΓA]
  {vR : Valuation R ΓR} {vA : Valuation A ΓA} [inst_5 : vR.HasExtension vA] [IsDomain R] [Module.IsTorsionFree R A],
  Module.IsTorsionFree ↥vR.integer ↥vA.integer
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.map_top : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : NonUnitalSemiring B]
  [inst_6 : StarRing B] [inst_7 : Module R B] [inst_8 : FunLike F A B] [inst_9 : NonUnitalAlgHomClass F R A B]
  [inst_10 : StarHomClass F A B] [inst_11 : IsScalarTower R A A] [inst_12 : SMulCommClass R A A]
  [inst_13 : StarModule R A] (f : F), NonUnitalStarSubalgebra.map f ⊤ = NonUnitalStarAlgHom.range f
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_functor_obj_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R),
  ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).left = X.left
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.copy.sizeOf_spec : ∀ (q : Turing.PartrecToTM2.Λ'), sizeOf q.copy = 1 + sizeOf q
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.topEquiv_apply : ∀ {R : Type u} [inst : NonAssocSemiring R] (r : ↥⊤), Subsemiring.topEquiv r = ↑r
-- Aesop.Script.Step
Aesop.Script.Step.render : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      Array Lean.Syntax.Tactic →
        Aesop.Script.Step → Aesop.Script.TacticState → m (Array Lean.Syntax.Tactic × Aesop.Script.TacticState)
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.Result.rfl : Lean.Meta.MonadSimp.Result
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor : ∀ (C₁ : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
  (x : C₁ × C₂),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor x =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor x.1).prod (CategoryTheory.MonoidalCategoryStruct.leftUnitor x.2)
-- Mathlib.CategoryTheory.Functor.Functorial
/-- If `F : C → D` (just a function) has `[Functorial F]`,
we can write `map F f : F X ⟶ F Y` for the action of `F` on a morphism `f : X ⟶ Y`.  -/
CategoryTheory.Functorial.map : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        (F : C → D) → [self : CategoryTheory.Functorial F] → {X Y : C} → (X ⟶ Y) → (F X ⟶ F Y)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonpositive, then
`f` is an antitone function on `D`.  -/
antitoneOn_of_deriv_nonpos : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D → DifferentiableOn ℝ f (interior D) → (∀ x ∈ interior D, deriv f x ≤ 0) → AntitoneOn f D
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.apply_zero_uncurry0 : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×0]→L[𝕜] G')
  {x : Fin 0 → G}, ContinuousMultilinearMap.uncurry0 𝕜 G (f x) = f
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.tanh_bijOn : Set.BijOn Real.tanh Set.univ (Set.Ioo (-1) 1)
-- Mathlib.Computability.Encoding
Computability.Encoding.mk.sizeOf_spec : ∀ {α : Type u} {Γ : Type v} [inst : SizeOf α] [inst_1 : SizeOf Γ] (encode : α → List Γ) (decode : List Γ → Option α)
  (decode_encode : ∀ (x : α), decode (encode x) = some x),
  sizeOf { encode := encode, decode := decode, decode_encode := decode_encode } = 1
-- Init.Core
/-- If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are
inhabited.
 -/
Sum.inhabitedLeft : {α : Type u} → {β : Type v} → [Inhabited α] → Inhabited (α ⊕ β)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_mem : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {ι : Type u_4} {S : Type u_5} {s : S}
  [inst_2 : SetLike S α] [SubmonoidClass S α], IsClosed ↑s → ∀ {f : ι → α}, (∀ (i : ι), f i ∈ s) → ∏' (i : ι), f i ∈ s
-- Mathlib.Topology.Instances.RealVectorSpace
/-- Reinterpret a continuous additive equivalence between two real vector spaces
as a continuous real-linear map.  -/
AddEquiv.toRealLinearEquiv : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : Module ℝ E] →
      [inst_2 : TopologicalSpace E] →
        [ContinuousSMul ℝ E] →
          {F : Type u_2} →
            [inst_4 : AddCommGroup F] →
              [inst_5 : Module ℝ F] →
                [inst_6 : TopologicalSpace F] →
                  [ContinuousSMul ℝ F] → [T2Space F] → (e : E ≃+ F) → Continuous ⇑e → Continuous ⇑e.symm → E ≃L[ℝ] F
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorHom_comp_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.Dial C} (f₁ : X₁ ⟶ Y₁)
  (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
      (CategoryTheory.CategoryStruct.comp f₂ g₂)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.bind.eq_1 : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 β → Part γ),
  f.bind g = { toOrderHom := (↑f).partBind g.toOrderHom, map_ωSup' := ⋯ }
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp'_symm_single_eq_tmul_single_one : ∀ (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] (i : ι × κ) (r : R),
  ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r) = (fun₀ | i.1 => r) ⊗ₜ[R] fun₀ | i.2 => 1
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.hasTerminalAction : Lean.Elab.Term.Do.Code → Bool
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Iio_of_Iio : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {b : ι → α}
  {B : α}, Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Iio B)) l fun i => Set.Iio (b i)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
/-- The **Cayley-Hamilton Theorem**, that the characteristic polynomial of a matrix,
applied to the matrix itself, is zero.

This holds over any commutative ring.

See `LinearMap.aeval_self_charpoly` for the equivalent statement about endomorphisms.
 -/
Matrix.aeval_self_charpoly : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  (Polynomial.aeval M) M.charpoly = 0
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_iInf₂_iff : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] {a : α} {f : (i : ι) → κ i → LowerSet α},
  a ∈ ⨅ i, ⨅ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_unit_app_app_inr : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B) (a' : A'),
  ((CategoryTheory.Sum.functorEquiv A A' B).unit.app X).app (Sum.inr a') =
    CategoryTheory.CategoryStruct.id (X.obj (Sum.inr a'))
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_rpow_of_exponent_lt : ∀ {x y z : ℝ}, 1 < x → y < z → x ^ y < x ^ z
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.boundedOrder : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasInitial C] →
      [CategoryTheory.Limits.InitialMonoClass C] → {B : C} → BoundedOrder (CategoryTheory.Subobject B)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.inhabited : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → Inhabited hI.SubDPIdeal
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.ofList l) k = none
-- Mathlib.Util.PrintSorries
/-- - `#print sorries` prints all sorries that the current module depends on.
- `#print sorries id1 id2 ... idn` prints all sorries that the provided declarations depend on.
- `#print sorries in CMD` prints all the sorries in declarations added by the command.

Displayed sorries are hoverable and support "go to definition".
 -/
Mathlib.PrintSorries.«command#printSorriesIn_» : Lean.ParserDescr
-- Mathlib.Analysis.Fourier.AddCircle
MeasureTheory.memLp_haarAddCircle_iff : ∀ {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal},
  MeasureTheory.MemLp f p AddCircle.haarAddCircle ↔ MeasureTheory.MemLp f p MeasureTheory.volume
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Grind.Linarith.Poly.gcdCoeffsAux : Lean.Grind.Linarith.Poly → ℕ → ℕ
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Clause.limplies_iff_mem : ∀ {α : Type u_1} {β : Type u_2} [DecidableEq α] [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
  (l : Std.Sat.Literal α) (c : β),
  Std.Tactic.BVDecide.LRAT.Internal.Limplies α l c ↔ l ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.keysArray_eq_toArray_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β},
  t.keysArray = (Std.Internal.List.keys t.toListModel).toArray
-- Mathlib.Algebra.Lie.Free
/-- The embedding of `X` into the free Lie algebra of `X` with coefficients in the commutative ring
`R`.  -/
FreeLieAlgebra.of : (R : Type u) → {X : Type v} → [inst : CommRing R] → X → FreeLieAlgebra R X
-- Init.System.FilePath
System.instInhabitedFilePath : Inhabited System.FilePath
-- Mathlib.Topology.MetricSpace.Thickening
/-- Any set is contained in the complement of the δ-thickening of the complement of its
δ-thickening.  -/
Metric.subset_compl_thickening_compl_thickening_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α), E ⊆ (Metric.thickening δ (Metric.thickening δ E)ᶜ)ᶜ
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
SimplexCategoryGenRel.instHasFactorizationP_σP_δ : SimplexCategoryGenRel.P_σ.HasFactorization SimplexCategoryGenRel.P_δ
-- Mathlib.Order.Fin.Tuple
StrictMono.vecCons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α},
  StrictMono f → a < f 0 → StrictMono (Matrix.vecCons a f)
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.sup_support_coeff_finsetProd_le`. -/
AddMonoidAlgebra.sup_support_finset_prod_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} {ι : Type u_6} [inst : SemilatticeSup B] [inst_1 : OrderBot B]
  [inst_2 : CommSemiring R] [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid B] [AddLeftMono B] [AddRightMono B]
  {degb : A → B},
  degb 0 ≤ 0 →
    (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
      ∀ (s : Finset ι) (f : ι → AddMonoidAlgebra R A),
        (∏ i ∈ s, f i).coeff.support.sup degb ≤ ∑ i ∈ s, (f i).coeff.support.sup degb
-- Mathlib.AlgebraicGeometry.Limits
/-- The empty scheme is the initial object in the category of schemes.  -/
AlgebraicGeometry.emptyIsInitial : CategoryTheory.Limits.IsInitial ∅
-- Mathlib.Algebra.Order.Nonneg.Lattice
Nonneg.distribLattice : {α : Type u_1} → [inst : DistribLattice α] → {a : α} → DistribLattice { x // a ≤ x }
-- Std.Data.ExtDHashMap.Basic
/-- Updates the values of the hash map by applying the given function to all mappings.  -/
Std.ExtDHashMap.map : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      {x : BEq α} →
        {x_1 : Hashable α} →
          [EquivBEq α] → [LawfulHashable α] → ((a : α) → β a → γ a) → Std.ExtDHashMap α β → Std.ExtDHashMap α γ
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_toHomeomorph : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), e.symm.toHomeomorph = e.toHomeomorph.symm