mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {fallback : β} {f : Option β → Option β},
      (t.alter k f).getD k' fallback = if cmp k k' = Ordering.eq then (f t[k]?).getD fallback else t.getD k' fallback
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜},
  HasGradientWithinAt f f' s x → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → HasGradientWithinAt f₁ f' s x
-- Aesop.Index.Forward
Aesop.ForwardIndex.mk.sizeOf_spec : ∀ (tree : Lean.Meta.DiscrTree (Aesop.ForwardRule × Aesop.PremiseIndex))
  (nameToRule : Lean.PHashMap Aesop.RuleName Aesop.ForwardRule) (constRules : Lean.PHashSet Aesop.ForwardRule),
  sizeOf { tree := tree, nameToRule := nameToRule, constRules := constRules } =
    1 + sizeOf tree + sizeOf nameToRule + sizeOf constRules
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.id_naturality_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.Oplax.StrongTrans.id F).naturality f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
-- Mathlib.GroupTheory.Perm.Sign
_private.Mathlib.GroupTheory.Perm.Sign.0.Equiv.Perm.signAux_swap_zero_one : ∀ {n : ℕ} (hn : 2 ≤ n), (Equiv.swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_le_iff : ∀ {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)) (G' : SimpleGraph V),
  G.deleteEdges s ≤ G' ↔ G ≤ SimpleGraph.fromEdgeSet s ⊔ G'
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.List.splitWrtCompositionAux.match_3.splitter : {α : Type u_1} →
  (motive : List α → List ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : List ℕ) →
        ((x : List α) → motive x []) → ((l : List α) → (n : ℕ) → (ns : List ℕ) → motive l (n :: ns)) → motive x x_1
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f))
      (CategoryTheory.ChosenPullbacksAlong.fst R.hom T.hom) =
    CategoryTheory.ChosenPullbacksAlong.fst R.hom S.hom
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.nil.sizeOf_spec : sizeOf Lean.Grind.Linarith.Poly.nil = 1
-- Init.Data.Nat.Div.Lemmas
/-- An induction principle mirroring the base-`b` representation of the number.  -/
Nat.base_induction : ∀ {P : ℕ → Prop} {n : ℕ} (b : ℕ), 1 < b → (∀ m < b, P m) → (∀ (m k : ℕ), k < b → 0 < m → P m → P (b * m + k)) → P n
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.MkHInjTypeResult.thmType : Lean.Meta.MkHInjTypeResult✝ → Lean.Expr
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.toSplittingField_coeff : ∀ {k : Type u} [inst : Field k] {s : Finset (AlgebraicClosure.Monics k)} {f : AlgebraicClosure.Monics k},
  f ∈ s → ∀ (n : ℕ), (AlgebraicClosure.toSplittingField s) ((AlgebraicClosure.subProdXSubC f).coeff n) = 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.ω₁δ_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (a' b' c' : EInt) (hab' : a' ≤ b') (hbc' : b' ≤ c')
  (φ :
    CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE hab) (CategoryTheory.homOfLE hbc) ⟶
      CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE hab') (CategoryTheory.homOfLE hbc'))
  {Z : CategoryTheory.Functor C C}
  (h :
    (t.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab'))).comp
        (CategoryTheory.shiftFunctor C 1) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (t.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 1) (φ.app 2) ⋯))
      (CategoryTheory.CategoryStruct.comp (t.ω₁δ a' b' c' hab' hbc') h) =
    CategoryTheory.CategoryStruct.comp (t.ω₁δ a b c hab hbc)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (t.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 0) (φ.app 1) ⋯))
          (CategoryTheory.shiftFunctor C 1))
        h)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.pos_of_mem_rowLens : ∀ (μ : YoungDiagram), ∀ x ∈ μ.rowLens, 0 < x
