mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.instModuleCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierModuleCatStructurePresheafInModuleCat : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          Module ↑((AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x)
            ↑((AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x)
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.orderDualEquivalence_unitIso : ∀ (X : Type u) [inst : Preorder X],
  (CategoryTheory.orderDualEquivalence X).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Xᵒᵈ)
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_mul_of_isCoprime : ∀ {F : Type u} [inst : Field F] (f g : Polynomial F),
  IsCoprime f g → (f * g).natSepDegree = f.natSepDegree + g.natSepDegree
-- Mathlib.Order.NonemptyFiniteChains
/-- The monotone map `NonemptyFiniteChains X →o NonemptyFiniteChains Y`
that is induced by `f : X →o Y`.  -/
PartialOrder.NonemptyFiniteChains.orderHomMap : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : PartialOrder X] →
      [inst_1 : PartialOrder Y] → (X →o Y) → PartialOrder.NonemptyFiniteChains X →o PartialOrder.NonemptyFiniteChains Y
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.triangleCategory_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism X Y)
  (g : CategoryTheory.Pretriangulated.TriangleMorphism Y Z), CategoryTheory.CategoryStruct.comp f g = f.comp g
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- Write the iterated Fréchet derivative as the composition of a continuous linear equiv and the
iterated derivative.  -/
iteratedFDerivWithin_eq_equiv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜},
  iteratedFDerivWithin 𝕜 n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin n f s
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal.num : ℕ → Lean.IR.LitVal
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.stabilizer_add_eq_right : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : AddGroup α] [VAddCommClass G α α]
  (a b : α), AddAction.stabilizer G (a + b) = AddAction.stabilizer G b
