mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.isOpen_sphere`.

---

For any valuation `v` compatible with the valuative relation on `R`, the sphere of radius `r`
around zero `{x | v.restrict x = r}` is open in the valuative topology.  -/
IsValuativeTopology.isOpen_sphere : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  {r : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, r ≠ 0 → IsOpen {x | v.restrict x = r}
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.comp_single : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι),
  DFunLike.coe ∘ RestrictedProduct.single A i = Pi.single i
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
iSup_ne_top : ∀ {α : Type u_5} [inst : CompleteLinearOrder α] {ι : Sort u_6} [Finite ι] [Nontrivial α] {f : ι → α},
  (∀ (x : ι), f x ≠ ⊤) → iSup f ≠ ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
multipliable_of_ne_finset_one : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  {s : Finset β}, (∀ b ∉ s, f b = 1) → ∀ [L.HasSupport], Multipliable f L
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.bot_arrow_eq_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {B : C}, ⊥.arrow = 0
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- If the Hausdorff distance is `< r`, then any point in one of the sets has
a corresponding point at distance `< r` in the other set.  -/
Metric.exists_edist_lt_of_hausdorffEDist_lt : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α} {r : ENNReal},
  x ∈ s → Metric.hausdorffEDist s t < r → ∃ y ∈ t, edist x y < r
-- Plausible.Functions
Plausible.TotalFunction.PiPred.sampleableExt : {α : Type u} → [Plausible.SampleableExt (α → Bool)] → Plausible.SampleableExt (α → Prop)
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lsum_lsingle : ∀ {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι]
  [inst_4 : Semiring S] [inst_5 : (i : ι) → Module S (M i)] [inst_6 : ∀ (i : ι), SMulCommClass R S (M i)],
  (DFinsupp.lsum S) DFinsupp.lsingle = LinearMap.id
-- Mathlib.Order.Filter.Germ.Basic
/-- Setoid used to define the filter product. This is a dependent version of
`Filter.germSetoid`.  -/
Filter.productSetoid : {α : Type u_1} → Filter α → (ε : α → Type u_5) → Setoid ((a : α) → ε a)
-- Mathlib.Order.Ideal
Order.Ideal.nonempty : ∀ {P : Type u_1} [inst : LE P] (s : Order.Ideal P), (↑s).Nonempty
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mk.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (toSubalgebra toSubalgebra_1 : Subalgebra K L) (e_toSubalgebra : toSubalgebra = toSubalgebra_1)
  (inv_mem' : ∀ x ∈ toSubalgebra.carrier, x⁻¹ ∈ toSubalgebra.carrier),
  { toSubalgebra := toSubalgebra, inv_mem' := inv_mem' } = { toSubalgebra := toSubalgebra_1, inv_mem' := ⋯ }
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.SpecMap_iff : ∀ {R S : CommRingCat} {f : R ⟶ S}, AlgebraicGeometry.Flat (AlgebraicGeometry.Spec.map f) ↔ (CommRingCat.Hom.hom f).Flat
-- Std.Do.Triple.Basic
Std.Do.Triple.entails_wp_of_pre_post : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Std.Do.WP m ps] {α : Type u} {x : m α}
  {P P' : Std.Do.Assertion ps} {Q Q' : Std.Do.PostCond α ps},
  ⦃P'⦄ x ⦃Q'⦄ → (P ⊢ₛ P') → Q'.entails Q → P ⊢ₛ (Std.Do.wp x).apply Q
-- Lean.Class
/-- Positions of universe level parameters that only appear in output parameter types.
For example, for `HAdd (α : Type u) (β : Type v) (γ : outParam (Type w))`,
`outLevelParams := #[2]` since universe `w` only appears in the output parameter `γ`.
This is used to normalize TC resolution cache keys.
 -/
Lean.ClassEntry.outLevelParams : Lean.ClassEntry → Array ℕ
-- Mathlib.SetTheory.Ordinal.Notation
NONote.lt_wf : WellFounded fun x1 x2 => x1 < x2
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.pi_norm_le_sum_norm : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] (x : WithCStarModule A ((i : ι) → E i)),
  ‖x‖ ≤ ∑ i, ‖x i‖
