mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Iterators
Std.Roc.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : LE α] →
        [inst_2 : DecidableLE α] →
          [Std.PRange.LawfulUpwardEnumerable α] →
            [Std.PRange.LawfulUpwardEnumerableLE α] →
              [inst_5 : LT α] →
                [Std.PRange.LawfulUpwardEnumerableLT α] →
                  [Monad m] → [Std.Iterators.Finite (Std.Rxc.Iterator α) Id] → ForIn' m (Std.Roc α) α inferInstance
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- **Alias** of `CategoryTheory.ObjectProperty.homMk`. -/
CategoryTheory.Sheaf.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} → {X Y : P.FullSubcategory} → (X.obj ⟶ Y.obj) → (X ⟶ Y)
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.coeff_eq : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R} {n : ℕ},
  p.IsMonicOfDegree n → q.IsMonicOfDegree n → ∀ {m : ℕ}, n ≤ m → p.coeff m = q.coeff m
-- Mathlib.GroupTheory.Commutator.Basic
commutator_eq_closure : ∀ (G : Type u_1) [inst : Group G], commutator G = Subgroup.closure (commutatorSet G)
-- Lean.Elab.MutualInductive
/-- Function to check universes and provide a custom error. (`structure` uses this to do checks per field to give nicer messages.)  -/
Lean.Elab.Command.InductiveElabStep2.checkUniverses : Lean.Elab.Command.InductiveElabStep2 → ℕ → Lean.Level → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Instances.CantorSet
/-- Canonical bijection between the Cantor set and infinite binary tree.  -/
cantorSetEquivNatToBool : ↑cantorSet ≃ (ℕ → Bool)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M) (n : M),
  MvPolynomial.weightedHomogeneousComponent w n =
    ↑(AddMonoidAlgebra.coeffLinearEquiv R).symm ∘ₗ
      (Finsupp.supported R R {d | (Finsupp.weight w) d = n}).subtype ∘ₗ
        Finsupp.restrictDom R R {d | (Finsupp.weight w) d = n} ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv R)
-- Lean.Setup
Lean.instReprPlugin.repr : Lean.Plugin → ℕ → Std.Format
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
continuousOn_tangentCoordChange : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x y : M),
  ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)
-- Mathlib.Data.Sum.Order
OrderIso.sumAssoc_apply_inl_inl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (a : α),
  (OrderIso.sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instMembershipOfTransCmp : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Membership α (Std.ExtTreeSet α cmp)
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- A surjective closed immersion is an isomorphism when the target is reduced.  -/
AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] [AlgebraicGeometry.Surjective f]
  [AlgebraicGeometry.IsReduced Y], CategoryTheory.IsIso f
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.mkNewSeq : Lean.Meta.Grind.Goal →
  Array Lean.Meta.Grind.EMatchTheorem →
    List Lean.Meta.Grind.TGrind → Bool → Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.TGrind)
