mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Slice
/-- Checks whether the slice can be interpreted as the decimal representation of a natural number.

A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
it are digits. Underscores \(`_`\) are allowed as digit separators for readability, but cannot appear
at the start, at the end, or consecutively.

Use `toNat?` or
`toNat!` to convert such a slice to a natural number.

Examples:

* `"".toSlice.isNat = false`

* `"0".toSlice.isNat = true`

* `"5".toSlice.isNat = true`

* `"05".toSlice.isNat = true`

* `"587".toSlice.isNat = true`

* `"1_000".toSlice.isNat = true`

* `"100_000_000".toSlice.isNat = true`

* `"-587".toSlice.isNat = false`

* `" 5".toSlice.isNat = false`

* `"2+3".toSlice.isNat = false`

* `"0xff".toSlice.isNat = false`

* `"_123".toSlice.isNat = false`

* `"123_".toSlice.isNat = false`

* `"12__34".toSlice.isNat = false`
 -/
String.Slice.isNat : String.Slice → Bool
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (a : ↑(p.primesOver S)),
  ↑((PrimeSpectrum.primesOverOrderIsoFiber R S p) a).asIdeal =
    ⇑(Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p (↑a) (Algebra.ofId R S) ⋯)
          (IsScalarTower.toAlgHom R S (↑a).ResidueField) ⋯) ⁻¹'
      {0}
