mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_mul_lt_iff_lt_mul' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, c⁻¹ * a < b ↔ a < b * c
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The center is commutative and associative.

This is not an instance as it forms a non-defeq diamond with
`NonUnitalSubringClass.toNonUnitalRing` in the `npow` field.  -/
Subsemiring.center.commSemiring' : (R : Type u) → [inst : NonAssocSemiring R] → CommSemiring ↥(Subsemiring.center R)
-- Init.Data.Int.Basic
Int.ofNat.inj : ∀ {a a_1 : ℕ}, Int.ofNat a = Int.ofNat a_1 → a = a_1
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ofIsReflexivePair_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsReflexivePair f g],
  (CategoryTheory.Limits.ofIsReflexivePair f g).map CategoryTheory.Limits.WalkingReflexivePair.Hom.right = g
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.ofList.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (l : List (α × β)),
  Std.DHashMap.Raw.Const.ofList l = Std.DHashMap.Raw.Const.insertMany ∅ l
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.Is.prop : ∀ {C : Type u} {inst : CategoryTheory.CategoryStruct.{v, u} C} {P : CategoryTheory.ObjectProperty C} {X : C}
  [self : P.Is X], P X
-- Mathlib.Algebra.Module.Basic
Function.support_smul : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [IsDomain R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] (f : α → R) (g : α → M),
  Function.support (f • g) = Function.support f ∩ Function.support g
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_le_iff_le : ∀ {a b : BitVec 64}, { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b
-- Init.Core
/-- Left injection into the sum type `α ⊕' β`. -/
PSum.inl : {α : Sort u} → {β : Sort v} → α → α ⊕' β
-- Init.Data.Slice.List.Basic
/-- Returns a slice of a list with the given bounds.

If `start` or `stop` are not valid bounds for a sublist, then they are clamped to the list's length.
Additionally, the starting index is clamped to the ending index.

This function is linear in `start` because it stores `as.drop start` in the slice.
 -/
List.toSlice : {α : Type u} → List α → ℕ → ℕ → ListSlice α
-- Mathlib.FieldTheory.IsPerfectClosure
IsPRadical.pow_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ) [IsPRadical i p]
  (x : L), ∃ n y, i y = x ^ p ^ n
-- Mathlib.NumberTheory.RatFunc.Ostrowski
/-- The maximal ideal of `K[X]` generated by the `uniformizingPolynomial` for `v`.  -/
RatFunc.valuationIdeal : {K : Type u_1} →
  {Γ : Type u_2} →
    [inst : Field K] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ] →
        {v : Valuation (RatFunc K) Γ} →
          [v.IsNontrivial] →
            [Valuation.IsTrivialOn K v] → v RatFunc.X ≤ 1 → IsDedekindDomain.HeightOneSpectrum (Polynomial K)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂).get k h' = m₁.get k ⋯
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- For a prime `p`, a ℚ-linear combination `∑_{i < p} αᵢ ζⁱ` vanishes if and only if all
coefficients `αᵢ` are equal. This follows from the irreducibility of the `p`-th cyclotomic
polynomial. See de Launey–Flannery, *Algebraic Design Theory*, Lemma 2.8.5.  -/
IsPrimitiveRoot.sum_eq_zero_iff_forall_eq : ∀ {K : Type u_1} [inst : Field K] [CharZero K] {p : ℕ} {ζ : K},
  Nat.Prime p → IsPrimitiveRoot ζ p → ∀ (α : Fin p → ℚ), ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ ∀ (i j : Fin p), α i = α j
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.sub_mul_left_left_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime (x - y * z) y ↔ IsCoprime x y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eraseKey_of_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α},
  (k == a) = false → Std.Internal.List.getValue? a (Std.Internal.List.eraseKey k l) = Std.Internal.List.getValue? a l
