mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The second simplicial identity  -/
SimplexCategory.δ_comp_σ_of_le : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc) (SimplexCategory.σ j.succ) =
      CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.δ i)
-- Init.Data.List.Zip
List.zipWith_eq_nil_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β},
  List.zipWith f l l' = [] ↔ l = [] ∨ l' = []
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instCharZero : ∀ {K : Type v} [inst : Field K] (f : Polynomial K) [CharZero K], CharZero f.SplittingField
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.isReduced_iff_reduce_eq : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeGroup.IsReduced L ↔ FreeGroup.reduce L = L
-- Init.Prelude
instLTBitVec : {w : ℕ} → LT (BitVec w)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The obvious functor `WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ`  -/
CategoryTheory.Limits.widePushoutShapeOp : (J : Type w) →
  CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ
-- Mathlib.Probability.Distributions.Uniform
PMF.uniformOfFintype_apply : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] (a : α), (PMF.uniformOfFintype α) a = (↑(Fintype.card α))⁻¹
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciSup_eq_ite : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {p : Prop} [inst_1 : Decidable p] {f : p → α},
  ⨆ (h : p), f h = if h : p then f h else sSup ∅
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.Slice.toList_split_prop : ∀ {s : String.Slice} {p : Char → Prop} [inst : DecidablePred p],
  List.map String.Slice.copy (s.split p).toList =
    List.map String.ofList (List.splitOnP (fun b => decide (p b)) s.copy.toList)
-- Init.Data.SInt.Lemmas
ISize.toInt_maxValue : ISize.maxValue.toInt = 2 ^ (System.Platform.numBits - 1) - 1
-- Mathlib.Tactic.Find
_private.Mathlib.Tactic.Find.0.Mathlib.Tactic.Find.matchHyps : List Lean.Expr → List Lean.Expr → List Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.MinimalAxioms.mk : ∀ {α : Type u} [inst : CompleteLattice α],
  (∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)) →
    CompletelyDistribLattice.MinimalAxioms α
-- Mathlib.RingTheory.LaurentSeries
/-- Every Laurent series of valuation less than `(1 : ℤᵐ⁰)` comes from a power series.  -/
LaurentSeries.val_le_one_iff_eq_coe : ∀ (K : Type u_2) [inst : Field K] (f : LaurentSeries K), Valued.v f ≤ 1 ↔ ∃ F, (HahnSeries.ofPowerSeries ℤ K) F = f
-- Lean.Expr
Lean.instForInMVarIdSetMVarIdOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.MVarIdSet Lean.MVarId
-- Lean.Data.Lsp.Diagnostics
/-- Some languages have specific codes for each error type.  -/
Lean.Lsp.DiagnosticCode : Type
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_nonempty : ∀ {α : Type u_1} [inst : LE α] {s : UpperSet α}, (↑s).Nonempty ↔ s ≠ ⊤
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.map_braiding_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_6 : F.Braided] {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (β_ X Y).hom) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y X) h))
-- Mathlib.Topology.CompactOpen
ContinuousMap.instRegularSpace : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [RegularSpace Y],
  RegularSpace C(X, Y)
-- Init.Data.Iterators.Consumers.Monadic.Partial
/-- The wrapped iterator, which was wrapped by `IterM.allowNontermination`.
 -/
Std.IterM.Partial.it : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.IterM.Partial m β → Std.IterM m β
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.range_snd : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S], (RingHom.snd R S).rangeS = ⊤
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.TensorProduct.tensorQuotientEquiv_symm_apply_tmul : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : CommRing A] [inst_6 : Algebra R A]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (I : Ideal T) (a : A) (t : T),
  (Algebra.TensorProduct.tensorQuotientEquiv S T A I).symm
      ((Ideal.Quotient.mk (Ideal.map Algebra.TensorProduct.includeRight I)) (a ⊗ₜ[R] t)) =
    a ⊗ₜ[R] (Ideal.Quotient.mk I) t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.union_insert_right_eq_insert_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {p : (_ : α) × β}, t₁ ∪ t₂.insert p.fst p.snd = (t₁ ∪ t₂).insert p.fst p.snd
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.mismatched_of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos startPos' endPos : s.Pos} {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidSearchFrom pat endPos l →
    startPos' < endPos →
      (∀ (pos : s.Pos), startPos' ≤ pos → pos < endPos → ¬String.Slice.Pattern.Model.MatchesAt pat pos) →
        startPos = startPos' →
          String.Slice.Pattern.Model.IsValidSearchFrom pat startPos'
            (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k}, k' ∈ m.modify k f ↔ k' ∈ m
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- The main loop of `getStackEntries`  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.getStackEntries.loop : Array Lean.Expr →
  List Lean.FVarId →
    Lean.Expr →
      ℕ → ℕ → List Lean.Meta.RefinedDiscrTree.StackEntry → Lean.MetaM (List Lean.Meta.RefinedDiscrTree.StackEntry)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_filter_eq_false_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {f : α → β → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter f m)).isEmpty = false ↔
      ∃ k, ∃ (h : m.contains k = true), f (m.getKey k h) (Std.DHashMap.Internal.Raw₀.Const.get m k h) = true)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeftIso_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (W : C)
  {X Y Z : C} (f : X ≅ Y) (g : Y ≅ Z),
  CategoryTheory.MonoidalCategory.whiskerLeftIso W (f ≪≫ g) =
    CategoryTheory.MonoidalCategory.whiskerLeftIso W f ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso W g
