mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Defs.Unbundled
comm : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] {a b : α}, r a b ↔ r b a
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A product can be partitioned into a product of products, each equivalent under a setoid.  -/
Finset.prod_partition : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} (R : Setoid ι)
  [inst_1 : DecidableRel ⇑R], ∏ x ∈ s, f x = ∏ xbar ∈ Finset.image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = xbar, f y
-- Mathlib.Analysis.Complex.Positivity
/-- A function that is holomorphic on the open disk around `c` with radius `r` and whose iterated
derivatives at `c` are all nonnegative real has nonnegative real values on `c + [0,r)`.  -/
DifferentiableOn.nonneg_of_iteratedDeriv_nonneg : ∀ {f : ℂ → ℂ} {c : ℂ} {r : ℝ},
  DifferentiableOn ℂ f (Metric.ball c r) →
    (∀ (n : ℕ), 0 ≤ iteratedDeriv n f c) → ∀ ⦃z : ℂ⦄, c ≤ z → z ∈ Metric.ball c r → 0 ≤ f z
-- Lean.Meta.Tactic.Grind.Extension
/-- Constraints of the form `not_value x` and `not_strict_value x`.
They are the negations of `is_value x` and `is_strict_value x`.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.notValue : ℕ → Bool → Lean.Meta.Grind.EMatchTheoremConstraint
-- Init.Data.Option.Lemmas
Option.elim_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
  (H : ∀ (a : α), o = some a → p a) (g : γ) (g' : β → γ),
  (Option.pmap f o H).elim g g' = o.pelim g fun a h => g' (f a ⋯)
-- Lean.Parser.Do
Lean.Parser.Term.getDoElems : Lean.DoSeq → Array Lean.DoElem
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The range of a normal operator is pairwise orthogonal to its kernel.

This is a weaker version of `LinearMap.IsSymmetric.orthogonal_range`
but with stronger type class assumptions (i.e., `CompleteSpace`).  -/
ContinuousLinearMap.IsStarNormal.orthogonal_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E], IsStarNormal T → (↑T).rangeᗮ = (↑T).ker
-- Mathlib.Data.Vector.Defs
/-- `List.Vector α n` is the type of lists of length `n` with elements of type `α`.

Note that there is also `Vector α n` in the root namespace,
which is the type of *arrays* of length `n` with elements of type `α`.

Typically, if you are doing programming or verification, you will primarily use `Vector α n`,
and if you are doing mathematics, you may want to use `List.Vector α n` instead.
 -/
List.Vector : Type u → ℕ → Type (max 0 u)
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.go : Lean.FileMap → String.Pos.Raw → Lean.Position → Lean.Syntax → ℕ → Option String.Pos.Raw → Bool
-- Mathlib.Data.Sigma.Order
Sigma.Lex.denselyOrdered : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [DenselyOrdered ι] [∀ (i : ι), Nonempty (α i)]
  [inst_3 : (i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)], DenselyOrdered (Σₗ (i : ι), α i)
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_two : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 2 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁₂ f₃ f₄).obj 2)
-- Init.Data.Bool
Bool.decide_or : ∀ (p q : Prop) [dpq : Decidable (p ∨ q)] [dp : Decidable p] [dq : Decidable q], decide (p ∨ q) = (decide p || decide q)
-- Init.Data.Nat.Gcd
Nat.gcd_one_right : ∀ (n : ℕ), n.gcd 1 = 1
-- Mathlib.RepresentationTheory.Equiv
/-- Equiv between representations induced by linear equiv between `(G →₀ k) ⊗[k] (α →₀ k)` and
`α →₀ G →₀ k`.  -/
Representation.leftRegularTensorTrivialIsoFree : {G : Type v} →
  [inst : Monoid G] →
    {k : Type u} →
      [inst_1 : CommSemiring k] →
        (α : Type w') →
          ((Representation.leftRegular k G).tprod (Representation.trivial k G (MonoidAlgebra k α))).Equiv
            (Representation.free k G α)
-- Mathlib.Analysis.Distribution.Support
TemperedDistribution.isVanishingOn_delta : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E),
  Distribution.IsVanishingOn ⇑(TemperedDistribution.delta x) {x}ᶜ
