mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Reflection
/-- `Matrix.vecMul` with better defeq for `Fin`  -/
Matrix.vecMulᵣ : {l m : ℕ} → {α : Type u_1} → [Mul α] → [Add α] → [Zero α] → (Fin l → α) → Matrix (Fin l) (Fin m) α → Fin m → α
-- Mathlib.Topology.Instances.Matrix
instContinuousStarMatrix : ∀ {m : Type u_4} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R],
  ContinuousStar (Matrix m m R)
-- Mathlib.CategoryTheory.Filtered.Final
/-- In this situation, `F` is also initial, see
`Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful`.  -/
CategoryTheory.IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty D] [F.Full] [F.Faithful],
  (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) → CategoryTheory.IsCofilteredOrEmpty C
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.left_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P}, s.IsDiameter p₁ p₂ → p₁ ∈ s
-- Mathlib.Tactic.ITauto
/-- `⊢ A`, causes failure during reconstruction  -/
Mathlib.Tactic.ITauto.Proof.sorry : Mathlib.Tactic.ITauto.Proof
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_smul : ∀ {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_6} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F']
  [inst_2 : NormedSpace 𝕜 F'] [inst_3 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {hm : m ≤ m0} [inst_4 : MeasureTheory.SigmaFinite (μ.trim hm)] (c : 𝕜) (f : α → F'),
  MeasureTheory.condExpL1 hm μ (c • f) = c • MeasureTheory.condExpL1 hm μ f
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K},
  w.IsReal → NumberField.ComplexEmbedding.conjugate w.embedding = w.embedding
-- Std.Data.ExtHashMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.
 -/
