mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.set_smul_bot : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (s : Set S), s • ⊥ = ⊥
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.nnnorm_apply_le_bound : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s : Set X}, ‖μ s‖₊ ≤ μ.bound
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.isSameSolverTerms.unsafe_impl_2 : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Bool
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nndist_apply_le : ∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → PseudoMetricSpace (β i)] (x y : PiLp p β) (i : ι), nndist (x.ofLp i) (y.ofLp i) ≤ nndist x y
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_subset_compl`. -/
Set.diff_subset_compl : ∀ {α : Type u_1} (s t : Set α), s \ t ⊆ tᶜ
-- Mathlib.Data.ZMod.Basic
zmod_smul_mem : ∀ {n : ℕ} {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : SetLike S G] [AddSubgroupClass S G] {K : S}
  [inst_3 : Module (ZMod n) G] {x : G}, x ∈ K → ∀ (a : ZMod n), a • x ∈ K
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_eq_normalize : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] [IsLeftCancelMulZero α] {a b : α},
  a ∣ b → b ∣ a → normalize a = normalize b
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.id_a : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  (AlgebraicTopology.DoldKan.MorphComponents.id X n).a = AlgebraicTopology.DoldKan.PInfty.f (n + 1)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Proof of positivity for `blocks`  -/
Composition.blocks_pos : ∀ {n : ℕ} (self : Composition n) {i : ℕ}, i ∈ self.blocks → 0 < i
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_naturality₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C))
  {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) [inst_3 : F.LaxMonoidal] {Z : C}
  (h : (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m' n')).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X))
      (CategoryTheory.CategoryStruct.comp ((F.obj n').map ((F.map f).app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m' n').app X) h)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)).app X) h)
-- Mathlib.Data.Multiset.Powerset
List.Subperm.eq_1 : ∀ {α : Type u_1} (l₁ l₂ : List α), l₁.Subperm l₂ = ∃ l, l.Perm l₁ ∧ l.Sublist l₂
-- Mathlib.Data.Finset.Powerset
/-- For predicate `p` decidable on subsets, it is decidable whether `p` holds for any subset.  -/
Finset.decidableExistsOfDecidableSubsets : {α : Type u_1} →
  {s : Finset α} →
    {p : (t : Finset α) → t ⊆ s → Prop} →
      [(t : Finset α) → (h : t ⊆ s) → Decidable (p t h)] → Decidable (∃ t, ∃ (h : t ⊆ s), p t h)
-- Mathlib.Data.Set.Basic
Set.mem_of_eq_of_mem : ∀ {α : Type u} {x y : α} {s : Set α}, x = y → y ∈ s → x ∈ s
-- Init.Data.Int.Order
Int.lt_iff_add_one_le : ∀ {a b : ℤ}, a < b ↔ a + 1 ≤ b
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_star : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] (a : A),
  autoParam (IsStarNormal a) CFC.abs_star._auto_1 → CFC.abs (star a) = CFC.abs a
-- Lean.Elab.Tactic.Basic
/-- Evaluate `tac` at `mvarId`, and return the list of resulting subgoals.  -/
Lean.Elab.Tactic.evalTacticAt : Lean.Syntax → Lean.MVarId → Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Std.Async.Basic
/-- Create an `AsyncTask` that resolves to the value of `x`.
 -/
Std.Async.AsyncTask.ofPurePromise : {α : Type} → IO.Promise α → optParam String "the promise linked to the Async Task was dropped" → Std.Async.AsyncTask α
-- Init.Data.Fin.Iterate
/-- `hIterate_elim` provides a mechanism for showing that the result of
`hIterate` satisfies a property `Q stop` by showing that the states
at the intermediate indices `i : start ≤ i < stop` satisfy `Q i`.
 -/
Fin.hIterate_elim : ∀ {P : ℕ → Sort u_1} (Q : (i : ℕ) → P i → Prop) {n : ℕ} (f : (i : Fin n) → P ↑i → P (↑i + 1)) (s : P 0),
  Q 0 s → (∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)) → Q n (Fin.hIterate P s f)
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_mul : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ χ : AddChar A M), ⇑(ψ * χ) = ⇑ψ * ⇑χ
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- To prove something for an arbitrary `Lp` simple function, with `0 < p < ∞`, it suffices to show
that the property holds for (multiples of) characteristic functions of finite-measure measurable
sets and is closed under addition (of functions with disjoint support).  -/
MeasureTheory.Lp.simpleFunc.induction : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α},
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {P : ↥(MeasureTheory.Lp.simpleFunc E p μ) → Prop},
        (∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤),
            P (MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)) →
          (∀ ⦃f g : MeasureTheory.SimpleFunc α E⦄ (hf : MeasureTheory.MemLp (⇑f) p μ)
              (hg : MeasureTheory.MemLp (⇑g) p μ),
              Disjoint (Function.support ⇑f) (Function.support ⇑g) →
                P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)) →
            ∀ (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)), P f
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.HasBiproduct.mk : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (d : CategoryTheory.Limits.LimitBicone F),
  CategoryTheory.Limits.HasBiproduct F
-- Mathlib.Topology.Algebra.Order.UpperLower
HasUpperLowerClosure.isOpen_upperClosure : ∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : HasUpperLowerClosure α] (s : Set α),
  IsOpen s → IsOpen ↑(upperClosure s)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.spaceUptoLine' : List Std.Format.WorkGroup✝ → ℕ → ℕ → Std.Format.SpaceResult✝
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (a_1 : a ⟶ b) (x : Bᵒᵖ) {X Y : Opposite.unop x ⟶ a}
  (x_1 : X ⟶ Y),
  ((CategoryTheory.Bicategory.yoneda.map a_1).app x).toFunctor.map x_1 = CategoryTheory.Bicategory.whiskerRight x_1 a_1
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.associativity : ∀ (X Y Z : SSet.Truncated 2),
  ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).prod (CategoryTheory.Functor.id Z.HomotopyCategory)).comp
      ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
            Z).comp
        (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
    (CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).functor.comp
      (((CategoryTheory.Functor.id X.HomotopyCategory).prod
            (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse Y Z)).comp
        (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_coe : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : Π₀ (x : ι), M), ⇑f.toFinsupp = ⇑f
-- Init.Data.List.Erase
List.length_eraseIdx_of_lt : ∀ {α : Type u_1} {l : List α} {i : ℕ}, i < l.length → (l.eraseIdx i).length = l.length - 1
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_single_apply`. -/
MonoidAlgebra.single_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {a a' : M} {b : R} [inst_1 : Decidable (a = a')],
  (MonoidAlgebra.single a b).coeff a' = if a = a' then b else 0
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_of_forall_fin_meas_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_9} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [MeasureTheory.SigmaFinite μ],
  ∀ C < ⊤,
    ∀ {f : α → ε},
      MeasureTheory.AEStronglyMeasurable f μ →
        (∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C) → MeasureTheory.Integrable f μ
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.map_nhds_of_mem : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → ∀ (x : X), Set.range f ∈ nhds (f x) → Filter.map f (nhds x) = nhds (f x)
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_iff_injective_of_separated : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂),
  CategoryTheory.Presieve.IsSeparated J (F₁.comp (CategoryTheory.forget D)) →
    (CategoryTheory.Presheaf.IsLocallyInjective J φ ↔
      ∀ (X : Cᵒᵖ), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (φ.app X)))
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_def : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Preorder ι] [inst_1 : InfSet ι] (u : ι → Ω → β) (s : Set β)
  (n m : ι),
  MeasureTheory.hittingBtwn u s n m = fun x =>
    if ∃ j ∈ Set.Icc n m, u j x ∈ s then sInf (Set.Icc n m ∩ {i | u i x ∈ s}) else m
