mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Main
Lean.Elab.DelabTermInfo.format : Lean.Elab.ContextInfo → Lean.Elab.DelabTermInfo → IO Std.Format
-- Init.Data.Option.Lemmas
Option.pmap_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), o = some a → p a},
  Option.pmap f o h = none ↔ o = none
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_addNat_Ioi : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.image (fun x => x.addNat m) (Finset.Ioi i) = Finset.Ioi (i.addNat m)
-- Mathlib.Data.Set.Pairwise.Lattice
Set.biUnion_sdiff_biUnion_eq : ∀ {α : Type u_1} {ι : Type u_2} {s t : Set ι} {f : ι → Set α},
  (s ∪ t).PairwiseDisjoint f → (⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.le_extensionProduct_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {Q : CategoryTheory.ObjectProperty C} [P.ContainsZero], Q ≤ P.extensionProduct Q
-- Mathlib.RingTheory.RingHom.Injective
RingHom.injective_respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Injective ⇑f
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAtFilter_add_const_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] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)} (c : F), HasFDerivAtFilter (fun x => f x + c) f' L ↔ HasFDerivAtFilter f f' L
-- Mathlib.CategoryTheory.Monoidal.Tor
/-- An alternative definition of `Tor`, where we left-derive in the first factor instead.  -/
CategoryTheory.Tor' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Abelian C] →
        [CategoryTheory.MonoidalPreadditive C] →
          [CategoryTheory.HasProjectiveResolutions C] → ℕ → CategoryTheory.Functor C (CategoryTheory.Functor C C)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure_eq_self : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [H.Normal], AddSubgroup.normalClosure ↑H = H
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.uniqueGalXSubC : {F : Type u_1} → [inst : Field F] → (x : F) → Unique (Polynomial.X - Polynomial.C x).Gal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_nat_mul_two_pi_sub : ∀ (x : ℝ) (n : ℕ), Real.sin (↑n * (2 * Real.pi) - x) = -Real.sin x
-- Std.Http.Protocol.H1
/-- Internal recursive helper for `pullBody`.

Keeps advancing body parsing until either a chunk is produced or no immediate
progress can be made.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.pullNextChunk : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.instCoeSortType : CoeSort UniformSpaceCat (Type u_1)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_of_mul_lt_of_nonneg_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α],
  a * b < c → d ≤ b → 0 ≤ a → a * d < c
-- Mathlib.Data.Finset.Insert
List.toFinset_nonempty_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.toFinset.Nonempty ↔ l ≠ []
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.remainingBytes.match_1.splitter : (motive : String.Legacy.Iterator → Sort u_1) →
  (x : String.Legacy.Iterator) → ((s : String) → (i : String.Pos.Raw) → motive { s := s, i := i }) → motive x
-- Mathlib.Data.Finset.Sups
Finset.diffs_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α},
  s.diffs t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Topology.Inseparable
/-- Lift a map `f : X → α` such that `Inseparable x y → f x = f y` to a map
`SeparationQuotient X → α`.  -/
SeparationQuotient.lift : {X : Type u_1} →
  {α : Type u_4} →
    [inst : TopologicalSpace X] → (f : X → α) → (∀ (x y : X), Inseparable x y → f x = f y) → SeparationQuotient X → α