-- Init.Data.List.Lemmas
List.isEmpty_reverse : ∀ {α : Type u_1} {xs : List α}, xs.reverse.isEmpty = xs.isEmpty
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.insertMany_list_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ : Std.TreeSet.Raw α cmp} {l : List α},
  (t₁.insertMany l).Equiv (List.foldl (fun acc a => acc.insert a) t₁ l)
-- Mathlib.MeasureTheory.Constructions.Pi
/-- **Alias** of `MeasureTheory.Measure.pi_nullSingletonClass`.

---

If one of the measures `μ i` has value zero on singeltons, them `Measure.pi µ`
has value zero on singletons. The instance below assumes that all `μ i` have value zero on
singletons.  -/
MeasureTheory.Measure.pi_noAtoms : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (i : ι)
  [MeasureTheory.NullSingletonClass (μ i)], MeasureTheory.NullSingletonClass (MeasureTheory.Measure.pi μ)
-- Mathlib.Analysis.Complex.Harmonic.Liouville
/-- **Liouville's theorem for harmonic functions on the complex plane** A bounded harmonic function on
the complex plane is constant.
 -/
InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℂ → E),
  InnerProductSpace.HarmonicOnNhd f Set.univ → Bornology.IsBounded (Set.range f) → ∀ (z w : ℂ), f z = f w
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Inductive construction of morphisms in `ComposableArrows C (n + 1)`: in order to construct
a morphism `F ⟶ G`, it suffices to provide `α : F.obj' 0 ⟶ G.obj' 0` and `β : F.δ₀ ⟶ G.δ₀`
such that `F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1`.  -/
CategoryTheory.ComposableArrows.homMkSucc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      {F G : CategoryTheory.ComposableArrows C (n + 1)} →
        (α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯) →
          (β : F.δ₀ ⟶ G.δ₀) →
            CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
                  (CategoryTheory.ComposableArrows.app' β 0 ⋯) =
                CategoryTheory.CategoryStruct.comp α (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯) →
              (F ⟶ G)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- A bicategory structure on the oplax functors between bicategories.  -/
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    (C : Type u₂) → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.Bicategory (CategoryTheory.OplaxFunctor B C)
-- Mathlib.Algebra.Order.Module.Synonym
OrderDual.instModule' : {α : Type u_1} → {β : Type u_2} → [inst : Semiring α] → [inst_1 : AddCommMonoid β] → [Module α β] → Module α βᵒᵈ
-- Mathlib.LinearAlgebra.FreeModule.IdealQuotient
/-- Decompose `S⧸I` as a direct sum of cyclic `R`-modules
(quotients by the ideals generated by Smith coefficients of `I`).  -/
Ideal.quotientEquivDirectSum : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            [inst_3 : IsDomain R] →
              [inst_4 : IsPrincipalIdealRing R] →
                [inst_5 : IsDomain S] →
                  [inst_6 : Finite ι] →
                    (F : Type u_4) →
                      [inst_7 : CommRing F] →
                        [inst_8 : Algebra F R] →
                          [inst_9 : Algebra F S] →
                            [IsScalarTower F R S] →
                              (b : Module.Basis ι R S) →
                                {I : Ideal S} →
                                  (hI : I ≠ ⊥) →
                                    (S ⧸ I) ≃ₗ[F] DirectSum ι fun i => R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i}
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.unop_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.Splitting), h.unop.r = h.s.unop
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α},
  t.maxKey? = some km → km ∈ t
-- Batteries.Util.ProofWanted
/-- This typeclass instance would be a welcome contribution to the library!

The syntax mirrors `instance` (the name is optional, auto-generated from the class head if
absent) and the payload must be a typeclass. The placeholder is recorded as
`DefWanted (TheClass …)` like `def_wanted`, but additionally the declared name is registered so a
subsequent `theorem_wanted` / `def_wanted` / `instance_wanted` can use it via typeclass synth
without an explicit `❰…❱` reference — matching the auto-availability of regular `instance`
declarations.