-- Mathlib.Order.Bounds.Image
Monotone.upperBounds_image_of_directedOn_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {γ : Type u_3} [inst_2 : Preorder γ]
  {g : α × β → γ},
  Monotone g →
    ∀ {d : Set (α × β)},
      DirectedOn (fun x1 x2 => x1 ≤ x2) d → upperBounds (g '' d) = upperBounds (g '' (Prod.fst '' d) ×ˢ (Prod.snd '' d))
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.ne_startPos_of_singleton : ∀ {t₁ : String} {c : Char} {t₂ : String} {s : String.Slice} {p : s.Pos},
  p.Splits (t₁ ++ String.singleton c) t₂ → p ≠ s.startPos
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelComparison_comp_kernel_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] {X' Y' : C} [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)] (g : X' ⟶ Y') [inst_7 : CategoryTheory.Limits.HasKernel g]
  [inst_8 : CategoryTheory.Limits.HasKernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y')
  (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g) {Z : D}
  (h : CategoryTheory.Limits.kernel (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
        h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.map f g p q hpq))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison g G) h)
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right : ∀ {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 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  [inst_5 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))).app
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X Y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X Y)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))
      (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).app
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G` preserves every pointwise extensions of `F` along `L` at `c`.  -/
CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt.preserves : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {inst : CategoryTheory.Category.{v_1, u_1} A}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {inst_2 : CategoryTheory.Category.{v_3, u_3} C}
  {inst_3 : CategoryTheory.Category.{v_4, u_4} D} {G : CategoryTheory.Functor B D} {F : CategoryTheory.Functor A B}
  {L : CategoryTheory.Functor A C} {c : C} [self : G.PreservesPointwiseLeftKanExtensionAt F L c] (E : L.LeftExtension F)
  (a : E.IsPointwiseLeftKanExtensionAt c),
  Nonempty (((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj E).IsPointwiseLeftKanExtensionAt c)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comm₂₄_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂)
  {Z : C} (h : sq₂.X₄ ⟶ Z),
  CategoryTheory.CategoryStruct.comp sq₁.f₂₄ (CategoryTheory.CategoryStruct.comp self.τ₄ h) =
    CategoryTheory.CategoryStruct.comp self.τ₂ (CategoryTheory.CategoryStruct.comp sq₂.f₂₄ h)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.denote_bitblast : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache (Std.Tactic.BVDecide.BVExpr w) aig)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig input.cache →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign.toAIGAssignment,
          { aig := (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).aig,
            ref := (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).vec.get idx hidx }⟧ =
        (Std.Tactic.BVDecide.BVExpr.eval assign input.val).getLsbD idx
-- Init.Data.SInt.Bitwise
instAssociativeInt64HOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom_π_app : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] (j : J),
  (CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom V F₁ F₂).π.app j =
    CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom V F₁ F₂ (CategoryTheory.Under.forget j)
-- Mathlib.Algebra.Order.Field.Basic
one_lt_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < b → (1 < a / b ↔ b < a)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.obj_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (X : C)
  (i : ℕ) (hi : i + 1 < n + 1 + 1), CategoryTheory.ComposableArrows.Precomp.obj F X ⟨i + 1, hi⟩ = F.obj' i ⋯
-- Init.Data.Order.Ord
/-- A typeclass for comparison functions satisfying `cmp a b = .eq` if and only if the boolean equality
`a == b` holds.

This typeclass distinguishes itself from `LawfulEqCmp` by using boolean equality (`==`) instead of
logical equality (`=`).
 -/
Std.LawfulBEqCmp : {α : Type u} → [BEq α] → (α → α → Ordering) → Prop
-- Std.Do.Internal.Ensures.Def
/-- Apply a `MayReturn` witness to an `Ensures` proof to extract the postcondition at `a`.  -/
Std.Do.Internal.MayReturn.imp : ∀ {m : Type u → Type v} [inst : Bind m] {α : Type u} {x : m α} {a : α},
  Std.Do.Internal.MayReturn x a → ∀ {P : α → Prop}, Std.Do.Internal.Ensures P x → P a
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.IsSimple.mk : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  (∀ (I : LieIdeal R L), I = ⊥ ∨ I = ⊤) → ¬IsLieAbelian L → LieAlgebra.IsSimple R L
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.self : ∀ (R : Type u) [inst : CommRing R], Module.FaithfullyFlat R R
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.HD_bound_aux2 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty X] (f : GromovHausdorff.Cb✝ X Y)
  (C : ℝ), BddAbove (Set.range fun y => ⨅ x, f (Sum.inl x, Sum.inr y) + C)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.dist_eq_of_dist_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) {y z : α}, dist y z = 0 → dist x y = dist x z
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `AddMonoidHom.domRestrict_apply`. -/
AddMonoidHom.restrict_apply : ∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_5} {S : Type u_6} [inst_1 : AddZeroClass N] [inst_2 : SetLike S M]
  [inst_3 : AddSubmonoidClass S M] (f : M →+ N) (s : S) (x : ↥s), (f.domRestrict s) x = f ↑x
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.zero' : ∀ {A : Type u} {inst : AddGroup A} [self : AddGroupFilterBasis A] {U : Set A}, U ∈ self.sets → 0 ∈ U
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldInfo.mk.inj : ∀ {projName fieldName : Lean.Name} {lctx : Lean.LocalContext} {val : Lean.Expr} {stx : Lean.Syntax}
  {projName_1 fieldName_1 : Lean.Name} {lctx_1 : Lean.LocalContext} {val_1 : Lean.Expr} {stx_1 : Lean.Syntax},
  { projName := projName, fieldName := fieldName, lctx := lctx, val := val, stx := stx } =
      { projName := projName_1, fieldName := fieldName_1, lctx := lctx_1, val := val_1, stx := stx_1 } →
    projName = projName_1 ∧ fieldName = fieldName_1 ∧ lctx = lctx_1 ∧ val = val_1 ∧ stx = stx_1
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.piAntidiag_univ_fin_eq_antidiagonalTuple : ∀ (n k : ℕ), Finset.univ.piAntidiag n = Finset.Nat.antidiagonalTuple k n
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.responseError.sizeOf_spec : sizeOf Lean.JsonRpc.MessageKind.responseError = 1
-- Lean.Widget.UserWidget
Lean.Widget.instFromJsonWidgetSource.fromJson : Lean.Json → Except String Lean.Widget.WidgetSource
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.AEEqFun.posPart.congr_simp : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : LinearOrder γ] [inst_3 : OrderClosedTopology γ] [inst_4 : Zero γ] (f f_1 : α →ₘ[μ] γ),
  f = f_1 → f.posPart = f_1.posPart
-- Mathlib.Data.FunLike.Equiv
/-- The two coercions to functions are jointly injective.  -/
EquivLike.coe_injective' : ∀ {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e g : E),
  EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_some_getD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a fallback : α},
  t.contains a = true → t.get? a = some (t.getD a fallback)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i : X.toComma ⟶ Y.toComma) [inst_7 : CategoryTheory.IsIso i],
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i) = i
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mem_image_of_mem_range_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] {r : β} {s : Set α}
  {f : MeasureTheory.SimpleFunc α β}, r ∈ (f.restrict s).range → r ≠ 0 → r ∈ ⇑f '' s
-- Mathlib.Data.Finset.Insert
Finset.insert_subset_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_eq_some_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.min? = some t.min!
-- Mathlib.Order.GaloisConnection.Basic
/-- **Alias** of `GaloisInsertion.l_iInf_of_u_l_eq_self`. -/
GaloisInsertion.l_iInf_of_ul_eq_self : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → α), (∀ (i : ι), u (l (f i)) = f i) → l (⨅ i, f i) = ⨅ i, l (f i)
-- Mathlib.GroupTheory.Coset.Card
QuotientGroup.fintype.eq_1 : ∀ {α : Type u_1} [inst : Group α] [inst_1 : Fintype α] (s : Subgroup α)
  [inst_2 : DecidableRel ⇑(QuotientGroup.leftRel s)],
  QuotientGroup.fintype s = Quotient.fintype (QuotientGroup.leftRel s)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.g_nat.eq_1 : ∀ (k : ℕ) (a t : ℝ) (n : ℕ), HurwitzKernelBounds.g_nat k a t n = (↑n + a) ^ k * Real.exp (-Real.pi * (↑n + a ^ 2) * t)
-- Init.Data.List.Lex
List.cons_lt_cons_self : ∀ {α : Type u_1} {a : α} [inst : LT α] [i₀ : Std.Irrefl fun x1 x2 => x1 < x2] {l₁ l₂ : List α},
  a :: l₁ < a :: l₂ ↔ l₁ < l₂
-- Mathlib.RingTheory.PicardGroup
/-- Given two invertible `R`-submodules in an `R`-algebra `A`, the `R`-linear map from
`I ⊗[R] J` to `I * J` induced by multiplication is an isomorphism.  -/
Submodule.tensorEquivMul : {R : Type u} →
  {A : Type u_4} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] → [FaithfulSMul R A] → (I J : (Submodule R A)ˣ) → TensorProduct R ↥↑I ↥↑J ≃ₗ[R] ↥↑(I * J)
-- Mathlib.Data.Fin.SuccPred
Fin.pred_lt_castPred_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ Fin.last n), a.pred ha < b.castPred hb ↔ a ≤ b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.abstract.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.abstract = 1
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w}
  [inst_3 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y}
  (hc : CategoryTheory.Limits.IsColimit c) (z : X ⟶ c.pt) [CategoryTheory.IsFiltered J],
  CategoryTheory.IsIso (CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.f z)
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
DifferentiableOn.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → F} {s : Set E},
  DifferentiableOn 𝕜' f s → DifferentiableOn 𝕜 f s
-- Lean.Elab.Term.TermElabM
/-- "Custom", `msgData` stores the additional error messages.  -/
Lean.Elab.Term.MVarErrorKind.custom : Lean.MessageData → Lean.Elab.Term.MVarErrorKind
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(0) = 0`.  -/
FractionalIdeal.count_zero : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  FractionalIdeal.count K v 0 = 0
-- Mathlib.Order.Defs.Unbundled
instIrreflEmptyRelation_mathlib : ∀ {α : Sort u_1}, Std.Irrefl emptyRelation
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.match_3.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    {δ : Type u_4} →
      (motive : Std.DHashMap.Internal.AssocList α β → δ → Sort u_3) →
        (x : Std.DHashMap.Internal.AssocList α β) →
          (x_1 : δ) →
            ((acc : δ) → motive Std.DHashMap.Internal.AssocList.nil acc) →
              ((k : α) →
                  (v : β k) →
                    (t : Std.DHashMap.Internal.AssocList α β) →
                      (acc : δ) → motive (Std.DHashMap.Internal.AssocList.cons k v t) acc) →
                motive x x_1
