mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
/-- For an additive functor `F : C ⥤ D` between abelian categories, the following are equivalent:
- `F` preserves short exact sequences on the left-hand side, i.e. if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact
  then `0 ⟶ F(A) ⟶ F(B) ⟶ F(C)` is exact.
- `F` preserves exact sequences on the left-hand side, i.e. if `A ⟶ B ⟶ C` is exact where `A ⟶ B`
  is mono, then `F(A) ⟶ F(B) ⟶ F(C)` is exact and `F(A) ⟶ F(B)` is mono as well.
- `F` preserves kernels.
- `F` preserves finite limits.
 -/
CategoryTheory.Functor.preservesFiniteLimits_tfae : ∀ {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] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f),
      ∀ (S : CategoryTheory.ShortComplex C),
        S.Exact ∧ CategoryTheory.Mono S.f → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F,
      CategoryTheory.Limits.PreservesFiniteLimits F].TFAE
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_uint64 : ∀ (x : UInt64), ↑x = ↑x.toNat
-- Mathlib.Order.Lex
toLex_symm_eq : ∀ {α : Type u_1}, toLex.symm = ofLex
-- Std.Http.Data.Method
/-- Create a redirect reference resource.
Source: https://www.rfc-editor.org/rfc/rfc4437#section-6
 -/
Std.Http.Method.mkredirectref : Std.Http.Method
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instIsCentralScalar : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E]
  [inst_4 : Module 𝕜ᵐᵒᵖ E] [inst_5 : IsBoundedSMul 𝕜ᵐᵒᵖ E] [IsCentralScalar 𝕜 E],
  IsCentralScalar 𝕜 ↥(MeasureTheory.Lp E p μ)
-- Init.Data.SInt.Bitwise
Bool.toInt8.eq_1 : ∀ (b : Bool), b.toInt8 = if b = true then 1 else 0
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_smul : ∀ {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R] [inst_1 : Monoid S] [inst_2 : DistribMulAction S R]
  [SMulCommClass S R R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃), star (s • a) = s • star a
-- Mathlib.NumberTheory.Bernoulli
bernoulli_eq_zero_of_odd : ∀ {n : ℕ}, Odd n → 1 < n → bernoulli n = 0
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.unit_inv_map : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : Monoid M] [inst_2 : Monoid N]
  [inst_3 : MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x), ↑⋯.unit⁻¹ = f ↑h.unit⁻¹
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- ContextInfo for running MetaM  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.ci : Mathlib.Linter.Flexible.StainData✝ → Lean.Elab.ContextInfo
-- Mathlib.Data.List.Lattice
List.bagInter.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x x_1 : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x []) (h_3 : (a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂) (x_2 : List α),
  x = [] →
    x_1 = x_2 →
      (match x, x_1 with
        | [], x => h_1 x
        | x, [] => h_2 x
        | a :: l₁, l₂ => h_3 a l₁ l₂) ≍
        h_1 x_2
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.HasIndepIncrements.neg : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] [inst_2 : AddCommGroup E] [MeasurableNeg E],
  ProbabilityTheory.HasIndepIncrements X P → ProbabilityTheory.HasIndepIncrements (-X) P
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_eq : ∀ (a : ℤ) (b : ℕ), a <<< b = a * 2 ^ b
-- Init.Core
Quot.liftIndepPr1 : ∀ {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a))
  (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) (q : Quot r), (Quot.lift (Quot.indep f) ⋯ q).fst = q