Inclusion is **on use** (like `variable [inst]`): a later declaration carries a `[d_…]` binder
for an earlier `instance_wanted` only when its statement or body actually uses it. A declaration
that does
not need the instance does not carry it, so unrelated instances do not accumulate as a file grows.
The registration is **module-scoped and order-sensitive**: only `instance_wanted`s declared earlier
in the current file are candidates. Registrations persist across `section` / `namespace` boundaries
within the file and are dropped at module boundaries (the placeholder defs are `private`, so
nothing propagates to importers).

Typical usage:
```
def_wanted Jacobian (C : Over (Spec (.of k))) [IsProper C.hom] : Over (Spec (.of k))

instance_wanted : GrpObj (❰Jacobian❱ C)

theorem_wanted comp_ofCurve … : … = η[❰Jacobian❱ C]
  -- automatically picks up the GrpObj instance, no haveI needed
```
 -/
instance_wanted : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
/-- If `F : C ⥤ D` is dense at `Y : D`, then it is also at `Y'`
if `Y` and `Y'` are isomorphic.  -/
CategoryTheory.Functor.DenseAt.ofIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} → {Y : D} → F.DenseAt Y → {Y' : D} → (Y ≅ Y') → F.DenseAt Y'
-- Init.Omega.Constraint
Option.merge.eq_4 : ∀ {α : Type u_1} (fn : α → α → α) (x_2 y : α), Option.merge fn (some x_2) (some y) = some (fn x_2 y)
-- Lean.DocString.Syntax
Lean.Doc.Syntax.metadataContents : Lean.Parser.Parser
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_multiplicative : ∀ {G : Type u_1} [inst : AddMonoid G], Monoid.exponent (Multiplicative G) = AddMonoid.exponent G
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π_assoc : ∀ (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.HasEnrichedHom V F₁ F₂] (τ : F₁ ⟶ F₂) (j : J) {Z : V}
  (h : (F₁.obj j ⟶[V] F₂.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) τ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (τ.app j)) h
-- Mathlib.Topology.Sequences
/-- Every first-countable space is a Fréchet-Urysohn space.  -/
FirstCountableTopology.frechetUrysohnSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FirstCountableTopology X], FrechetUrysohnSpace X
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_le_neg_one_of_neg : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : ℤ}, a < 0 → ↑a ≤ -1
-- Init.Data.Array.Lemmas
Array.forall_mem_ne' : ∀ {α : Type u_1} {a : α} {xs : Array α}, (∀ a' ∈ xs, ¬a' = a) ↔ a ∉ xs
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instAddMonoidWithOne : {α : Type u_1} → [AddMonoidWithOne α] → AddMonoidWithOne (WithZero α)
-- Std.Data.HashMap.Basic
/-- Returns a list of all keys present in the hash map in some order.  -/
Std.HashMap.keys : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → List α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_of_mul_self_lt_mul_self₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀],
  0 ≤ b → a * a < b * b → a < b
-- Mathlib.LinearAlgebra.StdBasis
/-- The natural linear equivalence: `Mⁱ ≃ Hom(Rⁱ, M)` for an `R`-module `M`.  -/
Module.piEquiv : (ι : Type u_1) →
  (R : Type u_2) →
    (M : Type u_3) →
      [Finite ι] →
        [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (ι → M) ≃ₗ[R] (ι → R) →ₗ[R] M
-- Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Determinant.Ctx.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)}
  (cα : Mathlib.Tactic.Ring.Common.Cache (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα))
  (rc :
    Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.RatCoeff
      (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα))
  (dimension : ℕ) (dimensionLit : Q(ℕ)) (arrayExpr : Q(Array «$α»)) (arrayEntries : Array Q(«$α»))
  (cα_1 : Mathlib.Tactic.Ring.Common.Cache (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα))
  (rc_1 :
    Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.RatCoeff
      (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα))
  (dimension_1 : ℕ) (dimensionLit_1 : Q(ℕ)) (arrayExpr_1 : Q(Array «$α»)) (arrayEntries_1 : Array Q(«$α»)),
  ({ cα := cα, rc := rc, dimension := dimension, dimensionLit := dimensionLit, arrayExpr := arrayExpr,
        arrayEntries := arrayEntries } =
      { cα := cα_1, rc := rc_1, dimension := dimension_1, dimensionLit := dimensionLit_1, arrayExpr := arrayExpr_1,
        arrayEntries := arrayEntries_1 }) =
    (cα = cα_1 ∧
      rc = rc_1 ∧
        dimension = dimension_1 ∧
          dimensionLit = dimensionLit_1 ∧ arrayExpr = arrayExpr_1 ∧ arrayEntries = arrayEntries_1)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- A twisted version of the relation `Λ * ↑ζ = log` in terms of complex sequences.  -/