-- Mathlib.RingTheory.Polynomial.GaussLemma
integralClosure.mem_lifts_of_monic_of_dvd_map : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] {f : Polynomial R},
  f.Monic →
    ∀ {g : Polynomial K},
      g.Monic → g ∣ Polynomial.map (algebraMap R K) f → g ∈ Polynomial.lifts (algebraMap (↥(integralClosure R K)) K)
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.inverse_apply : ∀ {A : Type u_10} {B : Type u_11} [inst : Monoid A] [inst_1 : Monoid B] (f : A →* B) (g : B → A)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : B), (f.inverse g h₁ h₂) a = g a
-- Mathlib.Tactic.GCongr.Core
/-- The discharger for side goals.  -/
Mathlib.Tactic.GCongr.Context.sideGoalDischarger : Mathlib.Tactic.GCongr.Context → Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_sub_intCast' : ∀ {y : ℝ} {n : ℤ}, y - ↑n ≠ 0 → ∀ (x : NNReal), x ^ (y - ↑n) = x ^ y / x ^ n
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.edges_dropUntil_subset_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).edges ⊆ p.edges
-- Lean.Parser.Extension
Lean.Parser.instCoeForallParserForallParserAliasValue : Coe (Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser) Lean.Parser.ParserAliasValue
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_erase_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α}, (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.size ≤ t.size
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The space of `L`-Lipschitz functions `α : Icc tmin tmax → E`  -/
ODE.FunSpace : {E : Type u_1} → [NormedAddCommGroup E] → {tmin tmax : ℝ} → ↑(Set.Icc tmin tmax) → E → NNReal → NNReal → Type u_1
-- Mathlib.Algebra.Group.Shrink
Shrink.instInv.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Inv α], Shrink.instInv = (equivShrink α).symm.Inv
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R) (p : Fin n → Polynomial R),
  (∀ (i : Fin n), (p i).natDegree ≤ ↑i) →
    (Matrix.of fun i j => Polynomial.eval (v i) (p j)) = Matrix.vandermonde v * Matrix.of fun i j => (p j).coeff ↑i
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsPathGraph3Compl.ne_snd : ∀ {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α}, G.IsPathGraph3Compl v w₁ w₂ → v ≠ w₂
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_le_iff_le_coe : ∀ {r : ℝ} {p : NNReal}, r.toNNReal ≤ p ↔ r ≤ ↑p
-- Mathlib.Algebra.Quaternion
Quaternion.re_sub : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a - b).re = a.re - b.re
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.getElem_toList_eq : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.succMany? i r.lower).get ⋯
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.elim.match_3.eq_1 : ∀ {α : Type u_1} {n : ℕ} (motive : List.Vector α n → Sort u_2) (l : List α) (h : l.length = n)
  (h_1 : (l : List α) → (h : l.length = n) → motive ⟨l, h⟩),
  (match ⟨l, h⟩ with
    | ⟨l, h⟩ => h_1 l h) =
    h_1 l h
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instT25Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T25Space M], T25Space Mᵈᵐᵃ
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.map_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U : CategoryTheory.Over X},
  ((CategoryTheory.Over.map f).obj U).hom = CategoryTheory.CategoryStruct.comp U.hom f
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
_private.Mathlib.MeasureTheory.Function.LpSpace.Basic.0.MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {ν : MeasureTheory.Measure α} {c c_1 : ENNReal}
  (e_c : c = c_1) (hc : c ≠ ⊤) (h : μ ≤ c • ν),
  MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ✝ hc h = MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ✝ ⋯ ⋯
-- Mathlib.Topology.CantorBendixson
/-- Taking the perfect kernel of a closed set is idempotent.  -/
CantorBendixson.perfectKernel_idem : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsClosed s → CantorBendixson.perfectKernel (CantorBendixson.perfectKernel s) = CantorBendixson.perfectKernel s
-- Mathlib.Order.Category.BddOrd
BddOrd.hom_ofHom : ∀ {X Y : Type u} [inst : PartialOrder X] [inst_1 : BoundedOrder X] [inst_2 : PartialOrder Y] [inst_3 : BoundedOrder Y]
  (f : BoundedOrderHom X Y), BddOrd.Hom.hom (BddOrd.ofHom f) = f
-- Std.Data.Internal.List.Associative
/-- Returns the largest key in an associative list.  -/
Std.Internal.List.maxKey? : {α : Type u} → {β : α → Type v} → [Ord α] → List ((a : α) × β a) → Option α
-- Mathlib.NumberTheory.ZetaValues
bernoulliFourierCoeff_eq : ∀ {k : ℕ}, k ≠ 0 → ∀ (n : ℤ), bernoulliFourierCoeff k n = -↑k.factorial / (2 * ↑Real.pi * Complex.I * ↑n) ^ k
-- Lean.Util.FindLevelMVar
Lean.FindLevelMVar.visit : (Lean.LMVarId → Bool) → Lean.Expr → Lean.FindLevelMVar.Visitor
-- Lean.DocString.Links
/-- Rewrites links from the internal Lean manual syntax to the correct URL. This rewriting is an
overapproximation: any parentheses containing the internal syntax of a Lean manual URL is rewritten.

