mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.step_iterFromIdx : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ},
  (xs.iterFromIdx pos).step =
    if h : pos < n then Std.PlausibleIterStep.yield (xs.iterFromIdx (pos + 1)) xs[pos] ⋯
    else Std.PlausibleIterStep.done ⋯
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_inf_sdiff : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y ⊓ y \ x = ⊥
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.symm_symm : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (e : A ≃⋆* B),
  e.symm.symm = e
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.zero_comp : ∀ {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : Zero M] (f : α → β), 0 ∘ f = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.toList_perm : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β},
  m₁.Equiv m₂ → m₁.toList.Perm m₂.toList
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.add_weierstrassMod : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f f' g : PowerSeries A)
  [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], (f + f') %ʷ g = f %ʷ g + f' %ʷ g
-- Mathlib.Topology.Algebra.Support
tsupport.eq_1 : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α),
  tsupport f = closure (Function.support f)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsEquivOfQuotEquiv_is_dvd_iso : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J) {L M : Ideal R} (hL : L ∣ I) (hM : M ∣ I),
  ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣
      ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔
    L ∣ M
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.addGroupWithOne : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → AddGroupWithOne (CauSeq β abv)
-- Mathlib.MeasureTheory.Measure.Support
/-- An inner regular measure has conull support when open sets are measurable.  -/
MeasureTheory.Measure.measure_compl_support_of_innerRegular : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] [μ.InnerRegular], μ μ.supportᶜ = 0
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.lift_map : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G : CategoryTheory.Functor C D) (hG : W.IsInvertedBy G)
  {X Y : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)} (hf : X ⟶ Y),
  (CategoryTheory.Localization.Construction.lift G hG).map hf =
    Quot.liftOn hf
      (fun f =>
        CategoryTheory.composePath
          ({ obj := fun X => G.obj X.obj,
                map := fun {X Y} a =>
                  Sum.rec (fun val => G.map val) (fun val => CategoryTheory.inv (G.map ↑val)) a }.mapPath
            f))
      ⋯
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_trunc_mul : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (f g : PowerSeries R),
  (PowerSeries.trunc n) (↑((PowerSeries.trunc n) f) * g) = (PowerSeries.trunc n) (f * g)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.sup : ∀ {α : Type u} {s t : Set α}, s.Finite → t.Finite → (s ⊔ t).Finite
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.coe_id : ∀ {M : Type u_10} [inst : Mul M], ⇑(MulHom.id M) = id
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Types.instIsStableUnderCompositionJointlySurjectivePrecoverage : CategoryTheory.Types.jointlySurjectivePrecoverage.IsStableUnderComposition
-- Mathlib.Data.Multiset.Bind
Multiset.card_join : ∀ {α : Type u_1} (S : Multiset (Multiset α)), S.join.card = (Multiset.map Multiset.card S).sum
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The singleton operation as a `MonoidHom`.  -/
Finset.singletonMonoidHom : {α : Type u_2} → [inst : DecidableEq α] → [inst_1 : MulOneClass α] → α →* Finset α
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce.cons : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α] (x : α × Bool),
  FreeGroup.reduce (x :: L) =
    List.casesOn (FreeGroup.reduce L) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.instIsAddMonHomFst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N]
  [inst_4 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsAddMonHom (CategoryTheory.SemiCartesianMonoidalCategory.fst M N)
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_compl_self : ∀ {α : Type u_1} (s : Set α), s ∩ sᶜ = ∅
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : SizeOf R] (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime),
  sizeOf { asIdeal := asIdeal, isPrime := isPrime } = 1 + sizeOf asIdeal + sizeOf isPrime
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edge.eq_1 : ∀ {V : Type u_1} (s t : V), SimpleGraph.edge s t = SimpleGraph.fromEdgeSet {s(s, t)}
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.sdiff_coloops_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep (I \ M.coloops) ↔ M.Indep I
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_midπ_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ) (i : ℤ) {Z : C}
  (h : ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.mid.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀).f i)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q).f i) h) =
    CategoryTheory.CategoryStruct.comp
      (((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.ι.f i) h
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoalParams.toTextDocumentPositionParams : Lean.Lsp.PlainGoalParams → Lean.Lsp.TextDocumentPositionParams
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.isPlausibleOutput_next : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] {it : Std.Iter α},
  it.internalState.next = some a → it.IsPlausibleOutput a
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- Auxiliary definition for `bicategorical_coherence`.  -/
Mathlib.Tactic.BicategoryCoherence.mkLiftMap₂LiftExpr : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The trifunctor `F (- ⊗ -) ⊗ F -`.  -/
CategoryTheory.MonoidalCategory.curriedTensorPostPre : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory D] →
            CategoryTheory.Functor C D →
              CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C D))
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.ipv6.injEq : ∀ (ipv6 ipv6_1 : Std.Net.IPv6Addr), (Std.Http.URI.Host.ipv6 ipv6 = Std.Http.URI.Host.ipv6 ipv6_1) = (ipv6 = ipv6_1)
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_iff_le_comap : ∀ {α : Type u_2} {β : Type u_3} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β},
  UniformContinuous f ↔ uα ≤ UniformSpace.comap f uβ
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The forgetful functor from `AddMon C` to `C` is monoidal when `C` is monoidal.  -/
CategoryTheory.AddMon.instMonoidalForget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.AddMon.forget C).Monoidal
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The formal direct factor of `P.X` given by the idempotent `P.p` in the category `C`
is actually a direct factor in the category `Karoubi C`.  -/
CategoryTheory.Idempotents.Karoubi.decompId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C),
  CategoryTheory.CategoryStruct.id P = CategoryTheory.CategoryStruct.comp P.decompId_i P.decompId_p
