mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.eq_2 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (it' : Std.IterM m β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')),
  Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.skip it', h⟩ =
    Std.IterStep.skip { internalState := { inner := it', invariant := ⋯ } }
-- Init.Data.SInt.Lemmas
Int16.neg_sub : ∀ {a b : Int16}, -(a - b) = b - a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rio_eq_zero_iff : ∀ {n i : ℕ}, (*...n).toArray[i]! = 0 ↔ n ≤ i ∨ i = 0
-- Init.Data.Char.Lemmas
Char.le_total : ∀ (a b : Char), a ≤ b ∨ b ≤ a
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_biSup_of_directedOn : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Type u_4} {p : ι → Prop},
  (∃ i, p i) →
    ∀ {S : ι → Submonoid M},
      DirectedOn (Function.onFun (fun x1 x2 => x1 ≤ x2) S) {i | p i} →
        ∀ {x : M}, x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i
-- Init.SizeOf
sizeOf_nat : ∀ (n : ℕ), sizeOf n = n
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.colLen_eq_card : ∀ (μ : YoungDiagram) {j : ℕ}, μ.colLen j = (μ.col j).card
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The set of coefficients that is enough to descend a submersive presentation `P`.  -/
Algebra.SubmersivePresentation.coeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] → [inst_3 : Finite σ] → Algebra.SubmersivePresentation R S ι σ → Set R
-- Mathlib.Data.Num.Basic
/-- The type of positive binary numbers.

```
13 = 1101(base 2) = bit1 (bit0 (bit1 one))
```  -/
PosNum : Type
-- Mathlib.FieldTheory.Perfect
PerfectField.ofCharZero : ∀ {K : Type u_1} [inst : Field K] [CharZero K], PerfectField K
-- Mathlib.Analysis.Normed.Group.Bounded
/-- A helper lemma used to prove that the (scalar or usual) product of a function that tends to one
and a bounded function tends to one. This lemma is formulated for any binary operation
`op : E → F → G` with an estimate `‖op x y‖ ≤ A * ‖x‖ * ‖y‖` for some constant A instead of
multiplication so that it can be applied to `(*)`, `flip (*)`, `(•)`, and `flip (•)`.  -/
Filter.Tendsto.op_one_isBoundedUnder_le' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : SeminormedGroup G] {f : α → E} {g : α → F} {l : Filter α},
  Filter.Tendsto f l (nhds 1) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g) →
      ∀ (op : E → F → G),
        (∃ A, ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 1)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  [T2Space α] [Nonempty β] [L.NeBot] [L.LeAtTop], ∏'[L] (x : β), 0 = 0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundariesOfIsMulCoboundary₁_coe : ∀ {G M : Type} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulDistribMulAction G M] {f : G → M}
  (hf : groupCohomology.IsMulCoboundary₁ f) (a : G),
  ↑(groupCohomology.coboundariesOfIsMulCoboundary₁ hf) a = (⇑Additive.ofMul ∘ f) a
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- Applying a compression strictly decreases the measure. This helps show that "compress until we
can't any more" is a terminating process.  -/
_private.Mathlib.Combinatorics.SetFamily.KruskalKatona.0.Finset.UV.familyMeasure_compression_lt_familyMeasure : ∀ {n : ℕ} {U V : Finset (Fin n)} {hU : U.Nonempty} {hV : V.Nonempty},
  U.max' hU < V.max' hV →
    ∀ {𝒜 : Finset (Finset (Fin n))},
      UV.compression U V 𝒜 ≠ 𝒜 → Finset.UV.familyMeasure✝ (UV.compression U V 𝒜) < Finset.UV.familyMeasure✝ 𝒜
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_array : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Algebra.Lie.Weights.Basic
/-- By Engel's theorem, the zero weight space of a Noetherian Lie module is nilpotent.  -/
LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M], LieModule.IsNilpotent L ↥(LieModule.genWeightSpace M 0)
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instGeometricallyIntegralSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyIntegral f],
  AlgebraicGeometry.GeometricallyIntegral (CategoryTheory.Limits.pullback.snd f g)
