mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.IsAllowedEncodedChars.push : ∀ {r : UInt8 → Bool} {c : UInt8} {bs : ByteArray},
  Std.Http.URI.IsAllowedEncodedChars r bs →
    Std.Http.URI.isEncodedChar r c = true → Std.Http.URI.IsAllowedEncodedChars r (bs.push c)
-- Mathlib.Util.Notation3
/-- Expands binders into nested combinators.
For example, the familiar exists is given by:
`expand_binders% (p => Exists p) x y : Nat, x < y`
which expands to the same expression as
`∃ x y : Nat, x < y`
 -/
Mathlib.Notation3.«termExpand_binders%(_=>_)_,_» : Lean.ParserDescr
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.doubleDualEquiv_symm_doubleDualEmb_apply : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Finite α] (a : AddChar (AddChar α ℂ) ℂ),
  AddChar.doubleDualEquiv.symm (AddChar.doubleDualEmb a) = a
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_multiset_prod_of_monic : ∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R),
  (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Turns a `CommGroup` `G` with a `MulDistribMulAction` of a monoid `M` into a
`ℤ`-linear `M`-representation on `Additive G`.  -/
Rep.ofMulDistribMulAction : (M : Type u_1) →
  (G : Type u_2) → [inst : Monoid M] → [inst_1 : CommGroup G] → [MulDistribMulAction M G] → Rep.{u_2, 0, u_1} ℤ M
-- Mathlib.Data.Nat.ModEq
Nat.coprime_of_mul_modEq_one : ∀ (b : ℕ) {a n : ℕ}, a * b ≡ 1 [MOD n] → a.Coprime n
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- If `E` is a normed space, `Lp.simpleFunc E p μ` is a `SMul`. Not declared as an
instance as it is (as of writing) used only in the construction of the Bochner integral.  -/
MeasureTheory.Lp.simpleFunc.smul : {α : Type u_1} →
  {E : Type u_4} →
    {𝕜 : Type u_6} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {p : ENNReal} →
            {μ : MeasureTheory.Measure α} →
              [inst_2 : NormedRing 𝕜] →
                [inst_3 : Module 𝕜 E] → [IsBoundedSMul 𝕜 E] → SMul 𝕜 ↥(MeasureTheory.Lp.simpleFunc E p μ)
-- Mathlib.Data.Set.Lattice
Set.iInter_ofPred : ∀ {α : Type u_1} {ι : Sort u_5} (P : ι → α → Prop), ⋂ i, {x | P i x} = {x | ∀ (i : ι), P i x}
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
_private.Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups.0.termSL : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_inv_right_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] (f g h : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift f
          (CategoryTheory.CategoryStruct.comp g CategoryTheory.GrpObj.inv))
        CategoryTheory.MonObj.mul =
      h ↔
    f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift h g) CategoryTheory.MonObj.mul
-- Init.Data.Array.Lemmas
List.filterMap_toArray : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α},
  Array.filterMap f l.toArray = (List.filterMap f l).toArray
-- Mathlib.Algebra.Lie.SerreConstruction
_private.Mathlib.Algebra.Lie.SerreConstruction.0.CartanMatrix.Relations.adE_of_eq_eq_zero : ∀ (R : Type u) {B : Type v} [inst : CommRing R] (CM : Matrix B B ℤ) (i : B),
  CM i i = 2 → CartanMatrix.Relations.adE R CM (i, i) = 0
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor_map_injective_of_app_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {F G : TopCat.Presheaf C X} {f : F ⟶ G},
  (∀ (U : TopologicalSpace.Opens ↑X),
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U)))) →
    ∀ (x : ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The natural transformation `t.truncLT a ⟶ t.truncLT b` when `a ≤ b`.  -/
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} 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) → (a b : ℤ) → a ≤ b → (t.truncLT a ⟶ t.truncLT b)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto a closed subspace is norm non-increasing.  -/
Submodule.norm_orthogonalProjectionOnto_apply_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (v : E), ‖K.orthogonalProjectionOnto v‖ ≤ ‖v‖
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.mk.sizeOf_spec : ∀ (mvar key : Lean.Expr) (mctx : Lean.MetavarContext) (subgoals : List Lean.Expr) (size : ℕ),
  sizeOf { mvar := mvar, key := key, mctx := mctx, subgoals := subgoals, size := size } =
    1 + sizeOf mvar + sizeOf key + sizeOf mctx + sizeOf subgoals + sizeOf size
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.RatCoeff.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} (value : ℚ) (hyp : Option Lean.Expr) (value_1 : ℚ)
  (hyp_1 : Option Lean.Expr),
  ({ value := value, hyp := hyp } = { value := value_1, hyp := hyp_1 }) = (value = value_1 ∧ hyp = hyp_1)