-- Init.Tactics
/-- The same as `rfl`, but without trying `eq_refl` at the end.
 -/
Lean.Parser.Tactic.applyRfl : Lean.ParserDescr
-- Mathlib.Tactic.FunProp.Core
/-- Prove function property of `fun x ↦ f x₁ ... xₙ` where `f` is declared function.  -/
Mathlib.Meta.FunProp.constAppCase : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    Mathlib.Meta.FunProp.FunctionData →
      (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
        Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If a module has a finite dimension, all bases are indexed by a finite type.  -/
Module.Basis.fintypeIndexOfRankLtAleph0 : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [StrongRankCondition R] → {ι : Type u_1} → Module.Basis ι R M → Module.rank R M < Cardinal.aleph0 → Fintype ι
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.finiteCoproduct.hom_ext : ∀ {P : TopCat → Prop} {α : Type w} [inst : Finite α] (X : α → CompHausLike P)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} (f g : CompHausLike.finiteCoproduct X ⟶ B),
  (∀ (a : α),
      CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) f =
        CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) g) →
    f = g
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
/-- Pull a subalgebra back to an opposite subalgebra along `MulOpposite.unop`  -/
Subalgebra.op : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A → Subalgebra R Aᵐᵒᵖ
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂)
  [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : ∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂] (K : HomologicalComplex₂ C c₁ c₂),
  (HomologicalComplex₂.totalFunctor C c₁ c₂ c₁₂).obj K = K.total c₁₂
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- Dirac measures are Gaussian.  -/
ProbabilityTheory.instIsGaussianDirac : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {x : E}, ProbabilityTheory.IsGaussian (MeasureTheory.Measure.dirac x)
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inrₗ_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (a : β), (OrderMonoidHom.inrₗ α β) a = toLex (1, a)
-- Init.Control.Lawful.Instances
ExceptT.bind_pure_comp : ∀ {m : Type u_1 → Type u_2} {α β ε : Type u_1} [inst : Monad m] (f : α → β) (x : ExceptT ε m α),
  x >>= pure ∘ f = f <$> x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.hasCoeOpens : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → CoeTC (OpenSubgroup G) (TopologicalSpace.Opens G)
-- Mathlib.Control.Fold
Traversable.foldMap_hom_free : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] [inst_2 : Monoid β]
  (f : FreeMonoid α →* β) (x : t α),
  f (Traversable.foldMap FreeMonoid.of x) = Traversable.foldMap (⇑f ∘ FreeMonoid.of) x
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Algebra.isGeometricallyReduced_iff : ∀ (R : Type u_3) (A : Type u_4) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  Algebra.IsGeometricallyReduced R A ↔
    ∀ (p : Ideal R) [inst_3 : p.IsPrime], IsReduced (TensorProduct R (AlgebraicClosure p.ResidueField) A)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.uniqueUpToIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t), (P.uniqueUpToIso Q).inv = Q.descCoconeMorphism s
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor : ∀ (R : Type u) [inst : Ring R] (M : ModuleCat R),
  CategoryTheory.IsIso
    ((LightCondensed.forget R).map
      ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app
        ((LightCondMod.LocallyConstant.functor R).obj M)))
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- A split coequalizer clearly induces a cofork.  -/
CategoryTheory.IsSplitCoequalizer.asCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} → {Z : C} → {h : Y ⟶ Z} → CategoryTheory.IsSplitCoequalizer f g h → CategoryTheory.Limits.Cofork f g
-- Lean.Language.Basic
/-- Transformation to be applied while walking a snapshot tree; applied implicitly on untyped walk
in `toSnapshotTreeM`. Used so that snapshot trees inside the transformation stay identical across
certain edits and thus allow for elab reuse.