-- Init.Data.UInt.Lemmas
UInt32.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < UInt32.size → b < UInt32.size → (UInt32.ofNat a < UInt32.ofNat b ↔ a < b)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} {ι : Sort u_3} (f : ι → ↥L),
  ↑(iSup f) = ⨆ i, ↑(f i)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.all_eq_true' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulBEq α] {p : α → β → Bool},
  (↑m).WF →
    ((↑m).all p = true ↔ ∀ (a : α) (h : m.contains a = true), p a (Std.DHashMap.Internal.Raw₀.Const.get m a h) = true)
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.List.applyId_cons : ∀ {α : Type u} [inst : DecidableEq α] (xs : List (α × α)) (x y z : α),
  Plausible.InjectiveFunction.List.applyId ((y, z) :: xs) x =
    if y = x then z else Plausible.InjectiveFunction.List.applyId xs x
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) →
      (x : Std.IterStep (Std.IterM m α) α) →
        ((it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out)) →
          ((it : Std.IterM m α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Algebra.GroupWithZero.Basic
zero_pow_eq : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] (n : ℕ), 0 ^ n = if n = 0 then 1 else 0
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Nat.xor.eq_1 : Nat.xor = Nat.bitwise bne
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_uniqueRingEquiv_symm : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : Subsingleton M] (r : R) (m : M),
  ((AddMonoidAlgebra.uniqueRingEquiv M).symm r).coeff m = r
-- Init.Data.Option.Lemmas
Option.ext : ∀ {α : Type u_1} {o₁ o₂ : Option α}, (∀ (a : α), o₁ = some a ↔ o₂ = some a) → o₁ = o₂
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfLocalizations_symm_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} {x : P},
  (f.addEquivOfLocalizations k).symm x = (k.lift ⋯) x
-- Mathlib.Tactic.FunProp.Theorems
/-- Get transition theorems applicable to `e`.

For example calling on `e` equal to `Continuous f` might return theorems implying continuity
from linearity over finite-dimensional spaces or differentiability.  -/
Mathlib.Meta.FunProp.getTransitionTheorems : Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Array Mathlib.Meta.FunProp.GeneralTheorem)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Icc_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ioo a b ⊆ Finset.Icc a b
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables.mk : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ) →
  List (Lean.Parser.Parser × ℕ) →
    Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ) → List (Lean.Parser.Parser × ℕ) → Lean.Parser.PrattParsingTables
-- Mathlib.Analysis.Real.Cardinality
Cardinal.Real.Ioo_countable_iff : ∀ {x y : ℝ}, (Set.Ioo x y).Countable ↔ y ≤ x
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- The underlying algebra map.  -/
CommAlgCat.Hom.hom' : {R : Type u} → [inst : CommRing R] → {A B : CommAlgCat R} → A.Hom B → ↑A →ₐ[R] ↑B
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.lambdaSquared.eq_1 : ∀ (weights : ℕ → ℝ) (d : ℕ),
  BoundingSieve.lambdaSquared weights d =
    ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
-- Mathlib.GroupTheory.Finiteness
Group.fg_range : ∀ {G : Type u_3} [inst : Group G] {G' : Type u_5} [inst_1 : Group G'] [Group.FG G] (f : G →* G'), Group.FG ↥f.range
-- Mathlib.GroupTheory.Divisible
Function.Surjective.divisibleBy.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {α : Type u_3} [inst : Zero α] [inst_1 : AddMonoid A] [inst_2 : AddMonoid B]
  [inst_3 : SMul α A] [inst_4 : SMul α B] [inst_5 : DivisibleBy A α] (f : A → B) (hf : Function.Surjective f)
  (hpow : ∀ (a : A) (n : α), f (n • a) = n • f a),
  Function.Surjective.divisibleBy f hf hpow = divisibleByOfSMulRightSurj B α ⋯
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ) (x : Rˣ),
  (v.valuationOfNeZeroMod n) ↑((Units.map ↑(algebraMap R K)) x) = 1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α}
  {fallback : β}, ∅.getD a fallback = fallback
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.comp_continuous_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [inst_8 : TopologicalSpace α] {f : α → E}, Continuous (⇑e ∘ f) ↔ Continuous f
-- Mathlib.Data.Seq.Computation
/-- Compose two computations into a monadic `bind` operation.  -/
Computation.bind : {α : Type u} → {β : Type v} → Computation α → (α → Computation β) → Computation β
-- Batteries.Tactic.Lint.Simp
/-- The hypotheses of the theorem  -/
Batteries.Tactic.Lint.SimpTheoremInfo.hyps : Batteries.Tactic.Lint.SimpTheoremInfo → Array Lean.Expr
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.of_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m)
  [inst_5 : IsAdicComplete I N] (x : M),
  (AdicCompletion.of I N) ((IsAdicComplete.StrictMono.lift I ha f ⋯) x) =
    (AdicCompletion.lift I (IsAdicComplete.StrictMono.extend ha f) ⋯) x