-- Mathlib.FieldTheory.SeparableClosure
/-- If `K / E / F` is a field extension tower, then `separableClosure F K` is contained in
`separableClosure E K`.  -/
separableClosure.le_restrictScalars : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  separableClosure F K ≤ IntermediateField.restrictScalars F (separableClosure E K)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_inf : ∀ {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] (N N' : LieSubmodule R L M) (x : M), x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.perm_keys : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)},
  (Std.Internal.List.keys l').Perm (Std.Internal.List.keys l) →
    Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys l'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.keyAtIdx!_eq_get!_map_getElem? : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Balanced → ∀ {i : ℕ}, t.keyAtIdx! i = (Option.map (fun x => x.fst) t.toListModel[i]?).get!
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C)
  (t : CategoryTheory.Limits.Cofan f) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I),
  ((CategoryTheory.Limits.FormalCoproduct.isColimitCofan 𝒜 f).desc t).f p = (t.inj p.fst).f p.snd
-- Lean.Meta.WHNF
Lean.Meta.hasSmartUnfoldingDecl : Lean.Environment → Lean.Name → Bool
-- Mathlib.Data.ENat.Basic
ENat.toNat_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).toNat = n
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.instInhabitedEntries : Inhabited Mathlib.Explode.Entries
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_f_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q n : ℕ) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n)
      (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) h) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) h
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.coe_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (K : AddSubgroup G),
  ↑(AddSubgroup.map f K) = ⇑f '' ↑K
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.eval₂_reflect_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : CommSemiring S] (i : R →+* S) (x : S)
  [inst_2 : Invertible x] (N : ℕ) (f : Polynomial R),
  f.natDegree ≤ N → (Polynomial.eval₂ i (⅟x) (Polynomial.reflect N f) = 0 ↔ Polynomial.eval₂ i x f = 0)
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.instLinearMapClass : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂}, LinearMapClass (B₁ →bᵢ B₂) R M₁ M₂
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.uniformContinuous_eval₂ : ∀ {σ : 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} [IsTopologicalSemiring R] [IsUniformAddGroup R]
  [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ → MvPowerSeries.HasEval a → UniformContinuous (MvPowerSeries.eval₂ φ a)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.symm_apply_mem_iff : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {y : Y},
  e.IsImage s t → y ∈ e.target → (↑e.symm y ∈ s ↔ y ∈ t)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x y : F},
  W.Nonsingular x y →
    WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C (W.negY x y)) *
        WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y) =
      WeierstrassCurve.Affine.CoordinateRing.XIdeal W x
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.instTransIsIndContained : {α : Type u_4} →
  {β : Type u_5} →
    {γ : Type u_6} → Trans SimpleGraph.IsIndContained SimpleGraph.IsIndContained SimpleGraph.IsIndContained
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.singleL.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rk : α) (rv : β rk)
  (rl rr : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.singleL k v l rk rv rl rr =
    Std.DTreeMap.Internal.Impl.bin rk rv (Std.DTreeMap.Internal.Impl.bin k v l rl) rr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote'.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Power)
  (m_1 : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote' ctx (Lean.Grind.CommRing.Mon.mult p m_1) =
    Lean.Grind.CommRing.Mon.denote'.go ctx m_1 (Lean.Grind.CommRing.Power.denote ctx p)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₉ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] →
      Lean.Expr →
        Lean.Expr →
          Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.CategoryTheory.Limits.Final
/-- Given a limit cone over `G : D ⥤ E` we can construct a limit cone over `F ⋙ G`.  -/
CategoryTheory.Functor.Initial.limitConeComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  CategoryTheory.Limits.LimitCone G → CategoryTheory.Limits.LimitCone (F.comp G)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffOn.smul_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {f : M → 𝕜} {s : (x : M) → V x} {u : Set M},
  ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n f u →
    ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u →
      ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (f • s) x⟩) u
-- Mathlib.Order.RelIso.Basic
RelIso.refl_symm : ∀ {α : Type u_1} {r : α → α → Prop}, (RelIso.refl r).symm = RelIso.refl r
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Abundant.of_dvd : ∀ {n m : ℕ}, m.Abundant → m ∣ n → n ≠ 0 → n.Abundant
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `MulAction.isBlock_iff_smul_eq_or_disjoint`. -/
MulAction.IsBlock.smul_eq_or_disjoint : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
-- Init.Data.String.Basic
/-- Returns the position in a string before a specified position, `p`. If `p = ⟨0⟩`, returns `0`. If `p`
is greater than `rawEndPos`, returns the position one byte before `p`. Otherwise, if `p` occurs in the
middle of a multi-byte character, returns the beginning position of that character.

For example, `"L∃∀N".prev ⟨3⟩` is `⟨1⟩`, since byte 3 occurs in the middle of the multi-byte
character `'∃'` that starts at byte 1.

This is a legacy function. The recommended alternative is `String.Pos.prev` or one of its
variants like `String.Pos.prev?`, combined with `String.pos` or another means of obtaining
a `String.Pos`.

Examples:
* `"abc".get ("abc".rawEndPos |> "abc".prev) = 'c'`
* `"L∃∀N".get ("L∃∀N".rawEndPos |> "L∃∀N".prev |> "L∃∀N".prev |> "L∃∀N".prev) = '∃'`
 -/
String.Pos.Raw.prev : String → String.Pos.Raw → String.Pos.Raw
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q], Q.IsStableUnderBaseChange → P.IsStableUnderBaseChange
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.toPartialEquiv_restr : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : Equidecomp X G) (A : Set X),
  (f.restr A).toPartialEquiv = f.restr A