More transformation elements may be added in the future.
 -/
Lean.Language.SnapshotTreeTransform : Type
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_zero_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {h : (i : ι) → β i → γ},
  DFinsupp.prod 0 h = 1
-- Mathlib.FieldTheory.Differential.Liouville
/-- A finite-dimensional Galois extension of `F` is a Liouville extension.
This is private because it's generalized by all finite-dimensional extensions being Liouville.
 -/
_private.Mathlib.FieldTheory.Differential.Liouville.0.isLiouville_of_finiteDimensional_galois : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K] [DifferentialAlgebra F K] [CharZero F] [FiniteDimensional F K] [IsGalois F K], IsLiouville F K
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.eqLocus_same : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), f.eqLocus f = ⊤
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.isEmpty.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.isEmpty = true
-- Mathlib.Order.SupClosed
Set.Finite.latticeClosure : ∀ {α : Type u_3} [inst : DistribLattice α] {s : Set α}, s.Finite → (latticeClosure s).Finite
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_opcyclesMap_of_isIso_of_epi' : ∀ {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₂),
  CategoryTheory.IsIso φ.τ₂ →
    CategoryTheory.Epi φ.τ₁ →
      ∀ [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
        CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.continuousOn_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α},
  ContinuousOn f s ↔ ∀ (x : E) (y : F), ContinuousOn (fun x_1 => inner 𝕜 y ((f x_1) x)) s
-- Batteries.Data.PairingHeap
/-- `O(1)`. Make a new empty pairing heap.  -/
Batteries.PairingHeap.empty : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le
-- Mathlib.NumberTheory.Padics.Complex
/-- `ℂ_[p]` is a valued field, where the valuation is the one extending that on `PadicAlgCl p`.  -/
PadicComplex.valued : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Valued ℂ_[p] NNReal
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.pow_prime_eq_one_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {p : ℕ} [hp : Fact (Nat.Prime p)],
  σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_zpow_iff_left₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a b : G₀} {n : ℤ} [PosMulReflectLT G₀]
  [MulPosMono G₀], 0 ≤ a → 0 ≤ b → 0 < n → (a ^ n < b ^ n ↔ a < b)
-- Batteries.Classes.Order
/-- Class for types where the ordering function is compatible with the `LE`, `LT` and `BEq`.  -/
Std.LawfulBOrd : (α : Type u_1) → [LE α] → [LT α] → [BEq α] → [Ord α] → Prop
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.divMonomial_monomial_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (a : σ →₀ ℕ) (x : MvPolynomial σ R),
  ((MvPolynomial.monomial a) 1 * x).divMonomial a = x
