mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- For `j + l ≤ m`, a path of length `m` restricts to a path of length `l`, namely
the subpath spanned by the vertices `j ≤ i ≤ j + l` and edges `j ≤ i < j + l`.  -/
SSet.Truncated.Path.interval : {n : ℕ} →
  {X : SSet.Truncated (n + 1)} →
    {m : ℕ} → X.Path m → (j l : ℕ) → autoParam (j + l ≤ m) SSet.Truncated.Path.interval._auto_1 → X.Path l
-- Mathlib.Probability.Moments.Basic
/-- Central moment of a real random variable, `μ[(X - μ[X]) ^ p]`.  -/
ProbabilityTheory.centralMoment : {Ω : Type u_1} → {m : MeasurableSpace Ω} → (Ω → ℝ) → ℕ → MeasureTheory.Measure Ω → ℝ
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decompose_mul : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring A]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜] (x y : A),
  (DirectSum.decompose 𝒜) (x * y) = (DirectSum.decompose 𝒜) x * (DirectSum.decompose 𝒜) y
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty_inter_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.Algebra.Star.Basic
Equiv.Perm.symm_star : ∀ {R : Type u} [inst : InvolutiveStar R], Equiv.symm Equiv.Perm.star = Equiv.Perm.star
-- Mathlib.MeasureTheory.Group.Arithmetic
instMeasurableEqOfCanonicallyOrderedAddOfOrderedSubOfMeasurableSub₂OfMeasurableSingletonClass : ∀ {β : Type u_5} [inst : AddCommMonoid β] [inst_1 : PartialOrder β] [CanonicallyOrderedAdd β] [inst_3 : Sub β]
  [OrderedSub β] {x : MeasurableSpace β} [MeasurableSub₂ β] [MeasurableSingletonClass β], MeasurableEq β
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The induced cocone on `Under X` from on the lifted functor.  -/
CategoryTheory.Under.liftCocone : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        (D : CategoryTheory.Functor J T) →
          {X : T} →
            (s : (CategoryTheory.Functor.const J).obj X ⟶ D) →
              (c : CategoryTheory.Limits.Cocone D) →
                (p : X ⟶ c.pt) →
                  (∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = p) →
                    CategoryTheory.Limits.Cocone (CategoryTheory.Under.lift D s)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The affine span of a set is `⊥` if and only if that set is empty.  -/
affineSpan_eq_bot : ∀ (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] {s : Set P}, affineSpan k s = ⊥ ↔ s = ∅
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.coeff_isPWOsupport : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W]
  (A : HVertexOperator Γ R V W) (v : V), (Function.support ((HahnModule.of R).symm (A v)).coeff).IsPWO
-- Mathlib.Data.List.Forall2
List.forall₂_eq_eq_eq : ∀ {α : Type u_1}, (List.Forall₂ fun x1 x2 => x1 = x2) = Eq
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.lt_irrefl : ∀ {n : ℕ} (a : BitVec n), a.ult a = false
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.vComp'_iff_of_essSurj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {L₂ : CategoryTheory.Functor C₂ C₃}
  {R₂ : CategoryTheory.Functor D₂ D₃} {H₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
  {L₁₂ : CategoryTheory.Functor C₁ C₃} {R₁₂ : CategoryTheory.Functor D₁ D₃} (eL : L₁.comp L₂ ≅ L₁₂)
  (eR : R₁.comp R₂ ≅ R₁₂) [R₁.EssSurj] [w.GuitartExact], (w.vComp' w' eL eR).GuitartExact ↔ w'.GuitartExact
-- Mathlib.Algebra.CharZero.Defs
Nat.cast_eq_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] {n : ℕ}, ↑n = 0 ↔ n = 0
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_toRingHom_apply_toRingHom_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S) (x : R),
  e.symm.toRingHom (e.toRingHom x) = x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k fallback : α},
  (Std.TreeMap.filter f t).getKeyD k fallback = ((t.getKey? k).pfilter fun x h' => f x t[x]).getD fallback
-- Mathlib.Algebra.Ring.Parity
Even.neg_one_zpow : ∀ {α : Type u_2} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, Even n → (-1) ^ n = 1
-- Mathlib.Data.Finset.Lattice.Fold
Finset.exists_mem_eq_sup' : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} (H : s.Nonempty) (f : ι → α),
  ∃ i ∈ s, s.sup' H f = f i
-- Lean.Meta.CtorIdxHInj
_private.Lean.Meta.CtorIdxHInj.0.Lean.Meta.mkHInjectiveTheorem? : Lean.Name → Lean.InductiveVal → Lean.MetaM Lean.TheoremVal
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.lidIsometry_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), (TensorProduct.lidIsometry 𝕜 E).symm x = 1 ⊗ₜ[𝕜] x
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Given two left-invariant measures which are finite on compacts, `haarScalarFactor μ' μ` is a
scalar such that `∫ f dμ' = (haarScalarFactor μ' μ) ∫ f dμ` for any compactly supported continuous
function `f`.

