mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Explicitly provided handlers.  -/
Lean.Elab.ConfigEval.EvalConfigItemView.handlers : Lean.Elab.ConfigEval.EvalConfigItemView → Array Lean.Elab.ConfigEval.EvalConfigItemHandler
-- Lean.Attributes
Lean.instBEqAttributeKind : BEq Lean.AttributeKind
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Given two smooth maps into the same fibers of a Riemannian bundle,
their scalar product is smooth.  -/
ContMDiffAt.inner_bundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (x : B) → NormedAddCommGroup (E x)] [inst_9 : (x : B) → InnerProductSpace ℝ (E x)]
  [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E] {EM : Type u_6} [inst_12 : NormedAddCommGroup EM]
  [inst_13 : NormedSpace ℝ EM] {HM : Type u_7} [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM}
  {M : Type u_8} [inst_15 : TopologicalSpace M] [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB n F E]
  {b : M → B} {v w : (x : M) → E (b x)} {x : M},
  ContMDiffAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun m => ⟨b m, v m⟩) x →
    ContMDiffAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun m => ⟨b m, w m⟩) x →
      ContMDiffAt IM (modelWithCornersSelf ℝ ℝ) n (fun b_1 => inner ℝ (v b_1) (w b_1)) x
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.sub_apply : ∀ {ι : Type u_1} {I₀ : WithTop (BoxIntegral.Box ι)} {M : Type u_4} [inst : AddCommGroup M]
  (f g : BoxIntegral.BoxAdditiveMap ι M I₀) (J : BoxIntegral.Box ι), (f - g) J = f J - g J
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.Faithful
-- Mathlib.Algebra.Order.Field.Basic
one_div_lt_neg_one : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α},
  a < 0 → -1 < a → 1 / a < -1
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
infEDist_cthickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (δ : ℝ) (s : Set E) (x : E),
  Metric.infEDist x (Metric.cthickening δ s) = Metric.infEDist x s - ENNReal.ofReal δ
-- Std.Time.DateTime
Std.Time.DateTime.instHAddOffset_5 : HAdd Std.Time.DateTime Std.Time.Millisecond.Offset Std.Time.DateTime
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.P : {R : Type u_4} →
  {S : Type u_5} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → StandardEtalePresentation R S → StandardEtalePair R
-- Mathlib.Control.Fold
Traversable.length : {α : Type u} → {t : Type u → Type u} → [Traversable t] → t α → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  [inst_2 : SizeOf C] (left : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left)
  (right : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right),
  sizeOf { left := left, right := right } = 1 + sizeOf left + sizeOf right
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The pullback in the category of a `SemilatticeInf` with `OrderTop` is the same as the infimum
over the objects.
 -/
CategoryTheory.Limits.CompleteLattice.pullback_eq_inf : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {x y z : α} (f : x ⟶ z) (g : y ⟶ z),
  CategoryTheory.Limits.pullback f g = x ⊓ y
-- Mathlib.Analysis.Normed.Module.Connected
Metric.contractibleSpace_closedEBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  ContractibleSpace ↑(Metric.closedEBall x r)
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.needsNoEscape : (s : String) → s.utf8ByteSize > 0 → Bool
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_bijective : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : Semiring D] [inst_8 : Algebra R D] {f : A →ₐ[R] B} {g : C →ₐ[R] D},
  Function.Bijective ⇑f → Function.Bijective ⇑g → Function.Bijective ⇑(Algebra.TensorProduct.map f g)
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
MeasureTheory.VectorMeasure.withDensity_zero_vectorMeasure : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G}, MeasureTheory.VectorMeasure.withDensity 0 f B = 0
-- Mathlib.Algebra.Star.StarAlgHom
/-- The second projection of a product is a ⋆-algebra homomorphism.  -/
StarAlgHom.snd : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] → [inst_4 : Semiring B] → [inst_5 : Algebra R B] → [inst_6 : Star B] → A × B →⋆ₐ[R] B
-- Mathlib.RingTheory.Localization.Defs
/-- Given `z : S`, `IsLocalization.sec M z` is defined to be a pair `(x, y) : R × M` such
that `z * f y = f x`, so this lemma is just an application of `S`'s commutativity.  -/
IsLocalization.sec_spec' : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S),
  (algebraMap R S) (IsLocalization.sec M z).1 = (algebraMap R S) ↑(IsLocalization.sec M z).2 * z
