mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabInfo.mk.inj : ∀ {toElabInfo : Lean.Elab.ElabInfo} {name : Lean.Name} {kind : Lean.Elab.DocElabKind}
  {toElabInfo_1 : Lean.Elab.ElabInfo} {name_1 : Lean.Name} {kind_1 : Lean.Elab.DocElabKind},
  { toElabInfo := toElabInfo, name := name, kind := kind } =
      { toElabInfo := toElabInfo_1, name := name_1, kind := kind_1 } →
    toElabInfo = toElabInfo_1 ∧ name = name_1 ∧ kind = kind_1
-- Init.Core
ne_of_beq_false : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {a b : α}, (a == b) = false → a ≠ b
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- Distribution of the trajectory obtained by starting with `μ₀` and iterating the kernels `κ`.  -/
ProbabilityTheory.Kernel.trajMeasure : {X : ℕ → Type u_1} →
  [inst : (n : ℕ) → MeasurableSpace (X n)] →
    MeasureTheory.Measure (X 0) →
      (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) →
        [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] → MeasureTheory.Measure ((n : ℕ) → X n)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instLieAddGroupOfTopWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {a : WithTop ℕ∞} [LieAddGroup I ⊤ G],
  LieAddGroup I a G
-- Std.Http.Protocol.H1
/-- Consumes chunk-data bytes for the current chunk, handling complete and partial
chunk payload reads.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.parseChunkedBodyState : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue) →
      ℕ → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instIsCharPUInt8OfNatNat : Lean.Grind.IsCharP UInt8 256
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_prodMap : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] [Module.Free R M] [Module.Free R M'] [Module.Finite R M]
  [Module.Finite R M'] (f : Module.End R M) (f' : Module.End R M'),
  LinearMap.det (LinearMap.prodMap f f') = LinearMap.det f * LinearMap.det f'
-- Mathlib.Algebra.Polynomial.Div
Polynomial.mul_divByMonic_cancel_left : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) {q : Polynomial R}, q.Monic → q * p /ₘ q = p
-- Mathlib.Logic.Unique
Pi.unique : {α : Sort u_1} → {β : α → Sort v} → [(a : α) → Unique (β a)] → Unique ((a : α) → β a)
-- Batteries.Tactic.Congr
Batteries.Tactic.Congr.Config.mk : Bool → Bool → Batteries.Tactic.Congr.Config
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_natural_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Y') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F Y Y') h)
-- Lean.Meta.Tactic.Simp.Simproc
/-- Similar to `try`, but only consider `DSimproc` case. That is, if `s.proc` is a `Simproc`, treat it as a `.continue`.  -/
Lean.Meta.Simp.SimprocEntry.tryD : Lean.Meta.Simp.SimprocEntry → ℕ → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.FieldTheory.SeparableDegree
Field.finSepDegree.eq_1 : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.finSepDegree F E = Nat.card (Field.Emb F E)
-- Std.Data.ExtTreeSet.Basic
/-- Computes the union of the given tree sets. If both maps contain elements that are equal according
to the comparison function, the element contained in the second argument will appear in the result.

This function always merges the smaller set into the larger set.
 -/