Note that there is a dissymmetry in the assumptions between `μ'` and `μ`: the measure `μ'` needs
only be finite on compact sets, while `μ` has to be finite on compact sets and positive on open
sets, i.e., a Haar measure, to exclude for instance the case where `μ = 0`, where the definition
doesn't make sense.  -/
MeasureTheory.Measure.haarScalarFactor : {G : Type u_1} →
  [inst : TopologicalSpace G] →
    [inst_1 : Group G] →
      [IsTopologicalGroup G] →
        [inst_3 : MeasurableSpace G] →
          [BorelSpace G] →
            (μ' μ : MeasureTheory.Measure G) →
              [μ.IsHaarMeasure] → [MeasureTheory.IsFiniteMeasureOnCompacts μ'] → [μ'.IsMulLeftInvariant] → NNReal
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isEquivalent_smoothingFn_sub_self : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (i : α),
  Asymptotics.IsEquivalent Filter.atTop
    (fun n => AkraBazziRecurrence.smoothingFn (b i * ↑n) - AkraBazziRecurrence.smoothingFn ↑n) fun n =>
    -Real.log (b i) / Real.log ↑n ^ 2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_nat_mul_two_pi_sub : ∀ (x : ℂ) (n : ℕ), Complex.sin (↑n * (2 * ↑Real.pi) - x) = -Complex.sin x
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.mk.sizeOf_spec : ∀ {T : Type u_1} {N : Type u_2} [inst : SizeOf T] [inst_1 : SizeOf N] (input : N) (output : List (Symbol T N)),
  sizeOf { input := input, output := output } = 1 + sizeOf input + sizeOf output
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
/-- If `c` is a cocone over a functor `J ⥤ C` and `f : X ⟶ c.pt`, then for every `j : J` we can take
the pullback of `c.ι.app j` and `f`. This gives a new cocone with cone point `X`, and this cocone
is again a colimit cocone as long as `J` is connected and `C` has exact colimits of shape `J`.
 -/
CategoryTheory.Limits.IsColimit.pullbackOfHasExactColimitsOfShape : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    [CategoryTheory.IsConnected J] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [inst_3 : CategoryTheory.Limits.HasPullbacks C] →
            [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] →
              [CategoryTheory.HasExactColimitsOfShape J C] →
                {F : CategoryTheory.Functor J C} →
                  {c : CategoryTheory.Limits.Cocone F} →
                    CategoryTheory.Limits.IsColimit c →
                      {X : C} →
                        (f : X ⟶ c.pt) →
                          CategoryTheory.Limits.IsColimit
                            { pt := X,
                              ι := CategoryTheory.Limits.pullback.snd c.ι ((CategoryTheory.Functor.const J).map f) }
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to a `UInt8`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toUInt8 : Float.Model → UInt8
-- Mathlib.Algebra.Group.Commute.Defs
Commute.left_comm : ∀ {S : Type u_3} [inst : Semigroup S] {a b : S}, Commute a b → ∀ (c : S), a * (b * c) = b * (a * c)
-- Mathlib.Data.PFun
/-- The domain of a partial function  -/
PFun.Dom : {α : Type u_1} → {β : Type u_2} → (α →. β) → Set α
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.trW_of_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.IsTriangulated] {X Y : Cᵒᵖ} {f : X ⟶ Y}, P.unop.trW f.unop → P.trW f
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Sum of a multiset of elements in an `AddSubmonoid` of an `AddCommMonoid` is
in the `AddSubmonoid`.  -/
multiset_sum_mem : ∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : SetLike B M] [AddSubmonoidClass B M]
  (m : Multiset M), (∀ a ∈ m, a ∈ S) → m.sum ∈ S
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `FunLike.coe_coeAddMonoidHom`. -/
ProbabilityTheory.Kernel.coeAddHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], ⇑(FunLike.coeAddMonoidHom F α β) = DFunLike.coe
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.simpLoop.visitPost : Lean.Expr → Lean.Meta.Simp.Config → Lean.Meta.Simp.Result → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasFDerivAtFilter_iff_hasDerivAtFilter`.

---

Expressing `HasFDerivAtFilter f f' x L` in terms of `HasDerivAtFilter`  -/
HasFDerivAtFilter.hasDerivAtFilter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {L : Filter (𝕜 × 𝕜)} [inst_4 : ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F},
  HasFDerivAtFilter f f' L → HasDerivAtFilter f (f' 1) L