Std.ExtHashMap.getThenInsertIfNew? : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → β → Option β × Std.ExtHashMap α β
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.sSup_unit_ball_eq_nnnorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F), sSup ((fun x => ‖f x‖₊) '' Metric.ball 0 1) = ‖f‖₊
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator'_lt_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
-- Mathlib.Algebra.GCDMonoid.Finset
/-- Greatest common divisor of a finite set  -/
Finset.gcd : {α : Type u_2} → {β : Type u_3} → [inst : CommMonoidWithZero α] → [NormalizedGCDMonoid α] → Finset β → (β → α) → α
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.smul_apply : ∀ {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [inst_4 : Monoid R']
  [inst_5 : Semiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : DistribMulAction R' N]
  [inst_9 : ContinuousConstSMul R' N] [inst_10 : SMulCommClass A R' N] (f : M [⋀^ι]→L[A] N) (c : R') (v : ι → M),
  (c • f) v = c • f v
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.ofVar.eq_1 : ∀ (x : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Poly.ofVar x = Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.ofVar x)
-- Mathlib.CategoryTheory.Presentable.Limits
/-- In case `C` is locally `w`-small, use `isCardinalPresentable_of_isColimit`.  -/
CategoryTheory.isCardinalPresentable_of_isColimit' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} K]
  {Y : CategoryTheory.Functor K C} (c : CategoryTheory.Limits.Cocone Y) (hc : CategoryTheory.Limits.IsColimit c)
  (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [CategoryTheory.Limits.HasLimitsOfShape Kᵒᵖ (Type v)],
  HasCardinalLT (CategoryTheory.Arrow K) κ →
    ∀ [∀ (k : K), CategoryTheory.IsCardinalPresentable (Y.obj k) κ], CategoryTheory.IsCardinalPresentable c.pt κ
-- Mathlib.NumberTheory.Zsqrtd.Basic
_private.Mathlib.NumberTheory.Zsqrtd.Basic.0.Zsqrtd.Nonnegg.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (a b : ℕ) (h_1 : (a b : ℕ) → motive (Int.ofNat a) (Int.ofNat b))
  (h_2 : (a b : ℕ) → motive (Int.ofNat a) (Int.negSucc b)) (h_3 : (a b : ℕ) → motive (Int.negSucc a) (Int.ofNat b))
  (h_4 : (a a_1 : ℕ) → motive (Int.negSucc a) (Int.negSucc a_1)),
  (match Int.negSucc a, Int.ofNat b with
    | Int.ofNat a, Int.ofNat b => h_1 a b
    | Int.ofNat a, Int.negSucc b => h_2 a b
    | Int.negSucc a, Int.ofNat b => h_3 a b
    | Int.negSucc a, Int.negSucc a_1 => h_4 a a_1) =
    h_3 a b
-- Mathlib.Algebra.Group.Defs
pow_three : ∀ {M : Type u_2} [inst : Monoid M] (a : M), a ^ 3 = a * (a * a)
-- Batteries.Tactic.GeneralizeProofs
_private.Batteries.Tactic.GeneralizeProofs.0.Batteries.Tactic.GeneralizeProofs.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Batteries.Tactic.GeneralizeProofs.Config
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKeyD_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k k' fallback : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k' (Std.Internal.List.Const.modifyKey k f l) fallback =
      if (k == k') = true then if Std.Internal.List.containsKey k l = true then k else fallback
      else Std.Internal.List.getKeyD k' l fallback
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.invFunIdAssoc_inv_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] (e : C ≌ D) (F : CategoryTheory.Functor D E) (X : D),
  (e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app X)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nnnorm_ofLp : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (f : WithLp ⊤ (α × β)), ‖f.ofLp‖₊ = ‖f‖₊
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.isHermitian_lapMatrix : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : NonAssocRing R] [inst_4 : StarRing R], (SimpleGraph.lapMatrix R G).IsHermitian
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiRing : ∀ {𝕜 : Type u} {ι : Type v} {G : Type wG} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : Fintype ι] (z : G), ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {he : (t.modify k f).isEmpty = false},
  (t.modify k f).maxKey he = if cmp (t.maxKey ⋯) k = Ordering.eq then k else t.maxKey ⋯
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
/-- The residual degree of the ideal corresponding to the class of `Q ∈ ℤ[X]` modulo `p` via
`NumberField.Ideal.primesOverSpanEquivMonicFactorsMod` is equal to the degree of `Q mod p`.
 -/
NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial ℤ}
  (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p),
  (↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm
            ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩)).inertiaDeg
      ℤ =
    (Polynomial.map (Int.castRingHom (ZMod p)) Q).natDegree
-- Lean.Elab.Tactic.Ext
/-- Constructs the hypotheses for the structure extensionality theorem that
states that two structures are equal if their fields are equal.

Calls the continuation `k` with the list of parameters to the structure,
two structure variables `x` and `y`, and a list of pairs `(field, ty)`
where each `ty` is of the form `x.field = y.field` or `x.field ≍ y.field`.

If `flat` parses to `true`, any fields inherited from parent structures
are treated as fields of the given structure type.
If it is `false`, then the behind-the-scenes encoding of inherited fields
is visible in the extensionality lemma.
 -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.withExtHyps : {α : Type} →
  Lean.Name →
    Bool → (Array Lean.Expr → Lean.Expr → Lean.Expr → Array (Lean.Name × Lean.Expr) → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.toOne : {E : Type u_3} → [inst : AddGroup E] → [DecidableEq E] → One (AddGroupNorm E)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects colimits, then `F : C ⥤ Dᵒᵖ` reflects limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair_obj_one : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y),
  (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.one = Y
-- Mathlib.NumberTheory.FactorisationProperties
Nat.instDecidableWeird : (n : ℕ) → Decidable n.Weird
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp₂_obj_hom_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {F₀ : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  {F₁ : CategoryTheory.Functor D H} (L' : CategoryTheory.Functor D D') (α : F₀ ⟶ L.comp F₁) (X : L'.LeftExtension F₁)
  (X_1 : C),
  ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).obj X).hom.app X_1 =
    CategoryTheory.CategoryStruct.comp (α.app X_1) (X.hom.app (L.obj X_1))
-- Lean.Expr
Lean.FVarIdMap.insert : {α : Type} → Lean.FVarIdMap α → Lean.FVarId → α → Lean.FVarIdMap α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinPred.toString : Std.Tactic.BVDecide.BVBinPred → String
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.realize_mul : ∀ {α : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
  [inst_5 : FirstOrder.Ring.CompatibleRing R] (x y : FirstOrder.Language.ring.Term α) (v : α → R),
  FirstOrder.Language.Term.realize v (x * y) =
    FirstOrder.Language.Term.realize v x * FirstOrder.Language.Term.realize v y
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (x : Std.Iterators.HetT m α)
  (f : (a : α) → x.Property a → m β),
  x.prun f = do
    let a ← x.operation
    f ↑a.inflate ⋯
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_bounded : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] {a : ι → ℝ} {f : ℝ → E} (I b : ℝ),
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ) →
    Filter.Tendsto a l Filter.atBot →
      (∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I) → MeasureTheory.IntegrableOn f (Set.Iic b) μ
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.snd_prod : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (f : ρ.IntertwiningMap σ) (g : ρ.IntertwiningMap τ),
  (Representation.IntertwiningMap.snd A σ τ).comp (f.prod g) = g
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Functor.IsLocalization.mk : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} (inverts : W.IsInvertedBy L),
  (CategoryTheory.Localization.Construction.lift L inverts).IsEquivalence → L.IsLocalization W
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.succ?_decode : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  {x : β}, Std.PRange.succ? (HasModel.decode✝ x) = Option.map HasModel.decode✝ (Std.PRange.succ? x)
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- If a sequence of peak functions `φᵢ` converges uniformly to zero away from a point `x₀` and its
integral on some finite-measure neighborhood of `x₀` converges to `1`, and `g` is integrable and
has a limit `a` at `x₀`, then `∫ φᵢ • g` converges to `a`.  -/
tendsto_integral_peak_smul_of_integrable_of_tendsto : ∀ {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E}
  {l : Filter ι} {x₀ : α} {φ : ι → α → ℝ} {a : E} [CompleteSpace E] {t : Set α},
  MeasurableSet t →
    t ∈ nhds x₀ →
      μ t ≠ ⊤ →
        (∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x) →
          (∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ) →
            Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (nhds 1) →
              (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) μ) →
                MeasureTheory.Integrable g μ →
                  Filter.Tendsto g (nhds x₀) (nhds a) → Filter.Tendsto (fun i => ∫ (x : α), φ i x • g x ∂μ) l (nhds a)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instInhabited : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] → [inst_6 : TopologicalSpace N] → Inhabited (M [⋀^ι]→L[R] N)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.algebraMap_eq : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] (r : R),
  (algebraMap R (QuadraticAlgebra R a b)) r = { re := r, im := 0 }