-- Mathlib.Order.RelClasses
instIsWellOrderEmptyRelationOfSubsingleton : ∀ {α : Type u} [Subsingleton α], IsWellOrder α emptyRelation
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropWhile_eq_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String}, s.startsWith pat = false → s.dropWhile pat = s.toSlice
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_eq_sum : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S), p.smeval x = p.sum (Polynomial.smul_pow x)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Disequalities.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.diseqs : Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.PArray Lean.Meta.Grind.Arith.CommRing.DiseqCnstr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffWithinAt.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℂ n f s x → ContDiffWithinAt ℂ n (fun x => Complex.sinh (f x)) s x
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- Evaluation of a continuous linear map `f` at a point is Lipschitz continuous in `f`.  -/
ContinuousLinearMap.lipschitz_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (x : E),
  LipschitzWith ‖x‖₊ fun f => f x
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.id_whisker_right : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c),
  CategoryTheory.FreeBicategory.Rel
    (CategoryTheory.FreeBicategory.Hom₂.whisker_right g (CategoryTheory.FreeBicategory.Hom₂.id f))
    (CategoryTheory.FreeBicategory.Hom₂.id (f.comp g))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_eq_head_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey he = t.keys.head ⋯
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
        Bool → Std.IterM m β → Std.Iterators.Types.DropWhile α m β P
-- Mathlib.Topology.Separation.Basic
/-- To prove a function to a `T1Space` is continuous at some point `x`, it suffices to prove that
`f` admits *some* limit at `x`.  -/
continuousAt_of_tendsto_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] {f : X → Y}
  {x : X} {y : Y}, Filter.Tendsto f (nhds x) (nhds y) → ContinuousAt f x
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : ↑S.X₂),
  (CategoryTheory.ConcreteCategory.hom S.moduleCatOpcyclesIso.hom)
      ((CategoryTheory.ConcreteCategory.hom S.pOpcycles) x) =
    Submodule.Quotient.mk x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.insertMany_append : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {l₁ l₂ : List α}, m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_conj : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  {f : X → 𝕜}, ∫ (x : X), (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : X), f x ∂μ)
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.hull_le_span : ∀ (R : Type u_1) {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (s : Set E), PointedCone.hull R s ≤ ↑(Submodule.span R s)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.zero_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.SimpleFunc.lintegral 0 μ = 0
-- Std.Data.HashSet.Basic
/-- Inserts multiple mappings into the hash set by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the first occurrence takes precedence.

Note: this precedence behavior is true for `HashSet` and `HashSet.Raw`. The `insertMany` function on
`HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves differently: it will prefer the last
appearance.
 -/
Std.HashSet.insertMany : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {ρ : Type v} → [ForIn Id ρ α] → Std.HashSet α → ρ → Std.HashSet α
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instOne : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → One (AdicCompletion I R)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.mul_zpow' : ∀ {α : Type u_1} [inst : CommGroupWithZero α] (n : ℤ) (a b : α),
  Mathlib.Tactic.FieldSimp.zpow' (a * b) n = Mathlib.Tactic.FieldSimp.zpow' a n * Mathlib.Tactic.FieldSimp.zpow' b n
-- Mathlib.RingTheory.RootsOfUnity.Complex
IsPrimitiveRoot.arg_eq_zero_iff : ∀ {n : ℕ} {ζ : ℂ}, IsPrimitiveRoot ζ n → n ≠ 0 → (ζ.arg = 0 ↔ ζ = 1)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagNode.mk : Lean.Meta.Grind.Origin → Lean.Expr → Lean.Meta.Grind.EMatchDiagNode
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.flatten.match_1.eq_1 : ∀ {α : Type u_1} (motive : List (List α) → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (l : List α) → (L : List (List α)) → motive (l :: L)),
  (match [] with
    | [] => h_1 ()
    | l :: L => h_2 l L) =
    h_1 ()
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(1 | b)` has the value `1`.  -/
jacobiSym.one_left : ∀ (b : ℕ), jacobiSym 1 b = 1
-- Mathlib.Algebra.CubicDiscriminant
Cubic.c_eq_three_roots : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
  P.a ≠ 0 → (Cubic.map φ P).roots = {x, y, z} → φ P.c = φ P.a * (x * y + x * z + y * z)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.insertMany t l) k = Std.DTreeMap.Raw.Const.get? t k
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A set of points is cospherical if and only if they lie in some sphere.  -/
EuclideanGeometry.cospherical_iff_exists_sphere : ∀ {P : Type u_2} [inst : MetricSpace P] {ps : Set P},
  EuclideanGeometry.Cospherical ps ↔ ∃ s, ps ⊆ Metric.sphere s.center s.radius
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
  (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ],
  Measurable (Function.uncurry f) → ∀ (a : α), (κ.withDensity f) a = (κ a).withDensity (f a)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasSmallestColimitsOfHasColimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C],
  CategoryTheory.Limits.HasColimitsOfSize.{0, 0, v, u} C
