mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A submodule of a locally compact space over a complete field is also locally compact (and even
proper).  -/
instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] [LocallyCompactSpace E] (S : Submodule 𝕜 E), ProperSpace ↥S
-- Lean.Data.Json.FromToJson.Basic
Lean.bignumToJson : ℕ → Lean.Json
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.instLawfulIteratorLoop : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] [LawfulMonad n], Std.LawfulIteratorLoop (Std.Rxi.Iterator α) Id n
-- Init.Data.Bool
Bool.cond_else_not_self : ∀ (c b : Bool), (bif c then b else !c) = (!c || b)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.not_dvd_of_one_right : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, FiniteMultiplicity a 1 → ¬a ∣ 1
-- Mathlib.Algebra.Group.Torsion
neg_eq_self : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {a : G}, -a = a ↔ a = 0
-- Mathlib.Data.List.MinMax
List.minimum_cons : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α) (l : List α), (a :: l).minimum = min (↑a) l.minimum
-- Mathlib.Data.List.Sort
/-- `l.SortedLT` means that the list is strictly monotonic.  -/
List.SortedLT : {α : Type u_1} → [Preorder α] → List α → Prop
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Registers a delaborator.

`@[delab k]` registers a declaration of type `Lean.PrettyPrinter.Delaborator.Delab` for the
`Lean.Expr` constructor `k`. Multiple delaborators for a single constructor are tried in turn until
the first success. If the term to be delaborated is an application of a constant `c`, elaborators
for `app.c` are tried first; this is also done for `Expr.const`s ("nullary applications") to reduce
special casing. If the term is an `Expr.mdata` with a single key `k`, `mdata.k` is tried first.
 -/
