mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.maxGenEigenSpace_toEnd_eq_top : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsNilpotent L M] (x : L), ((LieModule.toEnd R L M) x).maxGenEigenspace 0 = ⊤
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_ushiftRight : ∀ {n : ℕ} (x : BitVec n) (i j : ℕ), (x >>> i).getLsbD j = x.getLsbD (i + j)
-- Mathlib.NumberTheory.FLT.Polynomial
_private.Mathlib.NumberTheory.FLT.Polynomial.0.Polynomial.flt_catalan_deriv : ∀ {k : Type u_1} [inst : Field k] {p q r : ℕ},
  p ≠ 0 →
    q ≠ 0 →
      r ≠ 0 →
        q * r + r * p + p * q ≤ p * q * r →
          ↑p ≠ 0 →
            ↑q ≠ 0 →
              ↑r ≠ 0 →
                ∀ {a b c : Polynomial k},
                  a ≠ 0 →
                    b ≠ 0 →
                      c ≠ 0 →
                        IsCoprime a b →
                          ∀ {u v w : k},
                            u ≠ 0 →
                              v ≠ 0 →
                                w ≠ 0 →
                                  Polynomial.C u * a ^ p + Polynomial.C v * b ^ q + Polynomial.C w * c ^ r = 0 →
                                    Polynomial.derivative a = 0 ∧
                                      Polynomial.derivative b = 0 ∧ Polynomial.derivative c = 0
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitAppArgs : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldlM.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (x : δ), Std.DHashMap.Internal.AssocList.foldlM f x Std.DHashMap.Internal.AssocList.nil = pure x
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.instAlgebraSubtypeMemSubringToSubringOfPrime : {K : Type u_3} →
  [inst : Field K] →
    (A : Subring K) → (P : Ideal ↥A) → [inst_1 : P.IsPrime] → Algebra ↥A ↥(LocalSubring.ofPrime A P).toSubring
-- Mathlib.Combinatorics.Graph.Lattice
Graph.inf_inc_iff : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  (G ⊓ H).Inc e x ↔ ∃ y, G.IsLink e x y ∧ H.IsLink e x y
-- Init.NotationExtra
unexpandTSepArray : Lean.PrettyPrinter.Unexpander
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {fallback : α}, t.getD t.min! fallback = t.min!
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.toSubgroup : {G : Type u_1} → [inst : Group G] → FiniteIndexNormalSubgroup G → Subgroup G
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageParams.mk : Lean.Lsp.MessageType → String → Lean.Lsp.ShowMessageParams
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- A linear set is proper if its submonoid generators (periods) are linearly independent.  -/
IsProperLinearSet : {M : Type u_1} → [AddCommMonoid M] → Set M → Prop
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Continuous linear maps themselves form a normed space with respect to the operator norm.  -/
ContinuousLinearMap.toNormedAddCommGroup : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_3} →
    {E : Type u_5} →
      {F : Type u_6} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedAddCommGroup F] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NontriviallyNormedField 𝕜₂] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜₂ F] →
                    {σ₁₂ : 𝕜 →+* 𝕜₂} → [RingHomIsometric σ₁₂] → NormedAddCommGroup (E →SL[σ₁₂] F)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion₂_smul : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : SMul α β] (s : (i : ι) → κ i → Set α)
  (t : Set β), (⋃ i, ⋃ j, s i j) • t = ⋃ i, ⋃ j, s i j • t
-- Mathlib.Data.Set.Pairwise.Basic
pairwise_ne_iff_injective : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → α}, (Pairwise fun i j => f i ≠ f j) ↔ Function.Injective f
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Triangles with triangle morphisms form a category.
 -/
CategoryTheory.Pretriangulated.triangleCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      CategoryTheory.Category.{v, max u v} (CategoryTheory.Pretriangulated.Triangle C)
-- Lean.Data.DeclarationRange
/-- Store position information for declarations.  -/
Lean.DeclarationRange : Type
-- Init.Control.ExceptCps
ExceptCpsT.run_lift : ∀ {m : Type u → Type u_1} {α ε : Type u} [inst : Monad m] (x : m α),
  (ExceptCpsT.lift x).run = do
    let a ← x
    pure (Except.ok a)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- For an element `f ∈ A` with positive degree and a homogeneous ideal in `D(f)`, we have that the