-- Mathlib.Tactic.WLOG
Mathlib.Tactic.WLOGResult.mk.sizeOf_spec : ∀ (reductionGoal : Lean.MVarId) (reductionFVarIds : Lean.FVarId × Lean.FVarId) (hypothesisGoal : Lean.MVarId)
  (hypothesisFVarId : Lean.FVarId) (revertedFVarIds : Array Lean.FVarId),
  sizeOf
      { reductionGoal := reductionGoal, reductionFVarIds := reductionFVarIds, hypothesisGoal := hypothesisGoal,
        hypothesisFVarId := hypothesisFVarId, revertedFVarIds := revertedFVarIds } =
    1 + sizeOf reductionGoal + sizeOf reductionFVarIds + sizeOf hypothesisGoal + sizeOf hypothesisFVarId +
      sizeOf revertedFVarIds
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  CategoryTheory.ShortComplex.homologyMap (CategoryTheory.CategoryStruct.id S) =
    CategoryTheory.CategoryStruct.id S.homology
-- Mathlib.CategoryTheory.Dialectica.Monoidal
/-- The object `X ⊗ Y` in the `Dial C` category just tuples the left and right components.  -/
CategoryTheory.Dial.tensorObjImpl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Dial C → CategoryTheory.Dial C → CategoryTheory.Dial C
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherian_iff' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsNoetherian R M ↔ WellFoundedGT (Submodule R M)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_nat_add_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] {f : ℤ → M},
  Summable f → ∑' (n : ℕ), (f ↑n + f (-(↑n + 1))) = ∑' (n : ℤ), f n
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Aut.inhabited : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : C) → Inhabited (CategoryTheory.Aut X)
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.derivation_ext_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (Polynomial R) A] {D₁ D₂ : Derivation R (Polynomial R) A},
  D₁ = D₂ ↔ D₁ Polynomial.X = D₂ Polynomial.X
-- Mathlib.GroupTheory.EckmannHilton
/-- If a type carries two unital binary operations that distribute over each other,
then these operations are associative.

In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`.  -/
EckmannHilton.mul_assoc : ∀ {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X},
  EckmannHilton.IsUnital m₁ e₁ →
    EckmannHilton.IsUnital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → Std.Associative m₂
-- Init.Data.BitVec.Lemmas
BitVec.add_right_neg : ∀ {w : ℕ} (x : BitVec w), x + -x = 0#w
-- Std.Time.Format.Modifier
/-- `classify` classifies the number of pattern letters into an `OffsetO` format.
 -/
Std.Time.OffsetO.classify : ℕ → Option Std.Time.OffsetO
-- Mathlib.CategoryTheory.Monoidal.Rigid.Functor
/-- The right dual functor from `C` to `(Cᵒᵖ)ᴹᵒᵖ`.  -/
CategoryTheory.rightDualFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.RightRigidCategory C] → CategoryTheory.Functor C Cᵒᵖᴹᵒᵖ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T')
  {Y X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f_1 : Y ⟶ X),
  ((CategoryTheory.CostructuredArrow.map f).map f_1).left = f_1.left
-- Mathlib.Algebra.Group.Action.Basic
MulDistribMulAction.toMonoidEnd_apply : ∀ (M : Type u_2) (A : Type u_3) [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A] (r : M),
  (MulDistribMulAction.toMonoidEnd M A) r = MulDistribMulAction.toMonoidHom A r
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso_hom_app_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] (X : C) (X_1 : D),
  ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso F).hom.app
          X).app
      X_1 =
    CategoryTheory.CategoryStruct.id ((F.obj X).obj X_1)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.toOrderAddMonoidHom_injective : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed),
  Function.Injective ⇑f.toOrderAddMonoidHom