-- Mathlib.Order.Preorder.Chain
isChain_union : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α},
  IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instMonoidWithZero : {α : Type u_1} → [Monoid α] → MonoidWithZero (WithZero α)
-- Mathlib.Algebra.Group.Submonoid.Support
/-- **Alias** of the forward direction of `isMulPointed_iff_mulSupport_eq_bot`. -/
Submonoid.IsMulPointed.mulSupport_eq_bot : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, M.IsMulPointed → M.mulSupport = ⊥
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.MorphismProperty.IsMonoidal.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : CategoryTheory.MonoidalCategory C] [toIsMultiplicative : W.IsMultiplicative],
  (∀ (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂), W g → W (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)) →
    (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂), W f → ∀ (Y : C), W (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)) →
      W.IsMonoidal
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_sInf : ∀ (s : Set ENNReal), (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.equivalence_inverse_obj_coe : ∀ (X : MonCat), ↑(AddMonCat.equivalence.inverse.obj X) = Additive ↑X
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `k ≠ 0` and `s ≤ k`.  -/
IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero : ∀ {p : ℕ} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k s : ℕ},
  IsPrimitiveRoot ζ (p ^ (k + 1)) →
    ∀ [hpri : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L],
      Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K) →
        s ≤ k → k ≠ 0 → (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a `CommRing` is a `CommRing`.  -/
SubringClass.toCommRing : {S : Type v} →
  (s : S) → {R : Type u_1} → [inst : CommRing R] → [inst_1 : SetLike S R] → [SubringClass S R] → CommRing ↥s
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.DescendsAlong.top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Q : CategoryTheory.MorphismProperty C},
  ⊤.DescendsAlong Q
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.top_toSubalgebra : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], ⊤.toSubalgebra = ⊤
-- Mathlib.CategoryTheory.Shift.Basic
/-- Constructs a `HasShift C A` instance from `ShiftMkCore`.  -/
CategoryTheory.hasShiftMk : (C : Type u) →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] → CategoryTheory.ShiftMkCore C A → CategoryTheory.HasShift C A
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.mulLeft.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  MeasurableEquiv.mulLeft g = MeasurableEquiv.smul g
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.pow_smul_mod_minimalPeriod : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] (a : G) (b : α) (n : ℕ),
  a ^ (n % Function.minimalPeriod (fun x => a • x) b) • b = a ^ n • b
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.const.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (declName : Lean.Name) (us : List Lean.Level)
  (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_3),
  sizeOf (Lean.Compiler.LCNF.LetValue.const declName us args h) =
    1 + sizeOf declName + sizeOf us + sizeOf args + sizeOf h
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instFaithfulOverOverForget : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T)
  [inst_1 : Q.IsMultiplicative], (CategoryTheory.MorphismProperty.Over.forget P Q X).Faithful