-- Init.Simproc
/-- A builtin defeq simplification procedure declaration.
 -/
Lean.Parser.«command_Builtin_dsimproc_decl_(_):=_» : Lean.ParserDescr
-- Mathlib.GroupTheory.Divisible
Function.Surjective.rootableBy.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {α : Type u_3} [inst : Zero α] [inst_1 : Monoid A] [inst_2 : Monoid B]
  [inst_3 : Pow A α] [inst_4 : Pow B α] [inst_5 : RootableBy A α] (f : A → B) (hf : Function.Surjective f)
  (hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n),
  Function.Surjective.rootableBy f hf hpow = rootableByOfPowLeftSurj B α ⋯
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.isoApp_inv : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  (f : X ≅ Y) (i : I), (CategoryTheory.Pi.isoApp f i).inv = f.inv i
-- Mathlib.Analysis.Analytic.Basic
AnalyticOn.comp_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  AnalyticOn 𝕜 f s → ∀ (y : E), AnalyticOn 𝕜 (fun z => f (z - y)) (s + {y})
-- Std.Http.Data.Body.Full
/-- Receives the body data. Returns the full byte array on the first call as a single chunk,
then `none` on all subsequent calls.
 -/
Std.Http.Body.Full.recv : Std.Http.Body.Full → Std.Async.Async (Option Std.Http.Chunk)
-- Mathlib.Algebra.Order.Pi
/-- The product of a family of canonically ordered monoids is a canonically ordered monoid.  -/
Pi.instCanonicallyOrderedMulForall : ∀ {ι : Type u_6} {Z : ι → Type u_7} [inst : (i : ι) → Monoid (Z i)] [inst_1 : (i : ι) → PartialOrder (Z i)]
  [∀ (i : ι), CanonicallyOrderedMul (Z i)], CanonicallyOrderedMul ((i : ι) → Z i)
-- Lean.Meta.HaveTelescope
/-- Information about a `have` telescope.
Created by `getHaveTelescopeInfo` and used in `simpHaveTelescope`.

The data is used to avoid applying `Expr.abstract` more than once on any given subexpression
when constructing terms and proofs during simplification. Abstraction is linear in the size `t` of a term,
and so in a depth-`n` telescope it is `O(nt)`, quadratic in `n`, since `n ≤ t`.
For example, given `have x₁ := v₁; ...; have xₙ := vₙ; b` and `h : b = b'`, we need to construct
```lean
have_body_congr (fun x₁ => ... have_body_congr (fun xₙ => h)))
```
We apply `Expr.abstract` to `h` *once* and then build the term, rather than
using `mkLambdaFVars #[fvarᵢ] pfᵢ` at each step.

As an additional optimization, we save the fvar-instantiated terms calculated by `getHaveTelescopeInfo`
so that we don't have to compute them again. This is only saving a constant factor.

It is also used for computing used `have`s in `computeFixedUsed`.
In `have x₁ := v; have x₂ := x₁; ⋯; have xₙ := xₙ₋₁; b`, if `xₙ` is unused in `b`, then all the
`have`s are unused. Without a global computation of used `have`s, the proof term would be quadratic
in the number of `have`s (with `n` iterations of `simp`). Knowing which `have`s are transitively
unused lets the proof term be linear in size.
 -/
Lean.Meta.HaveTelescopeInfo : Type
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.simpDIte : Lean.Meta.Simp.Simproc
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanImportClosureParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanImportClosureParams
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesColimitIso_inv_comp_desc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G]
  [inst_4 : CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F) {Z : D} (h : G.obj t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.desc F t)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone t)) h
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.cast_toZModPow : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (m n : ℕ),
  m ≤ n → ∀ (x : ℤ_[p]), ((PadicInt.toZModPow n) x).cast = (PadicInt.toZModPow m) x
-- Mathlib.NumberTheory.Padics.Hensel
/-- Given `z : ℤ_[p]` satisfying `ih n z`, construct `z' : ℤ_[p]` satisfying `ih (n+1) z'`. We need
the hypothesis `ih n z`, since otherwise `z'` is not necessarily an integer.  -/
_private.Mathlib.NumberTheory.Padics.Hensel.0.ih_n : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra R ℤ_[p]] →
          {F : Polynomial R} →
            {a : ℤ_[p]} →
              ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
                {n : ℕ} → {z : ℤ_[p]} → ih_gen✝ n z → { z' // ih_gen✝ (n + 1) z' }