Std.ExtTreeSet.union : {α : Type u} →
  {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.comp_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {X_1 Y Z : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (f : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X X_1 Y)
  (g : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X Y Z) (X_2 : X),
  (CategoryTheory.CategoryStruct.comp f g).fst.app X_2 =
    CategoryTheory.CategoryStruct.comp (f.fst.app X_2) (g.fst.app X_2)
-- Mathlib.Data.List.Cycle
Cycle.nontrivial_reverse_iff : ∀ {α : Type u_1} {s : Cycle α}, s.reverse.Nontrivial ↔ s.Nontrivial
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_cons_iff : ∀ {α : Type u_1} {β : Type u_2} {l₂ : List β} {l : List α} {b : β} {f : (i : ℕ) → α → i < l.length → β},
  l.mapFinIdx f = b :: l₂ ↔
    ∃ a l₁, ∃ (w : l = a :: l₁), f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h => f (i + 1) a_1 ⋯) = l₂
-- Mathlib.Data.FunLike.IsApply
IsNegApply.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instAddCommGroup : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → AddCommGroup (CuspForm Γ k)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
_private.Mathlib.RingTheory.Spectrum.Prime.Basic.0.PrimeSpectrum.primeSpectrumProdOfSum.match_1.splitter : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        (motive : PrimeSpectrum R ⊕ PrimeSpectrum S → Sort u_3) →
          (x : PrimeSpectrum R ⊕ PrimeSpectrum S) →
            ((I : Ideal R) → (isPrime : I.IsPrime) → motive (Sum.inl { asIdeal := I, isPrime := isPrime })) →
              ((J : Ideal S) → (isPrime : J.IsPrime) → motive (Sum.inr { asIdeal := J, isPrime := isPrime })) → motive x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.instCategoryStruct : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → CategoryTheory.CategoryStruct.{max v w, u} (CategoryTheory.Bicategory.Adj B)
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.Quot.addMonoidHom_ext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] {α : Type u_1} [inst_2 : AddMonoid α] {f g : AddCommGrpCat.Colimits.Quot F →+ α},
  (∀ (j : J) (x : ↑(F.obj j)), f ((AddCommGrpCat.Colimits.Quot.ι F j) x) = g ((AddCommGrpCat.Colimits.Quot.ι F j) x)) →
    f = g
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapEquiv_refl : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R],
  IsLocalRing.ResidueField.mapEquiv (RingEquiv.refl R) = RingEquiv.refl (IsLocalRing.ResidueField R)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_mk_iff' : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (p : Submodule R L)
  (h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, y⁆ ∈ p.carrier) {x : L},
  x ∈ { toSubmodule := p, lie_mem' := h } ↔ x ∈ p
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalars_comp_id_assoc : ∀ {R₁ R₂ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] (f₁₂ : R₁ →+* R₂)
  {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₂)} (h : ModuleCat.extendScalars f₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp f₁₂ (RingHom.id R₂)).hom
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars f₁₂).whiskerLeft (ModuleCat.extendScalarsId R₂).hom)
        (CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalars f₁₂).rightUnitor.hom h)) =
    h
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakSpace.map_apply : ∀ {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : ContinuousAdd 𝕜] [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E]
  [inst_6 : TopologicalSpace E] [inst_7 : AddCommMonoid F] [inst_8 : Module 𝕜 F] [inst_9 : TopologicalSpace F]
  (f : E →L[𝕜] F) (x : E), (WeakSpace.map f) x = f x
-- Std.Data.ExtDTreeMap.Basic
/-- Compares two tree maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.ExtDTreeMap.Const.beq : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] → [BEq β] → Std.ExtDTreeMap α (fun x => β) cmp → Std.ExtDTreeMap α (fun x => β) cmp → Bool
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_image_target_inter_eq : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β),
  ↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConstC : ℤ → Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D],
  (CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).functor =
    CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.wl_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g)
  (i : E.I₀) {Z : C} (h : F.X (f.s₀ i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.a i) (CategoryTheory.CategoryStruct.comp (F.p₁ (self.H i)) h) =
    CategoryTheory.CategoryStruct.comp (f.h₀ i) h
-- Aesop.RuleTac.Cases
Aesop.CasesTarget' : Type
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w outWidth : ℕ} (aig : Std.Sat.AIG α) (idx : ℕ)
  (x : aig.RefVec w) (acc : aig.RefVec (w * idx)) (h : idx ≤ w) (h' : outWidth = w * w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go idx x acc h h').aig.decls.size
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.instIsOverToSpecΓSpec : ∀ {R : CommRingCat} {X : AlgebraicGeometry.Scheme} [inst : X.Over (AlgebraicGeometry.Spec R)]
  [inst_1 : AlgebraicGeometry.IsAffine X], AlgebraicGeometry.Scheme.Hom.IsOver X.toSpecΓ (AlgebraicGeometry.Spec R)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_sub : ∀ {α : Type u_1} {G : Type u_6} [inst : AddGroup G] (s : Set α) (f g : α → G),
  (s.indicator fun a => f a - g a) = fun a => s.indicator f a - s.indicator g a
-- Mathlib.MeasureTheory.Function.EssSup
meas_essSup_lt : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLinearOrder β] {f : α → β} [inst_1 : TopologicalSpace β] [FirstCountableTopology β]
  [OrderTopology β],
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) meas_essSup_lt._auto_1 →
    μ {y | essSup f μ < f y} = 0
-- Mathlib.Data.Multiset.AddSub
Multiset.countP_add : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s t : Multiset α),
  Multiset.countP p (s + t) = Multiset.countP p s + Multiset.countP p t