stalk of `Spec A⁰_ f` at `y` is isomorphic to `A⁰ₓ` where `y` is the point in `Proj` corresponding
to `x`.
 -/
AlgebraicGeometry.ProjectiveSpectrum.Proj.specStalkEquiv : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                (x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)) →
                  {m : ℕ} →
                    f ∈ 𝒜 m →
                      0 < m →
                        ((AlgebraicGeometry.Spec.structureSheaf (HomogeneousLocalization.Away 𝒜 f)).presheaf.stalk
                            ((CategoryTheory.ConcreteCategory.hom
                                (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base)
                              x) ≅
                          CommRingCat.of (HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
-- Mathlib.Data.Set.Sups
Set.Nonempty.infs : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α}, s.Nonempty → t.Nonempty → (s ⊼ t).Nonempty
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.mem_smul_set_iff_inv_smul_mem₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ (A : Set β) (x : β), x ∈ a • A ↔ a⁻¹ • x ∈ A
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_isBasis'_sdiff_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis' I X → J ⊆ I → (M.contract J).IsBasis' (I \ J) X
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.coe_integer : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K],
  ↑(S.integer K) = {x | ∀ v ∉ S, (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≤ 1}
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- `limitCone F` is limit.  -/
CategoryTheory.ShortComplex.isLimitLimitCone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [inst_3 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [inst_4 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.limitCone F)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- An abbreviation for a Weierstrass curve in affine coordinates.  -/
WeierstrassCurve.Affine : Type r → Type r
-- Mathlib.Topology.IsClosedRestrict
Topology.reorderRestrictProd_restrict_compl : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι}
  (x : ↑(Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s)),
  Topology.reorderRestrictProd S s (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i => ↑x ↑i) = ↑x
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.den_mem_inv : ∀ {K : Type u_3} [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I ≠ ⊥ → (algebraMap R₁ K) ↑I.den ∈ I⁻¹
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.eval_one_cyclotomic_prime : ∀ {R : Type u_1} [inst : CommRing R] {p : ℕ} [hn : Fact (Nat.Prime p)],
  Polynomial.eval 1 (Polynomial.cyclotomic p R) = ↑p
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- **Alias** of `CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_lift`. -/
CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D}
  (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) {c : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Limits.IsLimit.ofConeEquiv h).symm P).lift s =
    CategoryTheory.CategoryStruct.comp (h.counitIso.inv.app s).hom
      (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Restriction of a `MonoidHom` to a `Submonoid` of the codomain.  -/
MonoidHom.codRestrict : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {S : Type u_5} →
          [inst_2 : SetLike S N] →
            [inst_3 : SubmonoidClass S N] → (f : M →* N) → (s : S) → (∀ (x : M), f x ∈ s) → M →* ↥s
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- **Alias** of the forward direction of `isCompactOperator_id_iff_locallyCompactSpace`. -/
LocallyCompactSpace.of_isCompactOperator_id : ∀ {E : Type u_1} [inst : AddGroup E] [inst_1 : TopologicalSpace E] [IsTopologicalAddGroup E],
  IsCompactOperator id → LocallyCompactSpace E
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesAt.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E},
  HasFPowerSeriesAt f p x → HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the `Fintype` deriving handler.) -/
Turing.PartrecToTM2.Γ'.enumList : List Turing.PartrecToTM2.Γ'
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- Recurrence for the `GenContFract.of` an element `v` of `K` in terms of that of the inverse of
the fractional part of `v`.
 -/
GenContFract.of_s_succ : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) [IsStrictOrderedRing K]
  (n : ℕ), (GenContFract.of v).s.get? (n + 1) = (GenContFract.of (Int.fract v)⁻¹).s.get? n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).getKey? k = if k ∈ t₂ then t₁.getKey? k else none
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_one_div : ∀ {x : ℝ}, Irrational (1 / x) → Irrational x
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.full_whiskeringLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (E : Type u_4)
  [inst_3 : CategoryTheory.Category.{v_4, u_4} E], ((CategoryTheory.Functor.whiskeringLeft C D E).obj L).Full
