mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.aroots.congr_simp : ∀ {T : Type w} [inst : CommRing T] (p p_1 : Polynomial T),
  p = p_1 →
    ∀ (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S], p.aroots S = p_1.aroots S
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
QuasispectrumRestricts.nonUnitalStarAlgHom.congr_simp : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S] [inst_6 : StarRing S]
  [inst_7 : TopologicalSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S] [inst_10 : NonUnitalRing A]
  [inst_11 : StarRing A] [inst_12 : Algebra R S] [inst_13 : Module R A] [inst_14 : Module S A]
  [inst_15 : IsScalarTower S A A] [inst_16 : SMulCommClass S A A] [inst_17 : IsScalarTower R S A]
  [inst_18 : StarModule R S] [inst_19 : ContinuousSMul R S] {a : A}
  (φ φ_1 : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A),
  φ = φ_1 →
    ∀ {f f_1 : C(S, R)} (e_f : f = f_1) (h : QuasispectrumRestricts a ⇑f),
      QuasispectrumRestricts.nonUnitalStarAlgHom φ h = QuasispectrumRestricts.nonUnitalStarAlgHom φ_1 ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Instance
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instFormulaPosFinDefaultClause : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.Formula (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
    (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {x : ↥X}, IsDomain ↑(X.presheaf.stalk x)
-- Std.Data.TreeSet.Raw.Basic
/-- Transforms an array into a tree set.  -/
Std.TreeSet.Raw.ofArray : {α : Type u} → Array α → (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.ofArray._auto_1) → Std.TreeSet.Raw α cmp
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X),
  CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f ∈ (AlgebraicGeometry.Scheme.grothendieckTopology P) X
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.Equiv.mk : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap.Raw α β cmp},
  m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus.eq_1 : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] (f g : Π₀ (a : α), N a), f.neLocus g = {x ∈ f.support ∪ g.support | f x ≠ g x}
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- If `f` and `g` are two maps `P → P'` between presentations,
then the image of `f - g` is in the kernel of `P' → S`.
 -/
Algebra.Extension.Hom.subToKer : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u'} →
              {S' : Type v'} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            [inst_8 : Algebra R S'] →
                              [inst_9 : IsScalarTower R R' S'] → P.Hom P' → P.Hom P' → P.Ring →ₗ[R] ↥P'.ker
-- Mathlib.Order.TypeTags
_private.Mathlib.Order.TypeTags.0.WithTop.instRepr.match_1.eq_2 : ∀ {α : Type u_1} (motive : WithTop α → Sort u_2) (a : α) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match some a with
    | none => h_1 ()
    | some a => h_2 a) =
    h_2 a
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- Every finite subset of an algebraically independent set is algebraically independent.  -/
algebraicIndependent_finset_map_embedding_subtype : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : Set A),
  AlgebraicIndependent R Subtype.val → ∀ (t : Finset ↑s), AlgebraicIndependent R Subtype.val
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.pathStar_surjective : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V),
  (∀ (u : U), Function.Surjective (φ.star u)) → ∀ (u : U), Function.Surjective (φ.pathStar u)
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.ext_iff : ∀ {x y : Std.Time.PlainTime},
  x = y ↔ x.hour = y.hour ∧ x.minute = y.minute ∧ x.second = y.second ∧ x.nanosecond = y.nanosecond
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.diff_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ m₄ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ \ m₂).Equiv (m₃ \ m₄)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_pow_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {a₂ c₂ : R} {ea₁ b c₁ : ℕ} {xa₁ c₃ d : R},
  ea₁ * b = c₁ → a₂ ^ b = c₂ → xa₁ ^ c₁ * Nat.rawCast 1 = c₃ → c₃ * c₂ = d → (xa₁ ^ ea₁ * a₂) ^ b = d
