mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.single_nonneg : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : DecidableEq X] [inst_2 : Zero Y]
  [inst_3 : Preorder Y] {x : X} {y : Y}, 0 ≤ Function.locallyFinsuppWithin.single x y ↔ 0 ≤ y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edges_ofDarts : ∀ {V : Type u} {G : SimpleGraph V} {l : List G.Dart} (hne : l ≠ []) (hchain : List.IsChain G.DartAdj l),
  (SimpleGraph.Walk.ofDarts l hne hchain).edges = List.map SimpleGraph.Dart.edge l
-- Batteries.Control.ForInStep.Lemmas
ForInStep.bindList_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β))
  (s : ForInStep β), ForInStep.bindList f [] s = pure s
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.subset_closedBall_norm : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [NormOneClass A] (a : A), spectrum 𝕜 a ⊆ Metric.closedBall 0 ‖a‖
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRooSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRooSlice._auto_1) →
      Std.Roo.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RooSlice α β)
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_mulSupport : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {f : α → M}, (Function.mulSupport f).mulIndicator f = f
-- Lean.Server.Rpc.Basic
/-- The RPC wire format to follow.  -/
Lean.Server.RpcObjectStore.wireFormat : Lean.Server.RpcObjectStore → Lean.Lsp.RpcWireFormat
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.multisetSum_zero : ∀ {n : ℤ} {s : Multiset ℤ}, (∀ x ∈ s, x ≡ 0 [ZMOD n]) → s.sum ≡ 0 [ZMOD n]
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {l : List α} {k : α}, k ∈ t → (t.insertMany l).get! k = t.get! k
-- Mathlib.Topology.EMetricSpace.Weak
/-- If `some : α → Option α` is an open embedding and `α` is has a weak pseudo extended metric
structure, the structure extends naturally to `Option α`.  -/
Option.WeakEMetricSpace.OfIsOpenEmbedding : {α : Type u} →
  [t : TopologicalSpace α] →
    [inst : TopologicalSpace (Option α)] →
      [m : WeakEMetricSpace α] →
        [inst_1 : EDist (Option α)] →
          inst_1 = Option.toEDist → Topology.IsOpenEmbedding some → WeakEMetricSpace (Option α)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.below.cons : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive : (a a_1 : s.Pos) → String.Slice.Pattern.Model.IsLongestMatchAtChain pat a a_1 → Prop}
  (startPos middlePos endPos : s.Pos) (a : String.Slice.Pattern.Model.IsLongestMatchAt pat startPos middlePos)
  (a_1 : String.Slice.Pattern.Model.IsLongestMatchAtChain pat middlePos endPos),
  String.Slice.Pattern.Model.IsLongestMatchAtChain.below a_1 →
    motive middlePos endPos a_1 → String.Slice.Pattern.Model.IsLongestMatchAtChain.below ⋯
-- Std.Time.Zoned.TimeZone
/-- Day light saving flag.
 -/
Std.Time.TimeZone.isDST : Std.Time.TimeZone → Bool
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isEncodedChar.eq_1 : ∀ (rule : UInt8 → Bool) (c : UInt8),
  Std.Http.URI.isEncodedChar rule c =
    decide
      (Std.Http.Internal.Char.isAsciiByte c = true ∧
        (rule c = true ∨ Std.Http.Internal.Char.isHexDigitByte c = true ∨ c = '%'.toUInt8))
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_multiset_count : ∀ {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq M] (s : Multiset M),
  s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a subtraction monoid under pointwise operations if `α` is.  -/