-- Lean.Meta.Sym.Simp.SimpM
/-- Marks a result as context-dependent.  -/
Lean.Meta.Sym.Simp.Result.withContextDependent : Lean.Meta.Sym.Simp.Result → Lean.Meta.Sym.Simp.Result
-- Mathlib.Analysis.InnerProductSpace.Spectrum
eigenvalue_pos_of_pos : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {μ : ℝ} {T : E →ₗ[𝕜] E}, Module.End.HasEigenvalue T ↑μ → (∀ (x : E), 0 < RCLike.re (inner 𝕜 x (T x))) → 0 < μ
-- Mathlib.RepresentationTheory.Semisimple
/-- A representation is semisimple when every subrepresentation has a complement.  -/
Representation.IsSemisimpleRepresentation : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Field k] → [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → Representation k G V → Prop
-- Mathlib.Algebra.Module.LocalizedModule.IsLocalization
/-- `A` is a localization of a commutative semiring `R` with respect to `S` iff
the associated linear map `R →ₗ[R] A` is a localization of modules with respect to `S`.  -/
isLocalizedModule_iff_isLocalization' : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A], IsLocalizedModule S (Algebra.linearMap R A) ↔ IsLocalization S A
-- Std.Async.Signal
Std.Async.Signal.sigusr1.sizeOf_spec : sizeOf Std.Async.Signal.sigusr1 = 1
-- Mathlib.Order.Hom.Basic
/-- Converts an `OrderIso` into a `RelIso (<) (<)`.  -/
OrderIso.toRelIsoLT : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.divAll.eq_2 : ∀ (k k_1 : ℤ) (v : Int.Internal.Linear.Var) (p_1 : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.divAll k (Int.Internal.Linear.Poly.add k_1 v p_1) =
    (k_1 % k == 0 && Int.Internal.Linear.Poly.divAll k p_1)
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ioo_eq_range' : ∀ (a b : ℕ), Finset.Ioo a b = { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := ⋯ }
-- Mathlib.Data.List.AList
AList.notMem_empty : ∀ {α : Type u} {β : α → Type v} (a : α), a ∉ ∅
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (m : M) (s : ↥S), LocalizedModule.mk m s = m /ₒ s
-- Batteries.Recycling.RBTree.Lemmas
/-- Auxiliary definition for `zoom_ins`: set the root of the tree to `v`, creating a node if necessary.
 -/
RBTree.RBNode.setRoot : {α : Type u_1} → α → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.mapsTo_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ℝ), Set.MapsTo f (Metric.ball x r) (Metric.ball (f x) r)
-- Batteries.Data.List.Basic
List.inits.eq_def : ∀ {α : Type u_1} (x : List α),
  x.inits =
    match x with
    | [] => [[]]
    | a :: l => [] :: List.map (fun t => a :: t) l.inits
-- Mathlib.Order.LatticeIntervals
Set.Iic.codisjoint_iff : ∀ {α : Type u_1} {a : α} [inst : SemilatticeSup α] {x y : ↑(Set.Iic a)}, Codisjoint x y ↔ ↑x ⊔ ↑y = a
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.Spec_iff : ∀ {R S : CommRingCat} {φ : R ⟶ S},
  AlgebraicGeometry.SurjectiveOnStalks (AlgebraicGeometry.Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- Lebesgue integral over a set is monotone in function.

This version assumes that the upper estimate is an a.e. measurable function
and the estimate holds a.e. on the set.
See also `setLIntegral_mono_ae'` for a version that assumes measurability of the set
but assumes no regularity of either function.  -/
MeasureTheory.setLIntegral_mono_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal},
  AEMeasurable g (μ.restrict s) → (∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x) → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
-- Mathlib.Logic.Basic
/-- **Alias** of `Classical.byContradiction`. -/
Classical.by_contradiction : ∀ {p : Prop}, (¬p → False) → p
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.toList_perm : ∀ {α : Type u} {m₁ m₂ : Std.HashSet.Raw α}, m₁.Equiv m₂ → m₁.toList.Perm m₂.toList
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidSaveTextDocumentParams.textDocument : Lean.Lsp.DidSaveTextDocumentParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.Data.Set.NAry
Set.subset_image2_sdiff_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
  Set.image2 f s t \ Set.image2 f s t' ⊆ Set.image2 f s (t \ t')