-- Mathlib.Analysis.Normed.Field.Basic
Real.denselyNormedField : DenselyNormedField ℝ
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.ker_le_range_iff : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : Group G] [inst_1 : Group H] [inst_2 : MulOneClass I] (f : G →* H)
  [inst_3 : f.range.Normal] (g : H →* I), g.ker ≤ f.range ↔ (QuotientGroup.mk' f.range).comp g.ker.subtype = 1
-- Lean.DocString.Parser
/-- Unordered lists may have three indicators: asterisks, dashes, or pluses.
 -/
Lean.Doc.Parser.UnorderedListType : Type
-- Lean.Environment
Lean.Kernel.Exception.letTypeMismatch.injEq : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (name : Lean.Name) (givenType expectedType : Lean.Expr)
  (env_1 : Lean.Kernel.Environment) (lctx_1 : Lean.LocalContext) (name_1 : Lean.Name)
  (givenType_1 expectedType_1 : Lean.Expr),
  (Lean.Kernel.Exception.letTypeMismatch env lctx name givenType expectedType =
      Lean.Kernel.Exception.letTypeMismatch env_1 lctx_1 name_1 givenType_1 expectedType_1) =
    (env = env_1 ∧ lctx = lctx_1 ∧ name = name_1 ∧ givenType = givenType_1 ∧ expectedType = expectedType_1)
-- Mathlib.Data.Finset.Sym
Sym2.instFintype : {α : Type u_1} → [Fintype α] → Fintype (Sym2 α)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_nonneg : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α],
  ProbabilityTheory.IsMeasurableRatCDF f →
    ∀ (a : α) (r : ℝ), 0 ≤ ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a r
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.ediam_preimage : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (s : Set β),
  Metric.ediam (⇑h ⁻¹' s) = Metric.ediam s
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.zero_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  (x : E), 0 x = 0
-- Init.Data.Vector.Lemmas
/-- We can prove that two folds over the same vector are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the
vector, preserves the relation.
 -/
Vector.foldr_rel : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ}
  {r : β → γ → Prop},
  r a b →
    (∀ a ∈ xs, ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) →
      r (Vector.foldr (fun a acc => f a acc) a xs) (Vector.foldr (fun a acc => g a acc) b xs)
-- Mathlib.Data.Set.NAry
Set.image2_subset_iff_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ},
  Set.image2 f s t ⊆ u ↔ ∀ a ∈ s, (fun b => f a b) '' t ⊆ u
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.braiding_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C), (β_ G H).hom.hom.hom = (β_ G.X H.X).hom
-- Mathlib.Lean.PrettyPrinter.Delaborator
/-- Annotates `stx` with the go-to-def information of the notation used in `stx`.  -/
Lean.PrettyPrinter.Delaborator.annotateGoToSyntaxDef : Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Lean.Data.DeclarationRange
Lean.instDecidableEqDeclarationLocation.decEq : (x x_1 : Lean.DeclarationLocation) → Decidable (x = x_1)
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousOn.zpow : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn f s → ∀ (z : ℤ), ContinuousOn (f ^ z) s
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.hq : ∀ {A : Type u} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  (self : Algebra.Smooth.DescentAux✝ A B) (i : Algebra.Smooth.DescentAux.vars✝ self),
  (MvPolynomial.eval (Algebra.Smooth.DescentAux.P✝ self).relation) (Algebra.Smooth.DescentAux.q✝ self i) =
    Algebra.Smooth.DescentAux.h✝ self i - MvPolynomial.X i
-- Mathlib.Analysis.Convex.Star
StarConvex.add_smul_sub_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] {x y : E} {s : Set E}, StarConvex 𝕜 x s → y ∈ s → ∀ {t : 𝕜}, 0 ≤ t → t ≤ 1 → x + t • (y - x) ∈ s
-- Mathlib.Data.Num.Basic
PosNum.one : PosNum
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_toL1 : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hf : MeasureTheory.Integrable f μ),
  MeasureTheory.setToFun μ T hT ↑↑(MeasureTheory.Integrable.toL1 f hf) = MeasureTheory.setToFun μ T hT f
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.id_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData),
  (CategoryTheory.ShortComplex.RightHomologyMapData.id h).φQ = CategoryTheory.CategoryStruct.id h.Q