-- Mathlib.RingTheory.AlgebraicIndependent.Adjoin
AlgebraicIndependent.aevalEquivField_apply_coe : ∀ {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  (hx : AlgebraicIndependent F x) (a : FractionRing (MvPolynomial ι F)),
  ↑(hx.aevalEquivField a) = (IsFractionRing.lift ⋯) a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.toList_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  {f : α → β → γ},
  m.WF →
    (Std.DHashMap.Raw.Const.toList (Std.DHashMap.Raw.map f m)).Perm
      (List.map (fun p => (p.1, f p.1 p.2)) (Std.DHashMap.Raw.Const.toList m))
-- Init.Data.Slice.List.Lemmas
ListSlice.size_mkSlice_roc : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.size (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = min (hi + 1) (Std.Slice.size xs) - (lo + 1)
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_add_left_neg : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α),
  a ∉ t → (s + t).erase a = s.erase a + t
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The morphism in the category of `ProfiniteGrp` from a profinite group `P` to
the projective limit of its quotients by open normal subgroups ordered by inclusion  -/
ProfiniteGrp.toLimit : (P : ProfiniteGrp.{u}) → P ⟶ ProfiniteGrp.limit P.diagram
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.embedding_obj_ι : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] (X : C),
  ((CategoryTheory.Mat_.embedding C).obj X).ι = PUnit.{1}
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.mkUnder_hom : ∀ (R : CommRingCat) (A : Type u) [inst : CommRing A] [inst_1 : Algebra (↑R) A],
  (R.mkUnder A).hom = CommRingCat.ofHom (algebraMap (↑R) A)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHAddOffset_4 : HAdd Std.Time.Timestamp Std.Time.Second.Offset Std.Time.Timestamp
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.rightUnitor_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C))
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ : C} (f : X₁ ⟶ X₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f
        (CategoryTheory.CategoryStruct.id 𝒯.cone.pt))
      (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom f
-- Mathlib.LinearAlgebra.LinearPMap
/-- A `LinearPMap σ E F` or `E →ₛₗ.[σ] F` is a (semi)linear map from a submodule of `E` to `F`.  -/
«term_→ₛₗ.[_]_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Perfection
PreTilt.valAux_eq : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O →
    ∀ {p : ℕ} [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p] {f : PreTilt O p} {n : ℕ},
      (PreTilt.coeff n) f ≠ 0 → PreTilt.valAux K v O p f = ModP.preVal K v O p ((PreTilt.coeff n) f) ^ p ^ n
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter β}, Filter.Tendsto f (Filter.comap f x) x
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.exists_ne_zero_of_setIntegral_ne_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {t : Set X} {μ : MeasureTheory.Measure X}, ∫ (x : X) in t, f x ∂μ ≠ 0 → ∃ x ∈ t, f x ≠ 0
-- Lean.DocString.Parser
/-- Construct a “fake” atom with the given string content, with zero-width source information at the
current position.

Normally, atoms are always substrings of the original input; however, Verso's concrete syntax is
different enough from Lean's that this isn't always a good match.
 -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.fakeAtomHere : String → Lean.Parser.ParserFn
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.deg_neg : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : NegMemClass σ A]
  {𝒜 : ι → σ} (x : Submonoid A) (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x), (-c).deg = c.deg
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.nnnorm_mk' : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (p : E), ‖SeparationQuotient.mk p‖₊ = ‖p‖₊
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.main : Lean.Expr → Lean.MetavarContext.LevelMVarToParam.M Lean.Expr
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGE_le_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos}, s.posGE p h ≤ q ↔ p ≤ q.offset
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Abundant.eq_1 : ∀ (n : ℕ), n.Abundant = (n < ∑ i ∈ n.properDivisors, i)
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.IsConnected.toSubsingleton : ∀ {X : SSet} [self : X.IsConnected], Subsingleton X.π₀
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getKey? a (Std.Internal.List.insertEntryIfNew k v l) =
    if (k == a) = true ∧ Std.Internal.List.containsKey k l = false then some k else Std.Internal.List.getKey? a l
-- Mathlib.Algebra.BigOperators.Pi
FunLike.coe_sum : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun.eq_1 : ∀ (k : ℕ) (x : ℝ), bernoulliFun k x = Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k))
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.isAccessible_of_isCardinalAccessible : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [F.IsCardinalAccessible κ],
  CategoryTheory.Functor.IsAccessible.{w, v₁, v₂, u₁, u₂} F
-- Mathlib.Order.Filter.Pointwise
Filter.pureMonoidHom_apply : ∀ {α : Type u_2} [inst : MulOneClass α] (a : α), Filter.pureMonoidHom a = pure a
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg : ∀ {x y : ℝ*}, x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_smul : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  (k : α) [inst_3 : Invertible k], IsUnit A.det → (k • A)⁻¹ = ⅟k • A⁻¹
-- Lean.Level
Lean.Level.normalize : Lean.Level → Lean.Level
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_bot : ∀ {R : Type u} [inst : NonAssocRing R] {x : R}, x ∈ ⊥ ↔ ∃ n, ↑n = x
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.IsCommComonObj.comul_comm_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) {inst_3 : CategoryTheory.ComonObj X}
  [self : CategoryTheory.IsCommComonObj X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (CategoryTheory.CategoryStruct.comp (β_ X X).hom h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h
-- Mathlib.LinearAlgebra.Complex.Module
/-- `ℂ` has a basis over `ℝ` given by `1` and `I`.  -/
Complex.basisOneI : Module.Basis (Fin 2) ℝ ℂ
-- Init.Data.Fin.Basic
Fin.modn.eq_1 : ∀ {n : ℕ} (x a : ℕ) (h : a < n), ⟨a, h⟩.modn x = ⟨a % x, ⋯⟩
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.homotopyEquiv_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j),
  (HomologicalComplex.cylinder.homotopyEquiv K hc).inv = HomologicalComplex.cylinder.ι₀ K
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.inter : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X} {s t : Set X},
  Convexity.IsStarConvexSet R x s → Convexity.IsStarConvexSet R x t → Convexity.IsStarConvexSet R x (s ∩ t)
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- A weight `k` cusp form is bounded in norm by a constant multiple of `(im τ) ^ (-k / 2)`.  -/
CuspFormClass.exists_bound : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ]
  [CuspFormClass F Γ k] (f : F), ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_modify_self : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKey? k = if k ∈ t then some k else none
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.DependsOn.dep : (Lean.FVarId → Bool) → (Lean.MVarId → Bool) → Lean.Expr → Lean.DependsOn.M✝ Bool
-- Mathlib.Data.List.Map2
List.map₂Right_nil_left : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (bs : List β),
  List.map₂Right f [] bs = List.map (f none) bs
