mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Closeds
IsUniformInducing.compacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}
  (hf : IsUniformInducing f), IsUniformInducing (TopologicalSpace.Compacts.map f ⋯)
-- Lean.Parser.Do
Lean.Parser.Term.optMetaFalse.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- Transfer preservation of finite colimits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.preservesFiniteColimits_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.Limits.PreservesFiniteColimits G
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.apply_le_nfpFamily : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι] [hι : Nonempty ι],
  (∀ (i : ι), Order.IsNormal (f i)) →
    ∀ {a b : Ordinal.{u}}, (∀ (i : ι), f i b ≤ Ordinal.nfpFamily f a) ↔ b ≤ Ordinal.nfpFamily f a
-- Lean.Parser.Extra
Lean.Parser.ppRealGroup.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Init.Grind.Util
/-- Gadget for protecting lambda abstractions created by `abstractGroundMismatches?`
from beta reduction during preprocessing. See `ProveEq.lean` for details.
 -/
Lean.Grind.abstractFn : {α : Sort u} → α → α
-- Mathlib.Algebra.Polynomial.SpecificDegree
Polynomial.irreducible_of_degree_le_three_of_not_isRoot : ∀ {K : Type u_1} [inst : Field K] {p : Polynomial K},
  p.natDegree ∈ Finset.Icc 1 3 → (∀ (x : K), ¬p.IsRoot x) → Irreducible p
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- Finitely presented additive groups are closed under additive isomorphism.  -/
AddGroup.IsFinitelyPresented.equiv : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (iso : G ≃+ H)
  [h : AddGroup.IsFinitelyPresented G], AddGroup.IsFinitelyPresented H
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.aevalDifferential_single : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ] [inst_4 : DecidableEq σ] (i j : σ),
  P.aevalDifferential (Pi.single i 1) j = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))