-- Mathlib.Topology.Bases
/-- In a separable space, a family of disjoint sets with nonempty interiors is countable.  -/
Set.PairwiseDisjoint.countable_of_nonempty_interior : ∀ {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α} {a : Set ι},
  a.PairwiseDisjoint s → (∀ i ∈ a, (interior (s i)).Nonempty) → a.Countable
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblen o₁ a < veblen o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a < b`
* `o₁ < o₂` and `a < veblen o₂ b`
* `o₁ > o₂` and `veblen o₁ a < b`  -/
Ordinal.veblen_lt_veblen_iff : ∀ {o₁ o₂ a b : Ordinal.{u}},
  Ordinal.veblen o₁ a < Ordinal.veblen o₂ b ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < Ordinal.veblen o₂ b ∨ o₂ < o₁ ∧ Ordinal.veblen o₁ a < b
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.instNontrivial : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] [Nontrivial M],
  Nontrivial (MulArchimedeanClass M)
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- An equivalence of additive group extensions from a homomorphism making a commuting diagram.
Such a homomorphism is necessarily an isomorphism.  -/
AddGroupExtension.Equiv.ofAddMonoidHom : {N : Type u_1} →
  {G : Type u_2} →
    [inst : AddGroup N] →
      [inst_1 : AddGroup G] →
        {E : Type u_3} →
          [inst_2 : AddGroup E] →
            {S : AddGroupExtension N E G} →
              {E' : Type u_4} →
                [inst_3 : AddGroup E'] →
                  {S' : AddGroupExtension N E' G} →
                    (f : E →+ E') → f.comp S.inl = S'.inl → S'.rightHom.comp f = S.rightHom → S.Equiv S'
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.BVPred.bitblast_le_size : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig),
  aig.decls.size ≤ (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).aig.decls.size
-- Mathlib.Data.Fintype.Sets
/-- **Alias** of the reverse direction of `Set.toFinset_subset_toFinset`. -/
Set.toFinset_mono : ∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s ⊆ t → s.toFinset ⊆ t.toFinset
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.refl.eq_1 : ∀ (M : Type u_9) [inst : Add M], AddEquiv.refl M = { toEquiv := Equiv.refl M, map_add' := ⋯ }
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map_cotangentComplex : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P') (x : P.Cotangent),
  (Algebra.Extension.CotangentSpace.map f) (P.cotangentComplex x) =
    P'.cotangentComplex ((Algebra.Extension.Cotangent.map f) x)
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite Int32
-- Std.Time.DateTime.WallTime
/-- Creates a `WallTime` from a `Millisecond.Offset`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.ofMilliseconds : Std.Time.Millisecond.Offset → Std.Time.WallTime
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.girth_anti : ∀ {α : Type u_1} {G G' : SimpleGraph α}, G ≤ G' → ¬G.IsAcyclic → G'.girth ≤ G.girth
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_image_target_inter_eq' : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β), ↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
-- Mathlib.Topology.Algebra.UniformConvergence
instAddUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Add β],
  instAddUniformOnFun = { add := instAddUniformOnFun._aux_1 }
-- Mathlib.Data.Num.Prime
_private.Mathlib.Data.Num.Prime.0.PosNum.minFac.match_1.splitter : (motive : PosNum → Sort u_1) →
  (x : PosNum) → (Unit → motive PosNum.one) → ((a : PosNum) → motive a.bit0) → ((n : PosNum) → motive n.bit1) → motive x
-- Init.Data.SInt.Lemmas
UInt32.toInt32_mul : ∀ (a b : UInt32), (a * b).toInt32 = a.toInt32 * b.toInt32
-- Mathlib.Algebra.Order.GroupWithZero.Basic
StrictMono.const_mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [inst_2 : Preorder α]
  {f : α → M₀} [PosMulStrictMono M₀], StrictMono f → 0 < a → StrictMono fun x => a * f x
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatchAtChain_iff : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain c pos pos' ↔
    pos ≤ pos' ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h : pos'' < pos'), pos''.get ⋯ = c
-- Mathlib.Data.NNRat.Defs
NNRat.num_pow : ∀ (q : ℚ≥0) (n : ℕ), (q ^ n).num = q.num ^ n
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_fin : ∀ {n : ℕ} (x : Fin n), ↑x = ↑↑x
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : AddMonoidAlgebra R ℕ), { toFinsupp := p }.support = p.coeff.support
-- Mathlib.Algebra.Opposites
/-- The element of `α` represented by `x : PreOpposite α`.  -/
PreOpposite.unop' : {α : Type u_3} → PreOpposite α → α
-- Std.Time.Format.Modifier
Std.Time.instReprNumber.repr : Std.Time.Number → ℕ → Std.Format
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.instIsCountablyGeneratedFinsetFilterConditionalOfAtTopOfAtBot : ∀ (β : Type u_2) [inst : Preorder β] [inst_1 : LocallyFiniteOrder β] [Filter.atTop.IsCountablyGenerated]
  [Filter.atBot.IsCountablyGenerated], (SummationFilter.conditional β).filter.IsCountablyGenerated
-- Init.Meta.Defs
/-- Creates an identifier with its position copied from `src`.

To refer to a specific constant without a risk of variable capture, use `mkCIdentFrom` instead.
 -/
Lean.mkIdentFrom : Lean.Syntax → Lean.Name → optParam Bool false → Lean.Ident
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfPair.ext : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} {inst : AddCommGroup M} {inst_1 : AddCommGroup N} {inst_2 : CommRing R}
  {inst_3 : Module R M} {inst_4 : Module R N} {p : M →ₗ[R] N →ₗ[R] R} {x y : p.IsPerfPair}, x = y
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuous.div_const' : ∀ {R : Type u_3} {β : Type u_4} [inst : DivisionRing R] [inst_1 : UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R]
  [inst_3 : UniformSpace β] {f : β → R}, UniformContinuous f → ∀ (a : R), UniformContinuous fun x => f x / a
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.whiskerRight_def : ∀ (R : Type u) [inst : CommRing R] {X₁ X₂ : BialgCat R} (f : X₁ ⟶ X₂) (X : BialgCat R),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = BialgCat.ofHom (BialgHom.rTensor X.carrier f.toBialgHom')
-- Mathlib.Logic.Unique
Unique.bijective : ∀ {A : Sort u_2} {B : Sort u_3} [Unique A] [Unique B] {f : A → B}, Function.Bijective f
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_one : ∀ {R : Type u} [inst : Semiring R] {k : ℕ}, 0 < k → (⇑Polynomial.derivative)^[k] 1 = 0
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_node3L : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  Ordnode.All P (l.node3L x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r
-- Lean.Meta.ArgsPacker
/-- Given unary expressions `e₁`, `e₂` with types `(x : A) → R`
and `(z : C) → R`, returns an expression of type
```
(x : A ⊕' C) → R
```
 -/
Lean.Meta.ArgsPacker.Mutual.uncurryND : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Grind.Config
/-- TODO  -/
Lean.Grind.Config.lookahead : Lean.Grind.Config → Bool
-- Init.Data.UInt.Lemmas
UInt8.toFin_ofFin : ∀ (n : Fin UInt8.size), (UInt8.ofFin n).toFin = n
-- Init.Grind.Lemmas
Lean.Grind.Bool.eq_false_of_not_eq_true : ∀ {a : Bool}, (!a) = true → a = false
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.instIsMonHomMulOfIsCommMonObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C]
  [CategoryTheory.IsCommMonObj M], CategoryTheory.IsMonHom CategoryTheory.MonObj.mul
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalence_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C),
  (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).functor =
    CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c
-- Init.Data.Order.Ord
Std.instLawfulEqOrdProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β] [Std.LawfulEqOrd α] [Std.LawfulEqOrd β],
  Std.LawfulEqOrd (α × β)
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- Sets of isotypic components in a semisimple module are in order-preserving 1-1
correspondence with fully invariant submodules. Consequently, the fully invariant submodules
form a complete atomic Boolean algebra.  -/
OrderIso.setIsotypicComponents : {R : Type u_2} →
  {M : Type u} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [IsSemisimpleModule R M] → Set ↑(isotypicComponents R M) ≃o ↥(fullyInvariantSubmodule R M)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.NeBot.le_pure_iff : ∀ {α : Type u} {f : Filter α} {a : α}, f.NeBot → (f ≤ pure a ↔ f = pure a)
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.decidableLE.match_1.splitter : {α : Type u_1} →
  (motive : WithBot α → WithBot α → Sort u_2) →
    (x x_1 : WithBot α) →
      ((x : WithBot α) → motive none x) →
        ((a : α) → motive (some a) none) → ((a b : α) → motive (some a) (some b)) → motive x x_1
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- `e : Edge x₀ x₁` is a composition of `Edge.id x₀` with `e`.  -/
SSet.Edge.CompStruct.idComp : {X : SSet} → {x₀ x₁ : X.obj (Opposite.op { len := 0 })} → (e : SSet.Edge x₀ x₁) → (SSet.Edge.id x₀).CompStruct e e
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.add_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r s t : R},
  r + s = t → (algebraMap R A) r + (algebraMap R A) s = (algebraMap R A) t
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePos_addPos_cancel : ∀ {assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment},
  ¬assignment.hasPosAssignment = true → assignment.addPosAssignment.removePosAssignment = assignment
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.IsFinite.of_locallyQuasiFinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.IsLocallyArtinian Y], AlgebraicGeometry.IsFinite f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokensLegend.fromJson : Lean.Json → Except String Lean.Lsp.SemanticTokensLegend
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.uliftFunctor_map : ∀ {X x : Type u} (f : X ⟶ x),
  CategoryTheory.uliftFunctor.{v, u}.map f =
    TypeCat.ofHom fun x_1 => { down := (CategoryTheory.ConcreteCategory.hom f) x_1.down }
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsEquivalenceFunctorId : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] (W₁ : CategoryTheory.MorphismProperty C₁),
  (CategoryTheory.LocalizerMorphism.id W₁).functor.IsEquivalence