-- Std.Data.ExtDTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtDTreeMap.getKey! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtDTreeMap α β cmp → α → α
-- Mathlib.Topology.LocallyFinite
LocallyFinite.prod_right : ∀ {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {f : ι → Set X}, LocallyFinite f → ∀ (g : ι → Set Y), LocallyFinite fun i => f i ×ˢ g i
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteBooleanAlgebra.toCompl : {α : Type u_1} → [self : CompleteBooleanAlgebra α] → Compl α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_add_two_pi : ∀ (x : ℝ), Real.cos (x + 2 * Real.pi) = Real.cos x
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody : Type
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : Cᵒᵖ}
  (f : X ⟶ Y) (Z : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).unop =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.unop (Opposite.unop Z)
-- Mathlib.Logic.Function.Basic
Function.Injective.surjective_comp_right : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} [Nonempty γ],
  Function.Injective f → Function.Surjective fun g => g ∘ f
-- Mathlib.Algebra.Order.ToIntervalMod
sub_toIcoDiv_zsmul_mem_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), b - toIcoDiv hp a b • p ∈ Set.Ico a (a + p)
-- Mathlib.Algebra.Order.Interval.Multiset
Multiset.map_add_right_Icc : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Multiset.map (fun x => x + c) (Multiset.Icc a b) = Multiset.Icc (a + c) (b + c)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Differentiable.const_cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {c : ℂ},
  Differentiable ℂ f → (c ≠ 0 ∨ ∀ (x : E), f x ≠ 0) → Differentiable ℂ fun x => c ^ f x
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  ⦃Q.2.1 e⦄ MonadExceptOf.throw e ⦃Q⦄
-- Mathlib.CategoryTheory.Sites.Point.Comap
CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} (Φ : K.Point)
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.RepresentablyFlat F]
  {J : CategoryTheory.GrothendieckTopology C} (hF : CategoryTheory.CoverPreserving J K F)
  [inst_3 : CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] (A : Type u_3)
  [inst_4 : CategoryTheory.Category.{v, u_3} A] [inst_5 : CategoryTheory.Limits.HasProducts A]
  [inst_6 : F.IsContinuous J K] [inst_7 : (F.sheafPushforwardContinuous A J K).IsRightAdjoint]
  [inst_8 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u_3} A] (X : CategoryTheory.Sheaf J A),
  (Φ.sheafFiberComapIso F hF A).inv.app X =
    CategoryTheory.CategoryStruct.comp
      (Φ.sheafFiber.map ((F.sheafPullback A J K).map ((Φ.comap F hF).skyscraperSheafAdjunction.unit.app X)))
      (CategoryTheory.CategoryStruct.comp
        (Φ.sheafFiber.map
          ((F.sheafPullback A J K).map
            ((Φ.skyscraperSheafFunctorCompSheafPushforwardContinuous F hF A).inv.app
              ((Φ.comap F hF).sheafFiber.obj X))))
        (CategoryTheory.CategoryStruct.comp
          (Φ.sheafFiber.map
            ((F.sheafAdjunctionContinuous A J K).counit.app
              (Φ.skyscraperSheafFunctor.obj ((Φ.comap F hF).sheafFiber.obj X))))
          (Φ.skyscraperSheafAdjunction.counit.app ((Φ.comap F hF).sheafFiber.obj X))))