-- Mathlib.Algebra.Lie.Quotient
/-- The quotient of a Lie module by a Lie submodule. It is a Lie module.  -/
LieSubmodule.instHasQuotient : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → HasQuotient M (LieSubmodule R L M)
-- Mathlib.Geometry.Diffeology.Basic
/-- A structure with plots specified on open subsets of ℝⁿ rather than ℝⁿ itself. Useful
for constructing diffeologies, as it often makes the locality condition easier to prove.  -/
DiffeologicalSpace.CorePlotsOn : Type u_1 → Type u_1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Given `x ∈ 𝒪[K]` we can find `a : A` such that `a` is close to `x` by the valuation `v`.  -/
IsDedekindDomain.HeightOneSpectrum.exists_valuation_sub_lt_of_integer : ∀ {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) {x : K},
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≤ 1 →
    ∀ (γ : (WithZero (Multiplicative ℤ))ˣ),
      ∃ a, (IsDedekindDomain.HeightOneSpectrum.valuation K v) ((algebraMap R K) a - x) < ↑γ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.mul_ineq_cert.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.mul_ineq_cert p₁ k p = (decide (k > 0) && (Lean.Grind.CommRing.Poly.mulConst_k k p₁).beq' p)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors_radical : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M},
  UniqueFactorizationMonoid.primeFactors (UniqueFactorizationMonoid.radical a) =
    UniqueFactorizationMonoid.primeFactors a
-- Mathlib.LinearAlgebra.LinearPMap
LinearMap.toPMap_domain : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ[σ] F)
  (p : Submodule R E), (f.toPMap p).domain = p