-- Aesop.Stats.Basic
Aesop.Stats.instEmptyCollection : EmptyCollection Aesop.Stats
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_one : ∀ {R : Type u_1} {A : Type u_2} [inst : One R] [inst_1 : Zero A], (Unitization.toProd 1).2 = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.not_differentiableAt_rpow_const_zero : ∀ {r : ℝ}, r < 1 → r ≠ 0 → ¬DifferentiableAt ℝ (fun x => x ^ r) 0
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
SymmetricPower.domDomCongr_tprod : ∀ {R : Type u} (ι : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (e : Equiv.Perm ι), MultilinearMap.domDomCongr e (SymmetricPower.tprod R) = SymmetricPower.tprod R
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.interiorPoint_inr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] (x : M'), I.IsInteriorPoint x → I.IsInteriorPoint (Sum.inr x)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.one_zpow' : ∀ {α : Type u_1} [inst : GroupWithZero α] (n : ℤ), Mathlib.Tactic.FieldSimp.zpow' 1 n = 1
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.fromStructuredArrow_π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D}
  (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)) (j : J),
  (CategoryTheory.Limits.Cone.fromStructuredArrow F G).π.app j = (G.obj j).hom
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
OneHom.withTopMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N] (f : OneHom M N), ⇑f.withTopMap = WithTop.map ⇑f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcompose.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ⟶ G),
  CategoryTheory.Limits.Cone.postcompose α =
    { obj := fun c => { pt := c.pt, π := CategoryTheory.CategoryStruct.comp c.π α },
      map := fun {X Y} f => { hom := f.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Group.Action.Defs
/-- `VAdd` version of `comp_add_left`  -/
comp_vadd_left : ∀ (M : Type u_1) {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α] (a₁ a₂ : M),
  ((fun x => a₁ +ᵥ x) ∘ fun x => a₂ +ᵥ x) = fun x => (a₁ + a₂) +ᵥ x
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_starProjection_of_le`.

---

If `U ≤ V`, then projecting on `V` and then on `U` is the same as projecting on `U`.  -/
Submodule.orthogonalProjection_starProjection_of_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection] [inst_4 : V.HasOrthogonalProjection],
  U ≤ V → ∀ (x : E), U.orthogonalProjectionOnto (V.starProjection x) = U.orthogonalProjectionOnto x
-- Lean.Meta.Tactic.Grind.Types
/-- Pushes `lhs ≍ rhs` with `proof` to `newEqs`.  -/
Lean.Meta.Grind.pushHEq : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Analysis.MeanInequalities
_private.Mathlib.Analysis.MeanInequalities.0.NNReal.inner_le_Lp_mul_Lp_of_norm_eq_zero : ∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p q : ℝ},
  p.HolderConjugate q →
    ∑ i ∈ s, f i ^ p = 0 → ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.addSimprocAttr : Lean.Name → Lean.Meta.Simp.SimprocExtension → Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit
-- Mathlib.Topology.Algebra.LinearMapCompletion
ContinuousLinearMap.completion_apply_coe : ∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  (f : α →SL[σ] β) (a : α), f.completion ↑a = ↑(f a)
-- Init.Data.List.Count
_private.Init.Data.List.Count.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.one_def : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : Zero ι] [inst_2 : GradedMonoid.GOne A]
  [inst_3 : (i : ι) → AddCommMonoid (A i)], 1 = (DirectSum.of A 0) GradedMonoid.GOne.one
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator_ne_one : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete], Valuation.IsRankOneDiscrete.generator v ≠ 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.compare_maxKey?_modify_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {f : β → β} {km kmm : α} (hkm : t.maxKey? = some km),
  (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey?.get ⋯ = kmm → compare kmm km = Ordering.eq
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_comap_le : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F}, Submonoid.map f (Submonoid.comap f S) ≤ S
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.getRingCore? : Option ℕ → Lean.Meta.Grind.GoalM (Option Lean.Meta.Grind.Arith.CommRing.Ring)
-- Init.Data.Nat.Lemmas
/-- If `1 < x`, then `x^k` divides `x^l` if and only if `k` is at most `l`.  -/
Nat.pow_dvd_pow_iff_le_right : ∀ {x k l : ℕ}, 1 < x → (x ^ k ∣ x ^ l ↔ k ≤ l)
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- (Implementation) Show the cocone constructed in `buildColimit` is colimiting,
provided the cocones used in its construction are.
 -/
CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        {F : CategoryTheory.Functor J C} →
          {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1} →
            {c₂ : CategoryTheory.Limits.Cofan F.obj} →
              (s t : c₁.pt ⟶ c₂.pt) →
                (hs :
                    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                      CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s =
                        CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) →
                  (ht :
                      ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                        CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) →
                    {i : CategoryTheory.Limits.Cofork s t} →
                      CategoryTheory.Limits.IsColimit c₁ →
                        CategoryTheory.Limits.IsColimit c₂ →
                          CategoryTheory.Limits.IsColimit i →
                            CategoryTheory.Limits.IsColimit
                              (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht
                                i)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.Spec_full : AlgebraicGeometry.AffineScheme.Spec.Full
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.rightUnitor_inv_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor α).inv.τr = (CategoryTheory.Bicategory.leftUnitor α.r).hom
-- Mathlib.Order.OrderDual
/-- Type synonym to equip a type with the dual order: `≤` means `≥` and `<` means `>`. `αᵒᵈ` is
notation for `OrderDual α`.  -/
«term_ᵒᵈ» : Lean.TrailingParserDescr
-- Mathlib.Order.Bounds.Basic
isGreatest_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → IsGreatest (Set.Ioc a b) b
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenex.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ), FirstOrder.Language.BoundedFormula.falsum.toPrenex = ⊥
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.GrothendieckTopology.arrows_mem_toPrecoverage_iff : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (J : CategoryTheory.GrothendieckTopology C) {S : C}
  (R : CategoryTheory.Sieve S), R.arrows ∈ J.toPrecoverage.coverings S ↔ R ∈ J S
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKey! k = t.getKey! k
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
DifferentiableWithinAtProp_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E} {x : E},
  DifferentiableWithinAtProp (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f s x ↔
    DifferentiableWithinAt 𝕜 f s x
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.lit.sizeOf_spec : ∀ (a : Lean.Literal), sizeOf (Lean.Meta.LazyDiscrTree.Key.lit a) = 1 + sizeOf a
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.IsFinite.of_isProper_of_locallyQuasiFinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.LocallyQuasiFinite f],
  AlgebraicGeometry.IsFinite f
-- Mathlib.Data.Finset.Sups
Finset.disjSups_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] (s t : Finset α), s.disjSups t = t.disjSups s
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.nonempty : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SSameSide x y → (↑s).Nonempty
-- Lean.Expr
Lean.Expr.proj.sizeOf_spec : ∀ (typeName : Lean.Name) (idx : ℕ) (struct : Lean.Expr),
  sizeOf (Lean.Expr.proj typeName idx struct) = 1 + sizeOf typeName + sizeOf idx + sizeOf struct
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_neg : ∀ {R : Type u_1} [inst : Ring R] (f : Polynomial R) (N : ℕ), Polynomial.reflect N (-f) = -Polynomial.reflect N f
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.prodEquivOfIsTopCompl.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (p q : Submodule R M) [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q),
  p.prodEquivOfIsTopCompl q h = p.prodEquivOfIsTopCompl q h
-- Lean.Parser.Tactic
Lean.Parser.Tactic.unknown : Lean.Parser.Parser
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesEntry.declName : Lean.Meta.Grind.CasesEntry → Lean.Name
-- Init.Data.String.Defs
instAppendString : Append String
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instIsStableUnderSupMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J K : CategoryTheory.Precoverage C) [J.IsStableUnderSup]
  [K.IsStableUnderSup], (J ⊓ K).IsStableUnderSup
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.isStrongFEPair_toStrongFEPair : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  IsStrongFEPair P.toStrongFEPair
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.gc_map_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), GaloisConnection (Submonoid.map f) (Submonoid.comap f)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] {f g : sInfHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.RingTheory.ZariskisMainTheorem
Subalgebra.saturation.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (s s_1 : Subalgebra R S) (e_s : s = s_1) (M M_1 : Submonoid S) (e_M : M = M_1) (H : M ≤ s.toSubmonoid),
  s.saturation M H = s_1.saturation M_1 ⋯
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `elemExponent_le_of_pow_mem` using `ExpChar`.  -/
IsPurelyInseparable.elemExponent_le_of_pow_mem' : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] {a : L} {n : ℕ},
  a ^ p ^ n ∈ (algebraMap K L).range → IsPurelyInseparable.elemExponent K a ≤ n
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.match_3.splitter : (motive : Lean.Expr × Option Lean.Expr → Sort u_1) →
  (x : Lean.Expr × Option Lean.Expr) → ((lhs : Lean.Expr) → (α? : Option Lean.Expr) → motive (lhs, α?)) → motive x
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.of_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {E' : Type u_4}
  [inst_5 : AddCommGroup E'] [inst_6 : Module 𝕜 E'] {f : E → F} {f' : F} {x : E'} {L : E' →ₗ[𝕜] E} {v : E'},
  HasLineDerivAt 𝕜 (f ∘ ⇑L) f' x v → HasLineDerivAt 𝕜 f f' (L x) (L v)
-- Mathlib.Analysis.Normed.Group.Subgroup
Subgroup.normedCommGroup : {E : Type u_1} → [inst : NormedCommGroup E] → {s : Subgroup E} → NormedCommGroup ↥s
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eVariationOn_Ioc_eq_Icc_of_continuousWithinAt : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [DenselyOrdered α] {f : α → E} {a b : α},
  ContinuousWithinAt f (Set.Ici a) a → eVariationOn f (Set.Ioc a b) = eVariationOn f (Set.Icc a b)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.range_lift_le : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f : α → β} {s : AddSubgroup β},
  Set.range f ⊆ ↑s → (FreeAddGroup.lift f).range ≤ s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasurableSet (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- **Alias** of the forward direction of `algebraicIndependent_subtype_range`. -/
AlgebraicIndependent.of_subtype_range : ∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_7}
  {f : ι → A}, Function.Injective f → AlgebraicIndependent R Subtype.val → AlgebraicIndependent R f
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_zero : ∀ {d : ℤ}, Zsqrtd.norm 0 = 0
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- **Alias** of the forward direction of `hasProdUniformly_iff_tendstoUniformly`. -/
HasProdUniformly.tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α], HasProdUniformly f g → TendstoUniformly (fun x1 x2 => ∏ i ∈ x1, f i x2) g Filter.atTop
-- Lean.LoadDynlib
_private.Lean.LoadDynlib.0.Lean.loadDynlib.unsafe_1 : Lean.Dynlib → BaseIO Lean.Dynlib
-- Mathlib.Order.Cover
wcovBy_iff_covBy_or_le_and_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_eval₂ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (k : σ → τ) (p : MvPolynomial σ R)
  (g : τ → MvPolynomial σ R),
  (MvPolynomial.rename k) (MvPolynomial.eval₂ MvPolynomial.C (g ∘ k) p) =
    MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.rename k) ∘ g) ((MvPolynomial.rename k) p)
-- Mathlib.Algebra.DirectSum.Basic
DFinsupp.equivFunOnFintype.eq_1 : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : Fintype ι],
  DFinsupp.equivFunOnFintype =
    { toFun := DFunLike.coe, invFun := fun f => { toFun := f, support' := Trunc.mk ⟨Finset.univ.val, ⋯⟩ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**

O(1). Construct a node with the correct size information, without rebalancing.  -/
Ordnode.node' : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- If `f` and `g` split, then so does `f × g`.  -/
ContinuousLinearMap.HasRightInverse.prodMap : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {E' : Type u_3} {F : Type u_4} {F' : Type u_5}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace E']
  [inst_5 : AddCommMonoid E'] [inst_6 : Module R E'] [inst_7 : TopologicalSpace F] [inst_8 : AddCommMonoid F]
  [inst_9 : Module R F] [inst_10 : TopologicalSpace F'] [inst_11 : AddCommMonoid F'] [inst_12 : Module R F']
  {f : E →L[R] F} {g : E' →L[R] F'}, f.HasRightInverse → g.HasRightInverse → (f.prodMap g).HasRightInverse
-- Lean.Parser.Level
Lean.Parser.Level.num.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instOrderTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] {x : CompleteLattice β},
  sInfHom.instOrderTop = { toTop := sInfHom.instTop, le_top := ⋯ }
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instAddGroup : {ι : Type u_1} → {G : Type u_6} → [inst : AddGroup G] → AddGroup (ι →₀ G)
-- Mathlib.Analysis.Normed.Lp.lpSpace
zero_mem_ℓp' : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)], Memℓp (fun i => 0) p
-- Init.Data.UInt.Lemmas
UInt64.toFin_ofNatLT : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatLT n hn).toFin = ⟨n, hn⟩
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- The contraction `M ／ C` is the matroid on `M.E \ C` in which a set `I ⊆ M.E \ C` is independent
if and only if `I ∪ J` is independent, where `J` is an arbitrarily chosen basis for `C`.
It is also equal by definition to `(M✶ ＼ C)✶`; see `Matroid.IsBasis.contract_indep_iff` for
a proof that its independent sets are the claimed ones.  -/
Matroid.contract : {α : Type u_1} → Matroid α → Set α → Matroid α
-- Mathlib.Data.Option.NAry
Option.map₂_right_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {c : Option γ}
  {δ' : Type u_7} {ε : Type u_8} {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) →
    Option.map₂ f (Option.map₂ g a b) c = Option.map₂ g' (Option.map₂ f' a c) b
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.foldr : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → {β : Type u_2} → (α → β → β) → β → Aesop.OrderedHashSet α → β
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Minute.Offset` to a `PlainDateTime`, adjusting the hour and date if the minutes overflow.
 -/
Std.Time.PlainDateTime.addMinutes : Std.Time.PlainDateTime → Std.Time.Minute.Offset → Std.Time.PlainDateTime
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.Ioc_union_Ioc_angleDiff_add_arg : ∀ {x y : Circle},
  x ≠ y →
    Set.Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Set.Ioc (↑y).arg (y.angleDiff x + (↑y).arg) =
      Set.Ioc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * Real.pi)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- **Alias** of the reverse direction of `contMDiffOn_iff_contDiffOn`. -/
ContDiffOn.contMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {s : Set E},
  ContDiffOn 𝕜 n f s → ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s
-- Mathlib.Algebra.Module.Equiv.Defs
/-- Interpret a `RingEquiv` `f` as an `f`-semilinear equiv.  -/
RingEquiv.toSemilinearEquiv : {R : Type u_1} → {S : Type u_6} → [inst : Semiring R] → [inst_1 : Semiring S] → (f : R ≃+* S) → R ≃ₛₗ[↑f] S
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instGeneralizedBooleanAlgebra : {α : Type u_1} → [inst : TopologicalSpace α] → [T2Space α] → GeneralizedBooleanAlgebra (TopologicalSpace.CompactOpens α)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_beq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  (h : k ∈ m), (m.getKey k h == k) = true
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.centralizer_eq_top_iff_subset : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M}, AddSubmonoid.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubmonoid.center M)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Groupoid C} {arrows : (c d : C) → Set (c ⟶ d)}
  {inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ arrows c d → CategoryTheory.Groupoid.inv p ∈ arrows d c}
  {mul :
    ∀ {c d e : C} {p : c ⟶ d},
      p ∈ arrows c d → ∀ {q : d ⟶ e}, q ∈ arrows d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows c e}
  {arrows_1 : (c d : C) → Set (c ⟶ d)}
  {inv_1 : ∀ {c d : C} {p : c ⟶ d}, p ∈ arrows_1 c d → CategoryTheory.Groupoid.inv p ∈ arrows_1 d c}
  {mul_1 :
    ∀ {c d e : C} {p : c ⟶ d},
      p ∈ arrows_1 c d → ∀ {q : d ⟶ e}, q ∈ arrows_1 d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows_1 c e},
  { arrows := arrows, inv := inv, mul := mul } = { arrows := arrows_1, inv := inv_1, mul := mul_1 } → arrows = arrows_1
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.refl_iso : ∀ (X : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.PartialIso.refl X).iso = CategoryTheory.Iso.refl ↑⊤