-- Mathlib.Order.ModularLattice
infIooOrderIsoIooSup'_symm_apply_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α) (a_1 : ↑(Set.Ioo a (a ⊔ b))),
  ↑((RelIso.symm (infIooOrderIsoIooSup' a b)) a_1) =
    ↑((infIooOrderIsoIooSup b a).symm ((OrderIso.setCongr (Set.Ioo a (b ⊔ a)) (Set.Ioo a (a ⊔ b)) ⋯).symm a_1))
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.leftOp_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ)
  (X_1 : SimplexCategoryᵒᵖ), X.leftOp.hom.app X_1 = (X.hom.app (Opposite.unop X_1)).unop
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.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]
  (n : ℕ) (f g : AdicCompletion.AdicCauchySequence I M), ↑(f + g) n = ↑f n + ↑g n
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfMultiset_lt_prod : ∀ {ι : Type u_1} (a s : ι → ℕ) {m : Multiset ι} (nod : m.Nodup) (hs : ∀ i ∈ m, s i ≠ 0)
  (pp : {x | x ∈ m}.Pairwise (Function.onFun Nat.Coprime s)),
  ↑(Nat.chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s m).prod
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- The order of the q-expansion of the modular discriminant is 1: the zeroth coefficient
vanishes (Δ is a cusp form) and the first coefficient equals 1.  -/
ModularForm.discriminant_qExpansion_order : (UpperHalfPlane.qExpansion 1 ModularForm.discriminant).order = 1
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.id : ∀ (R : Type u) [inst : CommRing R], Algebra.IsStandardSmoothOfRelativeDimension 0 R R
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.liftRight_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N)
  (hf : ∀ (x : M), IsAddUnit (f x)) (x : M), (IsAddUnit.liftRight f hf) x = ⋯.addUnit
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.pow_dvd_nthHom_sub : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)],
  (∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) →
    ∀ (r : R) (i j : ℕ), i ≤ j → ↑p ^ i ∣ PadicInt.nthHom f r j - PadicInt.nthHom f r i
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.toRatVec.eq_1 : ∀ {ι : Type u_3}, toRatVec✝ = (Nat.castAddMonoidHom ℚ).compLeft ι
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.ofAscListAux₁.match_1.eq_1 : ∀ {α : Type u_1} (ys : List α) (motive : Ordnode α × { l' // l'.length ≤ ys.length } → Sort u_2) (r : Ordnode α)
  (zs : List α) (h' : zs.length ≤ ys.length)
  (h_1 : (r : Ordnode α) → (zs : List α) → (h' : zs.length ≤ ys.length) → motive (r, ⟨zs, h'⟩)),
  (match (r, ⟨zs, h'⟩) with
    | (r, ⟨zs, h'⟩) => h_1 r zs h') =
    h_1 r zs h'
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAdd : {R : Type u_1} →
  [inst : AddMonoid R] → {S : AddSubmonoid R} → [inst_1 : AddOreLocalization.AddOreSet S] → Add (AddOreLocalization S R)
-- Mathlib.Order.RelIso.Basic
RelIso.instCoeOutRelEmbedding : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → CoeOut (r ≃r s) (r ↪r s)
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map.eq_4 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) (n : ℕ),
  CategoryTheory.Functor.OfSequence.map x_1 n.succ 0 = fun a => nomatch a
-- Mathlib.Tactic.Simps.Basic
/-- is the projection name a prefix?  -/
Simps.ParsedProjectionData.isPrefix : Simps.ParsedProjectionData → Bool
-- Init.Data.Nat.Gcd
Nat.gcd_zero_left : ∀ (y : ℕ), Nat.gcd 0 y = y
-- Init.Data.String.Defs
/-- The byte position of the start of the string slice.  -/
String.Slice.startInclusive : (self : String.Slice) → self.str.Pos
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.coe_id : ∀ {M : Type u_10} [inst : MulOne M], ⇑(MonoidHom.id M) = id
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The range of the inclusion map is a normal subgroup.  -/
GroupExtension.normal_inl_range : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G), S.inl.range.Normal
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.isEmpty = false ↔ ∃ a, a ∈ t
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E], balancedCore 𝕜 ∅ = ∅
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
Matrix.IsReducedRowEchelon.mk : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} [inst : Zero R] [inst_1 : LT m] [inst_2 : LT n] [inst_3 : One R]
  {A : Matrix m n R},
  A.IsRowEchelon →
    (∀ ⦃i : m⦄ ⦃c : n⦄, A.IsLeadingEntry i c → A i c = 1) →
      (∀ ⦃i₁ i₂ : m⦄ ⦃c : n⦄, i₁ < i₂ → A.IsLeadingEntry i₂ c → A i₁ c = 0) → A.IsReducedRowEchelon
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.eq_of_bisim_strong : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {x y : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  (motive :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl → Prop),
  motive x y →
    (∀ (x y : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
        motive x y →
          x = y ∨
            ∃ exp coef x' y',
              x = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef x' ∧
                y = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef y' ∧ motive x' y') →
      x = y
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.ext_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] {f g : A ≃A[R] B}, f = g ↔ ⇑f = ⇑g
-- Lean.Util.SCC
_private.Lean.Util.SCC.0.Lean.SCC.modifyDataOf : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → α → (Lean.SCC.Data → Lean.SCC.Data) → Lean.SCC.M α Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- If `C` has equalizers, then it has coreflexive equalizers.  -/
CategoryTheory.Limits.hasCoreflexiveEqualizers_of_hasEqualizers : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C],
  CategoryTheory.Limits.HasCoreflexiveEqualizers C
-- Std.Time.Format.Modifier
Std.Time.Number.mk.inj : ∀ {padding padding_1 : ℕ}, { padding := padding } = { padding := padding_1 } → padding = padding_1
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decompId_i_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C} (f : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp f Q.decompId_i =
    CategoryTheory.CategoryStruct.comp P.decompId_i { f := f.f, comm := ⋯ }
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
DifferentiableWithinAt.lineDifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {s : Set E} {x v : E}, DifferentiableWithinAt 𝕜 f s x → LineDifferentiableWithinAt 𝕜 f s x v
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- Abbreviation to enable dot notation on the hypothesis `h` stating that the subobjects presheaf
is representable by some object `Ω`.  -/
CategoryTheory.SubobjectRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasPullbacks C] → C → Type (max (max u u v) v)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k
-- Mathlib.LinearAlgebra.StdBasis
Pi.mem_spanSubset_iff : ∀ {R : Type u_2} {η : Type u_4} [inst : Semiring R] [inst_1 : Finite η] {s : Set η} {v : η → R},
  v ∈ Pi.spanSubset R s ↔ ∀ i ∉ s, v i = 0
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_smul : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : Lex α), ofLex (b • a) = b • ofLex a
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProd.brecOn.eq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  {motive_1 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e → Sort u}
  {motive_2 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExProd BaseType sα e → Sort u}
  {motive_3 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExSum BaseType sα e → Sort u} {e : Q(«$α»)}
  (t : Mathlib.Tactic.Ring.Common.ExProd BaseType sα e)
  (F_1 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e) → t.below → motive_1 e t)
  (F_2 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExProd BaseType sα e) → t.below → motive_2 e t)
  (F_3 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e) → t.below → motive_3 e t),
  t.brecOn F_1 F_2 F_3 = F_2 e t (Mathlib.Tactic.Ring.Common.ExProd.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsContDiffCompatible.isPlot_iff : ∀ {X : Type u_1} {inst : NormedAddCommGroup X} {inst_1 : NormedSpace ℝ X} {inst_2 : DiffeologicalSpace X}
  [self : Diffeology.IsContDiffCompatible X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  Diffeology.IsPlot p ↔ ContDiff ℝ (↑⊤) p
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_div_mul_right : ∀ {c : ENNReal} (a b : ENNReal), c ≠ 0 → c ≠ ⊤ → a * c / (b * c) = a / b
-- Mathlib.Analysis.Calculus.Taylor
/-- Evaluating the Taylor polynomial at `x = x₀` yields `f x`.  -/
taylorWithinEval_self : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ),
  taylorWithinEval f n s x₀ x₀ = f x₀
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioi_disjoint_Iic : ∀ {α : Type v} [inst : Preorder α] {a b : α}, b ≤ a → Disjoint (Set.Ioi a) (Set.Iic b)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubOfPoint.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P) (b : P),
  s.weightedVSubOfPoint p b = ∑ i ∈ s, (LinearMap.proj i).smulRight (p i -ᵥ b)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticOnNhd.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → DifferentiableOn 𝕜 f s