-- Mathlib.RingTheory.Flat.Stability
Module.Flat.ulift_right_iff : ∀ {R : Type u} {M : Type w} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.Flat R (ULift.{t, w} M) ↔ Module.Flat R M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a} {k : α}, k ∈ Std.DTreeMap.map f t ↔ k ∈ t
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.instInhabited : Inhabited FinBoolAlg
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.Context.mk : Lean.Name → Array Lean.FVarId → Lean.Elab.Term.ToDepElimPattern.Context
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.str : String → Lean.Compiler.LCNF.LitValue
-- Mathlib.Analysis.Calculus.Deriv.Abs
differentiableAt_abs_pos : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ (fun x => |x|) x
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Iic : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {a x : α}, x ∈ Finset.Iic a ↔ x ≤ a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.contains t.max! = true
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.AddCommGrpCat.Hom.mk.sizeOf_spec : ∀ {A B : AddCommGrpCat} (hom' : ↑A →+ ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.add b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_5 a b
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.coeff_hermite : ∀ (n k : ℕ),
  (Polynomial.hermite n).coeff k =
    if Even (n + k) then (-1) ^ ((n - k) / 2) * ↑(n - k - 1).doubleFactorial * ↑(n.choose k) else 0
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n : M}
  {X Y : C} (f : X ⟶ Y) [inst_3 : F.LaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.obj m).map f))
      ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m n)).map f)
-- Mathlib.RingTheory.RingHom.EssFiniteType
RingHom.EssFiniteType.holdsForLocalization : RingHom.HoldsForLocalization fun {R S} [CommRing R] [CommRing S] => RingHom.EssFiniteType
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α}, m.getKey? k = some k' → k' ∈ m
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.lift_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g)
      ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f g)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact.injEq : ∀ (lhs : Bool) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr) (lhs_1 : Bool)
  (c₁_1 : Lean.Meta.Grind.AC.EqCnstr) (c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr),
  (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact lhs c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact lhs_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Logic.Function.Iterate
Function.Iterate.rec_zero : ∀ {α : Type u} (motive : α → Sort u_1) {f : α → α} (app : (a : α) → motive a → motive (f a)) {a : α} (arg : motive a),
  Function.Iterate.rec motive arg app 0 = arg
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Complex.cos` is complex analytic.  -/
Complex.analyticOnNhd_cos : ∀ {s : Set ℂ}, AnalyticOnNhd ℂ Complex.cos s
-- Init.Data.Nat.Lcm
Nat.lcm_self : ∀ (m : ℕ), m.lcm m = m
-- Mathlib.CategoryTheory.Filtered.Basic
/-- A category `IsCofilteredOrEmpty` if
1. for every pair of objects there exists another object "to the left", and
2. for every pair of parallel morphisms there exists a morphism to the left so the compositions
   are equal.
 -/
CategoryTheory.IsCofilteredOrEmpty : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalListStx : {α : Type} →
  Lean.Expr → (Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)) → Lean.Term → Lean.Elab.TermElabM (List α × Lean.Expr)
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.u_l_eq : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisCoinsertion l u) (b : β), u (l b) = b
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.map_toSubmodule : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {k : ℕ} {A : Type w}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] {B : Type w} [inst_5 : CommRing B] [inst_6 : Algebra R B] (f : A →ₐ[R] B)
  (N : Module.Grassmannian A (TensorProduct R A M) k),
  (Module.Grassmannian.map f N).toSubmodule = (Module.Grassmannian.baseChangeMkQ B N.toSubmodule).ker
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.mem_range : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {x : M₂}, x ∈ f.range ↔ ∃ y, f y = x
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.instSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsPreimmersion f],
  AlgebraicGeometry.IsPreimmersion (CategoryTheory.Limits.pullback.snd f g)