-- Mathlib.CategoryTheory.Category.TwoP
/-- The underlying type of a two-pointed type.  -/
TwoP.X : TwoP → Type u
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.alterKey_append_of_containsKey_right_eq_false : ∀ {α : Type u} [inst : BEq α] {β : Type v} {a : α} {f : Option β → Option β} {l l' : List ((_ : α) × β)},
  Std.Internal.List.containsKey a l' = false →
    Std.Internal.List.Const.alterKey a f (l ++ l') = Std.Internal.List.Const.alterKey a f l ++ l'
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.toFreeAddGroup.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : IsFreeAddGroup G],
  IsFreeAddGroup.toFreeAddGroup G = (IsFreeAddGroup.addEquiv G).symm
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β],
  SupBotHom.instFunLike = { coe := fun f => f.toFun, coe_injective := ⋯ }
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.coe_bracket_of_module : ∀ (M : Type w) [inst : AddCommGroup M] {R : Type u_1} {L : Type u_2} [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] (I : LieIdeal R L) [inst_4 : LieRingModule L M] (x : ↥I) (m : M), ⁅x, m⁆ = ⁅↑x, m⁆
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.mk.inj : ∀ {keys : Array Lean.Meta.SimpTheoremKey} {levelParams : Array Lean.Name} {proof : Lean.Expr} {priority : ℕ}
  {post perm : Bool} {origin : Lean.Meta.Origin} {rfl backwardRfl : Bool} {keys_1 : Array Lean.Meta.SimpTheoremKey}
  {levelParams_1 : Array Lean.Name} {proof_1 : Lean.Expr} {priority_1 : ℕ} {post_1 perm_1 : Bool}
  {origin_1 : Lean.Meta.Origin} {rfl_1 backwardRfl_1 : Bool},
  { keys := keys, levelParams := levelParams, proof := proof, priority := priority, post := post, perm := perm,
        origin := origin, rfl := rfl, backwardRfl := backwardRfl } =
      { keys := keys_1, levelParams := levelParams_1, proof := proof_1, priority := priority_1, post := post_1,
        perm := perm_1, origin := origin_1, rfl := rfl_1, backwardRfl := backwardRfl_1 } →
    keys = keys_1 ∧
      levelParams = levelParams_1 ∧
        proof = proof_1 ∧
          priority = priority_1 ∧
            post = post_1 ∧ perm = perm_1 ∧ origin = origin_1 ∧ rfl = rfl_1 ∧ backwardRfl = backwardRfl_1
-- Mathlib.ModelTheory.Definability
/-- A 2-dimensional version of `Definable`, for `Set (M × M)`.  -/
Set.Definable₂ : {M : Type w} → Set M → (L : FirstOrder.Language) → [L.Structure M] → Set (M × M) → Prop
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.map_mrange : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (g : N →* P) (f : M →* N), Submonoid.map g (MonoidHom.mrange f) = MonoidHom.mrange (g.comp f)
-- Mathlib.Data.Set.Function
Set.InjOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g : β → γ},
  Set.InjOn g t → Set.InjOn f s → Set.MapsTo f s t → Set.InjOn (g ∘ f) s
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.lift : ∀ {κ : Cardinal.{v}}, κ.IsRegular → (Cardinal.lift.{u, v} κ).IsRegular
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.nondegenerate_of_det_ne_zero : ∀ {R : Type u_1} {M₁ : Type u_6} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [IsDomain R] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] (b : Module.Basis m R M₁) {B : M₁ →ₗ[R] M₁ →ₗ[R] R},
  ((LinearMap.toMatrix₂ b b) B).det ≠ 0 → B.Nondegenerate
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- Auxiliary definition for `colimitCoconeIsColimit`.  -/
SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J SemiRingCat} →
      [inst_1 : CategoryTheory.IsFiltered J] →
        (t : CategoryTheory.Limits.Cocone F) → ↑(SemiRingCat.FilteredColimits.R F) →+ ↑t.pt
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.restrictScalars_adjoin : ∀ (F : Type u_4) [inst : CommSemiring F] {E : Type u_5} [inst_1 : CommSemiring E] [inst_2 : Algebra F E]
  (K : Subalgebra F E) (S : Set E), Subalgebra.restrictScalars F (Algebra.adjoin (↥K) S) = Algebra.adjoin F (↑K ∪ S)
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueProds.of_mulOpposite : ∀ {G : Type u} [inst : Mul G], TwoUniqueProds Gᵐᵒᵖ → TwoUniqueProds G
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns `true`, if there is an entry `declName ↦ prio` in `s`.
Recall that symbols not in `s` are assumed to have default priority.
 -/