The internal syntax is the URL scheme `lean-manual` followed by the path `/KIND/MORE...`, where
`KIND` is a kind of content being linked to. Presently, the only valid kind is `section`, and it
requires that the remainder of the path consists of one element, which is a section or part identifier.

The correct URL is based on a manual root URL, which is determined by the `LEAN_MANUAL_ROOT`
environment variable. If this environment variable is not set, a manual root provided when Lean was
built is used (typically this is the version corresponding to the current release). If no such root
is available, the latest version of the manual is used.
 -/
Lean.rewriteManualLinksCore : String → Id (Array (Lean.Syntax.Range × String) × String)
-- Mathlib.Order.Partition.Basic
/-- A constructor for `Partition s` that removes `⊥` from the set of parts.  -/
Partition.removeBot : {α : Type u_1} → {s : α} → [inst : CompleteLattice α] → (P : Set α) → sSupIndep P → sSup P = s → Partition s
-- Mathlib.Topology.Instances.Sign
continuousAt_sign_of_pos : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : TopologicalSpace α] [inst_2 : PartialOrder α] [inst_3 : DecidableLT α]
  [OrderTopology α] {a : α}, 0 < a → ContinuousAt (⇑SignType.sign) a
-- Init.Core
/-- `inline (f x)` is an indication to the compiler to inline the definition of `f`
at the application site itself (by comparison to the `@[inline]` attribute,
which applies to all applications of the function).
 -/
inline : {α : Sort u} → α → α
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.leadingCoeff_mono : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal (Polynomial R)}, I ≤ J → I.leadingCoeff ≤ J.leadingCoeff
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprodEquiv_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module S M₃] [inst_9 : SMulCommClass R S M₃]
  (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)), (LinearMap.coprodEquiv S) f = f.1.coprod f.2
-- Mathlib.Analysis.Matrix.Order
/-- A positive semi-definite matrix `M` induces an inner product on `Matrix n n 𝕜`:
`⟪x, y⟫ = (y * M * xᴴ).trace`.  -/
Matrix.toMatrixInnerProductSpace : {𝕜 : Type u_1} →
  {n : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : Fintype n] → (M : Matrix n n 𝕜) → (hM : M.PosSemidef) → InnerProductSpace 𝕜 (Matrix n n 𝕜)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.cons_reverseAux : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (q : G.Walk w x) (h : G.Adj w u),
  (SimpleGraph.Walk.cons h p).reverseAux q = p.reverseAux (SimpleGraph.Walk.cons ⋯ q)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.minKeyD.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : α),
  x.minKeyD x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => k
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => l.minKeyD fallback
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_mapAccumr₂_left_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {φ : Type u_8} {n : ℕ} {s₁ : σ₁}
  {s₂ : σ₂} (xs : List.Vector α n) (ys : List.Vector β n) (f₁ : γ → α → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ),
  List.Vector.mapAccumr₂ f₁ (List.Vector.mapAccumr₂ f₂ xs ys s₂).2 xs s₁ =
    have m :=
      List.Vector.mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            have r₂ := f₂ x y s₂;
            have r₁ := f₁ r₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)
