mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.revFind?_char_eq_revFind?_beq : ∀ {c : Char} {s : String.Slice}, s.revFind? c = s.revFind? fun x => x == c
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.cospanOp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospanOp f g).hom.app X_1 =
    (match X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.op X)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op Y)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Z)).hom
-- Mathlib.Algebra.Group.Units.Defs
isAddUnit_iff_eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} [Subsingleton (AddUnits M)], IsAddUnit a ↔ a = 0
-- Mathlib.Algebra.Module.Equiv.Defs
/-- A linear equivalence is an invertible linear map.  -/
LinearEquiv : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (σ : R →+* S) →
          {σ' : S →+* R} →
            [RingHomInvPair σ σ'] →
              [RingHomInvPair σ' σ] →
                (M : Type u_16) →
                  (M₂ : Type u_17) →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → Type (max u_16 u_17)
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a congruence relation `c` on a ring and a homomorphism `f`
constant on the equivalence classes of `c`, `f` has the same image
as the homomorphism that `f` induces on the quotient.  -/
RingCon.range_lift : ∀ {M : Type u_1} {P : Type u_3} [inst : Ring M] [inst_1 : Ring P] {c : RingCon M} {f : M →+* P} (H : c ≤ RingCon.ker f),
  (c.lift f H).range = f.range
-- Lean.Elab.Parallel
_private.Lean.Elab.Parallel.0.Std.Iterators.Types.Internal.TaskIterator.mk : {α : Type w} → List (Task α) → Std.Iterators.Types.Internal.TaskIterator α
-- Mathlib.Data.Int.Cast.Lemmas
Int.castAddHom_int : Int.castAddHom ℤ = AddMonoidHom.id ℤ
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimTargetView.mk : Option Lean.Ident → Lean.Syntax → Lean.Elab.Tactic.ElimTargetView
-- Mathlib.Topology.Homotopy.Lifting
/-- Choosing an arbitrary basepoint `e ∈ f ⁻¹' {x}` induces a bijection `f ⁻¹' {x} ≃ G`, and the
`G`-action on `f ⁻¹' {x}` corresponds to left multiplication. The monodromy action commutes
with the `G`-action, so each monodromy must corresponds must correspond to a right multiplication.
 -/
IsQuotientCoveringMap.fundamentalGroupToMulOpposite : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} →
          {G : Type u_4} →
            [inst_2 : Group G] →
              [inst_3 : MulAction G E] →
                IsQuotientCoveringMap p G → {x : X} → ↑(p ⁻¹' {x}) → FundamentalGroup X x →* Gᵐᵒᵖ
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Copy of a `BialgHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
BialgHom.copy : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] → (f : A →ₐc[R] B) → (f' : A → B) → f' = ⇑f → A →ₐc[R] B
-- Mathlib.Order.PropInstances
/-- Propositions form a bounded order.  -/
Prop.instBoundedOrder : BoundedOrder Prop
-- Mathlib.Algebra.Free
Magma.AssocQuotient.of.eq_1 : ∀ {α : Type u} [inst : Mul α], Magma.AssocQuotient.of = { toFun := Quot.mk (Magma.AssocRel α), map_mul' := ⋯ }
-- Mathlib.Topology.Category.LightProfinite.Basic
instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite : ∀ (X : FintypeCat), Finite ↑(FintypeCat.toLightProfinite.obj X).toTop
-- Mathlib.Data.Multiset.Defs
/-- `s ⊆ t` is the lift of the list subset relation. It means that any
element with nonzero multiplicity in `s` has nonzero multiplicity in `t`,
but it does not imply that the multiplicity of `a` in `s` is less or equal than in `t`;
see `s ≤ t` for this relation.  -/
Multiset.Subset : {α : Type u_1} → Multiset α → Multiset α → Prop
-- Init.Data.List.Erase
List.eraseP_map : ∀ {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {l : List β},
  List.eraseP p (List.map f l) = List.map f (List.eraseP (p ∘ f) l)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eVariationOn_Ico_eq_Icc_of_continuousWithinAt' : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {a b : α} [h : (nhdsWithin a (Set.Iio a)).NeBot],
  ContinuousWithinAt f (Set.Iic a) a → eVariationOn f (Set.Ico b a) = eVariationOn f (Set.Icc b a)
-- Std.Sat.AIG.RefVec
_private.Std.Sat.AIG.RefVec.0.Std.Sat.AIG.RefVec.countKnown.go.match_1.splitter : {α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (decl : Std.Sat.AIG.Decl α) →
      (Unit → motive Std.Sat.AIG.Decl.false) →
        ((x : Std.Sat.AIG.Decl α) → (x = Std.Sat.AIG.Decl.false → False) → motive x) → motive decl
-- Mathlib.Algebra.Category.Grp.EpiMono
CommGrpCat.forget_commGrp_preserves_epi : (CategoryTheory.forget CommGrpCat).PreservesEpimorphisms
-- Mathlib.Order.ModularLattice
/-- A generalization of the theorem that if `N` is a submodule of `M` and
`N` and `M / N` are both Artinian, then `M` is Artinian.  -/
wellFounded_lt_exact_sequence : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {β : Type u_2} {γ : Type u_3} [inst_2 : Preorder β]
  [inst_3 : Preorder γ] [h₁ : WellFoundedLT β] [h₂ : WellFoundedLT γ] (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α)
  (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂) (gi : GaloisInsertion g₂ g₁),
  (∀ (a : α), f₁ (f₂ a) = a ⊓ K) → (∀ (a : α), g₁ (g₂ a) = a ⊔ K) → WellFoundedLT α
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsMultiplicativeEpiModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.epiModSerre.IsMultiplicative
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalAddGroup.of_nhds_zero : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0) →
      (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) →
        (∀ (x₀ : G), Filter.Tendsto (fun x => x₀ + x + -x₀) (nhds 0) (nhds 0)) → IsTopologicalAddGroup G
-- Lean.Data.Lsp.Diagnostics
/-- Parameters for the [`textDocument/publishDiagnostics` notification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_publishDiagnostics).  -/
Lean.Lsp.PublishDiagnosticsParams : Type
-- Mathlib.Algebra.Polynomial.Basic
/-- **Alias** of `Polynomial.support_C_mul_X_subset`. -/
Polynomial.support_C_mul_X' : ∀ {R : Type u} [inst : Semiring R] (c : R), (Polynomial.C c * Polynomial.X).support ⊆ {1}
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
IterateAddAct.instDiscreteMeasurableSpace : ∀ {α : Type u_1} {f : α → α}, DiscreteMeasurableSpace (IterateAddAct f)
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_conj : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedCommRing 𝔸]
  [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (U A : Matrix m m 𝔸),
  IsUnit U → NormedSpace.exp (U * A * U⁻¹) = U * NormedSpace.exp A * U⁻¹
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- The bundled `R`-module giving the filtered colimit of a diagram.  -/
ModuleCat.FilteredColimits.colimit : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J (ModuleCat R) → ModuleCat R
-- Mathlib.Data.Nat.Bits
Nat.bodd_bit : ∀ (b : Bool) (n : ℕ), (Nat.bit b n).bodd = b
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.equiv_empty : ∀ {a b : ℕ}, Batteries.UnionFind.empty.Equiv a b ↔ a = b
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.mem_iff_find_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) {x : X} {n : ℕ}, x ∈ K n ↔ K.find x ≤ n
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeTrustOfNat : Lean.Options → Bool
-- Mathlib.FieldTheory.SplittingField.Construction
/-- See note [fact non-instances].  -/
Polynomial.fact_irreducible_factor : ∀ {K : Type v} [inst : Field K] (f : Polynomial K), Fact (Irreducible f.factor)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `hasLimitsOfSizeShrink.{v u} C` tries to obtain `HasLimitsOfSize.{v u} C`
from some other `HasLimitsOfSize C`.
 -/
CategoryTheory.Limits.hasLimitsOfSizeShrink : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasLimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C],
  CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.StronglyConnectedComponent.eq : ∀ {V : Type u_2} [inst : Quiver V] (a b : V),
  Quiver.StronglyConnectedComponent.mk a = Quiver.StronglyConnectedComponent.mk b ↔
    Nonempty (Quiver.Path a b) ∧ Nonempty (Quiver.Path b a)
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (self : k.Hom l),
  CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map self.base) =
    CategoryTheory.CategoryStruct.comp self.hom ((P l.fst).ι.app l.snd)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  (g : CategoryTheory.CostructuredArrow F f.left),
  ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).hom.left = g.hom
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.fix : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Cont'
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If `X` and `Y` are two Gaussian random variables such that `X` and `Y - X` are independent,
then `Y - X` is Gaussian.

This lemma is useful to prove that a process with independent increments and whose marginals
are Gaussian has Gaussian increments.  -/
ProbabilityTheory.IndepFun.hasGaussianLaw_sub_of_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {X Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P →
    ProbabilityTheory.HasGaussianLaw Y P →
      ProbabilityTheory.IndepFun X (Y - X) P → ProbabilityTheory.HasGaussianLaw (Y - X) P
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_int32 : ∀ (x : Int32), ↑x = x.toInt
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.toFullSubcategory_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : P.FullSubcategory}
  (Q : HomotopicalAlgebra.PrepathObject X.obj) (hQ : P Q.P),
  (Q.toFullSubcategory hQ).ι = CategoryTheory.ObjectProperty.homMk Q.ι
-- Init.SizeOf
String.ofByteArray.sizeOf_spec : ∀ (toByteArray : ByteArray) (isValidUTF8 : toByteArray.IsValidUTF8),
  sizeOf { toByteArray := toByteArray, isValidUTF8 := isValidUTF8 } = 1 + sizeOf toByteArray + sizeOf isValidUTF8
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.pointwise_smul_support_finite : ∀ {α : Type u₁} {β : Type u₂} {γ : Type u₃} [inst : Zero γ] [inst_1 : SMulZeroClass β γ] (f : α → β) (g : α →₀ γ),
  (Function.support fun x => f x • g x).Finite
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImport.mk.sizeOf_spec : ∀ (module : Lean.Lsp.LeanModule) (kind : Lean.Lsp.LeanImportKind),
  sizeOf { module := module, kind := kind } = 1 + sizeOf module + sizeOf kind
-- Lean.Elab.Term.TermElabM
/-- Try to synthesize metavariable using type class resolution.
This method assumes the local context and local instances of `instMVar` coincide
with the current local context and local instances.
Return `true` if the instance was synthesized successfully, and `false` if
the instance contains unassigned metavariables that are blocking the type class
resolution procedure. Throw an exception if resolution or assignment irrevocably fails.

If `extraErrorMsg?` is not none, it contains additional information that should be attached
to type class synthesis failures.
 -/
Lean.Elab.Term.synthesizeInstMVarCore : Lean.MVarId → optParam (Option ℕ) none → optParam (Option Lean.MessageData) none → Lean.Elab.TermElabM Bool
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.dvd_comp_neg_X_iff : ∀ {R : Type u} [inst : CommRing R] (p q : Polynomial R), p ∣ q.comp (-Polynomial.X) ↔ p.comp (-Polynomial.X) ∣ q
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.pow_pow : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : M} {n : ℕ}, Associated a b → Associated (a ^ n) (b ^ n)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.f'_cyclesMap'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) {Z : C}
  (h : h₂.K ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.f'
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) h) =
    CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.CategoryStruct.comp h₂.f' h)
-- Mathlib.LinearAlgebra.Dimension.Finite
rank_pos_iff_exists_ne_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M], 0 < Module.rank R M ↔ ∃ x, x ≠ 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.liftOn_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S),
  ((AddLocalization.addMonoidOf S).mk' a b).liftOn f H = f a b
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E E_1 : CategoryTheory.PreZeroHypercover X)
  (e_E : E = E_1) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g],
  E.pullbackCoverOfLeft f g = E_1.pullbackCoverOfLeft f g
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hurwitzZetaOdd.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.hurwitzZetaOdd a s = HurwitzZeta.completedHurwitzZetaOdd a s / (s + 1).Gammaℝ
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.edgeSetSumEquiv.match_1.splitter : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} →
      {H : SimpleGraph W} →
        (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) →
          (x x_1 : V ⊕ W) →
            (x_2 : (G ⊕g H).Adj x x_1) →
              ((u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h) →
                ((u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h) →
                  ((u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h) →
                    ((u : W) →
                        (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h) →
                      motive x x_1 x_2
-- Mathlib.Data.Set.Basic
Set.union_subset_union_right : ∀ {α : Type u} (s : Set α) {t₁ t₂ : Set α}, t₁ ⊆ t₂ → s ∪ t₁ ⊆ s ∪ t₂
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.le_sSup_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedGT ι] {s : Set (Colex ((i : ι) → α i))} {i : ι} {e : Colex ((i : ι) → α i)},
  e ∈ s → (∀ j > i, e j = sSup s j) → e i ≤ sSup s i
-- Batteries.Data.HashMap.Basic
Batteries.HashMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (inner : Std.HashMap α β), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_apply_eq_zero_of_mem_lcs_of_mem_center : ∀ (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] {x y : L},
  x ∈ LieModule.lowerCentralSeries R L L 1 → y ∈ LieAlgebra.center R L → ((LieModule.traceForm R L M) x) y = 0
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.equivOfIsColimit.congr_simp : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.CofanTypes F}
  (hc : CategoryTheory.Functor.CoconeTypes.IsColimit c),
  CategoryTheory.Limits.CofanTypes.equivOfIsColimit hc = CategoryTheory.Limits.CofanTypes.equivOfIsColimit hc
-- Mathlib.FieldTheory.SeparableClosure
/-- If `E` and `K` are isomorphic as `F`-algebras, then they have the same finite
inseparable degree over `F`.  -/
Field.finInsepDegree_eq_of_equiv : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E ≃ₐ[F] K), Field.finInsepDegree F E = Field.finInsepDegree F K
-- Mathlib.Data.Bool.Basic
Bool.of_decide_true : ∀ {p : Prop} [inst : Decidable p], decide p = true → p
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π_assoc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] [inst_4 : CategoryTheory.Limits.HasLimit F]
  [inst_5 : CategoryTheory.Limits.HasLimit F'] (i : C) {Z : H} (h : F.obj i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F'.limitIsoOfIsRightKanExtension α).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F i) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F' (L.obj i))
      (CategoryTheory.CategoryStruct.comp (α.app i) h)
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.unknownErrorCode.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.unknownErrorCode = 1
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.HasCardinalFilteredGenerator.exists_small_generator : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.HasCardinalFilteredGenerator C κ],
  ∃ P, ∃ (_ : CategoryTheory.ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.isoOfHom_hom : ∀ {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) [inst_2 : L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f),
  (CategoryTheory.Localization.isoOfHom L W f hf).hom = L.map f
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.inf_rng : ∀ {α : Type ua} {β : Type ub} {f : α → β} {u₁ : UniformSpace α} {u₂ u₃ : UniformSpace β},
  UniformContinuous f → UniformContinuous f → UniformContinuous f
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.sections.match_1.eq_1 : ∀ {α : Type u_1} (motive : List (List α) → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (l : List α) → (L : List (List α)) → motive (l :: L)),
  (match [] with
    | [] => h_1 ()
    | l :: L => h_2 l L) =
    h_1 ()
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_add : ∀ {R : Type u_1} [inst : Semiring R] {a b : R}, SkewPolynomial.C (a + b) = SkewPolynomial.C a + SkewPolynomial.C b
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State : Type
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k k' : α}, (k == k') = true → m.getKey? k = m.getKey? k'
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.coe_inv : ∀ {α : Type u} [inst : Inv α] (a : α), ↑a⁻¹ = (↑a)⁻¹
-- Init.Core
EmptyCollection.mk : {α : Type u} → α → EmptyCollection α
-- Mathlib.Algebra.Tropical.Basic
Tropical.min_eq_add : ∀ {R : Type u} [inst : LinearOrder R], min = fun x1 x2 => x1 + x2
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.cached? : Bool → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.range_eq_map_top : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B] [inst_7 : StarRing B]
  [inst_8 : StarModule R A] [inst_9 : StarModule R B] (φ : A →⋆ₐ[R] B), φ.range = StarSubalgebra.map φ ⊤
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injectiveDimension_ge_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ),
  ↑n ≤ CategoryTheory.injectiveDimension X ↔ ¬CategoryTheory.HasInjectiveDimensionLT X n
-- Mathlib.Algebra.Group.Defs
/-- An abbreviation for `nsmulRec` with an additional typeclass assumptions on associativity
so that we can use `@[csimp]` to replace it with an implementation by repeated doubling in compiled
code as an automatic parameter.  -/
nsmulRecAuto : {M : Type u_2} → [AddSemigroup M] → [Zero M] → ℕ → M → M
-- Mathlib.Data.Erased
Erased.pure_def : ∀ {α : Type u_1}, pure = Erased.mk
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a right homology data `h` of a short complex `S` is preserved by a functor `F`,
this is the induced right homology data `h.map F` for the short complex `S.map F`.  -/
CategoryTheory.ShortComplex.RightHomologyData.map : {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.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S : CategoryTheory.ShortComplex C} →
              (h : S.RightHomologyData) →
                (F : CategoryTheory.Functor C D) →
                  [inst_4 : F.PreservesZeroMorphisms] → [h.IsPreservedBy F] → (S.map F).RightHomologyData
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.instIsStrictOrderedRingLex : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : Ring R]
  [inst_3 : AddCommMonoid Γ] [inst_4 : IsOrderedCancelAddMonoid Γ] [IsStrictOrderedRing R],
  IsStrictOrderedRing (Lex (HahnSeries Γ R))