Lean.Meta.Grind.SymbolPriorities.contains : Lean.Meta.Grind.SymbolPriorities → Lean.Name → Bool
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instSetLike : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → SetLike (ClosedSubmodule R M) M
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.edge_firstDart : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil), (p.firstDart hp).edge = s(v, p.snd)
-- Mathlib.CategoryTheory.Join.Basic
/-- A situational lemma to help putting identities in the form `(inclLeft _ _).map _` when using
`homInduction`.  -/
CategoryTheory.Join.id_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (c : C),
  CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left c) =
    (CategoryTheory.Join.inclLeft C D).map (CategoryTheory.CategoryStruct.id c)
-- Mathlib.Analysis.Normed.Ring.Basic
one_le_norm_one : ∀ (β : Type u_5) [inst : NormedRing β] [Nontrivial β], 1 ≤ ‖1‖
-- Mathlib.Algebra.Group.Defs
/-- The fundamental power operation in a group. `zpowRec n a = a*a*...*a` n times, for integer `n`.
Use instead `a ^ n`, which has better definitional behavior.  -/
zpowRec : {G : Type u_1} → [inst : One G] → [inst_1 : Mul G] → [Inv G] → optParam (ℕ → G → G) npowRec → ℤ → G → G
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₂_inv_comp_iCycles_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 2 → G) →₀ ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).inv
      (CategoryTheory.CategoryStruct.comp (groupHomology.iCycles A 2) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.i
        (groupHomology.chainsIso₂ A).inv)
      h
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
/-- **Alias** of `cfcₙHom_mem_elemental`. -/
cfcₙHom_apply_mem_elemental : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousConstSMul 𝕜 A] [inst_8 : StarModule 𝕜 A] [inst_9 : IsTopologicalRing A]
  [inst_10 : ContinuousStar A] [inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] {a : A} (ha : p a)
  (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜), (cfcₙHom ha) f ∈ NonUnitalStarAlgebra.elemental 𝕜 a
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instSMulInt : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [AddSubgroupClass σ A] → {𝒜 : ι → σ} → (x : Submonoid A) → SMul ℤ (HomogeneousLocalization 𝒜 x)
-- Batteries.Data.ByteSlice
/-- Returns the subslice obtained by removing the last element.  -/
ByteSlice.pop : ByteSlice → ByteSlice
-- Mathlib.Algebra.Order.Ring.Defs
one_sub_le_one_sub_mul_one_add : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {a b c : R},
  b + b * c ≤ a + c → 1 - a ≤ (1 - b) * (1 + c)
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lowerCentralSeries_eq_bot_iff_lcs_eq_bot : ∀ {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] (k : ℕ) (N : LieSubmodule R L M)
  [LieModule R L M], LieModule.lowerCentralSeries R L (↥N) k = ⊥ ↔ LieSubmodule.lcs k N = ⊥
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack_inj_of_valid : ∀ {spec : Float.Model.Format} {b b' : BitVec spec.numBits},
  spec.Valid b →
    spec.Valid b' →
      autoParam (2 ≤ spec.exponentBits) Float.Model.UnpackedFloat.unpack_inj_of_valid._auto_1 →
        (Float.Model.UnpackedFloat.unpack spec b = Float.Model.UnpackedFloat.unpack spec b' ↔ b = b')
-- Mathlib.Data.Matrix.Basic
Matrix.transposeLinearEquiv_apply : ∀ (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α] (a : Matrix m n α),
  (Matrix.transposeLinearEquiv m n R α) a = (Matrix.transposeAddEquiv m n α).toFun a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.union_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ m₄ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∪ m₂).Equiv (m₃ ∪ m₄)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rcc_eq_none : ∀ {m n : ℤ} {i : ℕ}, (n + 1 - m).toNat ≤ i → (m...=n).toList[i]? = none
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_mono' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal},
  MeasurableSet s → (∀ x ∈ s, f x ≤ g x) → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.List.range_zero' : ∀ {n : ℕ}, Mathlib.Meta.NormNum.IsNat n 0 → List.range n = []
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearEquiv.equivOfRightInverse.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  [inst_7 : IsTopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ f₂_1 : M₂ →L[R] M) (e_f₂ : f₂ = f₂_1)
  (h : Function.RightInverse ⇑f₂ ⇑f₁),
  ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h = ContinuousLinearEquiv.equivOfRightInverse f₁ f₂_1 ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint8.sizeOf_spec : ∀ (val : UInt8), sizeOf (Lean.Compiler.LCNF.LitValue.uint8 val) = 1 + sizeOf val