-- Std.Data.DHashMap.Internal.RawLemmas
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.«tacticSimp_to_model[_]Using_» : Lean.ParserDescr
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- A cone over `S.diagram` whose cone point is `S`.  -/
LightProfinite.asLimitCone : (S : LightProfinite) → CategoryTheory.Limits.Cone S.diagram
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
IsLocalRing.closedPoint.congr_simp : ∀ (R : Type u) [inst : CommSemiring R] [inst_1 : IsLocalRing R], IsLocalRing.closedPoint R = IsLocalRing.closedPoint R
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.toLinearMap_includeRight : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  Algebra.TensorProduct.includeRight.toLinearMap = (TensorProduct.AlgebraTensorModule.mk R R A B) 1
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.le_orderHomOfSimplex : ∀ {p q n : ℕ}
  (x :
    ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
            (SSet.stdSimplex.obj { len := q })).nonDegenerate
        n))
  {m : ℕ} (hm : p + q = m) (i : Fin (n + 1)), ↑i ≤ ↑((SSet.prodStdSimplex.orderHomOfSimplex (↑x) hm) i)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Summable.tsum_ofReal_ne_top : ∀ {α : Type u_1} {f : α → ℝ}, Summable f → ∑' (i : α), ENNReal.ofReal (f i) ≠ ⊤
-- Mathlib.Algebra.Star.Module
/-- The decomposition of elements of a star module into their self- and skew-adjoint parts,
as a linear equivalence.  -/
StarModule.decomposeProdAdjoint : (R : Type u_1) →
  (A : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [inst_2 : TrivialStar R] →
          [inst_3 : AddCommGroup A] →
            [inst_4 : Module R A] →
              [inst_5 : StarAddMonoid A] →
                [inst_6 : StarModule R A] → [Invertible 2] → A ≃ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)
-- Mathlib.FieldTheory.ChevalleyWarning
/-- The **Chevalley–Warning theorem**, unary version.
Let `f` be a multivariate polynomial in finitely many variables (`X s`, `s : σ`)
over a finite field of characteristic `p`.
Assume that the total degree of `f` is less than the cardinality of `σ`.
Then the number of solutions of `f` is divisible by `p`.
See `char_dvd_card_solutions_of_sum_lt` for a version that takes a family of polynomials `f i`.  -/
char_dvd_card_solutions : ∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ] [inst_3 : DecidableEq σ]
  [inst_4 : DecidableEq K] (p : ℕ) [CharP K p] {f : MvPolynomial σ K},
  f.totalDegree < Fintype.card σ → p ∣ Fintype.card { x // (MvPolynomial.eval x) f = 0 }
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.transpose_mul_self_isDiag_iff_hasOrthogonalCols : ∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Fintype m] [inst_1 : Mul α] [inst_2 : AddCommMonoid α]
  {A : Matrix m n α}, (A.transpose * A).IsDiag ↔ A.HasOrthogonalCols
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.toMonObj_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C}, Function.Injective (@CategoryTheory.GrpObj.toMonObj C inst inst_1 X)
-- Mathlib.Topology.Category.TopCat.Basic
/-- This prevents `TopCat.of X` being printed as `{ carrier := X, str := ... }` by
`delabStructureInstance`.  -/
TopCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- A closed operator is trivially closable.  -/
LinearPMap.IsClosed.isClosable : ∀ {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.IsClosed → f.IsClosable
-- Init.Data.List.MapIdx
List.getElem_mapFinIdx_go : ∀ {α : Type u_1} {β : Type u_2} {bs : List α} {acc : Array β} {as : List α} {f : (i : ℕ) → α → i < as.length → β}
  {i : ℕ} {h : bs.length + acc.size = as.length} {w : i < (List.mapFinIdx.go as f bs acc h).length},
  (List.mapFinIdx.go as f bs acc h)[i] = if w' : i < acc.size then acc[i] else f i bs[i - acc.size] ⋯
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_inter_null_of_null_left : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {S : Set α} (T : Set α),
  μ S = 0 → μ (S ∩ T) = 0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- An arbitrarily chosen partial map representing `f`. Use `RationalMap.toPartialMap` instead
if `X` is reduced and `Y` is separated.  -/
AlgebraicGeometry.Scheme.RationalMap.representative : {X Y : AlgebraicGeometry.Scheme} → X.RationalMap Y → X.PartialMap Y
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.IsCompatible.desc.congr_simp : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 2)} {f f_1 : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (e_f : f = f_1) (hf : SSet.horn.IsCompatible f), hf.desc = ⋯.desc