-- Lean.Elab.Tactic.Grind.Basic
/-- Per-variant persistent `Sym.simp` cache. Keyed by variant name + extra theorem names.  -/
Lean.Elab.Tactic.Grind.Cache.simpState : Lean.Elab.Tactic.Grind.Cache → Std.HashMap Lean.Elab.Tactic.Grind.SimpCacheKey Lean.Meta.Sym.Simp.State
-- Mathlib.Topology.Compactness.Compact
IsCompact.nhdsSet_prod_eq_biSup : ∀ {X : Type u} [inst : TopologicalSpace X] {K : Set X},
  IsCompact K → ∀ {Y : Type u_2} (l : Filter Y), nhdsSet K ×ˢ l = ⨆ x ∈ K, nhds x ×ˢ l
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_mul_nc_go : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ acc : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      acc.NonnegCoeffs →
        Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.mul_nc.go p₂ p₁ acc) =
          Lean.Grind.CommRing.Poly.denoteS ctx acc +
            Lean.Grind.CommRing.Poly.denoteS ctx p₁ * Lean.Grind.CommRing.Poly.denoteS ctx p₂
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_one : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Algebra ℝ A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A], CFC.abs 1 = 1
-- Mathlib.RingTheory.PowerSeries.NoZeroDivisors
/-- The variable of the power series ring over an integral domain is prime.  -/
PowerSeries.X_prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R], Prime PowerSeries.X
-- Mathlib.CategoryTheory.Category.Cat
/-- Functor that gets the set of objects of a category. It is not
called `forget`, because it is not a faithful functor.  -/
CategoryTheory.Cat.objects : CategoryTheory.Functor CategoryTheory.Cat (Type u)
-- Mathlib.Algebra.Group.Defs
Semigroup.mk : {G : Type u} → [toMul : Mul G] → (∀ (a b c : G), a * b * c = a * (b * c)) → Semigroup G
-- Mathlib.Logic.Equiv.Set
Equiv.setCongr_apply : ∀ {α : Type u_3} {s t : Set α} (h : s = t) (a : { a // (fun x => x ∈ s) a }), (Equiv.setCongr h) a = ⟨↑a, ⋯⟩
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.eq_symm_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S) {x : S}
  {y : R}, y = e.symm x ↔ e y = x
-- Mathlib.RingTheory.Polynomial.Basic
/-- **Hilbert basis theorem**: a polynomial ring over a Noetherian ring is a Noetherian ring.  -/
Polynomial.isNoetherianRing : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsNoetherianRing R], IsNoetherianRing (Polynomial R)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeId_hom_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (X : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.Cocone.precomposeId.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.C_one : CartanMatrix.C 1 = CartanMatrix.A 1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When both `S.f` and `S.g` are zero, the middle object `S.X₂` gives a left homology data on S  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofZeros : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → S.f = 0 → S.g = 0 → S.LeftHomologyData
-- Mathlib.Data.Set.Basic
Set.sep_inter : ∀ {α : Type u} {s t : Set α} {p : α → Prop}, {x | (x ∈ s ∧ x ∈ t) ∧ p x} = {x | x ∈ s ∧ p x} ∩ {x | x ∈ t ∧ p x}
-- Mathlib.Topology.Algebra.Group.Basic
continuousSub_of_indiscreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Sub H] [IndiscreteTopology H], ContinuousSub H
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_injective : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  Function.Injective WithVal.ofVal
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_eq_maxKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.maxKey! = t.maxKeyD default
-- Mathlib.MeasureTheory.Function.Piecewise
IndexedPartition.stronglyMeasurable_piecewise : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {s : ι → Set α} {f : ι → α → β} [Countable ι]
  (hs : IndexedPartition s),
  (∀ (i : ι), MeasurableSet (s i)) →
    ∀ [inst_2 : TopologicalSpace β],
      (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable (hs.piecewise f)
-- Mathlib.Order.CompleteLattice.Basic
iSup_split : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (p : β → Prop),
  ⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A real absolute value on a ring determines a `NormedRing` structure.  -/
AbsoluteValue.toNormedRing : {R : Type u_5} → [inst : Ring R] → AbsoluteValue R ℝ → NormedRing R
-- Init.Data.Array.Lemmas
Array.getElem_range : ∀ {n i : ℕ} (h : i < (Array.range n).size), (Array.range n)[i] = i
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) → ((guess : ℕ) → motive 0 guess) → ((fuel guess : ℕ) → motive fuel.succ guess) → motive x x_1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnionIndex.eq_1 : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (J : BoxIntegral.Box ι),
  π.biUnionIndex πi J = if hJ : J ∈ π.biUnion πi then ⋯.choose else I
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.ofHom_hom : ∀ {X Y : NonemptyFinLinOrd} (f : X ⟶ Y), NonemptyFinLinOrd.ofHom (LinOrd.Hom.hom f.hom) = f
-- Mathlib.Algebra.Regular.Basic
/-- The "most used" implication of `mul_and_mul_iff`, with split hypotheses, instead of `∧`.  -/
IsRegular.and_of_mul_of_mul : ∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsRegular (a * b) → IsRegular (b * a) → IsRegular a ∧ IsRegular b
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Sieve.SecondObj.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))} {X : C}
  {S : CategoryTheory.Sieve X} {z₁ z₂ : CategoryTheory.Equalizer.Sieve.SecondObj P S},
  z₁ = z₂ ↔
    ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
      (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
          z₁ =
        (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
          z₂
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddRightCancelSemigroup α],
  OrderDual.instAddRightCancelSemigroup = { toAddSemigroup := OrderDual.instAddSemigroup, toIsRightCancelAdd := ⋯ }
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.nth_modifyNth : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (f : Γ → Γ) (n i : ℕ) (L : Turing.ListBlank Γ),
  (Turing.ListBlank.modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
-- Lean.Parser.Command
/-- Shows the current Lean version. Prints `Lean.versionString`.  -/
Lean.Parser.Command.version : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.unop : C ⥤ D` creates
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.createsLimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
                [CategoryTheory.CreatesColimit K.op F] → CategoryTheory.CreatesLimit K F.unop
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.toPretrivialization.isLinear : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_4 : AddCommMonoid F] [inst_5 : Module R F]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)] [Bundle.Trivialization.IsLinear R e],
  Bundle.Pretrivialization.IsLinear R e.toPretrivialization
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.
If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`,
then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.DTreeMap.Raw.containsThenInsertIfNew : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → (a : α) → β a → Bool × Std.DTreeMap.Raw α β cmp
-- Aesop.Tree.Data
Aesop.Iteration.instDecidableEq : DecidableEq Aesop.Iteration
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- A family indexed by a `Fintype` is affinely independent if and
only if no nontrivial weighted subtractions over `Finset.univ` (where
the sum of the weights is 0) are 0.  -/
affineIndependent_iff_of_fintype : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Fintype ι] (p : ι → P),
  AffineIndependent k p ↔ ∀ (w : ι → k), ∑ i, w i = 0 → (Finset.univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ}
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α α_1 : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) (e_α : α = α_1) [inst_3 : L.IsLeftKanExtension α]
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) (E : ℰ),
  CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv L α P E =
    CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv L α_1 P E
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.instDecidableRelROfFintype : {α : Type u_1} → [Fintype α] → [inst : DecidableEq α] → (i j : α) → DecidableRel ⇑(Equiv.Perm.modSwap i j)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  (Ideal.span {hζ.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- We say a quotient of `α` by `G` `HasAddFundamentalDomain` if there is a measurable set
`s` for which `IsAddFundamentalDomain G s` holds.  -/
MeasureTheory.HasAddFundamentalDomain : (G : Type u_6) →
  (α : Type u_7) →
    [Zero G] →
      [VAdd G α] →
        [inst : MeasurableSpace α] →
          autoParam (MeasureTheory.Measure α) MeasureTheory.HasAddFundamentalDomain._auto_1 → Prop
-- Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
ContinuousMultilinearMap.restrictScalarsLinear.congr_simp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ∀ (i : ι), ContinuousSMul 𝕜 (E i)] (𝕜' : Type u_5)
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : (i : ι) → Module 𝕜' (E i)]
  [inst_12 : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F]
  [inst_15 : ContinuousConstSMul 𝕜' F],
  ContinuousMultilinearMap.restrictScalarsLinear 𝕜' = ContinuousMultilinearMap.restrictScalarsLinear 𝕜'
-- Mathlib.GroupTheory.PushoutI
/-- Take the product of a normal word as an element of the `PushoutI`. We show that this is
bijective, in `NormalWord.equiv`.  -/
Monoid.PushoutI.NormalWord.prod : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} → Monoid.PushoutI.NormalWord d → Monoid.PushoutI φ
-- Mathlib.RingTheory.FreeCommRing
/-- If `α` is a type, then `FreeCommRing α` is the free commutative ring generated by `α`.
This is a commutative ring equipped with a function `FreeCommRing.of : α → FreeCommRing α` which has
the following universal property: if `R` is any commutative ring, and `f : α → R` is any function,
then this function is the composite of `FreeCommRing.of` and a unique ring homomorphism
`FreeCommRing.lift f : FreeCommRing α →+* R`.

A typical element of `FreeCommRing α` is a `ℤ`-linear combination of
formal products of elements of `α`.
For example if `x` and `y` are terms of type `α` then `3 * x * x * y - 2 * x * y + 1` is a
"typical" element of `FreeCommRing α`. In particular if `α` is empty
then `FreeCommRing α` is isomorphic to `ℤ`, and if `α` has one term `t`
then `FreeCommRing α` is isomorphic to the polynomial ring `ℤ[t]`.
One can think of `FreeRing α` as the free polynomial ring
with coefficients in the integers and variables indexed by `α`.
 -/
FreeCommRing : Type u → Type u
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
DifferentiableWithinAt.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {g : ι → E → F} {s : Set E}
  {x : E} [Finite ι],
  DifferentiableWithinAt 𝕜 f s x →
    (∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x) → DifferentiableWithinAt 𝕜 (fun x => (f x) fun x_1 => g x_1 x) s x
-- Lean.MetavarContext
/-- Return true iff `e` depends on the free variable `fvarId`  -/
Lean.dependsOn : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Expr → Lean.FVarId → m Bool
-- Init.Data.Nat.Lemmas
Nat.mod_mul_mod : ∀ (m n l : ℕ), m % l * n % l = m * n % l
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_touchpointWeights_empty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {i j : Fin (n + 1)},
  i ≠ j → SignType.sign (s.touchpointWeights ∅ i j) = 1
-- Mathlib.Data.Multiset.Replicate
Multiset.lt_replicate_succ : ∀ {α : Type u_1} {m : Multiset α} {x : α} {n : ℕ}, m < Multiset.replicate (n + 1) x ↔ m ≤ Multiset.replicate n x
-- Mathlib.Algebra.Algebra.Prod
AlgHom.prod_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (g : A →ₐ[R] C) (x : A), (f.prod g) x = (f x, g x)
-- Std.Data.HashMap.AdditionalOperations
Std.HashMap.Raw.WF.map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {f : α → β → γ},
  m.WF → (Std.HashMap.Raw.map f m).WF
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If `G` preserves the initial object and `C` has an initial object, then the image of the initial
object is initial.
 -/
CategoryTheory.Limits.isColimitOfHasInitialOfPreservesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasInitial C] →
            [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] →
              CategoryTheory.Limits.IsInitial (G.obj (⊥_ C))
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_mul_left_eq_conj_mul : ∀ {G : Type u_1} [inst : Group G] (a b c : G), ⁅a * b, c⁆ = a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆
-- Mathlib.Algebra.Group.Action.Sum
Sum.instMulAction : {M : Type u_1} →
  {α : Type u_3} → {β : Type u_4} → {m : Monoid M} → [MulAction M α] → [MulAction M β] → MulAction M (α ⊕ β)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.coe_mul_rpow : ∀ (x y : NNReal) (z : ℝ), (↑x * ↑y) ^ z = ↑x ^ z * ↑y ^ z
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.sub : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {f g : M → E'}, MDiff[s] f → MDiff[s] g → MDiff[s] (f - g)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order.0.termσₙ : Lean.ParserDescr