-- Mathlib.Data.Finset.Range
/-- **Alias** of the reverse direction of `Finset.nonempty_range_iff`. -/
Finset.Aesop.range_nonempty : ∀ {n : ℕ}, n ≠ 0 → (Finset.range n).Nonempty
-- Mathlib.Data.Int.Range
Int.decidableLTLE : (P : ℤ → Prop) → [DecidablePred P] → (m n : ℤ) → Decidable (∀ (r : ℤ), m < r → r ≤ n → P r)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.IsIntegral.kerLift : ∀ {S : Type u_4} {T : Type u_5} [inst : CommRing S] [inst_1 : CommRing T] {f : S →+* T},
  f.IsIntegral → f.kerLift.IsIntegral
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_eq_zero_iff_apply_eq_zero : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsSFiniteKernel κ] [inst_1 : ProbabilityTheory.IsSFiniteKernel η] (a : α),
  (κ.singularPart η) a = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapRingHom_comp_mapDomainRingHom : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Monoid M] [inst_3 : Monoid N] (f : R →+* S) (g : M →* N),
  (MonoidAlgebra.mapRingHom N f).comp (MonoidAlgebra.mapDomainRingHom R g) =
    (MonoidAlgebra.mapDomainRingHom S g).comp (MonoidAlgebra.mapRingHom M f)
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.not_smul_set_ssubset_smul_set : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X} {g₁ g₂ : G}, MulAction.IsBlock G B → ¬g₁ • B ⊂ g₂ • B
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- At every point `x`, for all `y < x` sufficiently close to `x`,
we have `toIcoDiv hp a y = toIocDiv hp a x`.

Note that we use different functions on the LHS and on the RHS.
 -/