-- Mathlib.NumberTheory.Divisors
Nat.properDivisors.eq_1 : ∀ (n : ℕ), n.properDivisors = {d ∈ Finset.Ico 1 n | d ∣ n}
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When the first map `S.f` is zero, this is the left homology data on `S` given
by any limit kernel fork of `S.g`  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        S.f = 0 → (c : CategoryTheory.Limits.KernelFork S.g) → CategoryTheory.Limits.IsLimit c → S.LeftHomologyData
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.ne_bot : ∀ {R : Type u_1} [inst : CommRing R] (self : IsDedekindDomain.HeightOneSpectrum R), self.asIdeal ≠ ⊥
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.vComp' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {L₂ : CategoryTheory.Functor C₂ C₃}
  {R₂ : CategoryTheory.Functor D₂ D₃} {H₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
  [w.GuitartExact] [w'.GuitartExact] {L₁₂ : CategoryTheory.Functor C₁ C₃} {R₁₂ : CategoryTheory.Functor D₁ D₃}
  (eL : L₁.comp L₂ ≅ L₁₂) (eR : R₁.comp R₂ ≅ R₁₂), (w.vComp' w' eL eR).GuitartExact
-- Mathlib.Algebra.Star.MonoidHom
/-- The composition of star monoid homomorphisms, as a star monoid homomorphism.  -/
StarMonoidHom.comp : {A : Type u_2} →
  {B : Type u_3} →
    {C : Type u_4} →
      [inst : Monoid A] →
        [inst_1 : Star A] →
          [inst_2 : Monoid B] →
            [inst_3 : Star B] → [inst_4 : Monoid C] → [inst_5 : Star C] → (B →⋆* C) → (A →⋆* B) → A →⋆* C
-- Mathlib.Algebra.Lie.Weights.Basic
/-- If `M` is a representation of a nilpotent Lie algebra `L` with coefficients in `R`, then
`posFittingComp R L M` is the span of the positive Fitting components of the action of `x` on `M`,
as `x` ranges over `L`.

It is a Lie submodule because `L` is nilpotent.  -/
LieModule.posFittingComp : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [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] → [LieModule R L M] → [LieRing.IsNilpotent L] → LieSubmodule R L M
-- Mathlib.Data.List.Permutation
List.nodup_permutations'Aux_of_notMem : ∀ {α : Type u_1} (s : List α), ∀ x ∉ s, (List.permutations'Aux x s).Nodup
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_inv_of_right_invariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving Inv.inv μ μ
-- Lean.Meta.Transform
/-- Zeta-reduces `let`/`have` expressions in `e`, and also zeta-delta reduces let-bound variables.
Removes unused `let`/`have` expressions.

Options:
- If `zetaDelta` is true (default: true), then zeta-delta reduces (unfolds) let-bound variables.
- If `zetaHave` is false (default: true), then does not zeta reduce `have` expressions.
- If `beta` is true (default: true), then beta reduce applications of substituted values
 -/
Lean.Meta.zetaReduce : Lean.Expr → optParam Bool true → optParam Bool true → optParam Bool true → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Artinian.Module
isArtinian_prod : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup P]
  [inst_3 : Module R M] [inst_4 : Module R P] [IsArtinian R M] [IsArtinian R P], IsArtinian R (M × P)