-- Mathlib.Data.Sigma.Lex
PSigma.Lex.mono : ∀ {ι : Sort u_1} {α : ι → Sort u_2} {r₁ r₂ : ι → ι → Prop} {s₁ s₂ : (i : ι) → α i → α i → Prop},
  (∀ (a b : ι), r₁ a b → r₂ a b) →
    (∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) → ∀ {a b : (i : ι) ×' α i}, PSigma.Lex r₁ s₁ a b → PSigma.Lex r₂ s₂ a b
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.toUniformSpace_eq : ∀ (R : Type u) [inst : Ring R] (Γ₀ : Type v) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
  _i.toUniformSpace = IsTopologicalAddGroup.rightUniformSpace R
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Pretty-prints a `forall` similarly to `delabForall`, but explicitly denotes all named parameters.
 -/
Lean.PrettyPrinter.Delaborator.delabForallWithSignature : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Grind.Order
Lean.Grind.Order.eq_trans_false : ∀ {p q : Prop}, p = q → q = False → p = False
-- Mathlib.Condensed.Light.Basic
/-- `LightCondensed.{u} C` is the category of light condensed objects in a category `C`, which are
defined as sheaves on `LightProfinite.{u}` with respect to the coherent Grothendieck topology.
 -/
LightCondensed : (C : Type w) → [CategoryTheory.Category.{v, w} C] → Type (max (max (max w v) (u + 1)) u)
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.str.inj : ∀ {s s_1 : String}, Lean.JsonRpc.RequestID.str s = Lean.JsonRpc.RequestID.str s_1 → s = s_1
-- Mathlib.Data.Finsupp.Interval
Finsupp.card_Ioo : ∀ {ι : Type u_1} {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] [inst_4 : DecidableEq α] (f g : ι →₀ α),
  (Finset.Ioo f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 2
-- Mathlib.GroupTheory.ArchimedeanDensely
instLocallyFiniteOrderUnitsWithZero : {X : Type u_2} → [inst : Preorder X] → [LocallyFiniteOrder X] → [inst_2 : Group X] → LocallyFiniteOrder (WithZero X)ˣ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The natural transformation `t.truncGELT a b ≅ t.truncLTGE a b`.  -/
CategoryTheory.Triangulated.TStructure.truncGELTIsoLTGE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                [CategoryTheory.IsTriangulated C] → (a b : ℤ) → t.truncGELT a b ≅ t.truncLTGE a b
-- Init.Control.StateCps
StateCpsT.instLawfulMonad : ∀ {σ : Type u} {m : Type u → Type v}, LawfulMonad (StateCpsT σ m)
-- Std.Time.Time.HourMarker
Std.Time.HourMarker.pm.sizeOf_spec : sizeOf Std.Time.HourMarker.pm = 1
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The morphism `F ⟶ K.pathObject` that is induced by two morphisms `φ₀ φ₁ : F ⟶ K`
and a homotopy `h : Homotopy φ₀ φ₁`.  -/
HomologicalComplex.pathObject.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          {F K : HomologicalComplex C c} →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasPathObject] → (φ₀ φ₁ : F ⟶ K) → Homotopy φ₀ φ₁ → (F ⟶ K.pathObject)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_apply : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (i j : n), (LinearMap.BilinForm.toMatrix b) B i j = (B (b i)) (b j)
-- Lean.Data.Trie
/-- Returns all values whose key have the given string `pre` as a prefix, in no particular order.  -/
Lean.Data.Trie.findPrefix : {α : Type} → Lean.Data.Trie α → String → Array α
-- Mathlib.Analysis.Real.Sqrt
/-- **Alias** of the reverse direction of `Real.sqrt_pos`. -/
Real.sqrt_pos_of_pos : ∀ {x : ℝ}, 0 < x → 0 < √x
-- Std.Time.Date.PlainDate
/-- Returns the week number within the week-based year for the given `PlainDate`, using `firstDay` as
the start of the week and `minDays` as the minimum number of days required in the first week of the
year (default 4 for ISO 8601). Dates before the first week of the calendar year are counted as part
of the last week of the previous year.
 -/
Std.Time.PlainDate.weekOfYear : Std.Time.PlainDate →
  optParam Std.Time.Weekday Std.Time.Weekday.monday →
    optParam (Std.Time.Internal.Bounded.LE 0 6)
        (Std.Time.Internal.Bounded.LE.mk 4 Std.Time.PlainDate.weekOfYear._proof_1) →
      Std.Time.Week.OfYear.Ordinal
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- Functor translating a commutative monoid object in a functor category
to a functor into the category of commutative monoid objects.
 -/
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.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] →
          [inst_3 : CategoryTheory.BraidedCategory D] →
            CategoryTheory.Functor (CategoryTheory.CommMon (CategoryTheory.Functor C D))
              (CategoryTheory.Functor C (CategoryTheory.CommMon D))
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (property : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' property
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_add : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, Order.IsSuccLimit b → Order.IsSuccLimit (a + b)
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Given a matrix (row-major) of strings, arranges them in tabular form.
First column is left-aligned, others right-aligned.
Single space as column separator.
 -/
Lean.Elab.WF.GuessLex.formatTable : Array (Array String) → String
-- Init.Control.Except
/-- Sequences two operations that may throw exceptions, allowing the second to depend on the value
returned by the first.

If the first operation throws an exception, then it is the result of the computation. If the first
succeeds but the second throws an exception, then that exception is the result. If both succeed,
then the result is the result of the second computation.

This is the implementation of the `>>=` operator for `Except ε`.
 -/
Except.bind : {ε : Type u} → {α : Type u_1} → {β : Type u_2} → Except ε α → (α → Except ε β) → Except ε β
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_mul_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionRing α] {p q : ℚ}, ↑p.den ≠ 0 → ↑q.den ≠ 0 → ↑(p * q) = ↑p * ↑q
-- Std.Data.HashSet.Lemmas
Std.HashSet.any_eq_not_all_not : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {p : α → Bool}, m.any p = !m.all fun a => !p a
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instFourierInvSMul : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F], FourierInvSMul ℂ (TemperedDistribution E F) (TemperedDistribution E F)
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.eraseIdx.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (a : α) (as : List α) (n : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match a :: as, n.succ with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_3 a as n
-- Mathlib.Algebra.BigOperators.Finprod
/-- The sum of any function over an empty set is `0`.  -/
finsum_mem_empty : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M}, ∑ᶠ (i : α) (_ : i ∈ ∅), f i = 0
-- Mathlib.Topology.Category.TopPair
TopPair.ofHom.congr_simp : ∀ {X Y : TopPair} (f f_1 : TopPair.fst ⟶ TopPair.fst) (e_f : f = f_1) (g g_1 : TopPair.snd ⟶ TopPair.snd)
  (e_g : g = g_1)
  (w : CategoryTheory.CategoryStruct.comp g TopPair.map = CategoryTheory.CategoryStruct.comp TopPair.map f),
  TopPair.ofHom f g w = TopPair.ofHom f_1 g_1 ⋯
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_centralizer : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A] (s : Set A),
  ↑(NonUnitalStarSubalgebra.centralizer R s) = (s ∪ star s).centralizer
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rcc α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- More flexible variant of `SheafOfModules.pushforwardNatIso`.  -/
SheafOfModules.pushforwardCongr₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F G : CategoryTheory.Functor C D} →
              {T : CategoryTheory.Sheaf J RingCat} →
                {S : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    [inst_3 : G.IsContinuous J K] →
                      (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) →
                        {ψ : T ⟶ (F.sheafPushforwardContinuous RingCat J K).obj S} →
                          (e : F ≅ G) →
                            CategoryTheory.CategoryStruct.comp φ
                                  ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans e.hom RingCat J K).app
                                    S) =
                                ψ →
                              (SheafOfModules.pushforward φ ≅ SheafOfModules.pushforward ψ)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_eq_iInf : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset α) (f : α → β), s.inf f = ⨅ a ∈ s, f a
