mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
FGAlgCatSkeleton.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (n_1 : ℕ)
  (I_1 : Ideal (MvPolynomial (Fin n_1) R)), ({ n := n, I := I } = { n := n_1, I := I_1 }) = (n = n_1 ∧ I ≍ I_1)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The functor taking an ideal sheaf to its associated subscheme.  -/
AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor : (Y : AlgebraicGeometry.Scheme) → CategoryTheory.Functor Y.IdealSheafDataᵒᵖ (CategoryTheory.Over Y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.ofList_singleton : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α} {v : β k},
  Std.DHashMap.Raw.ofList [⟨k, v⟩] = ∅.insert k v
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm c_1) = (c = c_1)
-- Mathlib.Order.Cofinal
instInhabitedSubtypeSetIsCofinal : {α : Type u_1} → [inst : Preorder α] → Inhabited { s // IsCofinal s }
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.HomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).right =
    CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h.right
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.constantsVarsEquiv_apply : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (a : (L.withConstants γ).Term α),
  FirstOrder.Language.Term.constantsVarsEquiv a = a.constantsToVars
-- Mathlib.Algebra.Group.Submonoid.Membership
IsScalarTower.of_mclosure_eq_top : ∀ {M : Type u_1} {N : Type u_4} {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M N] [inst_2 : SMul N α]
  [inst_3 : MulAction M α] {s : Set M},
  Submonoid.closure s = ⊤ → (∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z) → IsScalarTower M N α