-- Mathlib.Algebra.CharP.Defs
ringChar.ringChar_eq_one : ∀ {R : Type u_1} [inst : NonAssocSemiring R], ringChar R = 1 ↔ Subsingleton R
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.instIsRegularEpiSnd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Regular C] {X Y B : C} (f : X ⟶ B) (g : Y ⟶ B)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [CategoryTheory.IsRegularEpi f],
  CategoryTheory.IsRegularEpi (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Notation for a lax functor between bicategories.  -/
CategoryTheory.Bicategory.«term_⥤ᴸ_» : Lean.TrailingParserDescr
-- Mathlib.Data.Set.Lattice
Set.coe_snd_unionEqSigmaOfDisjoint : ∀ {α : Type u_12} {β : Type u_13} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) (x : ↑(⋃ i, t i)),
  ↑((Set.unionEqSigmaOfDisjoint h) x).snd = ↑x
-- Mathlib.CategoryTheory.Presentable.Directed
/-- Constructor for `Diagram.IsTerminal` for which no data is provided,
but only its existence.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.ofExistsUnique : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} →
        {e : J} →
          D.W (CategoryTheory.CategoryStruct.id e) →
            (∀ ⦃j : J⦄, D.P j → ∃ lift, D.W lift) →
              (∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂) →
                (∀ ⦃i j : J⦄ (f : i ⟶ j),
                    D.W f → ∃ li lj, D.W li ∧ D.W lj ∧ CategoryTheory.CategoryStruct.comp f lj = li) →
                  D.IsTerminal e
-- Mathlib.Probability.Martingale.Convergence
/-- **Lévy's upward theorem**, L¹ version: given a function `g` and a filtration `ℱ`, the
sequence defined by `𝔼[g | ℱ n]` converges in L¹ to `𝔼[g | ⨆ n, ℱ n]`.  -/
MeasureTheory.tendsto_eLpNorm_condExp : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] (g : Ω → ℝ),
  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (μ[g | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) 1 μ) Filter.atTop (nhds 0)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.inter_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ t₄ : Std.TreeMap.Raw α β cmp},
  t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∩ t₂).Equiv (t₃ ∩ t₄)
-- Std.Async.System
Std.Async.System.instDecidableEqUserId.decEq : (x x_1 : Std.Async.System.UserId) → Decidable (x = x_1)
-- Mathlib.Topology.DenseEmbedding
/-- Two continuous functions to a t2-space that agree on the dense range of a function are equal.  -/
DenseRange.equalizer : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ] [T2Space γ]
  {f : α → β}, DenseRange f → ∀ {g h : β → γ}, Continuous g → Continuous h → g ∘ f = h ∘ f → g = h
-- Mathlib.Algebra.Quandle
_private.Mathlib.Algebra.Quandle.0.Rack.toEnvelGroup.mapAux.match_1.eq_4 : ∀ {R : Type u_1} (motive : Rack.PreEnvelGroup R → Sort u_2) (a : Rack.PreEnvelGroup R)
  (h_1 : Unit → motive Rack.PreEnvelGroup.unit) (h_2 : (x : R) → motive (Rack.PreEnvelGroup.incl x))
  (h_3 : (a b : Rack.PreEnvelGroup R) → motive (a.mul b)) (h_4 : (a : Rack.PreEnvelGroup R) → motive a.inv),
  (match a.inv with
    | Rack.PreEnvelGroup.unit => h_1 ()
    | Rack.PreEnvelGroup.incl x => h_2 x
    | a.mul b => h_3 a b
    | a.inv => h_4 a) =
    h_4 a
-- Lean.CoreM
/-- CoreM is a monad for manipulating the Lean environment.
It is the base monad for `MetaM`.
The main features it provides are:
- name generator state
- environment state
- Lean options context
- the current open namespace
 -/
Lean.Core.CoreM : Type → Type
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  CategoryTheory.MonObj.one = CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor
-- Mathlib.Order.Circular
sbtw_asymm : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬sbtw c b a
-- Mathlib.Algebra.Order.Sub.Prod
Prod.orderedSub : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [OrderedSub α] [inst_4 : Sub β]
  [inst_5 : Preorder β] [inst_6 : Add β] [OrderedSub β], OrderedSub (α × β)
-- Init.Data.SInt.Lemmas
Int32.le_iff_lt_or_eq : ∀ {a b : Int32}, a ≤ b ↔ a < b ∨ a = b
-- Batteries.Data.List.Scan
List.partialProds.eq_1 : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] (l : List α), l.partialProds = List.scanl (fun x1 x2 => x1 * x2) 1 l
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- If `L/K` and `φ : L →+* ℂ`, then `IsMixed K φ` if the image of `φ` is complex while the image
of `φ` restricted to `K` is real.