-- Mathlib.Data.Finset.Max
Finset.max'_pair : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), {a, b}.max' ⋯ = max a b
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.go_spec : ∀ {n p : ℕ} (hnp : 1 < p ∧ n ≠ 0),
  (Nat.maxPowDvdDiv.go n p hnp).2 * p ^ (Nat.maxPowDvdDiv.go n p hnp).1 = n ∧ ¬p ∣ (Nat.maxPowDvdDiv.go n p hnp).2
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonList : {α : Type u_1} → [Lean.ToJson α] → Lean.ToJson (List α)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_Ico_castAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m ⁻¹' Set.Ico (Fin.castAdd m i) (Fin.castAdd m j) = Set.Ico i j
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ),
  ¬ProbabilityTheory.IsSFiniteKernel η → κ.compProd η = 0
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The set `codeSupp c k` is a finite set that witnesses the effective finiteness of the `tr`
Turing machine. Starting from the initial state `trNormal c k`, forward simulation uses only
states in `codeSupp c k`, so this is a finite state machine. Even though the underlying type of
state labels `Λ'` is infinite, for a given partial recursive function `c` and continuation `k`,
only finitely many states are accessed, corresponding roughly to subterms of `c`.  -/
Turing.PartrecToTM2.tr_supports : ∀ (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.TM2.Supports Turing.PartrecToTM2.tr (Turing.PartrecToTM2.codeSupp c k)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coeFnAddMonoidHom_apply : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] (f : ContinuousMapZero X R),
  ContinuousMapZero.coeFnAddMonoidHom f = ⇑f
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.GAlgebra.mk : {ι : Type uι} →
  {R : Type uR} →
    {A : ι → Type uA} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [inst_3 : AddMonoid ι] →
              [inst_4 : DirectSum.GSemiring A] →
                (toFun : R →+ A 0) →
                  toFun 1 = GradedMonoid.GOne.one →
                    (∀ (r s : R),
                        GradedMonoid.mk 0 (toFun (r * s)) =
                          GradedMonoid.mk (0 + 0) (GradedMonoid.GMul.mul (toFun r) (toFun s))) →
                      (∀ (r : R) (x : GradedMonoid A),
                          GradedMonoid.mk 0 (toFun r) * x = x * GradedMonoid.mk 0 (toFun r)) →
                        (∀ (r : R) (x : GradedMonoid A), r • x = GradedMonoid.mk 0 (toFun r) * x) →
                          DirectSum.GAlgebra R A
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.isEdgeReachable_comm : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V}, G.IsEdgeReachable k u v ↔ G.IsEdgeReachable k v u
-- Mathlib.Analysis.Convex.StdSimplex
/-- The convex hull of a finite set is the image of the standard simplex in `s → ℝ`
under the linear map sending each function `w` to `∑ x ∈ s, w x • x`.