-- Mathlib.Algebra.Module.PID
Ideal.torsionOf_eq_span_pow_pOrder : ∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] {p : R},
  Irreducible p →
    ∀ (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) [dec : (x : M) → Decidable (x = 0)] (x : M),
      Ideal.torsionOf R M x = Ideal.span {p ^ Submodule.pOrder hM x}
-- Mathlib.RingTheory.IdealFilter.Topology
/-- The topology is linear in the sense that `𝓝 0` has a basis of ideals.  -/
WithIdealFilter.instIsLinearTopology : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A}, IsLinearTopology (WithIdealFilter F) (WithIdealFilter F)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_apply : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  (ha : autoParam (p a) _auto_57✝) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto_59✝),
  cfc f a = (cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_empty : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], ProjectiveSpectrum.zeroLocus 𝒜 ∅ = Set.univ
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instCoeFun : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} → [inst : NormedAddCommGroup E] → CoeFun ↥(MeasureTheory.Lp E p μ) fun x => α → E
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.ExprVisited.mk : Lean.Expr → Lean.Meta.Canonicalizer.ExprVisited
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.differentiableAt_sin : ∀ {x : ℝ}, DifferentiableAt ℝ Real.sin x
-- Mathlib.Order.Heyting.Basic
/-- The **deduction theorem** in the Heyting algebra model of intuitionistic logic:
an implication holds iff the conclusion follows from the hypothesis.  -/
himp_eq_top_iff : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇨ b = ⊤ ↔ a ≤ b
-- Mathlib.Topology.Algebra.Group.Basic
Units.instCompactSpaceOfT1SpaceOfContinuousMul : ∀ {α : Type u} [inst : Monoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousMul α] [CompactSpace α],
  CompactSpace αˣ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toList_ric : ∀ {n i : ℕ} (_h : i < (*...=n).toList.length), (*...=n).toList[i] = i
-- Lean.Elab.DocString
/-- The options.

The `MonadLift TermElabM DocM` instance runs the lifted action with these options, so elaboration
commands that mutate this state cause it to take effect in subsequent commands.
 -/
Lean.Doc.State.options : Lean.Doc.State → Lean.Options
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.associator_inv_apply_1_2 : ∀ {X Y Z : TopCat}
  {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).1.2 = x.2.1
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {F' : Type u_21} [inst_6 : NormedCommRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {ι : Type} {t : Finset ι} {f : ι → M → F'},
  (∀ i ∈ t, MDiff[s] (f i)) → MDiff[s] (∏ i ∈ t, f i)