-- Mathlib.Algebra.BigOperators.Finprod
Multiset.hasFiniteMulSupport_fun_pow_count : ∀ {α : Type u_1} {M : Type u_2} [inst : DecidableEq α] [inst_1 : CommMonoid M] (s : Multiset α) (f : α → M),
  Function.HasFiniteMulSupport fun a => f a ^ Multiset.count a s
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv : ∀ {A : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} A] [inst_1 : CategoryTheory.Abelian A]
  {Y : CategoryTheory.SimplicialObject A},
  AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.inv =
    AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex Y
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteDistribLattice.toCoframe : {α : Type u_1} → [self : CompleteDistribLattice α] → Order.Coframe α
-- Mathlib.Tactic.Linter.UpstreamableDecl
/-- Does this declaration come from the current file?  -/
Lean.Name.isLocal : Lean.Environment → Lean.Name → Bool
-- Mathlib.Probability.HasCondDistrib
/-- Predicate stating that the conditional distribution of `Y` given `X` under the measure `P`
is equal to the kernel `κ`.  -/
ProbabilityTheory.HasCondDistrib : {Ω : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        {m𝓧 : MeasurableSpace 𝓧} →
          {m𝓨 : MeasurableSpace 𝓨} → (Ω → 𝓨) → (Ω → 𝓧) → ProbabilityTheory.Kernel 𝓧 𝓨 → MeasureTheory.Measure Ω → Prop
-- Mathlib.Algebra.Regular.Pow
IsRegular.prod : ∀ {ι : Type u_2} {R : Type u_3} [inst : CommMonoid R] {s : Finset ι} {f : ι → R},
  (∀ i ∈ s, IsRegular (f i)) → IsRegular (∏ i ∈ s, f i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_append_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l' = false → Std.Internal.List.getEntry? a (l ++ l') = Std.Internal.List.getEntry? a l
-- Lean.Elab.DeclarationRange
/-- Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and
`cmdStx` the remaining part of the syntax tree for `declName`.

This method is for the builtin declarations only. User-defined commands should use
`Lean.Elab.addDeclarationRangesFromSyntax` or `Lean.addDeclarationRanges` to store this information
for their commands.
 -/
Lean.Elab.addDeclarationRangesForBuiltin : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadFileMap m] → Lean.Name → Lean.TSyntax `Lean.Parser.Command.declModifiers → Lean.Syntax → m Unit
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_maxKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → t.maxKey?.isSome = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DTreeMap.Raw.Const.get? (m₁ \ m₂) k = Std.DTreeMap.Raw.Const.get? m₁ k
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.disjoint : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {la₁ la₂ : Filter α} {lb₁ lb₂ : Filter β},
  Filter.Tendsto f la₁ lb₁ → Disjoint lb₁ lb₂ → Filter.Tendsto f la₂ lb₂ → Disjoint la₁ la₂
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 ↔ ∃ x, Polynomial.C x = p
-- Mathlib.Data.Seq.Basic
Stream'.Seq.join_nil : ∀ {α : Type u}, Stream'.Seq.nil.join = Stream'.Seq.nil
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_add_iff_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddRightMono α] [AddRightReflectLE α] (a : α) {b c : α},
  b + a ≤ c + a ↔ b ≤ c
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instFiniteHom : ∀ (K : Type u) [inst : Field K] (V W : FGModuleCat K), Module.Finite K (V ⟶ W)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_mono : ∀ {V : Type u} {G : SimpleGraph V} {s : Set V} {G' G'' : G.Subgraph}, G' ≤ G'' → G'.deleteVerts s ≤ G''.deleteVerts s
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.mem_op : ∀ {R : Type u_2} [inst : NonAssocRing R] {x : Rᵐᵒᵖ} {S : Subring R}, x ∈ S.op ↔ MulOpposite.unop x ∈ S
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)),
  (CochainComplex.mappingCone.trianglehMapOfHomotopy H).hom₃ =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.mapOfHomotopy H)
-- Init.Data.Int.Bitwise.Lemmas
Int.mul_shiftLeft : ∀ (a b : ℤ) (n : ℕ), a * b <<< n = (a * b) <<< n
-- Mathlib.Order.Concept
Concept.ofAttributes_le_of_intent_subset : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} {c : Concept α β r},
  c.intent ⊆ t → Concept.ofAttributes r t ≤ c
-- Mathlib.Algebra.Order.Floor.Ring
Int.sub_floor_div_mul_nonneg : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {b : k} (a : k),
  0 < b → 0 ≤ a - ↑⌊a / b⌋ * b
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- `it.IsPlausibleNthOutputStep n step` is the proposition that according to the
`IsPlausibleStep` relation, it is plausible that `step` returns the step in which the `n`-th value
of `it` is emitted, or `.done` if `it` can plausibly terminate before emitting `n` values.
 -/
Std.IterM.IsPlausibleNthOutputStep : {α β : Type w} →
  {m : Type w → Type w'} → [Std.Iterator α m β] → ℕ → Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Std.Sync.Channel
/-- Producers that are blocked on a consumer taking their value.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.producers : {α : Type} → Std.CloseableChannel.Zero.State✝ α → Std.Queue (α × IO.Promise Bool)
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_mul : ∀ {R : Type u} [inst : Add R] (x y : Tropical R), Tropical.untrop (x * y) = Tropical.untrop x + Tropical.untrop y