-- Mathlib.Analysis.Normed.Operator.Basic
/-- For a continuous real linear map `f`, if one controls the norm of every `f x`, `‖x‖ = 1`, then
one controls the norm of `f`.  -/
ContinuousLinearMap.opNorm_le_of_unit_norm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜]
  {f : E →SL[σ₁₂] F} {C : ℝ}, 0 ≤ C → (∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C) → ‖f‖ ≤ C
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.max_prod_le : ∀ {α : Type u_2} {M : Type u_3} [inst : Monoid M] (l : List α) (f g : α → M) [inst_1 : LinearOrder M] [MulLeftMono M]
  [MulRightMono M], max (List.map f l).prod (List.map g l).prod ≤ (List.map (fun i => max (f i) (g i)) l).prod
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.ιFree_freeMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {I J_1 : Type u} (f : I → J_1) (i : I),
  CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (SheafOfModules.freeMap f) = SheafOfModules.ιFree (f i)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.lift_obj : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G : CategoryTheory.Functor C D) (hG : W.IsInvertedBy G)
  (a : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)),
  (CategoryTheory.Localization.Construction.lift G hG).obj a = G.obj a.as.obj
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsIntegralHom f],
  AlgebraicGeometry.IsIntegralHom (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.precompHomeomorph_apply : ∀ {R A B : CommRingCat} [inst : TopologicalSpace ↑R] (f : A ≅ B) (φ : B ⟶ R),
  (CommRingCat.HomTopology.precompHomeomorph f) φ = CategoryTheory.CategoryStruct.comp f.hom φ
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The `covolume` can be computed by taking the `volume` of any given fundamental domain `s`.  -/
MeasureTheory.IsFundamentalDomain.covolume_eq_volume : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  (ν : MeasureTheory.Measure α) [Countable G] [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α ν]
  {s : Set α}, MeasureTheory.IsFundamentalDomain G s ν → MeasureTheory.covolume G α ν = ν s
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.iff_mul_eq : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R} [inst_1 : DecidableEq I],
  OrthogonalIdempotents e ↔ ∀ (i j : I), e i * e j = if i = j then e i else 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.powC_nc : Lean.Grind.CommRing.Poly → ℕ → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.Lifting₃.mk : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_13} →
              [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
                [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                    [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁] →
                      [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] →
                        [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃] →
                          [inst_6 : CategoryTheory.Category.{v_13, u_13} E] →
                            {L₁ : CategoryTheory.Functor C₁ D₁} →
                              {L₂ : CategoryTheory.Functor C₂ D₂} →
                                {L₃ : CategoryTheory.Functor C₃ D₃} →
                                  {W₁ : CategoryTheory.MorphismProperty C₁} →
                                    {W₂ : CategoryTheory.MorphismProperty C₂} →
                                      {W₃ : CategoryTheory.MorphismProperty C₃} →
                                        {F :
                                            CategoryTheory.Functor C₁
                                              (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))} →
                                          {F' :
                                              CategoryTheory.Functor D₁
                                                (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))} →
                                            (((((CategoryTheory.Functor.whiskeringLeft₃ E).obj L₁).obj L₂).obj L₃).obj
                                                  F' ≅
                                                F) →
                                              CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F'
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.mem_cylinder_iff_le_firstDiff : ∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n}, x ≠ y → ∀ (i : ℕ), x ∈ PiNat.cylinder y i ↔ i ≤ PiNat.firstDiff x y