DirichletCharacter.convolution_twist_vonMangoldt : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N),
  (LSeries.convolution ((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.vonMangoldt n)) fun n => χ ↑n) =
    (fun n => χ ↑n) * fun n => Complex.log ↑n
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedSnapshot.mk : Lean.Language.Snapshot →
  Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf →
    Lean.Parser.InputContext →
      Lean.Syntax → Option Lean.Language.Lean.HeaderParsedState → Lean.Language.Lean.HeaderParsedSnapshot
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- The product of two functions of temperate growth is again of temperate growth.

Version for bilinear maps.  -/
ContinuousLinearMap.bilinear_hasTemperateGrowth : ∀ {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [inst_6 : NormedAddCommGroup D] [inst_7 : NormedSpace ℝ D]
  [inst_8 : NormedAddCommGroup G] [inst_9 : NormedSpace ℝ G] [inst_10 : NormedSpace 𝕜 F] [inst_11 : NormedSpace 𝕜 G]
  [inst_12 : NormedSpace 𝕜 E] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth fun x => (B (f x)) (g x)
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The structure presheaf, valued in `ModuleCat`, constructed by dressing up the `Type`-valued
structure presheaf.  -/
AlgebraicGeometry.structurePresheafInModuleCat : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] → [Module R M] → TopCat.Presheaf (ModuleCat R) (AlgebraicGeometry.PrimeSpectrum.Top R)
-- Init.GrindInstances.ToInt
Lean.Grind.ToInt.toInt.eq_1 : ∀ (α : Type u) {range : Lean.Grind.IntInterval} [self : Lean.Grind.ToInt α range], Lean.Grind.ToInt.toInt = self.1
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.OrdSet.set : {α : Type} → [inst : Hashable α] → [inst_1 : BEq α] → Lean.Meta.Try.Collector.OrdSet α → Std.HashSet α
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.rightUnitorNatIsoCat_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitorNatIsoCat a b).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.rightUnitor X).hom
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasStrictDerivAt_abs : ∀ {x : ℝ}, x ≠ 0 → HasStrictDerivAt (fun x => |x|) (↑(SignType.sign x)) x
-- Mathlib.Algebra.Module.NatInt
DistribSMul.toAddMonoidHom_eq_zsmulAddGroupHom : ∀ (M : Type u_3) [inst : AddCommGroup M], DistribSMul.toAddMonoidHom M = zsmulAddGroupHom
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.rTensor_zero : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U}, Representation.IntertwiningMap.rTensor ρ 0 = 0
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix₂_eq_partialExtrinsicFix : ∀ {α : Sort u_2} {β : α → Sort u_3} {C₂ : (a : α) → β a → Sort u_1} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
  {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b} {a : α} {b : β a},
  Acc R ⟨a, b⟩ →
    WellFounded.partialExtrinsicFix₂ R F a b =
      WellFounded.partialExtrinsicFix R (fun p r => F p.fst p.snd fun a' b' hR => r ⟨a', b'⟩ hR) ⟨a, b⟩
-- Mathlib.Combinatorics.Configuration
Configuration.Nondegenerate.exists_line : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.Nondegenerate P L] (p : P), ∃ l, p ∉ l
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_symm_map_eval : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (M : Polynomial (Matrix n n R)) (r : R),
  (matPolyEquiv.symm M).map (Polynomial.eval r) = Polynomial.eval ((Matrix.scalar n) r) M
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Like `MonoidWithZero.toMulActionWithZero`, but multiplies on the right. See also
`Semiring.toOppositeModule`  -/
MonoidWithZero.toOppositeMulActionWithZero : (M₀ : Type u_2) → [inst : MonoidWithZero M₀] → MulActionWithZero M₀ᵐᵒᵖ M₀
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.dualBasis_coord_toDualEquiv_apply : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι] (i : ι) (f : M),
  (b.dualBasis.coord i) (b.toDualEquiv f) = (b.coord i) f
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.module.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.MellinTransform
/-- If `f` is locally integrable, decays exponentially at infinity, and is `O(x ^ (-b))` at 0, then
its Mellin transform converges for `b < s.re`.  -/
mellinConvergent_of_isBigO_rpow_exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ},
  0 < a →
    ∀ {f : ℝ → E} {s : ℂ},
      MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
        (f =O[Filter.atTop] fun t => Real.exp (-a * t)) →
          (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → b < s.re → MellinConvergent f s
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.w_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ),
  FermatLastTheoremForThreeGen.Solution'.c✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) =
    (hζ.toInteger - 1) ^ FermatLastTheoremForThreeGen.Solution.multiplicity✝ S *
      FermatLastTheoremForThreeGen.Solution.w✝ S
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSMul'.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α], Colex.instSMul' = inst