-- Lean.Meta.Basic
/-- Declare an auxiliary local declaration `shortDeclName : type` for elaborating recursive
declaration `declName`, update the mapping `auxDeclToFullName`, and then execute `k`.
 -/
Lean.Meta.withAuxDecl : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.Name → Lean.Expr → Lean.Name → (Lean.Expr → n α) → n α
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- We collect a partial numerator `aᵢ` and partial denominator `bᵢ` in a pair `⟨aᵢ, bᵢ⟩`.  -/
GenContFract.Pair : Type u_1 → Type u_1
-- Init.Data.List.Scan.Lemmas
List.idRun_scanlM : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → Id β} {as : List α},
  (List.scanlM f init as).run = List.scanl (fun x1 x2 => (f x1 x2).run) init as
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_toUInt64 : ∀ (n : UInt32), n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieAlgebra.ext : ∀ {R : Type u_1} {inst : CommRing R} {L : Type u_2} {inst_1 : LeftPreLieRing L} {x y : LeftPreLieAlgebra R L},
  SMul.smul = SMul.smul → x = y
-- Mathlib.Analysis.Complex.HasPrimitives
/-- If a function `f` `IsConservativeOn` on a disk of center `c`, then for points `z` in this disk,
the wedge integral from `c` to `z` is additive under a detour through a nearby point `w`.  -/
Complex.IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E},
  ContinuousOn f (Metric.ball c r) →
    ∀ {z : ℂ},
      z ∈ Metric.ball c r →
        Complex.IsConservativeOn f (Metric.ball c r) →
          ∀ᶠ (w : ℂ) in nhds z, c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_le_pred_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ Fin.last n) (hb : b ≠ 0), a.castPred ha ≤ b.pred hb ↔ a < b
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.mulEquiv_coe_eq : ∀ {X Y : Type u_1} [inst : Semigroup X] [inst_1 : Semigroup Y] (e : X ≃* Y), Semigrp.Hom.hom (Semigrp.ofHom ↑e) = ↑e
-- Lean.DocString.Syntax
/-- A description of an item  -/
Lean.Doc.Syntax.desc : Lean.ParserDescr
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.le : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → LE (E →ₛₗ.[σ] F)
-- Mathlib.FieldTheory.SeparablyGenerated
/-- Any finitely generated extension over perfect fields are separably generated.  -/
exists_isTranscendenceBasis_and_isSeparable_of_perfectField : ∀ (k : Type u_1) (K : Type u_2) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [PerfectField k]
  [Algebra.EssFiniteType k K],
  ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k ↑s)) K