-- Mathlib.Topology.Compactness.Compact
Filter.hasBasis_cocompact : ∀ {X : Type u} [inst : TopologicalSpace X], (Filter.cocompact X).HasBasis IsCompact compl
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType.default : Mathlib.Meta.FunProp.LambdaTheoremType
-- Lean.Parser.Level
Lean.Parser.Level.hole.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Nat.Nth
Nat.nth_mem_of_lt_card : ∀ {p : ℕ → Prop} {n : ℕ} (hf : (Set.ofPred p).Finite), n < hf.toFinset.card → p (Nat.nth p n)
-- Mathlib.Order.LiminfLimsup
OrderIso.apply_blimsup : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α}
  [inst_1 : CompleteLattice γ] (e : α ≃o γ), e (Filter.blimsup u f p) = Filter.blimsup (⇑e ∘ u) f p
-- Mathlib.GroupTheory.OrderOfElement
AddCommute.addOrderOf_add_dvd_lcm : ∀ {G : Type u_1} [inst : AddMonoid G] {x y : G}, AddCommute x y → addOrderOf (x + y) ∣ (addOrderOf x).lcm (addOrderOf y)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The type copy of `E →SL[σ] F` endowed with the weak operator topology, denoted as
`E →SWOT[σ] F`. Likewise, when `σ := RingHom.id 𝕜`, the notation `E →WOT[𝕜] F` is available.  -/
ContinuousLinearMapWOT.«term_→SWOT[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The pushout in the category of a `SemilatticeSup` with `OrderBot` is the same as the supremum
over the objects.
 -/
CategoryTheory.Limits.CompleteLattice.pushout_eq_sup : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (x y z : α) (f : z ⟶ x) (g : z ⟶ y),
  CategoryTheory.Limits.pushout f g = x ⊔ y
-- Lean.DocString.Parser
/-- Parses a directive.  -/
Lean.Doc.Parser.directive : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.mk : {R : Type u_4} →
  {S : Type u_5} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : StandardEtalePair R) →
            (x : S) → (hasMap : P.HasMap x) → Function.Bijective ⇑(P.lift x hasMap) → StandardEtalePresentation R S
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- The forgetful functor from a full subcategory into the original category
("forgetting" the condition).
 -/
CategoryTheory.ObjectProperty.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.ObjectProperty C) → CategoryTheory.Functor P.FullSubcategory C
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_self : ∀ {E : Type v} [inst : Field E] (A : Subfield E), A.relrank A = 1
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go_as_denote' : ∀ (aig : Std.Sat.AIG ℕ) (start : ℕ) (inv : Bool) (h1 : start < aig.decls.size) (assign1 : ℕ → Bool),
  ⟦assign1, { aig := aig, ref := { gate := start, invert := inv, hgate := h1 } }⟧ = true →
    Std.Sat.AIG.toCNF.State.eval✝ (Std.Sat.AIG.toCNF.cnfSatAssignment✝ aig assign1)
        ↑(Std.Sat.AIG.toCNF.go✝ aig start h1 (Std.Sat.AIG.toCNF.State.empty✝ aig)) =
      true
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- The logarithmic derivative converts products into sums: away from a codiscrete subset of `𝕜`, the
logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic
derivatives.
 -/