Filter.subtractionMonoid : {α : Type u_2} → [SubtractionMonoid α] → SubtractionMonoid (Filter α)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Icc_succ_top : ∀ {M : Type u_3} [inst : CommMonoid M] {a b : ℕ},
  a ≤ b + 1 → ∀ (f : ℕ → M), ∏ k ∈ Finset.Icc a (b + 1), f k = (∏ k ∈ Finset.Icc a b, f k) * f (b + 1)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.C_off_diag_nonpos : ∀ (n : ℕ) (i j : Fin n), i ≠ j → CartanMatrix.C n i j ≤ 0
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isField_of_isDomain : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R] [IsDomain R], IsField R
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.ofSubsingleton.congr_simp : ∀ (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : TopologicalSpace M₂]
  [inst_6 : TopologicalSpace M₃] [inst_7 : Subsingleton ι] (i i_1 : ι),
  i = i_1 → ContinuousMultilinearMap.ofSubsingleton R M₂ M₃ i = ContinuousMultilinearMap.ofSubsingleton R M₂ M₃ i_1
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.HalfBraiding.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {X : C}
  {β :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X}
  {monoidal :
    autoParam
      (∀ (U U' : C),
        (β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam}
  {naturality :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β U').hom =
          CategoryTheory.CategoryStruct.comp (β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam}
  {β_1 :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X}
  {monoidal_1 :
    autoParam
      (∀ (U U' : C),
        (β_1 (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_1 U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β_1 U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam}
  {naturality_1 :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_1 U').hom =
          CategoryTheory.CategoryStruct.comp (β_1 U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam},
  { β := β, monoidal := monoidal, naturality := naturality } =
      { β := β_1, monoidal := monoidal_1, naturality := naturality_1 } →
    β = β_1
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.pos : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Lattice E] [ContinuousSup E] [HasSolidNorm E]
  [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {f : ι → Ω → E},
  MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Submartingale f⁺ ℱ μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon.go.eq_1 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (k_1 : ℤ),
  Lean.Grind.CommRing.Poly.mulMon.go k m (Lean.Grind.CommRing.Poly.num k_1) =
    bif k_1 == 0 then Lean.Grind.CommRing.Poly.num 0
    else Lean.Grind.CommRing.Poly.add (k * k_1) m (Lean.Grind.CommRing.Poly.num 0)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.andthen : Lean.ParseImports.Parser → Lean.ParseImports.Parser → Lean.ParseImports.Parser
-- Lean.Server.Rpc.Basic
Lean.Server.RpcObjectStore.mk.injEq : ∀ (aliveRefs : Lean.PersistentHashMap Lean.Lsp.RpcRef Lean.Server.ReferencedObject)
  (refsById : Lean.PersistentHashMap USize Lean.Lsp.RpcRef) (nextRef : USize) (wireFormat : Lean.Lsp.RpcWireFormat)
  (aliveRefs_1 : Lean.PersistentHashMap Lean.Lsp.RpcRef Lean.Server.ReferencedObject)
  (refsById_1 : Lean.PersistentHashMap USize Lean.Lsp.RpcRef) (nextRef_1 : USize)
  (wireFormat_1 : Lean.Lsp.RpcWireFormat),
  ({ aliveRefs := aliveRefs, refsById := refsById, nextRef := nextRef, wireFormat := wireFormat } =
      { aliveRefs := aliveRefs_1, refsById := refsById_1, nextRef := nextRef_1, wireFormat := wireFormat_1 }) =
    (aliveRefs = aliveRefs_1 ∧ refsById = refsById_1 ∧ nextRef = nextRef_1 ∧ wireFormat = wireFormat_1)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- Given a functor `F` and a collection of colimit cocones for each diagram `X ↦ F X k`, we can stitch
them together to give a cocone for the diagram `F`.
`combinedIsColimit` shows that the new cocone is colimiting, and `evalCombined` shows it is
(essentially) made up of the original cocones.
 -/
CategoryTheory.Limits.combineCocones : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              ((k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) → CategoryTheory.Limits.Cocone F
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.isCyclotomicExtension_zero_iff : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  IsCyclotomicExtension {0} A B ↔ Function.Surjective ⇑(algebraMap A B)
-- Init.Data.Ord.Basic
Ordering.isEq_lt : Ordering.lt.isEq = false
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig.decls.size),
  (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig.decls[idx] = aig.decls[idx]
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul : Option Lean.Expr →
  Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.norm_fourier_toBoundedContinuousFunction_le_toLp_one : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] (f : SchwartzMap V F),
  ‖(FourierTransform.fourier f).toBoundedContinuousFunction‖ ≤ ‖f.toLp 1 MeasureTheory.volume‖
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.congr_of_mem : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → (∀ y ∈ s, f₁ y = f y) → x ∈ s → MDiffAt[s] f₁ x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentSymbolParams.toJson : Lean.Lsp.DocumentSymbolParams → Lean.Json
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.image_Ioc_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictMonoOn f (Set.Icc a b) → f '' Set.Ioc a b ⊆ Set.Ioc (f a) (f b)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.map.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (sz : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α),
  Ordnode.map f (Ordnode.node sz l x_1 r) = Ordnode.node sz (Ordnode.map f l) (f x_1) (Ordnode.map f r)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_smul : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] [IsScalarTower S R R] (s : S)
  (p : Polynomial R) (k : ℕ), (⇑Polynomial.derivative)^[k] (s • p) = s • (⇑Polynomial.derivative)^[k] p
-- Lean.Meta.Tactic.Grind.Extension
/-- Contains all symbols used in the term `f` at the theorem's conclusion: `Function.Injective f`.  -/
Lean.Meta.Grind.InjectiveTheorem.symbols : Lean.Meta.Grind.InjectiveTheorem → List Lean.HeadIndex
-- Mathlib.Data.Finset.NAry
Finset.card_image₂_singleton_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α) {b : β},
  (Function.Injective fun a => f a b) → (Finset.image₂ f s {b}).card = s.card
-- Lean.Data.Options
Lean.getOptionDecls : IO Lean.OptionDecls
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.State.mk.inj : ∀ {set set_1 : Lean.PHashSet Lean.Meta.Sym.AlphaKey}, { set := set } = { set := set_1 } → set = set_1
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.edist_approxOn_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α}
  (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s] (x : β) {m n : ℕ},
  m ≤ n →
    edist ((MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) (f x) ≤
      edist ((MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ m) x) (f x)
-- Mathlib.NumberTheory.LSeries.PrimesInAP
_private.Mathlib.NumberTheory.LSeries.PrimesInAP.0.ArithmeticFunction.vonMangoldt.summable_F'' : Summable ArithmeticFunction.vonMangoldt.F''✝
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.eval_eq_sum_range : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (x : R),
  Polynomial.eval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GMonoid.toGMul : {ι : Type u_1} → {A : ι → Type u_2} → {inst : AddMonoid ι} → [self : GradedMonoid.GMonoid A] → GradedMonoid.GMul A
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul.go : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertMany_append : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {l₁ l₂ : List (α × β)},
  Std.DHashMap.Const.insertMany m (l₁ ++ l₂) = Std.DHashMap.Const.insertMany (Std.DHashMap.Const.insertMany m l₁) l₂
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.map_quotient_self : ∀ {R : Type u} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided], Ideal.map (Ideal.Quotient.mk I) I = ⊥
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- See `zero_lt_four` for a version with the type implicit.  -/
zero_lt_four' : ∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 4
-- Mathlib.Topology.Order.OrderClosed
OrderClosedTopology.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α], IsClosed {p | p.1 ≤ p.2} → OrderClosedTopology α
-- Init.Data.List.MinMaxIdx
List.isSome_maxIdxOn?_of_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} {x : α},
  x ∈ xs → (List.maxIdxOn? f xs).isSome = true
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
/-- Upper bound for `γ`. (The true value is about 0.57.)  -/
Real.eulerMascheroniConstant_lt_two_thirds : Real.eulerMascheroniConstant < 2 / 3
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.map_mk : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {d : ι} (g : 𝒜 →+*ᵍ ℬ) (f : A) (hf : f ∈ 𝒜 d)
  (n : ℕ) (x : A) (hx : x ∈ 𝒜 (n • d)),
  (HomogeneousLocalization.Away.map g f) (HomogeneousLocalization.Away.mk 𝒜 hf n x hx) =
    HomogeneousLocalization.Away.mk ℬ ⋯ n (g x) ⋯
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for positive exponents.  -/
Module.End.HasUnifEigenvalue.lt : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k m : ℕ∞}, 0 < m → f.HasUnifEigenvalue μ k → f.HasUnifEigenvalue μ m
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.Ind.isIndObject_inclusion_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Ind C),
  CategoryTheory.Limits.IsIndObject ((CategoryTheory.Ind.inclusion C).obj X)
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- If `χ` is a nontrivial quadratic Dirichlet character, then `L(χ, 1) ≠ 0`. This is private
since it is later superseded by `LFunction_apply_one_ne_zero`.  -/
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.LFunction_apply_one_ne_zero_of_quadratic : ∀ {N : ℕ} [inst : NeZero N] {χ : DirichletCharacter ℂ N}, χ ^ 2 = 1 → χ ≠ 1 → DirichletCharacter.LFunction χ 1 ≠ 0
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar_mono : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ K₂ : TopologicalSpace.Compacts G},
  ↑K₁ ⊆ ↑K₂ → MeasureTheory.Measure.haar.chaar K₀ K₁ ≤ MeasureTheory.Measure.haar.chaar K₀ K₂
-- Init.Grind.Attr
/-- The `←` modifier instructs `grind` to select a multi-pattern from the conclusion of theorem.
In other words, `grind` will use the theorem for backwards reasoning.
This may fail if not all of the arguments to the theorem appear in the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
Lean.Parser.Attr.grindBwd : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.biproduct.map_lift_mapBiprod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C)
  [inst_5 : CategoryTheory.Limits.HasBiproduct f] [inst_6 : CategoryTheory.Limits.PreservesBiproduct f F] {W : C}
  (g : (j : J) → W ⟶ f j),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.biproduct.lift g)) (F.mapBiproduct f).hom =
    CategoryTheory.Limits.biproduct.lift fun j => F.map (g j)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.instEquivLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Add α] → [inst_3 : Add β] → EquivLike (α ≃+o β) α β
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_eq_gcd_leadingCoeff_content_eraseLead : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R),
  p.content = gcd p.leadingCoeff p.eraseLead.content
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_zsmul : ∀ {M : Type u_10} {F : Type u_11} [inst : AddGroup M] [inst_1 : FunLike F M M] [AddMonoidHomClass F M M] (f : F) (n : ℕ)
  (x : M) (k : ℤ), (⇑f)^[n] (k • x) = k • (⇑f)^[n] x