-- Mathlib.Data.List.Rotate
List.rotate_length_mul : ∀ {α : Type u} (l : List α) (n : ℕ), l.rotate (l.length * n) = l
-- Mathlib.Data.Finset.Defs
Finset.forall_mem_not_eq : ∀ {α : Type u_1} {s : Finset α} {a : α}, (∀ b ∈ s, ¬a = b) ↔ a ∉ s
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.leadingCoeff_of_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R},
  ((HahnSeries.single a) r).leadingCoeff = r
-- Mathlib.Data.List.Triplewise
List.Triplewise.cons : ∀ {α : Type u_1} {p : α → α → α → Prop} {a : α} {l : List α},
  List.Pairwise (p a) l → List.Triplewise p l → List.Triplewise p (a :: l)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey!
-- Lean.Meta.PProdN
/-- `PProd.fst` or `And.left` (using `.proj`)  -/
Lean.Meta.mkPProdFst : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.free_obj : ∀ (V : CategoryTheory.Quiv), CategoryTheory.Cat.free.obj V = CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)
-- Mathlib.RingTheory.Extension.Generators
/-- Given generators `P` with variable type `ι'` and an equivalence `ι ≃ ι'`, these
are the induced generators indexed by `ι`.  -/
Algebra.Generators.reindex : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] → {ι' : Type u_1} → Algebra.Generators R S ι' → ι ≃ ι' → Algebra.Generators R S ι
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.instDecidableIsNCliqueOfDecidableEqOfDecidableRelAdj : {α : Type u_1} →
  (G : SimpleGraph α) → [DecidableEq α] → [DecidableRel G.Adj] → {n : ℕ} → {s : Finset α} → Decidable (G.IsNClique n s)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_comp_neg : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalRing A] [inst_8 : StarRing A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  [ContinuousMapZero.UniqueHom R A],
  autoParam (ContinuousOn f ((fun x => -x) '' quasispectrum R a)) cfcₙ_comp_neg._auto_1 →
    autoParam (f 0 = 0) cfcₙ_comp_neg._auto_3 →
      autoParam (p a) cfcₙ_comp_neg._auto_5 → cfcₙ (fun x => f (-x)) a = cfcₙ f (-a)
-- Init.Control.Lawful.Basic
Id.run_seqLeft : ∀ {α β : Type u_1} (x : Id α) (y : Id β), (x <* y).run = x.run
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
/-- If `p` is a prime and `IsCyclotomicExtension {p ^ (k + 1)} K L`, then the discriminant of
`hζ.powerBasis K` is `(-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`
if `Irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`.  -/
IsCyclotomicExtension.discr_prime_pow_ne_two' : ∀ {p k : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K) →
    p ^ (k + 1) ≠ 2 →
      Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
        (-1) ^ (p ^ k * (p - 1) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- `(X₁ ×[Y₁] X₂) ×[Y₂] X₃` is the pullback `(X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃)`.  -/
CategoryTheory.Limits.pullbackPullbackLeftIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ Y₂ : C} →
      (f₁ : X₁ ⟶ Y₁) →
        (f₂ : X₂ ⟶ Y₁) →
          (f₃ : X₂ ⟶ Y₂) →
            (f₄ : X₃ ⟶ Y₂) →
              [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPullback
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄] →
                    CategoryTheory.Limits.IsLimit
                      (CategoryTheory.Limits.PullbackCone.mk
                        (CategoryTheory.Limits.pullback.fst
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
                        (CategoryTheory.Limits.pullback.lift
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Limits.pullback.fst
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
                            (CategoryTheory.Limits.pullback.snd f₁ f₂))
                          (CategoryTheory.Limits.pullback.snd
                            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
                          ⋯)
                        ⋯)
-- Lean.Compiler.IR.CompilerM
/-- Like ``findInterpDecl env (declName ++ `_boxed)`` but with optimized negative lookup.  -/
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.findInterpDeclBoxed : Lean.Environment → Lean.Name → Option Lean.IR.Decl
-- Mathlib.Data.Ordmap.Invariants
Ordnode.rotateL_nil : ∀ {α : Type u_1} (l : Ordnode α) (x : α), l.rotateL x Ordnode.nil = l.node' x Ordnode.nil
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
bounded by `C` on `s`, then the function is `C`-Lipschitz on `s`.
Version with `HasDerivWithinAt` and `LipschitzOnWith`.  -/
Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
  {f f' : 𝕜 → G} {s : Set 𝕜} {C : NNReal},
  Convex ℝ s → (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → (∀ x ∈ s, ‖f' x‖₊ ≤ C) → LipschitzOnWith C f s
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.O : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.TimeZone.Offset
-- Mathlib.Data.Fin.Basic
Fin.liftFun_iff_succ : ∀ {n : ℕ} {α : Type u_1} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α},
  Relator.LiftFun (fun x1 x2 => x1 < x2) r f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.continuousOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → ContinuousOn f s
-- Mathlib.Data.Tree.Get
/-- **Alias** of `BinaryTree.get`.  -/
Tree.get : {α : Type u_1} → PosNum → Tree α → Option α
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.max : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMinOn f s a → IsLocalMinOn g s a → IsLocalMinOn (fun x => max (f x) (g x)) s a
-- Mathlib.Logic.Basic
beq_ext : ∀ {α : Type u_1} (inst1 inst2 : BEq α), (∀ (x y : α), (x == y) = (x == y)) → inst1 = inst2
-- Mathlib.Order.Filter.Pointwise
Filter.isUnit_iff_singleton : ∀ {α : Type u_2} [inst : Group α] {f : Filter α}, IsUnit f ↔ ∃ a, f = pure a
-- Mathlib.Order.Sublattice
Sublattice.mem_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {M : Sublattice β}
  {p : α × β}, p ∈ L.prod M ↔ p.1 ∈ L ∧ p.2 ∈ M
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getOne : {m : Type → Type} →
  [Monad m] →
    [Lean.Meta.Sym.Arith.MonadCanon m] →
      [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → [MonadLiftT Lean.Meta.Grind.GoalM m] → m Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.ToLin
toMatrix_distrib_mul_action_toLinearMap : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (x : R),
  (LinearMap.toMatrix v₁ v₁) (DistribSMul.toLinearMap R M₁ x) = Matrix.diagonal fun x_1 => x
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinsert_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s → Multiset.ndinsert a s = s
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusMap_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [inst_4 : CategoryTheory.Preadditive D]
  (P Q : CategoryTheory.Functor Cᵒᵖ D), J.plusMap 0 = 0
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.keyAtIdxD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ) (fallback : α)
  (h_1 : (x : ℕ) → (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf x fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (n : ℕ) → (fallback : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => h_1 x fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback => h_2 size k v l r n fallback) =
    h_2 size k v l r n fallback
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_le : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ≤ u → t ≤ u → s ∪ t ≤ u
-- Lean.Message
Lean.ToMessageData : Type → Type
-- Mathlib.Data.List.Basic
List.map_diff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β] {f : α → β},
  Function.Injective f → ∀ {l₁ l₂ : List α}, List.map f (l₁.diff l₂) = (List.map f l₁).diff (List.map f l₂)
-- Mathlib.GroupTheory.Congruence.Hom
Con.hom_ext_iff : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f g : c.Quotient →* P},
  f = g ↔ f.comp c.mk' = g.comp c.mk'