mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.trans : ∀ (R : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Type u_1)
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [inst_5 : Module S M] [IsScalarTower R S M]
  [Module.FinitePresentation R S] [Module.FinitePresentation S M], Module.FinitePresentation R M
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_ΨSq : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ),
  (W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.nhdsWithin_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set (OnePoint X)) (x : X),
  nhdsWithin (↑x) s = Filter.map OnePoint.some (nhdsWithin x (OnePoint.some ⁻¹' s))
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.mem_perpBisector_pointReflection_iff_inner_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
  c ∈ AffineSubspace.perpBisector p₁ ((Equiv.pointReflection p₂) p₁) ↔ inner ℝ (c -ᵥ p₂) (p₁ -ᵥ p₂) = 0
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.modify.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : β k → β k)
  (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.modify k f t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l r =>
      match h : compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.inner sz k' v' (Std.DTreeMap.Internal.Impl.modify k f l) r
      | Ordering.gt => Std.DTreeMap.Internal.Impl.inner sz k' v' l (Std.DTreeMap.Internal.Impl.modify k f r)
      | Ordering.eq => Std.DTreeMap.Internal.Impl.inner sz k (f (cast ⋯ v')) l r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (↑(t.insertMany l ⋯)).getKey! k' = k
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeOption.match_1.splitter : {n : ℕ} →
  (motive : Fin (n + 1) → Sort u_1) →
    (x : Fin (n + 1)) → (Unit → motive ⟨0, ⋯⟩) → ((i : ℕ) → (h : i + 1 < n + 1) → motive ⟨i.succ, h⟩) → motive x
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Reinterpreting a linear map in the category of `R`-modules  -/
ModuleCat.«term↟_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.mul_prod_Ioo_eq_prod_Ioc : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a < b → f b * ∏ x ∈ Finset.Ioo a b, f x = ∏ x ∈ Finset.Ioc a b, f x
-- Mathlib.Logic.Function.Conjugate
/-- If `f` and `f'` commute with `g`, then `f ∘ f'` commutes with `g` as well.  -/
Function.Commute.comp_left : ∀ {α : Type u_1} {f f' g : α → α}, Function.Commute f g → Function.Commute f' g → Function.Commute (f ∘ f') g
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
AddEquiv.toHomeomorph_toContinuousAddEquiv : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  {e : G ≃+ H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s), ↑(e.toContinuousAddEquiv he) = e.toHomeomorph he
-- Init.Data.String.Basic
/-- Given a valid position on a slice `s`, obtains the corresponding valid position on the
underlying string `s.str`.  -/
String.Slice.Pos.str : {s : String.Slice} → s.Pos → s.str.Pos
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.not_limZero_of_not_congr_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv}, ¬f ≈ 0 → ¬f.LimZero
-- Mathlib.Tactic.TermCongr
/-- Elaborates a congruence hole and returns either the left-hand side or the right-hand side,
annotated with information necessary to generate a congruence lemma.  -/
Mathlib.Tactic.TermCongr.elabCHole : Lean.Syntax → Bool → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.extract.match_1.eq_1 : ∀ (motive : Substring.Raw → String.Pos.Raw → String.Pos.Raw → Sort u_1) (s : String) (b e b' e' : String.Pos.Raw)
  (h_1 : (s : String) → (b e b' e' : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := e } b' e'),
  (match { str := s, startPos := b, stopPos := e }, b', e' with
    | { str := s, startPos := b, stopPos := e }, b', e' => h_1 s b e b' e') =
    h_1 s b e b' e'
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapIsometry_id_id : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F],
  TensorProduct.mapIsometry LinearIsometry.id LinearIsometry.id = LinearIsometry.id
-- Aesop.Tree.Tracing
_private.Aesop.Tree.Tracing.0.Aesop.Goal.traceMetadata.trcNode : Aesop.TraceOption → Lean.MessageData → Lean.MetaM Unit → Lean.MetaM Unit
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommMonoidOfAddMonoidHomClass.eq_1 : ∀ {ι : 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 : Nonempty ι]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instAddCommMonoidOfAddMonoidHomClass = { toAddMonoid := DirectLimit.instAddMonoid, add_comm := ⋯ }
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructor.match_3.eq_1 : ∀ (motive : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (p : Lean.Elab.Tactic.RCases.RCasesPatt) → motive [p])
  (h_3 : (ps : List Lean.Elab.Tactic.RCases.RCasesPatt) → motive ps),
  (match [] with
    | [] => h_1 ()
    | [p] => h_2 p
    | ps => h_3 ps) =
    h_1 ()
-- Mathlib.RingTheory.Localization.FractionRing
/-- As a corollary, `Rat` is also a localization at only positive integers.  -/
instIsLocalizationIntPosRat : IsLocalization (Submonoid.pos ℤ) ℚ
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- For complex-valued functions, expand the definition of `proximity f a₀` in case where `a₀` is zero.
This is a simple variant of `proximity_zero` defined above.
 -/
ValueDistribution.proximity_zero_of_complexValued : ∀ {f : ℂ → ℂ}, ValueDistribution.proximity f 0 = Real.circleAverage (fun x => ‖f⁻¹ x‖.posLog) 0
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumcenterWeightsWithCircumcenter.eq_1 : ∀ (n : ℕ) (a : Fin (n + 1)),
  Affine.Simplex.circumcenterWeightsWithCircumcenter n (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a) = 0
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.prop : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} (h : D.IsTerminal e), D.P e
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
max_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] [AddRightMono α] (a b c : α), max a b + c = max (a + c) (b + c)
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
Profinite.NobelingProof.GoodProducts.Plimit : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  Order.IsSuccLimit o → (∀ o' < o, Profinite.NobelingProof.P I o') → Profinite.NobelingProof.P I o
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_eq_restrict_iUnion_iff : ∀ {α : Type u_2} {δ : Type u_4} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι]
  (s : ι → Set α) (f g : α → δ), f =ᵐ[μ.restrict (⋃ i, s i)] g ↔ ∀ (i : ι), f =ᵐ[μ.restrict (s i)] g
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- The complete hypergraph with a given vertex set, which has each subset of the vertex set as an
edge.  -/
Hypergraph.completeOn : {α : Type u_1} → Set α → Hypergraph α
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- Let `v : Valuation R Γ₀`. If `R` has `Valued R Γ₀'` defined via construction through
`w : Valuation R Γ₀'`, with `v` equivalent to `w`, then `WithVal.equiv` defines a uniform
space isomorphism `WithVal v ≃ᵤ R`.  -/
WithVal.uniformEquiv : {R : Type u_4} →
  {Γ₀ : Type u_5} →
    {Γ₀' : Type u_6} →
      [inst : Ring R] →
        [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
          [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] →
            {v : Valuation R Γ₀} →
              {w : Valuation R Γ₀'} → [inst_3 : Valued R Γ₀'] → Valued.v = w → v.IsEquiv w → WithVal v ≃ᵤ R
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.not_in₂₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {c c' : γ},
  ¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₂ c')
-- Mathlib.Computability.Encoding
/-- A unary decoding function from `List Bool` to `ℕ`.  -/
Computability.unaryDecodeNat : List Bool → ℕ
-- Init.Data.Option.Lemmas
Option.toArray_none : ∀ (α : Type u_1), none.toArray = #[]
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The equivalence `(M →+ N₁) ≃ (M →+ N₂)` obtained by postcomposition with
an additive equivalence `e : N₁ ≃+ N₂`.  -/
AddEquiv.addMonoidHomCongrRightEquiv : {M : Type u_4} →
  {N₁ : Type u_9} →
    {N₂ : Type u_10} →
      [inst : AddZeroClass M] → [inst_1 : AddMonoid N₁] → [inst_2 : AddMonoid N₂] → N₁ ≃+ N₂ → (M →+ N₁) ≃ (M →+ N₂)
-- Std.Data.TreeSet.Basic
Std.TreeSet.mk.inj : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.TreeSet._auto_1} {inner inner_1 : Std.TreeMap α Unit cmp},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.eq_1 : ∀ (L : FirstOrder.Language) (M : Type w) (N : Type u_1) [inst : L.Structure M] [inst_1 : L.Structure N],
  L.ElementarilyEquivalent M N = (L.completeTheory M = L.completeTheory N)
-- Mathlib.Logic.Equiv.Prod
/-- A subtype of a product defined by componentwise conditions
is equivalent to a product of subtypes.  -/
Equiv.subtypeProdEquivProd : {α : Type u_9} →
  {β : Type u_10} → {p : α → Prop} → {q : β → Prop} → { c // p c.1 ∧ q c.2 } ≃ { a // p a } × { b // q b }
-- Lean.Syntax
Lean.SyntaxNode.getArgs : Lean.SyntaxNode → Array Lean.Syntax
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The additive Haar measure is regular.  -/
MeasureTheory.Measure.regular_addHaarMeasure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G},
  (MeasureTheory.Measure.addHaarMeasure K₀).Regular
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.alter_equiv_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      (↑m₁).Equiv ↑m₂ →
        ∀ {k : α} (f : Option β → Option β),
          (↑(Std.DHashMap.Internal.Raw₀.Const.alter m₁ k f)).Equiv ↑(Std.DHashMap.Internal.Raw₀.Const.alter m₂ k f)
-- Mathlib.Data.Fintype.Quotient
Trunc.finLiftOn_mk : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] {α : ι → Sort u_2} {β : Sort u_3} (a : (i : ι) → α i),
  (Trunc.finLiftOn fun x => ⟦a x⟧) = fun f x => f a
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.public.sizeOf_spec : sizeOf Lean.Elab.Visibility.public = 1
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp.congr_simp : ∀ {𝔸 : Type u_3} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] (x x_1 : 𝔸),
  x = x_1 → NormedSpace.exp x = NormedSpace.exp x_1
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Int.Internal.Linear.instReprPoly_lean : Repr Int.Internal.Linear.Poly
-- Mathlib.Data.List.Defs
List.permutations'.eq_2 : ∀ {α : Type u_1} (a : α) (tail : List α),
  (a :: tail).permutations' = List.flatMap (List.permutations'Aux a) tail.permutations'