Since we have no sums over finite sets, we use sum over `@Finset.univ _ hs.fintype`.
The map is defined in terms of operations on `(s → ℝ) →ₗ[ℝ] ℝ` so that later we will not need
to prove that this map is linear.  -/
Set.Finite.convexHull_eq_image : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {E : Type u_3}
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] {s : Set E} (hs : s.Finite),
  (convexHull R) s = ⇑(∑ x, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s
-- Init.Grind.ToInt
/-- The embedding into the integers takes exponentiation to exponentiation, wrapped into the range interval.
 -/
Lean.Grind.ToInt.Pow : (α : Type u) → [HPow α ℕ α] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.Tactic.CongrExclamation
Congr!.Config.mk.sizeOf_spec : ∀ (closePre closePost : Bool) (transparency preTransparency postTransparency : Lean.Meta.TransparencyMode)
  (preferLHS partialApp sameFun : Bool) (maxArgs : Option ℕ) (typeEqs etaExpand useCongrSimp beqEq : Bool),
  sizeOf
      { closePre := closePre, closePost := closePost, transparency := transparency, preTransparency := preTransparency,
        postTransparency := postTransparency, preferLHS := preferLHS, partialApp := partialApp, sameFun := sameFun,
        maxArgs := maxArgs, typeEqs := typeEqs, etaExpand := etaExpand, useCongrSimp := useCongrSimp, beqEq := beqEq } =
    1 + sizeOf closePre + sizeOf closePost + sizeOf transparency + sizeOf preTransparency + sizeOf postTransparency +
                    sizeOf preferLHS +
                  sizeOf partialApp +
                sizeOf sameFun +
              sizeOf maxArgs +
            sizeOf typeEqs +
          sizeOf etaExpand +
        sizeOf useCongrSimp +
      sizeOf beqEq
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.emultiplicity_choose_prime_pow : ∀ {p n k : ℕ}, Nat.Prime p → k ≤ p ^ n → k ≠ 0 → emultiplicity p ((p ^ n).choose k) = ↑(n - multiplicity p k)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis ''
      closure (NumberField.mixedEmbedding.fundamentalCone.paramSet K) ⊆
    NumberField.mixedEmbedding.fundamentalCone.compactSet K
-- Mathlib.Topology.Algebra.IsOpenUnits
IsOpenUnits.mk : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : TopologicalSpace M], Topology.IsOpenEmbedding Units.val → IsOpenUnits M
-- Init.Data.Rat.Lemmas
Rat.divInt_ofNat : ∀ (num : ℤ) (den : ℕ), Rat.divInt num ↑den = mkRat num den
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {X Y : B} (a : X ⟶ Y),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.mk' S).map a = S.map a
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.tprodMonoidHom_apply : ∀ {ι : Type u_1} (R : Type u_3) {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → NonAssocSemiring (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)]
  [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)] (a : (i : ι) → A i),
  (PiTensorProduct.tprodMonoidHom R) a = (PiTensorProduct.tprod R) a
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.bind.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s : σ)
  (h_1 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok a s with
    | EStateM.Result.ok a s => h_1 a s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 a s
-- Mathlib.RingTheory.Ideal.Maps
Ideal.le_comap_pow : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F) {K : Ideal S} (n : ℕ), Ideal.comap f K ^ n ≤ Ideal.comap f (K ^ n)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow.eq_1 : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  hζ.subOneIntegralPowerBasisOfPrimePow = PowerBasis.ofAdjoinEqTop' ⋯ ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_single_mul_of_forall_add_ne : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m m' : M} [inst_1 : Add M] (r : R) (x : AddMonoidAlgebra R M),
  (∀ (d : M), m + d ≠ m') → (AddMonoidAlgebra.single m r * x).coeff m' = 0
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_pow : ∀ (b x : ℝ) (k : ℕ), Real.logb b (x ^ k) = ↑k * Real.logb b x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_eq_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {he : t.isEmpty = false}, t.maxKey he = t.maxKey!
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.preimage_subset_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {s : Set B}, s ⊆ e.baseSet → proj ⁻¹' s ⊆ e.source
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instIsScalarTowerQuotientCotangent : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), IsScalarTower R (R ⧸ I) I.Cotangent
-- Mathlib.Data.Nat.Digits.Defs
/-- The core implementation of `Nat.toDigits` returns a String with length less than or equal to the
number of digits in the base-`b` number (represented by `e`). For example, the string
representation of any number less than `b ^ 3` has a length less than or equal to 3.  -/
Nat.toDigits_length : ∀ (b n e : ℕ), 0 < e → n < b ^ e → (b.toDigits n).length ≤ e
-- Mathlib.Combinatorics.Quiver.Covering
Quiver.symmetrifyCostar.eq_1 : ∀ {U : Type u_1} [inst : Quiver U] (u : U),
  Quiver.symmetrifyCostar u =
    Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Quiver.Symmetrify.of.obj u) (Quiver.Hom (Quiver.Symmetrify.of.obj u))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).f' =
    CategoryTheory.CategoryStruct.comp φ.τ₁ h.f'
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.union_ae_eq_right : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s ∪ t =ᵐ[μ] t ↔ μ (s \ t) = 0
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Var)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match Lean.Grind.CommRing.Expr.var x with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_2 x
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.finite_setOfPred_absNorm_le : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  [CharZero S] (n : ℕ), {I | Ideal.absNorm I ≤ n}.Finite
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (I : Set k) {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
  (h : fs.card = m + 1) {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ((Finset.affineCombination k Finset.univ s.points) w ∈ Affine.Simplex.setInterior I (s.face h) ↔
      (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Additive.ofMul.eq_1 : ∀ {α : Type u}, Additive.ofMul = { toFun := fun x => x, invFun := fun x => x, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.transvection_mulVec_single_self : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F), (↑(Matrix.SpecialLinearGroup.transvection hij b)).mulVec (Pi.single i 1) = Pi.single i 1
-- Mathlib.Algebra.GroupWithZero.Action.Basic
DistribMulAction.toAddEquiv_apply : ∀ {G : Type u_1} (A : Type u_3) [inst : Group G] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction G A] (x : G) (a : A),
  (DistribMulAction.toAddEquiv A x) a = x • a
-- Mathlib.Order.Sublattice
/-- The maximum sublattice of a lattice.  -/
Sublattice.instTop : {α : Type u_2} → [inst : Lattice α] → Top (Sublattice α)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₂ : ∀ {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 : ℤ) (h : a ≤ b) (j : C),
  ((t.triangleLTLTGELT a b h).obj j).mor₂ = (t.truncGEπ a).app ((t.truncLT b).obj j)
-- Aesop.Forward.LevelIndex
Aesop.instDecidableRelLevelIndexLe : DecidableRel fun x1 x2 => x1 ≤ x2