-- Std.Http.Data.Status
/-- 304 Not Modified
 -/
Std.Http.Status.notModified : Std.Http.Status
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B)
  (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U')
  [inst_3 : CategoryTheory.Limits.HasCoreflexiveEqualizers C]
  (h : (X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) (Y : C) (X : B)
  (a : Y ⟶ CategoryTheory.LiftRightAdjoint.constructRightAdjointObj L U' adj₁ adj₂ X),
  (CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv L U' adj₁ adj₂ h Y X) a =
    (CategoryTheory.Limits.Fork.IsLimit.homIso (CategoryTheory.LiftRightAdjoint.unitEqualises adj₁ h X) (L.obj Y)).symm
      ⟨(adj₁.homEquiv (L.obj Y) (F.obj X))
          ((adj₂.homEquiv Y (F.obj X)).symm
            ↑((CategoryTheory.Limits.Fork.IsLimit.homIso
                  (CategoryTheory.Limits.limit.isLimit
                    (CategoryTheory.Limits.parallelPair (U'.map (F.map (adj₁.unit.app X)))
                      (CategoryTheory.LiftRightAdjoint.otherMap L U' adj₁ adj₂ X)))
                  Y)
                a)),
        ⋯⟩
-- Mathlib.Analysis.Normed.MulAction
lipschitzWith_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
  [inst_2 : SMulZeroClass α β] [IsBoundedSMul α β] (s : α), LipschitzWith ‖s‖₊ fun x => s • x
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.isEqvAux.match_1.splitter : {α : Type u_1} →
  (xs : Array α) →
    (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) →
      (x : ℕ) →
        (x_1 : x ≤ xs.size) →
          ((x : 0 ≤ xs.size) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h) → motive x x_1
-- Mathlib.Order.Irreducible
infPrime_toDual : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, InfPrime (OrderDual.toDual a) ↔ SupPrime a
-- Mathlib.Geometry.Manifold.Instances.Real
range_euclideanHalfSpace : ∀ (n : ℕ) [inst : NeZero n], Set.range Subtype.val = {y | 0 ≤ y.ofLp 0}
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_add_single_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r₁ r₂ : R} {m₁ m₂ m₁' m₂' : M},
  r₁ ≠ 0 →
    r₂ ≠ 0 →
      (MonoidAlgebra.single m₁ r₁ + MonoidAlgebra.single m₂ r₂ =
          MonoidAlgebra.single m₁' r₁ + MonoidAlgebra.single m₂' r₂ ↔
        m₁ = m₁' ∧ m₂ = m₂' ∨ r₁ = r₂ ∧ m₁ = m₂' ∧ m₂ = m₁' ∨ r₁ + r₂ = 0 ∧ m₁ = m₂ ∧ m₁' = m₂')
-- Mathlib.Algebra.BigOperators.Group.List.Defs
/-- The alternating sum of a list.  -/
List.alternatingSum : {G : Type u_4} → [Zero G] → [Add G] → [Neg G] → List G → G
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
/-- Comparison isomorphism from the Mayer-Vietoris sequence and the
contravariant sequence of `Ext`-groups.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequenceIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
            (S : J.MayerVietorisSquare) →
              (F : CategoryTheory.Sheaf J AddCommGrpCat) →
                (n₀ n₁ : ℕ) →
                  (h : n₀ + 1 = n₁) →
                    S.sequence F n₀ n₁ h ≅ CategoryTheory.Abelian.Ext.contravariantSequence ⋯ F n₀ n₁ ⋯
-- Mathlib.Lean.Elab.InfoTree
/-- Returns the context and `info` on the outermost `.node info _` which has
context, having merged and updated contexts appropriately.

If `ctx?` is `some ctx`, `ctx` is used as an initial context. A `ctx?` of `none` should **only** be
used when operating on the first node of the entire infotree. Otherwise, it is likely that no
context will be found.
 -/
Lean.Elab.InfoTree.getHighestInfo? : Lean.Elab.InfoTree → Option Lean.Elab.ContextInfo → Option (Lean.Elab.ContextInfo × Lean.Elab.Info)
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.cofibrations_eq : HomotopicalAlgebra.cofibrations SSet = CategoryTheory.MorphismProperty.monomorphisms SSet
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalRing.hom_ext_iff : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] {P : Type u_7}
  [inst_7 : NonUnitalNonAssocSemiring P] {g₁ g₂ : DirectLimit G f →ₙ+* P},
  g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (DirectLimit.NonUnitalRing.of G f i) = g₂.comp (DirectLimit.NonUnitalRing.of G f i)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.yoneda_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) (x : CategoryTheory.Discrete PUnit.{v + 1}),
  (CategoryTheory.Limits.IndObjectPresentation.yoneda X).ι.app x =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.fromPUnit X).comp CategoryTheory.yoneda).obj x)
-- Mathlib.RingTheory.Derivation.DifferentialRing
instContainConstants : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : Differential A], Differential.ContainConstants A A
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_nsmul : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℕ) (x : WittVector p R) (n : ℕ),
  WittVector.init n (m • x) = WittVector.init n (m • WittVector.init n x)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.mem_tangentSet_of_mem_tangentsFrom : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : EuclideanGeometry.Sphere P} {p : P},
  as ∈ s.tangentsFrom p → as ∈ s.tangentSet
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.under_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (h : optParam (IsLocalRing S) ⋯),
  Ideal.under R (IsLocalRing.maximalIdeal S) = I