-- Lean.PrettyPrinter.Delaborator.Metavariable
/-- Follows a chain of delayed assignments to find the pending metavariable.
 -/
Lean.PrettyPrinter.Delaborator.getDelayedMVarIdPending : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- A coloring of a graph `G` is a homomorphism from it to the mapped graph.
This is `Hom.map` spelled using colorings. The mapped graph `G.map f` can be thought of as taking
the original graph `G` and considering every color class (independent set) as a single vertex.  -/
SimpleGraph.Coloring.homMap : {V : Type u} → {G : SimpleGraph V} → {α : Type u_4} → (f : G.Coloring α) → G →g SimpleGraph.map (⇑f) G
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
/-- The bijection `(M ⟶ N) ≃ (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))`.  -/
CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {S : C} →
        {M N : ↑(F.obj { as := Opposite.op S })} →
          (M ⟶ N) ≃ (F.presheafHom M N).obj (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S)))
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.base.sizeOf_spec : ∀ (m : Aesop.BaseRuleSetMember), sizeOf (Aesop.GlobalRuleSetMember.base m) = 1 + sizeOf m
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.map_subtype_coe_factors' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  Multiset.map Subtype.val (Associates.factors' a) = Multiset.map Associates.mk (UniqueFactorizationMonoid.factors a)
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_coeff : ∀ (ctx : Int.Internal.Linear.Context) (p p' : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.eq_coeff_cert p p' k = true →
    Int.Internal.Linear.Poly.denote' ctx p = 0 → Int.Internal.Linear.Poly.denote' ctx p' = 0
-- Mathlib.Analysis.Seminorm
/-- Balls containing the origin are absorbent.  -/
absorbent_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ} {x : E}, ‖x‖ < r → Absorbent 𝕜 (Metric.ball x r)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_differentiableAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E},
  DifferentiableAt 𝕜 (f ∘ ⇑iso) x ↔ DifferentiableAt 𝕜 f (iso x)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- A functor which maps objects to objects satisfying a certain property induces a lift through
the full subcategory of objects satisfying that property.  -/
CategoryTheory.ObjectProperty.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        (P : CategoryTheory.ObjectProperty D) →
          (F : CategoryTheory.Functor C D) → (∀ (X : C), P (F.obj X)) → CategoryTheory.Functor C P.FullSubcategory
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- a retraction of `S.f`  -/
CategoryTheory.ShortComplex.Splitting.r : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S : CategoryTheory.ShortComplex C} → S.Splitting → (S.X₂ ⟶ S.X₁)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPower.beq.eq_2 : ∀ (x x_1 : Lean.Grind.CommRing.Power),
  (∀ (a : Lean.Grind.CommRing.Var) (a_1 : ℕ) (b : Lean.Grind.CommRing.Var) (b_1 : ℕ),
      x = { x := a, k := a_1 } → x_1 = { x := b, k := b_1 } → False) →
    Lean.Grind.CommRing.instBEqPower.beq x x_1 = false