-- Mathlib.Topology.NhdsSet
Filter.EventuallyEq.self_of_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {Y : Type u_4} {f g : X → Y},
  f =ᶠ[nhdsSet s] g → Set.EqOn f g s
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- The gluing of two good cylinders.  -/
HomotopicalAlgebra.Cylinder.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {A : C} →
        [HomotopicalAlgebra.IsCofibrant A] →
          HomotopicalAlgebra.Cylinder A →
            (P' : HomotopicalAlgebra.Cylinder A) → [P'.IsGood] → HomotopicalAlgebra.Cylinder A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  t.WF → (Std.DTreeMap.Raw.filterMap f t).contains k = true → t.contains k = true
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  (∀ (f g : CategoryTheory.Arrow C) (x : f ≅ g), P f.hom → P g.hom) → P.RespectsIso
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_eq_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] {f : M →ₗ[R] M'}
  [inst_5 : IsLocalizedModule S f] {m : M} (s : ↥S), IsLocalizedModule.mk' f m s = 0 ↔ f m = 0
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
AlgebraicGeometry.Scheme.GlueData.oneHypercover_f : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J), D.oneHypercover.f i = D.ι i
-- Mathlib.Topology.MetricSpace.PiNat
/-- If the functions `f i : X → Y i` separate points of `X`, then `X` can be embedded into
`∀ i, Y i`.  -/
Metric.PiNatEmbed.metricSpace : {ι : Type u_2} →
  {X : Type u_3} →
    {Y : ι → Type u_4} →
      {f : (i : ι) → X → Y i} →
        [Encodable ι] →
          [(i : ι) → MetricSpace (Y i)] →
            (Pairwise fun x y => ∃ i, f i x ≠ f i y) → MetricSpace (Metric.PiNatEmbed X Y f)
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (g : E → ℂ) (f : TemperedDistribution E F),
  (TemperedDistribution.fourierMultiplierCLM F g) f =
    FourierTransformInv.fourierInv ((TemperedDistribution.smulLeftCLM F g) (FourierTransform.fourier f))
-- Init.Data.BitVec.Lemmas
BitVec.mul_add : ∀ {w : ℕ} {x y z : BitVec w}, x * (y + z) = x * y + x * z
-- Init.Grind.Config
Lean.Grind.OrderConfig.mk.inj : ∀ {toNoopConfig toNoopConfig_1 : Lean.Grind.NoopConfig},
  { toNoopConfig := toNoopConfig } = { toNoopConfig := toNoopConfig_1 } → toNoopConfig = toNoopConfig_1
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
AlgCat.Hom.Simps.hom : {R : Type u} → [inst : CommRing R] → (A B : AlgCat R) → A.Hom B → ↑A →ₐ[R] ↑B
-- Mathlib.Algebra.Lie.Nilpotent
/-- Given an ideal `I` of a Lie algebra `L`, the lower central series of `L ⧸ I` is the same
whether we regard `L ⧸ I` as an `L` module or an `L ⧸ I` module.

TODO: This result obviously generalises but the generalisation requires the missing definition of
morphisms between Lie modules over different Lie algebras.  -/
coe_lowerCentralSeries_ideal_quot_eq : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L}
  (k : ℕ), ↑(LieModule.lowerCentralSeries R L (L ⧸ I) k) = ↑(LieModule.lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.trans_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Add α] [inst_4 : Add β] [inst_5 : Add γ] (f : α ≃+o β) (g : β ≃+o γ) (a : α), (f.trans g) a = g (f a)
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.single_strictMono : ∀ {α : Type u_1} [inst : LinearOrder α], StrictMono fun a => toColex fun₀ | a => 1
-- Mathlib.GroupTheory.GroupAction.Transitive
MulAction.isPretransitive_congr : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} {β : Type u_6} [inst : Monoid M] [inst_1 : Monoid N]
  [inst_2 : MulAction M α] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Surjective φ → Function.Bijective ⇑f → (MulAction.IsPretransitive M α ↔ MulAction.IsPretransitive N β)
-- Mathlib.Order.Filter.Extr
isExtrOn_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn (⇑OrderDual.toDual ∘ f) s a ↔ IsExtrOn f s a
-- Mathlib.Computability.DFA
DFA.accepts_compl : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), Mᶜ.accepts = M.acceptsᶜ
-- Mathlib.RingTheory.WittVector.Identities
/-- The composition of Frobenius and Verschiebung is multiplication by `p`.  -/
WittVector.frobenius_verschiebung : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x : WittVector p R),
  WittVector.frobenius (WittVector.verschiebung x) = x * ↑p