-- Mathlib.Order.Cover
WithTop.not_covBy_top : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] {a : WithTop α}, ¬a ⋖ ⊤
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.eval₂Hom_eq_extend : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ : R →+* S} {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : MvPowerSeries.HasEval a) (f : MvPowerSeries σ R),
  (MvPowerSeries.eval₂Hom hφ ha) f = ⋯.extend (MvPolynomial.eval₂ φ a) f
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X X' : C} {Y : F.PartialRightAdjointSource} (f : F.obj X' ⟶ Y.obj) (g : X ⟶ X'),
  CategoryTheory.CategoryStruct.comp g (F.partialRightAdjointHomEquiv.symm f) =
    F.partialRightAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp (F.map g) f)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_zero_of_forall_eq_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M}, (∀ (x : α), f x = 0) → ∑ᶠ (i : α), f i = 0
-- Mathlib.GroupTheory.Index
/-- An additive subgroup has index dividing 2 if and only if there exists `a` such
that for all `b`, at least one of `b + a` and `b` belongs to `H`.  -/
AddSubgroup.index_dvd_two_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index ∣ 2 ↔ ∃ a, ∀ (b : G), b + a ∈ H ∨ b ∈ H
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- A set in `WeakDual 𝕜 E` is bounded iff its image in `StrongDual 𝕜 E` is bounded.  -/
WeakDual.isBounded_toStrongDual_preimage_iff_isBounded : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set (StrongDual 𝕜 E)},
  Bornology.IsBounded (⇑WeakDual.toStrongDual ⁻¹' s) ↔ Bornology.IsBounded s
-- Mathlib.Order.Hom.Basic
OrderHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = f
-- Std.Data.TreeMap.Raw.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.
 -/
Std.TreeMap.Raw.insert : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → β → Std.TreeMap.Raw α β cmp
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.epi_of_isLocallySurjective' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Sheaf J (Type w)} (φ : F₁ ⟶ F₂) [CategoryTheory.Sheaf.IsLocallySurjective φ],
  CategoryTheory.Epi φ
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.aeval_sumIDeriv_eq_eval : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Polynomial R)
  (r : A),
  (Polynomial.aeval r) (Polynomial.sumIDeriv p) =
    Polynomial.eval r (Polynomial.sumIDeriv (Polynomial.map (algebraMap R A) p))