Lean.PrettyPrinter.Delaborator.delabAttribute : Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_cancel_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → (a * b).tdiv a = b
-- Init.Data.String.Lemmas.Basic
String.push_inj : ∀ {s : String} {c : Char} {t : String} {d : Char}, s.push c = t.push d ↔ s = t ∧ c = d
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.macroInline.sizeOf_spec : sizeOf Lean.Compiler.InlineAttributeKind.macroInline = 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io.inj : ∀ {hi hi_1 : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound},
  Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi = Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi_1 →
    hi = hi_1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.brecOn : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} {a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g}
  (t : CategoryTheory.FreeBicategory.Rel a_1 a_2),
  (∀ {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (a_3 a_4 : CategoryTheory.FreeBicategory.Hom₂ f g)
      (t : CategoryTheory.FreeBicategory.Rel a_3 a_4), CategoryTheory.FreeBicategory.Rel.below t → motive a_3 a_4 t) →
    motive a_1 a_2 t
-- Init.Data.Bool
Bool.cond_true_right : ∀ (c t : Bool), (bif c then t else true) = (!c || t)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.liftEquiv_apply : ∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : { φ // f.comp φ = g.comp φ }),
  NormedAddGroupHom.Equalizer.liftEquiv φ = NormedAddGroupHom.Equalizer.lift ↑φ ⋯
-- Mathlib.Algebra.Group.Units.Basic
instCanLiftAddUnitsValIsAddUnit : ∀ {M : Type u_1} [inst : AddMonoid M], CanLift M (AddUnits M) AddUnits.val IsAddUnit
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- A pair belongs to `mulAntidiagonal n` iff the product of its components is equal to `n`.  -/
Finset.HasMulAntidiagonal.mem_mulAntidiagonal : ∀ {A : Type u_1} {inst : Monoid A} [self : Finset.HasMulAntidiagonal A] {n : A} {a : A × A},
  a ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n ↔ a.1 * a.2 = n
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentIdentifier.toJson : Lean.Lsp.TextDocumentIdentifier → Lean.Json
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousComp_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (A : Type u) [inst_3 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (L : CategoryTheory.GrothendieckTopology E) [inst_4 : F.IsContinuous J K] [inst_5 : G.IsContinuous K L]
  (X : CategoryTheory.Sheaf L A) (X_1 : Cᵒᵖ),
  ((F.sheafPushforwardContinuousComp G A J K L).inv.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj (Opposite.op (G.obj (F.obj (Opposite.unop X_1)))))
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.Monics.splits_finsetProd : ∀ {k : Type u} [inst : Field k] {s : Finset (AlgebraicClosure.Monics k)} {f : AlgebraicClosure.Monics k},
  f ∈ s → (Polynomial.map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).Splits
-- Mathlib.Util.PrintSorries
/-- The uses of `sorry` that were found.  -/
Mathlib.PrintSorries.State.sorryMsgs : Mathlib.PrintSorries.State → Array Lean.MessageData
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- A rotation of a vector equals that vector if and only if the vector or the angle is zero.  -/
Orientation.rotation_eq_self_iff : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) (θ : Real.Angle), (o.rotation θ) x = x ↔ x = 0 ∨ θ = 0
-- Mathlib.Data.Quot
/-- Choose an element of the equivalence class using the axiom of choice.
Sound but noncomputable.  -/
Quot.out : {α : Sort u_1} → {r : α → α → Prop} → Quot r → α
-- Lean.Data.PersistentArray
Lean.PArray : Type u → Type u
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.smul : ∀ {R : Type u_1} {S : Type u_2} [inst : MonoidWithZero R] [inst_1 : MonoidWithZero S] [inst_2 : MulActionWithZero R S]
  [SMulCommClass R S S] [IsScalarTower R S S] {a : S}, IsNilpotent a → ∀ (t : R), IsNilpotent (t • a)
-- Mathlib.Topology.ContinuousMap.Algebra
continuousSubgroup.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : IsTopologicalGroup β], continuousSubgroup α β = { toSubmonoid := continuousSubmonoid α β, inv_mem' := ⋯ }
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  FaithfulSMul (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.Logic.Basic
not_or_of_imp : ∀ {a b : Prop}, (a → b) → ¬a ∨ b
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.exists_cartanMatrix_mul_diagaonal_posDef : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] [inst_9 : DecidableEq ι] [P.IsRootSystem],
  ∃ d, (∀ (i : ↥b.support), 0 < d i) ∧ (b.cartanMatrix * Matrix.diagonal d).PosDef
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.congr_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' g' : F} {x : 𝕜}, HasDerivAt f f' x → f' = g' → HasDerivAt f g' x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.reflectsIsomorphisms`.

---

If the source of a faithful functor has a subobject classifier, the functor reflects
isomorphisms. This holds for any balanced category.
 -/
CategoryTheory.HasClassifier.reflectsIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.HasSubobjectClassifier C] (D : Type u₀)
  [inst_2 : CategoryTheory.Category.{v₀, u₀} D] (F : CategoryTheory.Functor C D) [F.Faithful], F.ReflectsIsomorphisms
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.domCongr_refl : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M], MonoidAlgebra.domCongr R A (MulEquiv.refl M) = AlgEquiv.refl
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrp.instInhabited = { default := CategoryTheory.AddGrp.trivial C }
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_le_nat : ∀ {m : ℕ∞} {n : ℕ}, ↑m ≤ ↑n ↔ m ≤ ↑n
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The inf of two orthogonal subspaces equals the subspace orthogonal
to the sup.  -/
Submodule.inf_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K₁ K₂ : Submodule 𝕜 E), K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ
-- Mathlib.Probability.Distributions.Uniform
PMF.mem_support_ofMultiset_iff : ∀ {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) (a : α), a ∈ (PMF.ofMultiset s hs).support ↔ a ∈ s.toFinset
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vec2_add : ∀ {α : Type u} [inst : Add α] (a₀ a₁ b₀ b₁ : α), ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_monotone : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Monotone f → Monotone (Ordinal.nfp f)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_lt_of_translationNumber_lt_nat : ∀ (f : CircleDeg1Lift) {n : ℕ}, f.translationNumber < ↑n → ∀ (x : ℝ), f x < x + ↑n
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_ofFinsupp : ∀ {R : Type u} [inst : Semiring R] (p : AddMonoidAlgebra R ℕ), { toFinsupp := p }.support = p.coeff.support
-- Mathlib.RingTheory.Valuation.Basic
Valuation.OrderMonoidWithZeroHom.ofClass_monotone : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedCommMonoidWithZero α]
  [inst_1 : LinearOrderedCommMonoidWithZero β] [inst_2 : FunLike F α β] [inst_3 : MonoidWithZeroHomClass F α β] {f : F},
  Monotone ⇑f → Monotone ⇑(MonoidWithZeroHom.ofClass f)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_of_isLimit_fan : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  {f : β → C},
  (CategoryTheory.ObjectProperty.ofObj f).IsCoseparating →
    ∀ {c : CategoryTheory.Limits.Fan f} (hc : CategoryTheory.Limits.IsLimit c), CategoryTheory.IsCoseparator c.pt
-- Init.Data.BitVec.Lemmas
BitVec.getElem_one : ∀ {i w : ℕ} (h : i < w), (1#w)[i] = decide (i = 0)
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.instIsDenseSubsiteOverSubtypeMemOverGrothendieckTopologyInverseSymmOverEquivalence : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X),
  CategoryTheory.Functor.IsDenseSubsite ((Opens.grothendieckTopology X).over U) (Opens.grothendieckTopology ↥U)
    U.overEquivalence.symm.inverse
-- Mathlib.Data.Set.Operations
Subtype.coind.congr_simp : ∀ {α : Sort u_4} {β : Sort u_5} (f f_1 : α → β) (e_f : f = f_1) {p : β → Prop} (h : ∀ (a : α), p (f a)) (a a_1 : α),
  a = a_1 → Subtype.coind f h a = Subtype.coind f_1 ⋯ a_1
-- Init.Data.Order.Ord
Std.TransCmp.lt_of_isLE_of_lt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  (cmp a b).isLE = true → cmp b c = Ordering.lt → cmp a c = Ordering.lt
-- Lean.Elab.Do.ForwardSyntax
Lean.Elab.Do.ForwardArg.body : Lean.Elab.Do.ForwardArg → Lean.DoSeq
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The subset of `C` consisting of those elements whose `o`-th entry is `false`.  -/
Profinite.NobelingProof.C0 : {I : Type u} →
  Set (I → Bool) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] → {o : Ordinal.{u}} → (o < Ordinal.type fun x1 x2 => x1 < x2) → Set (I → Bool)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_eq_singleton_append_iff : ∀ {xs : Array ℕ} {n a : ℕ}, (*...n).toArray = #[a] ++ xs ↔ 0 = a ∧ 0 < n ∧ (1...n).toArray = xs
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.linearEquiv_apply : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (a : WithLp p V), (WithLp.linearEquiv p K V) a = (WithLp.addEquiv p V).toFun a
-- Mathlib.GroupTheory.CosetCover
/-- A vector space over an infinite field cannot be a finite union of proper subspaces.  -/
Subspace.top_mem_of_biUnion_eq_univ : ∀ {k : Type u_1} {E : Type u_2} [inst : DivisionRing k] [Infinite k] [inst_2 : AddCommGroup E] [inst_3 : Module k E]
  {s : Finset (Subspace k E)}, ⋃ p ∈ s, ↑p = Set.univ → ⊤ ∈ s
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.isNat_clog : ∀ {b nb n nn k : ℕ},
  Mathlib.Meta.NormNum.IsNat b nb →
    Mathlib.Meta.NormNum.IsNat n nn → Nat.clog nb nn = k → Mathlib.Meta.NormNum.IsNat (Nat.clog b n) k
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- Let `P` be stable under composition and base change. If `P` satisfies cancellation on the right,
the subcategory of `Over X` defined by `P` is closed under pullbacks.

Without the cancellation property, this does not in general. Consider for example
`P = Function.Surjective` on `Type`.  -/
CategoryTheory.Over.closedUnderLimitsOfShape_pullback : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X : T}
  [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderComposition] [P.IsStableUnderBaseChange]
  [P.HasOfPostcompProperty P], P.overObj.IsClosedUnderLimitsOfShape CategoryTheory.Limits.WalkingCospan
-- Init.Internal.Order.Basic
/-- `FlatOrder b` wraps the type `α` with the flat partial order generated by `∀ x, b ⊑ x`.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.FlatOrder : {α : Sort u} → α → Sort u
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.comp'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A₁ A₂ A₃ : CategoryTheory.AddGrp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) {Z : CategoryTheory.AddMon C} (h : A₃.toAddMon ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Sigma.π.hcongr_8 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (inst_1 : CategoryTheory.Limits.HasZeroMorphisms C) (inst'_1 : CategoryTheory.Limits.HasZeroMorphisms C'),
          inst_1 ≍ inst'_1 →
            ∀ (β β' : Type w),
              β = β' →
                ∀ (inst_2 : DecidableEq β) (inst'_2 : DecidableEq β'),
                  inst_2 ≍ inst'_2 →
                    ∀ (f : β → C) (f' : β' → C'),
                      f ≍ f' →
                        ∀ (inst_3 : CategoryTheory.Limits.HasCoproduct f)
                          (inst'_3 : CategoryTheory.Limits.HasCoproduct f'),
                          inst_3 ≍ inst'_3 →
                            ∀ (b : β) (b' : β'),
                              b ≍ b' → CategoryTheory.Limits.Sigma.π f b ≍ CategoryTheory.Limits.Sigma.π f' b'
-- Mathlib.Algebra.CharP.Two
neg_one_eq_one_iff : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R], -1 = 1 ↔ ringChar R = 2
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.tryCatch.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (ok : EStateM.Result ε σ α)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)) (h_2 : (ok : EStateM.Result ε σ α) → motive ok),
  (∀ (e : ε) (s : σ), ok = EStateM.Result.error e s → False) →
    (match ok with
      | EStateM.Result.error e s => h_1 e s
      | ok => h_2 ok) =
      h_2 ok
-- Qq.MetaM
Qq.MaybeLevelDefEq.defEq.sizeOf_spec : ∀ {u v : Lean.Level} (a : u =QL v), sizeOf (Qq.MaybeLevelDefEq.defEq a) = 1 + sizeOf a
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_at_natCast : ∀ {S : Type u_2} [inst : NonAssocSemiring S] [inst_1 : Pow S ℕ] [NatPowAssoc S] (q : Polynomial ℕ) (n : ℕ),
  q.smeval ↑n = ↑(q.smeval n)
-- Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
/-- For a principal ideal `I`, `R ⧸ I ≃ I ^ n ⧸ I ^ (n + 1)`. Supplied as a plain equiv to bypass
typeclass synthesis issues on complex `Module` goals.  To convert into a form
that uses the ideal of `R ⧸ I ^ (n + 1)`, compose with
`Ideal.powQuotPowSuccEquivMapMkPowSuccPow`.  -/
Ideal.quotEquivPowQuotPowSuccEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDomain R] → {I : Ideal R} → Submodule.IsPrincipal I → I ≠ ⊥ → (n : ℕ) → R ⧸ I ≃ ↥(I ^ n) ⧸ I • ⊤
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.comp_noncommCoprod : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) {Q : Type u_4} [inst_3 : Monoid Q]
  (h : P →* Q), h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.eq_lift_inv_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] (f g h : A ⟶ B),
  f =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp g CategoryTheory.GrpObj.inv)
          h)
        CategoryTheory.MonObj.mul ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g f) CategoryTheory.MonObj.mul = h
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppEquivDFinsupp_add : ∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [inst : AddZeroClass N] (f g : (i : ι) × η i →₀ N),
  sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdLeanDiagnosticTag.ord : Lean.Lsp.LeanDiagnosticTag → Lean.Lsp.LeanDiagnosticTag → Ordering
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofBddAugment_E : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).E = E
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.BirationalOver.partialIso_isOver : ∀ {S X Y : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) (h : AlgebraicGeometry.Scheme.BirationalOver sX sY),
  AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY (AlgebraicGeometry.Scheme.BirationalOver.partialIso sX sY h)
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafify_hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η γ : CategoryTheory.sheafify J P ⟶ Q),
  CategoryTheory.Presheaf.IsSheaf J Q →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) η =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) γ →
      η = γ
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.infinite_div : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, (s / t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
-- Mathlib.Data.PNat.Factors
instDistribLatticePrimeMultiset : DistribLattice PrimeMultiset
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_ext₂_left_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {X Y Z : C} {f : J → C}
  {g h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)) ⟶ Z},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j)))
          g =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j)))
          h
-- Lean.Elab.Tactic.Location
/-- Apply the tactic everywhere.  -/
Lean.Elab.Tactic.Location.wildcard : Lean.Elab.Tactic.Location
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.of_inheritedFromTarget : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  (Q : CategoryTheory.MorphismProperty C) [P.InheritedFromTarget Q] [Q.RespectsIso] [Q.ContainsIdentities],
  P.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.smul_def : ∀ {R' : Type u_1} {α : Type u_2} [inst : NonAssocSemiring R'] [inst_1 : SMul R' α] {S : Subsemiring R'} (g : ↥S)
  (m : α), g • m = ↑g • m
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_sum : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {ι : Type u_8} [inst_5 : DecidableEq ι] (Q : QuadraticMap R M N)
  (s : Finset ι) (f : ι → M),
  Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, QuadraticMap.polarSym2 (⇑Q) (Sym2.map f ij)
-- Mathlib.Data.EReal.Inv
EReal.le_mul_of_forall_lt : ∀ {a b c : EReal}, 0 < a ∨ b ≠ ⊤ → a ≠ ⊤ ∨ 0 < b → (∀ a' > a, ∀ b' > b, c ≤ a' * b') → c ≤ a * b
-- Mathlib.Algebra.Order.Group.Synonym
toLex_neg : ∀ {α : Type u_1} [inst : Neg α] (a : α), toLex (-a) = -toLex a
-- Mathlib.RingTheory.Binomial
Ring.multichoose_eq : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R) (n : ℕ),
  Ring.multichoose r n = Ring.choose (r + ↑n - 1) n
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.firstDart.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (p p_1 : G.Walk v w) (e_p : p = p_1) (hp : ¬p.Nil),
  p.firstDart hp = p_1.firstDart ⋯
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.coe_mk' : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal], ⇑(QuotientGroup.mk' N) = QuotientGroup.mk