-- Mathlib.Logic.Unique
/-- If a constant function is surjective, then the codomain is a singleton.  -/
Function.Surjective.uniqueOfSurjectiveConst : (α : Type u_3) → {β : Type u_4} → (b : β) → Function.Surjective (Function.const α b) → Unique β
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instCharP : ∀ {K : Type u} [inst : Field K] {p : ℕ} [CharP K p], CharP (RatFunc K) p
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_comp : ∀ {S : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {F : Type u_8}
  [inst_2 : AddCommGroup S] [inst_3 : FunLike F N S] [AddMonoidHomClass F N S] (f : M → N) (g : F) (x y : M),
  QuadraticMap.polar (⇑g ∘ f) x y = g (QuadraticMap.polar f x y)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.one_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.one.mul x) x
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_cons : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {f f' g g' h h' i i' : C} {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i} {β : f' ≅ g'} {θ : g' ⟶ h'} {θs : h' ⟶ i'}
  {ηθ : CategoryTheory.MonoidalCategoryStruct.tensorObj g g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj h h'}
  {ηθs : CategoryTheory.MonoidalCategoryStruct.tensorObj h h' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i i'}
  {ηθ₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i i'}
  {ηθ₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj f f' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i i'},
  CategoryTheory.MonoidalCategoryStruct.tensorHom η θ = ηθ →
    CategoryTheory.MonoidalCategoryStruct.tensorHom ηs θs = ηθs →
      CategoryTheory.CategoryStruct.comp ηθ ηθs = ηθ₁ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorIso α β).hom ηθ₁ = ηθ₂ →
          CategoryTheory.MonoidalCategoryStruct.tensorHom
              (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs))
              (CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp θ θs)) =
            ηθ₂
-- Mathlib.NumberTheory.FLT.Three
/-- For any `S' : Solution'`, the multiplicity of `λ` in `S'.c` is finite.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  FiniteMultiplicity (hζ.toInteger - 1) (FermatLastTheoremForThreeGen.Solution'.c✝ S')
-- Mathlib.Topology.CWComplex.Classical.Graph
Topology.CWComplex.edgeSet_OneSkeletonGraph : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [inst_1 : Topology.CWComplex C],
  (Topology.CWComplex.OneSkeletonGraph C).edgeSet = Set.univ
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_comp : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} (hnp : ℬ →+*ᵍ 𝒞) (hmn : 𝒜 →+*ᵍ ℬ),
  ⇑(hnp.comp hmn) = ⇑hnp ∘ ⇑hmn
-- Mathlib.RingTheory.Ideal.BigOperators
Ideal.sum_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) {ι : Type u_1} {t : Finset ι} {f : ι → α},
  (∀ c ∈ t, f c ∈ I) → ∑ i ∈ t, f i ∈ I
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mulAction : {R : Type u} → {M : Type v} → [inst : Monoid R] → [inst_1 : MulAction R M] → (p : SubMulAction R M) → MulAction R ↥p
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- Map from `lpMeas` to `Lp F p (μ.trim hm)`.  -/
MeasureTheory.lpMeasToLpTrim : {α : Type u_1} →
  (F : Type u_2) →
    (𝕜 : Type u_3) →
      (p : ENNReal) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup F] →
            [inst_2 : NormedSpace 𝕜 F] →
              {m m0 : MeasurableSpace α} →
                (μ : MeasureTheory.Measure α) →
                  (hm : m ≤ m0) → ↥(MeasureTheory.lpMeas F 𝕜 m p μ) → ↥(MeasureTheory.Lp F p (μ.trim hm))
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
Nat.Coprime.card_divisors_mul : ∀ {m n : ℕ}, m.Coprime n → (m * n).divisors.card = m.divisors.card * n.divisors.card
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.intro : Lean.Meta.Grind.AttrKind