-- Lean.LibrarySuggestions.SineQuaNon
/-- The state is just an array of array of maps.
We don't assemble these on import for efficiency reasons: most modules will not query this extension.

Instead, we use an `IO.Ref` below so that within each module we can assemble the global `NameMap (List (Name × Float))` once.

Since we never modify the extension state except on export, the `IO.Ref` does not need updating after first access.
 -/
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt : Lean.PersistentEnvExtension (Lean.NameMap (List (Lean.Name × Float))) Empty
  (Array (Array (Lean.NameMap (List (Lean.Name × Float)))))
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.objEquiv_toOrderHom_apply : ∀ {n i : ℕ} (x : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := i })) (j : Fin (i + 1)),
  (SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.objEquiv x)) j = x j
-- Aesop.Tree.Data
Aesop.MVarClusterData.mk.inj : ∀ {Goal Rapp : Type} {parent? : Option (IO.Ref Rapp)} {goals : Array (IO.Ref Goal)} {isIrrelevant : Bool}
  {state : Aesop.NodeState} {parent?_1 : Option (IO.Ref Rapp)} {goals_1 : Array (IO.Ref Goal)} {isIrrelevant_1 : Bool}
  {state_1 : Aesop.NodeState},
  { parent? := parent?, goals := goals, isIrrelevant := isIrrelevant, state := state } =
      { parent? := parent?_1, goals := goals_1, isIrrelevant := isIrrelevant_1, state := state_1 } →
    parent? = parent?_1 ∧ goals = goals_1 ∧ isIrrelevant = isIrrelevant_1 ∧ state = state_1
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₁ i₂ i₃ i₄ i₅ : ι}
  (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ),
  autoParam ((X.H n₂).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0)
      CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀._auto_5),
      CategoryTheory.IsIso
        (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed thickening is a closed set.  -/
Metric.isClosed_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {E : Set α}, IsClosed (Metric.cthickening δ E)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ ∪ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.conjTranspose_replicateRow : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Star α] (v : m → α),
  (Matrix.replicateRow ι v).conjTranspose = Matrix.replicateCol ι (star v)
-- Mathlib.Data.Rat.Lemmas
/-- A version of `Rat.mul_num` without division.  -/
Rat.num_mul_num_eq_num_mul_gcd : ∀ (q₁ q₂ : ℚ), q₁.num * q₂.num = (q₁ * q₂).num * ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))