-- Mathlib.NumberTheory.NumberField.ClassNumber
/-- Let `K` be a number field and let `M K` be the Minkowski bound of `K`.
To show that `𝓞 K` is a PID it is enough to show that, for all (natural) primes
`p ∈ Finset.Icc 1 ⌊(M K)⌋₊`, all ideals `P` above `p` such that
`p ^ (span ({p}).inertiaDeg P) ≤ ⌊(M K)⌋₊` are principal. This is the standard technique to prove
that `𝓞 K` is principal, see [marcus1977number], discussion after Theorem 37.
If `K/ℚ` is Galois, one can use the more convenient
`RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc`
below.

The way this theorem should be used is to first compute `⌊(M K)⌋₊` and then to use `fin_cases`
to deal with the finite number of primes `p` in the interval.  -/
RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  (∀
      p ∈
        Finset.Icc 1
          ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
              (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
                √|↑(NumberField.discr K)|)⌋₊,
      Nat.Prime p →
        ∀ P ∈ (Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K),
          p ^ P.inertiaDeg ℤ ≤
              ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
                  (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
                    √|↑(NumberField.discr K)|)⌋₊ →
            Submodule.IsPrincipal P) →
    IsPrincipalIdealRing (NumberField.RingOfIntegers K)
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.exportIREntries.unsafe_1 : Array Lean.IR.Decl → Array Lean.EnvExtensionEntry
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2}
  [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C]
  (F : (i : α) → CategoryTheory.Functor (I i) C) {β : Type u_3} (f : β ≃ α)
  [inst_3 : CategoryTheory.Limits.HasProductsOfShape β C] (X : (i : α) → I i),
  (CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct F f).inv.app X =
    CategoryTheory.Limits.Pi.map' ⇑f fun j => CategoryTheory.CategoryStruct.id ((F (f j)).obj (X (f j)))
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.continuousAt_const_rpow : ∀ {a b : ℝ}, a ≠ 0 → ContinuousAt (fun x => a ^ x) b
-- Mathlib.Tactic.GCongr.Core
/-- If `r` is of the form `rel a b`, replace either `a` or `b` with `e`.  -/
Mathlib.Tactic.GCongr.updateRel : Lean.Expr → Lean.Expr → Bool → Lean.Expr
-- Init.Data.Int.Order
Int.natAbs_ne_zero : ∀ {a : ℤ}, a.natAbs ≠ 0 ↔ a ≠ 0
-- Init.Omega.Constraint
Lean.Omega.Constraint.map.eq_1 : ∀ (c : Lean.Omega.Constraint) (f : ℤ → ℤ),
  c.map f = { lowerBound := Option.map f c.lowerBound, upperBound := Option.map f c.upperBound }
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The family of seminorms on `WeakDual 𝕜 E` given by `fun x f ↦ ‖f x‖`, indexed by `E`.
This is the seminorm family associated to the weak-\* topology via `topDualPairing`.  -/
WeakDual.seminormFamily : (𝕜 : Type u_1) →
  (E : Type u_3) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → SeminormFamily 𝕜 (WeakDual 𝕜 E) E
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Embedding of ordered finpartitions in a sigma type. The sigma type on the right is quite big,
but this is enough to get finiteness of ordered finpartitions.  -/
OrderedFinpartition.embSigma : (n : ℕ) → OrderedFinpartition n → (l : Fin (n + 1)) × (p : Fin ↑l → Fin (n + 1)) × ((i : Fin ↑l) → Fin ↑(p i) → Fin n)
-- Std.Do.Triple.SpecLemmas
/-- The position of the cursor in the list.
It's a shortcut for the number of elements in the prefix.
 -/