-- Mathlib.Computability.Partrec
/-- Partially recursive partial functions `α → β → σ` between `Primcodable` types  -/
Partrec₂ : {α : Type u_1} →
  {β : Type u_2} → {σ : Type u_3} → [Primcodable α] → [Primcodable β] → [Primcodable σ] → (α → β →. σ) → Prop
-- Mathlib.NumberTheory.DirichletCharacter.Orthogonality
/-- If `R` is an integral domain that has enough roots of unity and `n ≠ 0`, then for `a` and `b`
in `ZMod n` with `a` a unit, the sum of `χ a⁻¹ * χ b` over all Dirichlet characters
mod `n` with values in `R` vanishes if `a ≠ b` and has the value `n.totient` if `a = b`.  -/
DirichletCharacter.sum_char_inv_mul_char_eq : ∀ (R : Type u_1) [inst : CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)]
  [inst_3 : IsDomain R] {a : ZMod n}, IsUnit a → ∀ (b : ZMod n), ∑ χ, χ a⁻¹ * χ b = if a = b then ↑n.totient else 0
-- Mathlib.Data.List.Defs
/-- Quinary version of `list.zipWith`.  -/
List.zipWith5 : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        {ε : Type u_5} → {ζ : Type u_6} → (α → β → γ → δ → ε → ζ) → List α → List β → List γ → List δ → List ε → List ζ
-- Init.PropLemmas
if_true_right : ∀ {p q : Prop} [h : Decidable p], (if p then q else True) ↔ p → q
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.empty : Lean.Parser.SyntaxStack
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
  [inst_2 : Inhabited (β a)],
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast! a (Std.Internal.List.eraseKey k l) =
      if (k == a) = true then default else Std.Internal.List.getValueCast! a l