eventuallyEq_toIcoDiv_nhdsLT : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  toIcoDiv hp a =ᶠ[nhdsWithin x (Set.Iio x)] fun x_1 => toIocDiv hp a x
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_pow : ∀ (a : BitVec 16) (n : ℕ), { toBitVec := a ^ n } = { toBitVec := a } ^ n
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.subConst_neg_left : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : DecidableEq G] (A B : Finset G), (-A).subConst B = A.addConst B
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- A strong mono category is a category in which every monomorphism is strong.  -/
CategoryTheory.StrongMonoCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_singleton : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (X : Cᵒᵖ),
  (CategoryTheory.ObjectProperty.singleton X).unop = CategoryTheory.ObjectProperty.singleton (Opposite.unop X)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] {κ : Type u_11} {q : SeminormFamily 𝕜₂ F ι'}
  [inst_7 : UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [IsUniformAddGroup F],
  WithSeminorms q →
    ∀ [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F),
      UniformEquicontinuous (DFunLike.coe ∘ f) ↔
        ∀ (i : ι'), BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.sum_tmul_basis_right_injective : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (𝒞 : Module.Basis κ R N),
  Function.Injective ⇑((Finsupp.lsum R) fun i => (TensorProduct.mk R M N).flip (𝒞 i))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
/-- **Alias** of `Polynomial.Chebyshev.integral_measureT_eq_integral_cos`. -/
Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous : ∀ {f : ℝ → ℝ}, ∫ (x : ℝ), f x ∂Polynomial.Chebyshev.measureT = ∫ (θ : ℝ) in 0..Real.pi, f (Real.cos θ)
-- Mathlib.Topology.Algebra.ProperConstSMul
/-- `(c • ·)` is a proper map.  -/
isProperMap_smul : ∀ {M : Type u_1} (c : M) (X : Type u_2) [inst : SMul M X] [inst_1 : TopologicalSpace X] [h : ProperConstSMul M X],
  IsProperMap fun x => c • x
-- Mathlib.Algebra.Free
FreeMagma.instInhabited : {α : Type u} → [Inhabited α] → Inhabited (FreeMagma α)
-- Init.Data.Dyadic.Basic
Int.trailingZeros.eq_1 : ∀ (i : ℤ), i.trailingZeros = if h : i = 0 then 0 else Int.trailingZeros.aux i.natAbs i h ⋯ 0
-- Mathlib.RingTheory.FinitePresentation
/-- The ring of polynomials in finitely many variables is finitely presented.  -/
Algebra.FinitePresentation.mvPolynomial : ∀ (R : Type w₁) (A : Type w₂) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A] (ι : Type u_1) [Finite ι], Algebra.FinitePresentation R (MvPolynomial ι A)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.val_zero : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Algebra.Extension.Cotangent.val 0 = 0
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I J : Ideal A}
  (h : I ≤ J),
  (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm).comp (Ideal.Quotient.mkₐ R J) = DoubleQuot.quotQuotMkₐ R I J
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {l : List ((a : α) × β a)} {k : α}
  (h₁ : (List.map Sigma.fst l).contains k = false) {h' : (↑(m.insertMany l)).contains k = true},
  (↑(m.insertMany l)).getKey k h' = m.getKey k ⋯
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If a multilinear map in finitely many variables on normed spaces satisfies the inequality
`‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell `ε i / ‖c i‖ < ‖m i‖ < ε i` for some positive numbers `ε i`
and elements `c i : 𝕜`, `1 < ‖c i‖`, then it satisfies this inequality for all `m`.  -/
MultilinearMap.bound_of_shell : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {ε : ι → ℝ} {C : ℝ}
  {c : ι → 𝕜},
  (∀ (i : ι), 0 < ε i) →
    (∀ (i : ι), 1 < ‖c i‖) →
      (∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
        ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_add_apply : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f g : AdicCompletion I M) (n : ℕ), ↑(f + g) n = ↑f n + ↑g n
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] {Z : C} (h : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyι (CategoryTheory.CategoryStruct.comp S.fromOpcycles h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparison.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C),
  CategoryTheory.CartesianMonoidalCategory.prodComparison F A B =
    CategoryTheory.CartesianMonoidalCategory.lift (F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst A B))
      (F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd A B))
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.isLocallyArtinian_iff_openCover : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover),
  AlgebraicGeometry.IsLocallyArtinian X ↔ ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsLocallyArtinian (𝒰.X i)
-- Mathlib.MeasureTheory.Group.Integral
/-- If some right-translate of a function negates it, then the integral of the function with respect
to a right-invariant measure is 0.  -/
MeasureTheory.integral_eq_zero_of_mul_right_eq_neg : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : Group G] [MeasurableMul G] [μ.IsMulRightInvariant],
  (∀ (x : G), f (x * g) = -f x) → ∫ (x : G), f x ∂μ = 0
-- Lean.Meta.Basic
Lean.Meta.SavedState.core : Lean.Meta.SavedState → Lean.Core.SavedState
-- Init.Data.UInt.Lemmas
UInt64.div_self : ∀ {a : UInt64}, a / a = if a = 0 then 0 else 1
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.maxValueSealed : Int16
-- Mathlib.Order.Bounds.Basic
isLeast_sdiff : ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), IsLeast {w | a ≤ b ⊔ w} (a \ b)
-- Lean.Meta.Tactic.Simp.Main
/-- Helper `dsimproc` for `doNotVisitOfNat` and `doNotVisitOfScientific`  -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.doNotVisit : (Lean.Expr → Bool) → Lean.Name → Lean.Meta.Simp.DSimproc
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.length_toList_pos_of_mem_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α),
  ∀ x ∈ p.support, 0 < (p.toList x).length
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
HasOuterApproxClosed.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (∀ (F : Set X),
      IsClosed F →
        ∃ fseq,
          (∀ (n : ℕ) (x : X), (fseq n) x ≤ 1) ∧
            (∀ (n : ℕ), ∀ x ∈ F, 1 ≤ (fseq n) x) ∧
              Filter.Tendsto (fun n x => (fseq n) x) Filter.atTop (nhds (F.indicator fun x => 1))) →
    HasOuterApproxClosed X
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mk.sizeOf_spec : ∀ {α : Type u_6} [inst : LE α] [inst_1 : SizeOf α] (toProd : α × α) (fst_le_snd : toProd.1 ≤ toProd.2),
  sizeOf { toProd := toProd, fst_le_snd := fst_le_snd } = 1 + sizeOf toProd + sizeOf fst_le_snd
-- Mathlib.Tactic.Linarith.Verification
/-- Log `f` under `linarith.detail`, with the provided name.  -/
_private.Mathlib.Tactic.Linarith.Verification.0.Mathlib.Tactic.Linarith.proveFalseByLinarith.detailTrace : {α : Type} → String → Lean.MetaM α → Lean.MetaM α
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
instWfDvdMonoidIdeal : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A], WfDvdMonoid (Ideal A)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.IsNilpotent_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ {f : MvPowerSeries σ R},
      IsNilpotent (MvPowerSeries.constantCoeff f) → IsNilpotent (MvPowerSeries.constantCoeff (MvPowerSeries.subst a f))
-- Mathlib.Data.EReal.Basic
EReal.toReal_neg : ∀ {x : EReal}, x < 0 → x ≠ ⊥ → x.toReal < 0
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.nontrivial_of_ediam_ne_zero : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam ≠ 0 → Nontrivial α
-- Mathlib.Data.Fintype.Quotient
/-- Recursion principle for quotients indexed by a finite type.  -/
Quotient.finHRecOn : {ι : Type u_1} →
  [Fintype ι] →
    [DecidableEq ι] →
      {α : ι → Sort u_2} →
        {S : (i : ι) → Setoid (α i)} →
          {C : ((i : ι) → Quotient (S i)) → Sort u_4} →
            (q : (i : ι) → Quotient (S i)) →
              (f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧) →
                (∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b) → C q
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.BicategoryLike.Normalize.instInhabitedResult : Inhabited Mathlib.Tactic.BicategoryLike.Normalize.Result
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
image_parallelepiped : ∀ {ι : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [inst_3 : AddCommGroup F] [inst_4 : Module ℝ F] (f : E →ₗ[ℝ] F) (v : ι → E),
  ⇑f '' parallelepiped v = parallelepiped (⇑f ∘ v)
-- Mathlib.Algebra.MvPolynomial.Invertible
MvPolynomial.invertibleC : (σ : Type u_1) → {R : Type u_2} → [inst : CommSemiring R] → (r : R) → [Invertible r] → Invertible (MvPolynomial.C r)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_map_filter_add_sum_map_filter_not : ∀ {α : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α → M)
  (l : List α),
  (List.map f (List.filter (fun b => decide (p b)) l)).sum + (List.map f (List.filter (fun x => decide ¬p x) l)).sum =
    (List.map f l).sum
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.lt_rpow_inv_iff : ∀ {x y : ENNReal} {z : ℝ}, 0 < z → (x < y ^ z⁻¹ ↔ x ^ z < y)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.ballAddSubgroup.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (c : FiniteArchimedeanClass M), c.ballAddSubgroup = FiniteArchimedeanClass.addSubgroup (UpperSet.Ioi c)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getLawfulOrderLTInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A group is commutative if the quotient by the center is cyclic.  -/
commGroupOfCyclicCenterQuotient : {G : Type u_2} →
  {G' : Type u_3} →
    [inst : Group G] → [inst_1 : Group G'] → [IsCyclic G'] → (f : G →* G') → f.ker ≤ Subgroup.center G → CommGroup G
-- Mathlib.RingTheory.RingHom.PurelyInseparable
RingHom.isPurelyInseparable_algebraMap_iff : ∀ {F : Type u} {E : Type v} [inst : CommRing F] [inst_1 : CommRing E] [inst_2 : Algebra F E],
  (algebraMap F E).IsPurelyInseparable ↔ IsPurelyInseparable F E
-- Mathlib.Order.Interval.Finset.Defs
WithTop.Ioo_coe_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α] (a b : α),
  Finset.Ioo ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioo a b)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntryD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : (a : α) × β a) →
          ((fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (x : (a : α) × β a) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l : Std.DTreeMap.Internal.Impl α β) →
                        (size_1 : ℕ) →
                          (k_1 : α) →
                            (v_1 : β k_1) →
                              (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                                (fallback : (a : α) × β a) →
                                  motive
                                    (Std.DTreeMap.Internal.Impl.inner size k v l
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                    fallback) →
                motive x x_1
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The morphism of short complexes `S.map F ⟶ S.map G` induced by
a natural transformation `F ⟶ G`.  -/
CategoryTheory.ShortComplex.mapNatTrans : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (S : CategoryTheory.ShortComplex C) →
              {F G : CategoryTheory.Functor C D} →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : G.PreservesZeroMorphisms] → (F ⟶ G) → (S.map F ⟶ S.map G)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- A version of `setIntegral_toReal_rnDeriv_mul` that requires both measures to be σ-finite,
but doesn't require `s` to be a measurable set.  -/
MeasureTheory.setIntegral_toReal_rnDeriv_mul' : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    ∀ (f : α → ℝ) (s : Set α), ∫ (x : α) in s, (μ.rnDeriv ν x).toReal * f x ∂ν = ∫ (x : α) in s, f x ∂μ
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_ne_zero : ∀ {r : NNReal}, ↑r ≠ 0 ↔ r ≠ 0
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.mk : {A : Type u_1} →
  [inst : AddMonoid A] →
    (antidiagonal : A → Finset (A × A)) →
      (∀ {n : A} {a : A × A}, a ∈ antidiagonal n ↔ a.1 + a.2 = n) → Finset.HasAntidiagonal A
-- Mathlib.Topology.ContinuousOn
ContinuousOn.preimage_isClosed_of_isClosed : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {t : Set β}, ContinuousOn f s → IsClosed s → IsClosed t → IsClosed (s ∩ f ⁻¹' t)
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instAddQ : {α : Type u} →
  [inst : Lean.Grind.CommSemiring α] →
    [Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)] → Add (Lean.Grind.Ring.OfSemiring.Q α)
-- Aesop.Forward.SlotIndex
Aesop.instToStringSlotIndex : ToString Aesop.SlotIndex