List.Cursor.pos : {α : Type u_1} → {l : List α} → l.Cursor → ℕ
-- Mathlib.Topology.Instances.Irrational
Irrational.instNoMinOrderSubtypeReal : NoMinOrder { x // Irrational x }
-- Lean.Elab.Tactic.Try
/-- Like `evalAndSuggest`, but returns the suggestion array instead of emitting it.  -/
Lean.Elab.Tactic.Try.evalAndCollectSuggestions : Lean.TSyntax `tactic →
  ℕ → optParam Lean.Try.Config { } → Lean.Elab.Tactic.TacticM (Array Lean.Meta.Tactic.TryThis.Suggestion)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.root_mul : ∀ {R : Type u} {a : R} [inst : CommSemiring R] {p q : Polynomial R} [NoZeroDivisors R],
  (p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a
-- Lean.Parser.Extra
Lean.Parser.incQuotDepth.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator.takeWhile_toList : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] {z : Std.DTreeMap.Internal.Zipper α β} {bound : α}
  {z_ord : z.Ordered},
  List.takeWhile (fun e => (compare e.fst bound).isLE) z.toList =
    List.filter (fun e => (compare e.fst bound).isLE) z.toList
-- Std.Data.TreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key.  -/
Std.TreeMap.entryAtIdx : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap α β cmp) → (n : ℕ) → n < t.size → α × β
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] (S : ι → Subsemigroup Mᵐᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- If `f` is closable, then the closure is closed.  -/
LinearPMap.IsClosable.closure_isClosed : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F}, f.IsClosable → f.closure.IsClosed
-- Mathlib.Analysis.Convex.Star
StarConvex.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {s t : Set E}, StarConvex 𝕜 x s → StarConvex 𝕜 x t → StarConvex 𝕜 x (s ∩ t)
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.IndiscreteTopology.pseudoMetrizableSpace : ∀ {X : Type u_2} [inst : TopologicalSpace X] [IndiscreteTopology X], TopologicalSpace.PseudoMetrizableSpace X
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH1_τ₁ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  (groupHomology.mapShortComplexH1 f φ).τ₁ = groupHomology.chainsMap₂ f φ
-- Mathlib.Analysis.Matrix.Order
Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜},
  A.PosSemidef ↔ A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a | 0 ≤ a}
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurveOn_comp_mul_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ} {a : ℝ},
  a ≠ 0 → (IsMIntegralCurveOn (γ ∘ fun x => x * a) (a • v) {t | t * a ∈ s} ↔ IsMIntegralCurveOn γ v s)
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The weak-star topology is coarser than the dual-norm topology.  -/
NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], ContinuousLinearMap.uniformSpace.toTopologicalSpace ≤ instTopologicalSpaceWeakDual 𝕜 E
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.mk : {n : ℕ} → (blocks : List ℕ) → (∀ {i : ℕ}, i ∈ blocks → 0 < i) → blocks.sum = n → Composition n