-- Init.Data.Nat.Lemmas
Nat.one_le_div_iff : ∀ {a b : ℕ}, 0 < b → (1 ≤ a / b ↔ b ≤ a)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.orbitRel_of_subAdd : ∀ {R : Type u} {M : Type v} [inst : AddGroup R] [inst_1 : AddAction R M] (p : SubAddAction R M),
  AddAction.orbitRel R ↥p = Setoid.comap Subtype.val (AddAction.orbitRel R M)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCocircuit.nonempty : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCocircuit C → C.Nonempty
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- When `F : C ⥤ D` is an additive functor, this is
the functor `C ⥤ HomotopyCategory D (ComplexShape.up ℕ)` which
sends `X : C` to `F` applied to an injective resolution of `X`.  -/
CategoryTheory.Functor.rightDerivedToHomotopyCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [CategoryTheory.HasInjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) →
                [F.Additive] → CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.up ℕ))
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAdd : {α : Type u_1} → [Add α] → Add αᵒᵈ
-- Mathlib.NumberTheory.Modular
/-- This replaces `(g•z).re = a/c + *` in the standard theory with the following novel identity:
`g • z = (a c + b d) / (c^2 + d^2) + (d z - c) / ((c^2 + d^2) (c z + d))`
which does not need to be decomposed depending on whether `c = 0`.  -/
ModularGroup.smul_eq_lcRow0_add : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} (z : UpperHalfPlane) {p : Fin 2 → ℤ},
  IsCoprime (p 0) (p 1) →
    ↑g 1 = p →
      ↑(g • z) =
        ↑((ModularGroup.lcRow0 p) ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) /
            (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
          (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
-- Init.Classical
Classical.not_and_iff_not_or_not : ∀ {a b : Prop}, ¬(a ∧ b) ↔ ¬a ∨ ¬b
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.edist_single_same : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b₁ b₂ : β i),
  edist (PiLp.single p i b₁) (PiLp.single p i b₂) = edist b₁ b₂
-- Mathlib.Analysis.Real.Pi.Wallis
Real.Wallis.W.eq_1 : ∀ (k : ℕ), Real.Wallis.W k = ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebung_injective : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [hp : Fact (Nat.Prime p)], Function.Injective ⇑WittVector.verschiebung
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Surjective.sigmaDesc_of_union_range_eq_univ : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type v} [inst : Small.{u, v} ι] {Y : ι → AlgebraicGeometry.Scheme}
  {f : (i : ι) → Y i ⟶ X},
  ⋃ i, Set.range ⇑(f i) = Set.univ → AlgebraicGeometry.Surjective (CategoryTheory.Limits.Sigma.desc f)
-- Mathlib.RingTheory.Noetherian.Defs
/-- A ring is Noetherian if and only if all its ideals are finitely-generated.  -/
isNoetherianRing_iff_ideal_fg : ∀ (R : Type u_1) [inst : Semiring R], IsNoetherianRing R ↔ ∀ (I : Ideal R), I.FG
-- Init.Prelude
/-- A type with a zero element.  -/
Zero : Type u → Type u
-- Mathlib.Tactic.Widget.Conv
/-- Given a `path : Path` and ```xs : TSepArray ``enterArg ","```, generate the `conv` syntax
corresponding to `enter [xs,*]` followed by traversing `path`. If `loc` is `some fvar`,
start with `conv at fvar =>`, otherwise if `loc` is `none` start with `conv =>`.
 -/