This is the complex embedding analogue of `InfinitePlace.IsRamified K w`, where
`w : InfinitePlace L`. It is not the same concept because conjugation of `φ` in this case
leads to two distinct mixed embeddings but only a single ramified place `w`, leading to a
two-to-one isomorphism between them.  -/
NumberField.ComplexEmbedding.IsMixed : (K : Type u_3) → {L : Type u_4} → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → (L →+* ℂ) → Prop
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.comp.eq_2 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (_x _y : C) (_z : D) (x_5 : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y))
  (x_6 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z)),
  CategoryTheory.Join.comp x_5 x_6 = PUnit.unit
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_mul_X : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (r : R),
  (SkewPolynomial.monomial n) r * SkewPolynomial.X = (SkewPolynomial.monomial (n + 1)) r
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Small.limitCone_π_app : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : Small.{u, max u v} ↑F.sections] (j : J),
  (CategoryTheory.Limits.Types.Small.limitCone F).π.app j = TypeCat.ofHom fun u => ↑((equivShrink ↑F.sections).symm u) j
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_ne : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i i' : ι} {f : Π₀ (i : ι), β i},
  i' ≠ i → (DFinsupp.erase i f) i' = f i'
-- Mathlib.Order.UpperLower.Closure
UpperSet.le_erase : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {a : α}, s ≤ s.erase a
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getBinHomoInst : Lean.Name → Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.universally.IsStableUnderBaseChange
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.exists_getElem_eq_of_drop_eq_cons : ∀ {α : Type u_1} {xs : List α} {k : ℕ} {y : α} {ys : List α},
  List.drop k xs = y :: ys → ∃ (hlt : k < xs.length), xs[k] = y
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instNullSingletonClassForallVolumeOfNonemptyOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {α : ι → Type u_4} [Nonempty ι]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume]
  [∀ (i : ι), MeasureTheory.NullSingletonClass MeasureTheory.volume],
  MeasureTheory.NullSingletonClass MeasureTheory.volume
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_id_comp_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ)
  {Z : ModuleCat k} (h : groupCohomology C n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n)
      h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) φ n)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) ψ n) h)
-- Mathlib.Algebra.Homology.LocalCohomology
/-- The full subcategory of all ideals with radical containing `J`  -/
localCohomology.SelfLERadical : {R : Type u} → [inst : CommRing R] → Ideal R → Type u
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.getVertEquiv_apply : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsHamiltonian)
  (a_1 : Fin p.support.length), hp.getVertEquiv a_1 = (p.getVert ∘ Fin.val) a_1
-- Init.Control.Lawful.Basic
/-- This is just a duplicate of `Functor.map_map`, but sometimes applies when that doesn't.
 -/
LawfulMonad.map_map : ∀ {α α_1 a : Type u_1} {g : α_1 → a} {f : α → α_1} {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] {x : m α},
  g <$> f <$> x = (fun a => g (f a)) <$> x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- the cokernel condition for `p`  -/
CategoryTheory.ShortComplex.RightHomologyData.wp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.RightHomologyData) {Z : C} (h : self.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.f (CategoryTheory.CategoryStruct.comp self.p h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Sites.Types
/-- The yoneda functor that sends a type to a sheaf over the category of types.  -/
CategoryTheory.yoneda' : CategoryTheory.Functor (Type u) (CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u))
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_iff_eventually : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
  Filter.Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.mem_inf' : ∀ {α : Type u_2} {ι : Type u_5} [inst : DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} (hs : s.Nonempty),
  a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i
-- Lean.Parser.Attr
/-- Declares this tactic to be an alias or alternative form of an existing tactic.

This has the following effects:
* The alias relationship is saved
* The docstring is taken from the original tactic, if present
 -/
Lean.Parser.Attr.tactic_alt : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Limits.coneOfSectionCompYoneda_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) (j : J),
  (CategoryTheory.Limits.coneOfSectionCompYoneda F X s).π.app j = Quiver.Hom.op (↑s j)
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toArray_valuesIter : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α fun x => β},
  m.valuesIter.toArray = (List.map Sigma.snd m.toList).toArray
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.disjoint_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  Disjoint (a • s) (a • t) ↔ Disjoint s t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂)[k]? = if k ∈ t₂ then t₁[k]? else none
-- Init.Sym.Simp.SimprocDSL
/-- Parenthesized simproc expression.  -/
Lean.Parser.Sym.Simp.simprocParen : Lean.ParserDescr
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instMulAction : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → MulAction α (UpperSet α)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- A Grothendieck topology on `C` consists of a set of sieves for each object `X`,
which satisfy some axioms.  -/
CategoryTheory.GrothendieckTopology.sieves : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → (X : C) → Set (CategoryTheory.Sieve X)