Meromorphic.logDeriv_prod_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜'},
  (∀ i ∈ s, Meromorphic (F i)) →
    (∀ i ∈ s, ∀ (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤) →
      logDeriv (∏ i ∈ s, F i) =ᶠ[Filter.codiscrete 𝕜] ∑ i ∈ s, logDeriv (F i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.skAdj.coreflective : (n : ℕ) → CategoryTheory.Coreflective (SSet.Truncated.sk n)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pushouts_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [Q.IsStableUnderCobaseChange], P.pushouts ≤ Q ↔ P ≤ Q
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finite products of meromorphic functions are meromorphic.  -/
MeromorphicAt.prod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {s : Finset ι} {F : ι → 𝕜 → 𝕜'} {x : 𝕜},
  (∀ σ ∈ s, MeromorphicAt (F σ) x) → MeromorphicAt (∏ i ∈ s, F i) x
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_add_one : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}),
  Ordinal.deriv f (o + 1) = Ordinal.nfp f (Ordinal.deriv f o + 1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.IsQuasicoherent.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R},
  autoParam (Nonempty M.QuasicoherentData) SheafOfModules.IsQuasicoherent.nonempty_quasicoherentData._autoParam →
    M.IsQuasicoherent
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The range of a ring homomorphism, as a subring of the target. See Note [range copy pattern].  -/
RingHom.range : {R : Type u} → {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → (R →+* S) → Subring S
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.u_sInf : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {s : Set α}, u (sInf s) = ⨅ a ∈ s, u a
-- Mathlib.Lean.Meta.Basic
/-- Restore the metavariable context after execution.
 -/
Lean.Meta.preservingMCtx : {α : Type} → Lean.MetaM α → Lean.MetaM α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addXYZ_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : Fin 3 → R},
  W'.Equation P → W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![0, 1, 0]
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr_eval : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  [inst_1 : Inhabited Λ] [inst_2 : Inhabited σ] (k : K) (L : List (Γ k)) {L₁ : Turing.ListBlank (Turing.TM2to1.Γ' K Γ)}
  {L₂ : List (Γ k)},
  L₁ ∈ Turing.TM1.eval (Turing.TM2to1.tr M) (Turing.TM2to1.trInit k L) →
    L₂ ∈ Turing.TM2.eval M k L →
      ∃ S L',
        Turing.TM2to1.addBottom L' = L₁ ∧
          (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L' = Turing.ListBlank.mk (List.map some (S k)).reverse) ∧
            S k = L₂
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer.eq_def : ∀ (R : Type u) [inst : Ring R] (x : ℕ),
  descPochhammer R x =
    match x with
    | 0 => 1
    | n.succ => Polynomial.X * (descPochhammer R n).comp (Polynomial.X - 1)
-- Mathlib.Algebra.Group.Hom.Defs
/-- Copy of an `AddMonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
AddMonoidHom.copy : {M : Type u_4} →
  {N : Type u_5} → [inst : AddZero M] → [inst_1 : AddZero N] → (f : M →+ N) → (f' : M → N) → f' = ⇑f → M →+ N
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.TreeMap.Raw.ofList l cmp).getKeyD k fallback = fallback
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.IsBounded.of_real : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [inst : SeminormedRing 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : SeminormedRing 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] {p : ι → Seminorm 𝕜 E}
  {q : ι' → Seminorm 𝕜₂ F} {f : E →ₛₗ[σ₁₂] F},
  (∀ (i : ι'), ∃ s C, ∀ (x : E), (q i) (f x) ≤ C * (s.sup p) x) → Seminorm.IsBounded p q f
-- Mathlib.ModelTheory.Algebra.Field.CharP
FirstOrder.Field.model_hasChar_of_charP : ∀ {p : ℕ} {K : Type u_1} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K] [CharP K p],
  K ⊨ FirstOrder.Language.Theory.fieldOfChar p
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.π.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] (M : Type u_1) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type v)
  [inst_3 : CommSemiring S] [inst_4 : Algebra R S] (s : Finset S) (p : TensorProduct R (MvPolynomial (Fin s.card) R) M),
  PolynomialLaw.π R M S ⟨s, p⟩ = (LinearMap.rTensor M (PolynomialLaw.φ R s).toLinearMap) p
-- Mathlib.Dynamics.Ergodic.Action.Basic
MulAction.aeconst_of_aestabilizer_eq_top : ∀ (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Group G]
  [inst_1 : MulAction G α] [inst_2 : ErgodicSMul G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → MulAction.aestabilizer G μ s = ⊤ → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toStream.eq_2 : ∀ {α : Type u_1} (x : RBTree.RBNode.Stream α) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.node c l v r).toStream x = l.toStream (RBTree.RBNode.Stream.cons v r x)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- If `φ : S₁ ⟶ S₂` is a morphism of short complexes such that `φ.τ₁` is epi, `φ.τ₂` is an iso
and `φ.τ₃` is mono, then a homology data for `S₂` induces a homology data for `S₁`.
The inverse construction is `ofEpiOfIsIsoOfMono`.  -/
CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          S₂.HomologyData →
            [CategoryTheory.Epi φ.τ₁] → [CategoryTheory.IsIso φ.τ₂] → [CategoryTheory.Mono φ.τ₃] → S₁.HomologyData
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.bind_const : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β),
  f.bind (MeasureTheory.SimpleFunc.const α) = f
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.fintype : {V : Type u_1} → {G : SimpleGraph V} → [Fintype V] → [DecidableRel G.Adj] → Fintype G.Dart
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_eq_zero_of_isNilpotent : ∀ (R : Type u_1) (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] [inst_6 : LieModule R L M] [IsReduced R]
  [LieModule.IsNilpotent L M], LieModule.traceForm R L M = 0
-- Init.Data.Nat.Lemmas
Nat.dvd_div_iff_mul_dvd : ∀ {a b c : ℕ}, c ∣ b → (a ∣ b / c ↔ c * a ∣ b)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- A meromorphic function which agrees with the Mellin transform of `f - f₀` where defined  -/
WeakFEPair.Λ : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℂ → E
-- Lean.Util.Profile
Lean.profileitIO : {ε α : Type} → String → Lean.Options → EIO ε α → optParam Lean.Name Lean.Name.anonymous → EIO ε α
-- Mathlib.Algebra.Order.Sub.Basic
/-- `Sub` structure in linearly canonically ordered monoid using choice.  -/
CanonicallyOrderedAdd.toSub : {α : Type u_1} → [inst : AddCommMonoid α] → [inst_1 : LinearOrder α] → [CanonicallyOrderedAdd α] → Sub α
-- Mathlib.Algebra.Group.Units.Basic
add_eq_zero : ∀ {α : Type u} [inst : AddCommMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isMaximalClique_compl : ∀ {α : Type u_3} {G : SimpleGraph α} (s : Finset α), Maximal Gᶜ.IsClique ↑s ↔ Maximal G.IsIndepSet ↑s
-- Mathlib.Data.Seq.Computation
Computation.think_mem : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s → a ∈ s.think
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.instSetLikeElemFinset : {α : Type u_1} → {n : ℕ} → SetLike (↑(Set.powersetCard α n)) α
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- Eta-expanded form of `MeasureTheory.Integrable.neg`

---

If `f` is integrable, then so is `-f`.  -/
MeasureTheory.Integrable.fun_neg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun i => -f i) μ
-- Mathlib.SetTheory.ZFC.Basic
/-- An abbrev of `ZFSet.Definable` for binary functions.  -/
ZFSet.Definable₂ : (ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) → Type (u + 1)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product is positive (semi)definite.  -/
PreInnerProductSpace.Core.re_inner_nonneg : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (self : PreInnerProductSpace.Core 𝕜 F) (x : F), 0 ≤ RCLike.re (inner 𝕜 x x)
-- Mathlib.Topology.DenseEmbedding
Dense.extend_eq_at : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} [T2Space β]
  (hs : Dense s) {f : ↑s → β} {x : ↑s}, ContinuousAt f x → hs.extend f ↑x = f x
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.symm_comp_self_toHom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.symm.toHom.comp f.toHom = FirstOrder.Language.Hom.id L M
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.IsCardinalPresentable X κ]
  [CategoryTheory.EssentiallySmall.{w, v_1, u_1} J] [CategoryTheory.IsCardinalFiltered J κ]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  (f : X ⟶ c.pt), ∃ j f', CategoryTheory.CategoryStruct.comp f' (c.ι.app j) = f
-- LeanSearchClient.Syntax
LeanSearchClient.searchTacticImpl : Lean.Elab.Tactic.Tactic
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A subfamily of a linearly independent family (i.e., a composition with an injective map) is a
linearly independent family.  -/
LinearIndependent.comp : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → ∀ (f : ι' → ι), Function.Injective f → LinearIndependent R (v ∘ f)
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.IsCaratheodory.eq_1 : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) (s : Set α),
  m.IsCaratheodory s = ∀ (t : Set α), m t = m (t ∩ s) + m (t \ s)
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
/-- Linear lower bound for `f (x + n)` on unit interval  -/
Real.BohrMollerup.f_add_nat_ge : ∀ {f : ℝ → ℝ} {x : ℝ} {n : ℕ},
  ConvexOn ℝ (Set.Ioi 0) f →
    (∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) → 2 ≤ n → 0 < x → f ↑n + x * Real.log (↑n - 1) ≤ f (↑n + x)
-- Mathlib.Data.Fin.Tuple.Reflection
/-- `∃` with better defeq for `∃ x : Fin m → α, P x`.  -/
FinVec.Exists : {α : Type u_1} → {m : ℕ} → ((Fin m → α) → Prop) → Prop
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swapTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → ℕ → Array α → Sort u_2) →
    (x : List α) →
      (x_1 x_2 : ℕ) →
        (x_3 : Array α) →
          ((x x_4 : ℕ) → (x_5 : Array α) → motive [] x x_4 x_5) →
            ((head : α) → (tail : List α) → (x : Array α) → motive (head :: tail) 0 0 x) →
              ((a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) 0 i.succ acc) →
                ((a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) i.succ 0 acc) →
                  ((a : α) → (xs : List α) → (i j : ℕ) → (acc : Array α) → motive (a :: xs) i.succ j.succ acc) →
                    motive x x_1 x_2 x_3
-- Aesop.Forward.Match
/-- Convert forward rule matches to safe rules. Fails if any of the matches is
not a safe rule match.  -/
Aesop.forwardRuleMatchesToSafeRules? : Array Aesop.ForwardRuleMatch → Option (Array Aesop.SafeRule)
-- Lean.Expr
Lean.ExprStructEq.mk.sizeOf_spec : ∀ (val : Lean.Expr), sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.LinearAlgebra.TensorProduct.Prod
TensorProduct.prodLeft_tmul : ∀ (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Algebra R S] [inst_6 : Module R M₁] [inst_7 : Module S M₁] [inst_8 : IsScalarTower R S M₁]
  [inst_9 : Module R M₂] [inst_10 : Module R M₃] [inst_11 : Module S M₂] [inst_12 : IsScalarTower R S M₂] (m₁ : M₁)
  (m₂ : M₂) (m₃ : M₃), (TensorProduct.prodLeft R S M₁ M₂ M₃) ((m₁, m₂) ⊗ₜ[R] m₃) = (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Mathlib.Order.Filter.CountableSeparatingOn
HasCountableSeparatingOn.subtype_iff : ∀ {α : Type u_1} {p : Set α → Prop} {t : Set α},
  HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) Set.univ ↔ HasCountableSeparatingOn α p t
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J),
  CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j 0) CommRingCat.Colimits.Prequotient.zero
-- Init.Data.SInt.Bitwise
Int32.shiftRight_and : ∀ {a b c : Int32}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_prime_cpow_le_one_half : ∀ (p : Nat.Primes) {s : ℂ}, 1 < s.re → ‖↑↑p ^ (-s)‖ ≤ 1 / 2