Mathlib.Tactic.Conv.pathToStx : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadQuotation m] →
      Lean.TSyntax `conv →
        Mathlib.Tactic.Conv.Path →
          Option Lean.Name →
            optParam (Lean.Syntax.TSepArray `Lean.Parser.Tactic.Conv.enterArg ",") ∅ → m (Lean.TSyntax `tactic)
-- Mathlib.LinearAlgebra.Ray
/-- `SameRay` is reflexive.  -/
SameRay.refl : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (x : M), SameRay R x x
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.isInt_jacobiSymNat : ∀ {a na b nb : ℕ} {r : ℤ},
  Mathlib.Meta.NormNum.IsNat a na →
    Mathlib.Meta.NormNum.IsNat b nb →
      Mathlib.Meta.NormNum.jacobiSymNat na nb = r → Mathlib.Meta.NormNum.IsInt (Mathlib.Meta.NormNum.jacobiSymNat a b) r
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_eq_iInf_measure_of_subsingleton : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [Subsingleton 𝓧] [Nonempty 𝓨],
  ProbabilityTheory.bayesRisk ℓ P π =
    ⨅ μ,
      ⨅ (_ : MeasureTheory.IsProbabilityMeasure μ), ProbabilityTheory.avgRisk ℓ P (ProbabilityTheory.Kernel.const 𝓧 μ) π
-- Mathlib.CategoryTheory.Shift.Basic
/-- When `i + j = 0`, shifting by `i` and by `j` gives the identity functor  -/
CategoryTheory.shiftFunctorCompIsoId : (C : Type u) →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (i j : A) →
            i + j = 0 →
              ((CategoryTheory.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C j) ≅ CategoryTheory.Functor.id C)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.saveSymbol : Lean.HeadIndex → Lean.Meta.Grind.NormalizePattern.M✝ Unit
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.preimageIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} [inst_2 : F.Full] [inst_3 : F.Faithful] (f : F.obj X ≅ F.obj Y),
  (F.preimageIso f).inv = F.preimage f.inv
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.isoImage_ι_inv_ι : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage U.ι V).inv V.ι = X.homOfLE ⋯
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.superset : ∀ {α : Type u} {g : Set (Set α)} {s t : Set α}, Filter.GenerateSets g s → s ⊆ t → Filter.GenerateSets g t
-- Init.Data.SInt.Lemmas
Int32.neg_ofNat : ∀ {n : ℕ}, -Int32.ofNat n = Int32.ofInt (-↑n)
-- Mathlib.Order.RelSeries
not_finiteDimensionalOrder_iff : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], ¬FiniteDimensionalOrder α ↔ InfiniteDimensionalOrder α
-- Mathlib.CategoryTheory.Limits.ColimitLimit
CategoryTheory.Limits.map_id_right_eq_curry_swap_map : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) {j j' : J}
  {f : j ⟶ j'} {k : K},
  F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id k)) =
    ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k).map f
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.insertMany_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {ρ : Type w}
  [inst_2 : ForIn Id ρ ((a : α) × β a)] {l : ρ}, m.insertMany l = ↑↑(Std.DHashMap.Internal.Raw₀.insertMany ⟨m, ⋯⟩ l)
-- Mathlib.Order.Preorder.Chain
isChain_of_trichotomous : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Trichotomous r] (s : Set α), IsChain r s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_3.eq_4 : ∀ (motive : Std.Tactic.BVDecide.Gate → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.Gate.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.Gate.xor) (h_3 : Unit → motive Std.Tactic.BVDecide.Gate.beq)
  (h_4 : Unit → motive Std.Tactic.BVDecide.Gate.or),
  (match Std.Tactic.BVDecide.Gate.or with
    | Std.Tactic.BVDecide.Gate.and => h_1 ()
    | Std.Tactic.BVDecide.Gate.xor => h_2 ()
    | Std.Tactic.BVDecide.Gate.beq => h_3 ()
    | Std.Tactic.BVDecide.Gate.or => h_4 ()) =
    h_4 ()
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_iff_ofNNReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → NNReal},
  MeasureTheory.HasFiniteIntegral (fun x => ↑(f x)) μ ↔ ∫⁻ (a : α), ↑(f a) ∂μ < ⊤
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- Open immersions are stable under base-change.  -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_snd_of_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.refl_apply : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A] (x : A), (BialgEquiv.refl R A) x = x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- If `f` is majorized with exponent `exp₁`, then it is majorized with any `exp₂ ≥ exp₁`.  -/
Tactic.ComputeAsymptotics.Majorized.of_le : ∀ {f b : ℝ → ℝ} {exp1 exp2 : ℝ},
  exp1 ≤ exp2 → Tactic.ComputeAsymptotics.Majorized f b exp1 → Tactic.ComputeAsymptotics.Majorized f b exp2
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instNoZeroDivisors : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [NoZeroDivisors α], NoZeroDivisors (WithTop α)