-- Mathlib.Data.Finset.Lattice.Fold
Finset.Nonempty.inf_eq_bot_iff : ∀ {ι : Type u_5} {α : Type u_7} [inst : LinearOrder α] [inst_1 : BoundedOrder α] {s : Finset ι} {f : ι → α},
  s.Nonempty → (s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥)
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_ite_eq' : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} [inst_2 : DecidableEq ι]
  (i : ι) (f : ι → M), (s.expect fun j => if j = i then f j else 0) = if i ∈ s then (↑s.card)⁻¹ • f i else 0
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumComm_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'],
  (Diffeomorph.sumComm I M n M').symm = Diffeomorph.sumComm I M' n M
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.insert_indep_iff_of_notMem : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → e ∉ I → (M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.ofHom.eq_1 : ∀ {X Y : Type u} [inst : Group X] [inst_1 : Finite X] [inst_2 : Group Y] [inst_3 : Finite Y] (f : X →* Y),
  FiniteGrp.ofHom f = CategoryTheory.InducedCategory.homMk (GrpCat.ofHom f)
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.none : {u : Lean.Level} →
  {α : Q(Type u)} →
    {zα : Q(Zero «$α»)} →
      {e : Q(«$α»)} → {pα? : Option Q(PartialOrder «$α»)} → Mathlib.Meta.Positivity.Strictness zα e pα?
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.instSMulCommClass : ∀ {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_6 : DistribSMul S M₂] [inst_7 : SMulCommClass R₂ S M₂]
  [inst_8 : DistribSMul T M₂] [inst_9 : SMulCommClass R₂ T M₂] [SMulCommClass S T M₂], SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.Analysis.Normed.Module.Dual
/-- The `polar` of closed ball in a normed space `E` is the closed ball of the dual with inverse
radius.  -/
NormedSpace.polar_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ},
  0 < r → StrongDual.polar 𝕜 (Metric.closedBall 0 r) = Metric.closedBall 0 r⁻¹
-- Mathlib.Algebra.Category.Ring.Basic
/-- Typecheck a `RingHom` as a morphism in `CommRingCat`.  -/
CommRingCat.ofHom : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → (CommRingCat.of R ⟶ CommRingCat.of S)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- An element of the fundamental group, constructed from a quotient of homotopic paths.  -/
FundamentalGroup.fromPath : {X : Type u_1} → [inst : TopologicalSpace X] → {x : X} → Path.Homotopic.Quotient x x → FundamentalGroup X x
-- Std.Data.HashMap.Raw
/-- Folds the given function over the mappings in the hash map in some order.  -/
Std.HashMap.Raw.fold : {α : Type u} → {β : Type v} → {γ : Type w} → (γ → α → β → γ) → γ → Std.HashMap.Raw α β → γ
-- Init.Prelude
_private.Init.Prelude.0.Lean.Syntax.getHeadInfo?.loop : Array Lean.Syntax → ℕ → Option Lean.SourceInfo
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.IsRelIff.mk : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'},
  (∀ (i₁ i₂ : ι), c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂) → e.IsRelIff
-- Mathlib.Order.CompleteLattice.Basic
sInf_le_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, s.Nonempty → sInf s ≤ sSup s
-- Init.Data.List.ToArray
List.back!_toArray : ∀ {α : Type u_1} [inst : Inhabited α] (l : List α), l.toArray.back! = l.getLast!
-- Init.Data.SInt.Lemmas
ISize.ne_of_lt : ∀ {a b : ISize}, a < b → a ≠ b
-- Mathlib.Geometry.Manifold.Immersion
/-- `f : M → N` is a `C^n` immersion if around each point `x ∈ M`,
there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
such that in these charts, `f` looks like `u ↦ (u, 0)`.

In other words, `f` is an immersion at each `x ∈ M`.

This definition has a fixed parameter `F`, which is a choice of complement of `E` in `E'`:
being an immersion at `x` includes a choice of linear isomorphism between `E × F` and `E'`.
 -/
Manifold.IsImmersionOfComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        (F : Type u_5) →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              ModelWithCorners 𝕜 E H →
                                ModelWithCorners 𝕜 E'' G →
                                  {M : Type u_11} →
                                    [inst : TopologicalSpace M] →
                                      [ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst : TopologicalSpace N] → [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → Prop
-- Mathlib.Topology.Order.LiminfLimsup
/-- Every cluster point `x` of a function `u` along a filter `f` is less than or equal to
`limsup u f`.  -/
MapClusterPt.le_limsup : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {u : β → α} {f : Filter β} {x : α},
  MapClusterPt x f u →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) MapClusterPt.le_limsup._auto_1 → x ≤ Filter.limsup u f
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The right homology of a short complex `S` identifies to the kernel of the canonical
morphism `cokernel S.f ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.rightHomologyIsoKernelDesc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasRightHomology] →
          [inst_3 : CategoryTheory.Limits.HasCokernel S.f] →
            [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)] →
              S.rightHomology ≅ CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
-- Batteries.Lean.Position
/-- If `pos` is a `String.Pos.Raw`, then `pos.getDeclsAfter` returns the array of names of declarations
whose selection range begins in position at least `pos`. By using the `selectionRange`, which is
usually smaller than the `range`, we err on the side of including declarations when possible.

By default, this is intended for use in linters, where only the current environment branch needs to
be checked. See the docstring for `Lean.Position.getDeclsAfter` for details.
 -/
String.Pos.Raw.getDeclsAfter : Lean.Environment →
  Lean.FileMap →
    String.Pos.Raw → optParam Lean.EnvExtension.AsyncMode Lean.EnvExtension.AsyncMode.local → Array Lean.Name
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- **Alias** of `IsNonarchimedean.apply_sum_le_sup`.

---

Ultrametric inequality with `Finset.sum`.  -/
IsNonarchimedean.apply_sum_le_sup_of_isNonarchimedean : ∀ {R : Type u_1} [inst : LinearOrder R] {α : Type u_2} {β : Type u_3} [inst_1 : AddCommMonoid α] {f : α → R},
  IsNonarchimedean f →
    ∀ {s : Finset β} (hnonempty : s.Nonempty) {l : β → α}, f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun i => f (l i)
-- Mathlib.Tactic.CrossRefAttribute
/-- The base URL for an external database's tag pages. Always ends with `/`.  -/
Mathlib.CrossRef.Database.url : Mathlib.CrossRef.Database → String
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.val_map_lt_one_iff : ∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : LinearOrderedCommMonoidWithZero ΓR] [inst_3 : LinearOrderedCommMonoidWithZero ΓA] [inst_4 : Algebra R A]
  (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x : R), vA ((algebraMap R A) x) < 1 ↔ vR x < 1
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piCongrLeft_apply_apply : ∀ {ι : Type u_7} {ι' : Type u_8} {Y : ι' → Type u_9} [inst : (j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι')
  (x : (i : ι) → Y (e i)) (i : ι), (Homeomorph.piCongrLeft e) x (e i) = x i
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.completeTheory.isSatisfiable : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M] [Nonempty M], (L.completeTheory M).IsSatisfiable
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.le_val_assemble₂ : ∀ {w x : UInt8} {c : Char}, ByteArray.utf8DecodeChar?.assemble₂ w x = some c → 128 ≤ c.val
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.ae_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} {a : α} {p : γ → Prop},
  MeasurableSet {z | p z} → ((∀ᵐ (z : γ) ∂(η.comp κ) a, p z) ↔ ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z)
-- Mathlib.Order.Cover
exists_covBy_of_wellFoundedLT : ∀ {α : Type u_1} [inst : Preorder α] [wf : WellFoundedLT α] ⦃a : α⦄, ¬IsMax a → ∃ a', a ⋖ a'
-- Init.Data.List.Find
List.find?_map : ∀ {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {l : List β},
  List.find? p (List.map f l) = Option.map f (List.find? (p ∘ f) l)
-- Batteries.Data.Array.Scan
Array.getElem_succ_scanl : ∀ {β : Type u_1} {α : Type u_2} {i : ℕ} {b : β} {as : Array α} {f : β → α → β} (h : i + 1 < (Array.scanl f b as).size),
  (Array.scanl f b as)[i + 1] = f (Array.scanl f b as)[i] as[i]
-- Mathlib.Order.Lattice
sup_le_sup_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → ∀ (c : α), c ⊔ a ≤ c ⊔ b