-- Mathlib.Order.FixedPoints
OrderHom.le_nextFixed : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x), x ≤ ↑(f.nextFixed x hx)
-- Mathlib.Topology.Inseparable
SeparationQuotient.mk_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X], SeparationQuotient.mk 0 = 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.contains t.max! = true
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The inclusion of a summand in `∐ obj₁`.  -/
CategoryTheory.OrthogonalReflection.D₁.ιLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {Z : C} →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          {X Y : C} → (f : X ⟶ Y) → W f → (X ⟶ Z) → (X ⟶ ∐ CategoryTheory.OrthogonalReflection.D₁.obj₁)
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_zpow_right : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute a ↑u → ∀ (m : ℤ), Commute a ↑(u ^ m)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The `bot` subgraph is the subgraph with no vertices or edges.  -/
SimpleGraph.Subgraph.instBot : {V : Type u} → {G : SimpleGraph V} → Bot G.Subgraph
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubalgebra_map : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (S : IntermediateField K L) (f : L →ₐ[K] L'),
  (IntermediateField.map f S).toSubalgebra = Subalgebra.map f S.toSubalgebra
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_ne_top`. -/
ENat.coe_ne_top : ∀ (a : ℕ), ↑a ≠ ⊤
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.Closeds.lipschitz_sup : ∀ {α : Type u_1} [inst : EMetricSpace α], LipschitzWith 1 fun p => p.1 ⊔ p.2
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concatRecAux.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1}
  (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
  (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)) {u v : V}
  (v_3 : V) (h : G.Adj u v_3) (p : G.Walk v_3 v),
  SimpleGraph.Walk.concatRecAux Hnil Hconcat (SimpleGraph.Walk.cons h p) =
    ⋯ ▸ Hconcat p.reverse ⋯ (SimpleGraph.Walk.concatRecAux Hnil Hconcat p)
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_add_right_neg : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α),
  a ∉ s → (s + t).erase a = s + t.erase a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {h : (Std.DTreeMap.Const.get? t a).isSome = true},
  (Std.DTreeMap.Const.get? t a).get h = Std.DTreeMap.Const.get t a ⋯
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile.mk : Lean.Lsp.DocumentUri → Lean.Lsp.DocumentUri → Option Lean.Lsp.CreateFile.Options → Option String → Lean.Lsp.RenameFile
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.forget_map : ∀ (S : AlgebraicGeometry.Scheme)
  {X Y :
    CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id AlgebraicGeometry.Scheme)
      (CategoryTheory.Functor.fromPUnit S) @AlgebraicGeometry.WeaklyEtale ⊤ ⊤}
  (f : X ⟶ Y), (AlgebraicGeometry.Scheme.ProEt.forget S).map f = CategoryTheory.MorphismProperty.Comma.Hom.hom f
-- Init.Data.Array.MapIdx
Array.mapFinIdx_empty : ∀ {α : Type u_1} {β : Type u_2} {f : (i : ℕ) → α → i < 0 → β}, #[].mapFinIdx f = #[]
-- Mathlib.RingTheory.Congruence.Hom
/-- The **third isomorphism theorem for (semi-)rings**.  -/
RingCon.quotientQuotientEquivQuotient : {M : Type u_1} →
  [inst : NonAssocSemiring M] → (c d : RingCon M) → (h : c ≤ d) → (RingCon.ker (c.map d h)).Quotient ≃+* d.Quotient
-- Mathlib.NumberTheory.WellApproximable
mem_approx_add_orderOf_iff : ∀ {A : Type u_1} [inst : SeminormedAddGroup A] {n : ℕ} {δ : ℝ} {a : A},
  a ∈ approxAddOrderOf A n δ ↔ ∃ b, addOrderOf b = n ∧ a ∈ Metric.ball b δ
-- Mathlib.Order.ModularLattice
eq_of_le_of_sup_le_of_inf_le : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x y z : α}, y ≤ x → x ⊔ z ≤ y ⊔ z → x ⊓ z ≤ y ⊓ z → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasTerminalChangeDiagram : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C}
  {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1}) C},
  CategoryTheory.Limits.HasLimit F₁ → CategoryTheory.Limits.HasLimit F₂
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- Given the data of the constructible set `s`, build the data of the constructible set
`{I | {x | f x ∈ I} ∈ s}`.  -/
PrimeSpectrum.ConstructibleSetData.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        (R →+* S) → PrimeSpectrum.ConstructibleSetData R → PrimeSpectrum.ConstructibleSetData S
-- Lean.Elab.ConfigEval.Types
/-- Ref for the entire configuration item  -/
Lean.Elab.ConfigEval.ConfigItem.ref : Lean.Elab.ConfigEval.ConfigItem → Lean.Syntax
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
ModuleCat.MonoidalCategory.tensorμ_apply : ∀ {R : Type u} [inst : CommRing R] {A B C D : ModuleCat R} (x : ↑A) (y : ↑B) (z : ↑C) (w : ↑D),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.tensorμ A B C D))
      (x ⊗ₜ[R] y ⊗ₜ[R] (z ⊗ₜ[R] w)) =
    x ⊗ₜ[R] z ⊗ₜ[R] (y ⊗ₜ[R] w)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {I : ProjectiveSpectrum 𝒜},
  I ∈ (ProjectiveSpectrum.zeroLocus 𝒜 {f})ᶜ ↔ f ∉ I.asHomogeneousIdeal
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.equivNum.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsDomain R] [inst_4 : Module.IsTorsionFree R P] [inst_5 : Nontrivial P] {I : FractionalIdeal S P}
  (h_nz : ↑I.den ≠ 0), FractionalIdeal.equivNum h_nz = FractionalIdeal.equivNum h_nz
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The valuation less-equal operator arising from `ValuativeRel`.  -/
«term_≤ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCongrRight_single : ∀ {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} [hp : Fact (1 ≤ p)]
  [inst : Fintype ι] [inst_1 : Semiring 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_4 : (i : ι) → Module 𝕜 (α i)]
  [inst_5 : (i : ι) → Module 𝕜 (β i)] (e : (i : ι) → α i ≃ₗᵢ[𝕜] β i) [inst_6 : DecidableEq ι] (i : ι) (v : α i),
  (LinearIsometryEquiv.piLpCongrRight p e) (PiLp.single p i v) = PiLp.single p i ((e i) v)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.smul : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α} {𝕜 : Type u_7} [inst_1 : NormedAddCommGroup 𝕜] [inst_2 : SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E]
  {f : α → E}, MeasureTheory.IntegrableAtFilter f l μ → ∀ (c : 𝕜), MeasureTheory.IntegrableAtFilter (c • f) l μ
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.mk.injEq : ∀ {M : Type u_10} {N : Type u_11} [inst : Mul M] [inst_1 : Mul N] (toFun : M → N)
  (map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y) (toFun_1 : M → N)
  (map_mul'_1 : ∀ (x y : M), toFun_1 (x * y) = toFun_1 x * toFun_1 y),
  ({ toFun := toFun, map_mul' := map_mul' } = { toFun := toFun_1, map_mul' := map_mul'_1 }) = (toFun = toFun_1)
-- Mathlib.Data.Sign.Defs
SignType.instDecidableLE : DecidableLE SignType
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.isRepresentable : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  (e : F.RepresentableBy Y), F.IsRepresentable
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The right adjoint of a 1-morphism.  -/
CategoryTheory.Bicategory.rightAdjoint : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] → {a b : B} → (f : a ⟶ b) → [CategoryTheory.Bicategory.IsLeftAdjoint f] → b ⟶ a
-- Mathlib.Algebra.Order.Module.Defs
MulPosStrictMono.toSMulPosStrictMono : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [inst_2 : Preorder α] [MulPosStrictMono α], SMulPosStrictMono α α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.filterMap_equiv_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : (a : α) → β a → Bool}
  (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap (fun k => Option.guard fun v => f k v) t ⋯).impl.Equiv
    (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_mem_Ico_zpow : ∀ {x y : ENNReal}, x ≠ 0 → x ≠ ⊤ → 1 < y → y ≠ ⊤ → ∃ n, x ∈ Set.Ico (y ^ n) (y ^ (n + 1))
-- Mathlib.Logic.Denumerable
Denumerable.decode_eq_ofNat : ∀ (α : Type u_3) [inst : Denumerable α] (n : ℕ), Encodable.decode n = some (Denumerable.ofNat α n)
-- Mathlib.Algebra.BigOperators.Ring.List
Commute.list_sum_right : ∀ {R : Type u_5} [inst : NonUnitalNonAssocSemiring R] (a : R) (l : List R), (∀ b ∈ l, Commute a b) → Commute a l.sum
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.f : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → {A B : HomologicalComplex V c} → A.Hom B → (i : ι) → A.X i ⟶ B.X i
-- Aesop.Forward.State
Aesop.ForwardState.mk.sizeOf_spec : ∀ (ruleStates : Lean.PHashMap Aesop.RuleName Aesop.RuleState)
  (hyps : Lean.PHashMap Lean.FVarId (Lean.PArray (Aesop.RuleName × Aesop.PremiseIndex)))
  (patSubsts : Lean.PHashMap Aesop.PatSubstSource (Lean.PArray (Aesop.RuleName × Aesop.Substitution))),
  sizeOf { ruleStates := ruleStates, hyps := hyps, patSubsts := patSubsts } =
    1 + sizeOf ruleStates + sizeOf hyps + sizeOf patSubsts
-- Mathlib.LinearAlgebra.Lagrange
Polynomial.eq_of_degrees_lt_of_eval_finset_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f g : Polynomial R} (s : Finset R),
  f.degree < ↑s.card → g.degree < ↑s.card → (∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g) → f = g
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.univ_natDegree : ∀ (R : Type u_1) (n : Type u_3) [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] [Nontrivial R],
  (Matrix.charpoly.univ R n).natDegree = Fintype.card n
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The morphism that is part of a morphism of structured arrows.  -/
CategoryTheory.StructuredArrow.Hom.right : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} → {X Y : CategoryTheory.StructuredArrow S T} → (X ⟶ Y) → (X.right ⟶ Y.right)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.leadingCoeff_map_eq_of_isUnit_leadingCoeff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] [Nontrivial S] (f : R →+* S),
  IsUnit p.leadingCoeff → (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.kleisliCatEquivKleisli_unitIso : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m],
  (CategoryTheory.kleisliCatEquivKleisli m).unitIso =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯
-- Mathlib.RingTheory.Ideal.IsPrimary
Submodule.IsPrimary.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (S : Submodule R M), S.IsPrimary = (S ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S)
-- Mathlib.Data.Finset.Dedup
List.toFinset_eq_iff_perm_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α}, l.toFinset = l'.toFinset ↔ l.dedup.Perm l'.dedup
-- Lean.Parser.Term
Lean.Parser.Term.whereDecls.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.kroneckerAlgEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (x : TensorProduct R (Matrix m m R) (Matrix n n R)),
  (Matrix.kroneckerAlgEquiv m n R) x = (kroneckerLinearEquiv m m n n R) x
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.associator_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H I : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Mathlib.Algebra.Ring.Subring.MulOpposite
/-- Bijection between a subring `S` and its opposite.  -/
Subring.addEquivOp : {R : Type u_2} → [inst : NonAssocRing R] → (S : Subring R) → ↥S ≃+ ↥S.op
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- The congruence subgroup `Gamma1` of `SL(2, ℤ)` consisting of matrices
whose bottom row is congruent to `(0,1)` modulo `N`.  -/
CongruenceSubgroup.Gamma1 : ℕ → Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)
-- Mathlib.Analysis.Normed.Lp.ProdLp
_private.Mathlib.Analysis.Normed.Lp.ProdLp.0.WithLp.prod_antilipschitzWith_ofLp_aux : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], AntilipschitzWith (2 ^ (1 / p).toReal) WithLp.ofLp
-- Lean.Util.PtrSet
/-- Set of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.
 -/
Lean.PtrSet : Type → Type
-- Mathlib.Algebra.Lie.Prod
LieHom.fst_apply : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (x : L₁ × L₂), (LieHom.fst R L₁ L₂) x = x.1
-- Mathlib.RingTheory.Regular.RegularSequence
_private.Mathlib.RingTheory.Regular.RegularSequence.0.RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing.match_3.splitter : (motive :
    (x : Type u_1) →
      (x_1 : CommRing x) →
        (x_2 : Type u_2) →
          (x_3 : AddCommGroup x_2) →
            (x_4 : Module x x_2) → (x_5 : List x) → RingTheory.Sequence.IsWeaklyRegular x_2 x_5 → Sort u_3) →
  (x : Type u_1) →
    (x_1 : CommRing x) →
      (x_2 : Type u_2) →
        (x_3 : AddCommGroup x_2) →
          (x_4 : Module x x_2) →
            (x_5 : List x) →
              (x_6 : RingTheory.Sequence.IsWeaklyRegular x_2 x_5) →
                ((R : Type u_1) →
                    (x : CommRing R) →
                      (M : Type u_2) →
                        (x_7 : AddCommGroup M) →
                          (x_8 : Module R M) →
                            (x_9 : RingTheory.Sequence.IsWeaklyRegular M []) → motive R x M x_7 x_8 [] x_9) →
                  ((α : Type u_1) →
                      (x : CommRing α) →
                        (M : Type u_2) →
                          (x_7 : AddCommGroup M) →
                            (x_8 : Module α M) →
                              (r : α) →
                                (rs : List α) →
                                  (h : RingTheory.Sequence.IsWeaklyRegular M (r :: rs)) →
                                    motive α x M x_7 x_8 (r :: rs) h) →
                    motive x x_1 x_2 x_3 x_4 x_5 x_6
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.prod_eq_top_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {s : Submonoid M} {t : Submonoid N},
  s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
-- Mathlib.Algebra.Group.Ext
Monoid.mk.congr_simp : ∀ {M : Type u} [toSemigroup : Semigroup M] [toSemigroup_1 : Semigroup M] (e_toSemigroup : toSemigroup = toSemigroup_1)
  [toOne : One M] [toOne_1 : One M] (e_toOne : toOne = toOne_1) (one_mul : ∀ (a : M), 1 * a = a)
  (mul_one : ∀ (a : M), a * 1 = a) [toNPow : NPow M] [toNPow_1 : NPow M] (e_toNPow : toNPow = toNPow_1)
  (npow_zero : ∀ (x : M), x ^ 0 = 1) (npow_succ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x),
  { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one, toNPow := toNPow,
      npow_zero := npow_zero, npow_succ := npow_succ } =
    { toSemigroup := toSemigroup_1, toOne := toOne_1, one_mul := ⋯, mul_one := ⋯, toNPow := toNPow_1, npow_zero := ⋯,
      npow_succ := ⋯ }
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_gt_d6 : 3.141592 < Real.pi
-- Mathlib.Order.Minimal
minimal_toDual : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α],
  Minimal (fun x => P (OrderDual.ofDual x)) (OrderDual.toDual x) ↔ Maximal P x
-- Mathlib.Control.Random
Random.instBoundedRandomNat : {m : Type → Type u_1} → [Monad m] → BoundedRandom m ℕ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_insertIfNew_le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α} {v : β}, (cmp (t.insertIfNew k v).minKey! t.minKey!).isLE = true
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- Two multivariate formal power series are equal
if and only if all their coefficients are equal.  -/
MvPowerSeries.ext_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ ψ : MvPowerSeries σ R},
  φ = ψ ↔ ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) φ = (MvPowerSeries.coeff n) ψ
-- Mathlib.RingTheory.Valuation.Basic
Valuation.leAddSubgroup_zero : ∀ {Γ₀ : Type u_4} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_7} [inst_1 : Field K] (v : Valuation K Γ₀),
  v.leAddSubgroup 0 = ⊥
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.isDiscreteValuationRing_of_compactSpace : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀]
  [hn : Valued.v.IsNontrivial] [CompactSpace ↥(Valued.integer K)], IsDiscreteValuationRing ↥(Valued.integer K)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.comp_inj : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (h : L.Embedding N P) (f g : L.Embedding M N), h.comp f = h.comp g ↔ f = g
-- Mathlib.Order.LiminfLimsup
liminf_min : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) liminf_min._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) liminf_min._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) liminf_min._auto_5 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) liminf_min._auto_7 →
          Filter.liminf (fun a => min (u a) (v a)) f = min (Filter.liminf u f) (Filter.liminf v f)
-- Mathlib.Order.Filter.Pi
/-- If a function tends to a product `Filter.pi f` of filters, then its `i`-th component tends to
`f i`. See also `Filter.Tendsto.apply_nhds` for the special case of converging to a point in a
product of topological spaces.  -/
Filter.Tendsto.apply : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {β : Type u_3} {m : β → (i : ι) → α i} {l : Filter β},
  Filter.Tendsto m l (Filter.pi f) → ∀ (i : ι), Filter.Tendsto (fun x => m x i) l (f i)
-- Mathlib.Algebra.FreeAlgebra
/-- Noncommutative version of `Algebra.adjoin_range_eq_range`.  -/
Algebra.adjoin_eq_range_freeAlgebra_lift : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Algebra.adjoin R s = ((FreeAlgebra.lift R) Subtype.val).range
-- Mathlib.Algebra.Field.TransferInstance
/-- Transfer `RatCast` across an `Equiv`  -/
Equiv.ratCast : {α : Type u_1} → {β : Type u_2} → α ≃ β → [RatCast β] → RatCast α
-- Lean.Meta.Tactic.Grind.Arith.Simproc
/-- Returns `true`, if `@OfNat.ofNat α n inst` is the standard way we represent `Int` numerals in Lean.
 -/
_private.Lean.Meta.Tactic.Grind.Arith.Simproc.0.Lean.Meta.Grind.Arith.isNormIntNum : Lean.Expr → Lean.Expr → Lean.Expr → Bool