-- Lean.ToExpr
/-- Expression representing the type `α`  -/
Lean.ToExpr.toTypeExpr : (α : Type u) → [self : Lean.ToExpr α] → Lean.Expr
-- Mathlib.Algebra.Free
/-- From an additive magma homomorphism `α → β` to an additive semigroup homomorphism
`AddMagma.AssocQuotient α → AddMagma.AssocQuotient β`.  -/
AddMagma.FreeAddSemigroup.map : {α : Type u} →
  [inst : Add α] →
    {β : Type v} → [inst_1 : Add β] → (α →ₙ+ β) → AddMagma.FreeAddSemigroup α →ₙ+ AddMagma.FreeAddSemigroup β
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.instCoeTCOfAddActionSemiHomClass.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {F : Type u_8} [inst_2 : FunLike F X Y] [inst_3 : AddActionSemiHomClass F φ X Y],
  AddActionHom.instCoeTCOfAddActionSemiHomClass = { coe := AddActionSemiHomClass.toAddActionHom }
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.card_domRestrictHom_ker : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G),
  Nat.card ↥(MonoidHom.domRestrictHom H Mˣ).ker = Nat.card (G ⧸ H)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs c) = 1 + sizeOf c
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.single_mul : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MulZeroClass (α i)] [inst_1 : DecidableEq ι] (i : ι) (x y : α i),
  Pi.single i (x * y) = Pi.single i x * Pi.single i y
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuous_iInf_dom : ∀ {ι : Type u_1} {κ : Type u_2} {X' : Type u_4} {α : Type u_6} [uα : UniformSpace α] {t : κ → TopologicalSpace X'}
  {F : ι → X' → α} {k : κ}, Equicontinuous F → Equicontinuous F
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.coe_monodromyPerm : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x : X} {γ : FundamentalGroup X x}, ⇑((cov.monodromyPerm x) γ) = cov.monodromy γ
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- The rank of a matrix equals the dimension of the range of the corresponding linear map,
and is therefore independent of the choice of bases.  -/
Matrix.rank_eq_finrank_range_toLin : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Finite m] [inst_2 : DecidableEq n]
  {M₁ : Type u_1} {M₂ : Type u_2} [inst_3 : CommSemiring R] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (A : Matrix m n R) (v₁ : Module.Basis m R M₁)
  (v₂ : Module.Basis n R M₂), A.rank = Module.finrank R ↥((Matrix.toLin v₂ v₁) A).range
-- Aesop.Rule.Forward
Aesop.ForwardRule.mk : Aesop.ForwardRuleInfo → Aesop.RuleName → Aesop.RuleTerm → Aesop.ForwardRulePriority → Aesop.ForwardRule
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] {k : α}
  {v : β k}, (m.containsThenInsertIfNew k v).1 = m.contains k
-- Batteries.CodeAction.Match
/-- Returns the String.range that encompasses `match e (with)`.  -/
Batteries.CodeAction.getMatchHeaderRange? : Lean.Syntax → Option Lean.Syntax.Range
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (N : ℕ → C)
  (ι : (n : ℕ) → N n ⟶ X.obj (Opposite.op { len := n }))
  (isColimit' :
    (Δ : SimplexCategoryᵒᵖ) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.SimplicialObject.Splitting.cofan' N X ι Δ))
  (N_1 : ℕ → C) (ι_1 : (n : ℕ) → N_1 n ⟶ X.obj (Opposite.op { len := n }))
  (isColimit'_1 :
    (Δ : SimplexCategoryᵒᵖ) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.SimplicialObject.Splitting.cofan' N_1 X ι_1 Δ)),
  ({ N := N, ι := ι, isColimit' := isColimit' } = { N := N_1, ι := ι_1, isColimit' := isColimit'_1 }) =
    (N = N_1 ∧ ι ≍ ι_1 ∧ isColimit' ≍ isColimit'_1)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A trivial block is a block.  -/
AddAction.IsTrivialBlock.isBlock : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsTrivialBlock B → AddAction.IsBlock G B
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.card_nsmul : ∀ {α : Type u_1} (s : Multiset α) (n : ℕ), (n • s).card = n * s.card
-- Mathlib.Computability.Encoding
Computability.Γ'.comma.sizeOf_spec : sizeOf Computability.Γ'.comma = 1
-- Mathlib.Data.List.Basic
List.mem_getLast?_append_of_mem_getLast? : ∀ {α : Type u} {l₁ l₂ : List α} {x : α}, x ∈ l₂.getLast? → x ∈ (l₁ ++ l₂).getLast?
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isNonarchimedean_nnnorm : ∀ {R : Type u_4} [inst : SeminormedAddCommGroup R] [IsUltrametricDist R], IsNonarchimedean fun x => ↑‖x‖₊
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsLeft.sInf : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {W : Set (CategoryTheory.MorphismProperty C)}
  {Q : CategoryTheory.MorphismProperty C}, (∀ W' ∈ W, W'.RespectsLeft Q) → (sInf W).RespectsLeft Q