-- Mathlib.Algebra.Group.End
MulAut.inv_def : ∀ (M : Type u_2) [inst : Mul M] (e₁ : MulAut M), e₁⁻¹ = MulEquiv.symm e₁
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instIterator.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : 0 = 0 → motive 0) (h_2 : (k : ℕ) → 0 = k.succ → motive k.succ),
  (match h' : 0 with
    | 0 => h_1 h'
    | k.succ => h_2 k h') =
    h_1 ⋯
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.biUnion_mem : ∀ {α : Type u_1} {C : Set (Set α)} {ι : Type u_2},
  MeasureTheory.IsSetRing C → ∀ {s : ι → Set α} (S : Finset ι), (∀ n ∈ S, s n ∈ C) → ⋃ i ∈ S, s i ∈ C
-- Mathlib.Topology.Constructions.SumProd
continuous_snd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Prod.snd
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
CategoryTheory.GrothendieckTopology.pointBotFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.GrothendieckTopology.pointBotFunctor.map f).hom = CategoryTheory.shrinkYoneda.{w, v, u}.flip.map f.op
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.liftGoalM : {α : Type} → Lean.Meta.Grind.GoalM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Init.Data.SInt.Lemmas
Int32.ofIntTruncate_bitVecToInt : ∀ (n : BitVec 32), Int32.ofIntClamp n.toInt = Int32.ofBitVec n
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.finish_isSpecial : ∀ (u : PNat.XgcdType), u.IsSpecial → u.finish.IsSpecial
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_add_zero : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A),
  CategoryTheory.shiftFunctorAdd' C a 0 a ⋯ =
    (CategoryTheory.shiftFunctor C a).rightUnitor.symm ≪≫
      (CategoryTheory.shiftFunctor C a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero C A).symm
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Get a prefix of `n₁` that is related to a prefix of `n₂`.  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel.find : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝ → Lean.Name → Lean.Name → Option (Lean.Name × Lean.Name)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.Equiv.beq_congr : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [inst : BEq β] {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {m₃ m₄ : Std.DTreeMap.Internal.Impl α fun x => β},
  m₁.WF →
    m₂.WF →
      m₃.WF →
        m₄.WF →
          m₁.Equiv m₃ →
            m₂.Equiv m₄ → Std.DTreeMap.Internal.Impl.Const.beq m₁ m₂ = Std.DTreeMap.Internal.Impl.Const.beq m₃ m₄
-- Mathlib.GroupTheory.Exponent
/-- A nontrivial monoid has prime exponent `p` if and only if every non-identity element has
order `p`.  -/
Monoid.exponent_eq_prime_iff : ∀ {G : Type u_1} [inst : Monoid G] [Nontrivial G] {p : ℕ},
  Nat.Prime p → (Monoid.exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. The number of items in the RBSet.  -/
RBTree.RBSet.size : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → ℕ
-- Mathlib.Tactic.NormNum.Parity
/-- `norm_num` extension for `Odd`.

Works for `ℕ` and `ℤ`.  -/
Mathlib.Meta.NormNum.evalOdd : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.arrowCongr_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₁'] [inst_4 : Semiring A₂'] [inst_5 : Algebra R A₁]
  [inst_6 : Algebra R A₂] [inst_7 : Algebra R A₁'] [inst_8 : Algebra R A₂'] [inst_9 : Star A₁] [inst_10 : Star A₂]
  [inst_11 : Star A₁'] [inst_12 : Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') (f : A₁ →⋆ₐ[R] A₂),
  (e₁.arrowCongr e₂) f = (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom
-- Init.Grind.Order
Lean.Grind.Order.lt_unsat : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α], ∀ a < a, False
-- Mathlib.Data.Fin.Basic
/-- `Fin.lt_or_ge` is an alias of `Fin.lt_or_le`.
It is preferred since it follows the mathlib naming convention.  -/
Fin.lt_or_ge : ∀ {n : ℕ} (a b : Fin n), a < b ∨ b ≤ a
-- Mathlib.Algebra.Group.Subgroup.Actions
AddSubgroup.instAddAction.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {S : AddSubgroup G},
  AddSubgroup.instAddAction =
    { toAddSemigroupAction := (AddSubmonoid.instAddActionSubtypeMem S).toAddSemigroupAction, zero_vadd := ⋯ }
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isOpen_forall_imp_mem : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) → ∀ {p : ι → Prop}, IsOpen {f | ∀ (i : ι), p i → ↑f i ∈ A i}
-- Init.Data.SInt.Lemmas
Int16.toInt64_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int16.maxValue.toInt → (Int16.ofNat n).toInt64 = Int64.ofNat n
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Limits.weakKernel.lift_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasWeakKernel f] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakKernel.lift f k h)
      (CategoryTheory.Limits.weakKernel.ι f) =
    k