mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAt_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : One F] (x : E), HasFDerivAt 1 0 x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology.cocycles C n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.cocyclesMap (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.resMap g φ) ψ) n) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ n)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap g ψ n) h)
-- Mathlib.Data.Sigma.Basic
Sigma.fst_surjective : ∀ {α : Type u_1} {β : α → Type u_4} [h : ∀ (a : α), Nonempty (β a)], Function.Surjective Sigma.fst
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
/-- Is `S` is an exact short complex and `h : S.HomologyData`, there is
a short exact sequence `0 ⟶ h.left.K ⟶ S.X₂ ⟶ h.right.Q ⟶ 0`.  -/
CategoryTheory.ShortComplex.Exact.shortExact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) (h : S.HomologyData),
  { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }.ShortExact
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.toTupleMvPolynomial_one_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R), p.toTupleMvPolynomial 1 = MvPolynomial.X 1 ^ p.natDegree
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instSMulWithZero_1 : {G₀ : Type u_1} → {M₀ : Type u_2} → [inst : Zero G₀] → [inst_1 : Zero M₀] → [SMulWithZero G₀ M₀] → SMulWithZero G₀ M₀ᵒᵈ
-- Init.Meta.Defs
/-- Creates literal syntax for the given string.

If `info` is provided, then the literal's source information is copied from it.
 -/
Lean.Syntax.mkStrLit : String → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.StrLit
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Homotopy between morphisms of short complexes is compatible with precomposition.  -/
CategoryTheory.ShortComplex.Homotopy.compLeft : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            (ψ : S₃ ⟶ S₁) →
              CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp ψ φ₁)
                (CategoryTheory.CategoryStruct.comp ψ φ₂)
-- Mathlib.GroupTheory.Divisible
Pi.rootableBy.eq_1 : ∀ {ι : Type u_3} {β : Type u_4} (B : ι → Type u_5) [inst : (i : ι) → Pow (B i) β] [inst_1 : Zero β]
  [inst_2 : (i : ι) → Monoid (B i)] [inst_3 : (i : ι) → RootableBy (B i) β],
  Pi.rootableBy B = { root := fun x n i => RootableBy.root (x i) n, root_zero := ⋯, root_cancel := ⋯ }
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roc_eq_some : ∀ {m n : ℤ} {i : ℕ}, i < (n - m).toNat → (m<...=n).toArray[i]? = some (m + 1 + ↑i)
-- Mathlib.Data.Stream.Init
Stream'.get_cons_append_zero : ∀ {α : Type u} {a : α} {x : List α} {s : Stream' α}, (a :: x ++ₛ s).get 0 = a
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Discrete.eqToHom'.congr_simp : ∀ {α : Type u₁} {a b : α} (h : a = b), CategoryTheory.Discrete.eqToHom' h = CategoryTheory.Discrete.eqToHom' h
-- Mathlib.Algebra.GroupWithZero.Prod
divMonoidWithZeroHom_apply : ∀ {M₀ : Type u_1} [inst : CommGroupWithZero M₀] (a : M₀ × M₀), divMonoidWithZeroHom a = (↑divMonoidHom).toFun a
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- An infinite place is real if it is defined by a real embedding.  -/
NumberField.InfinitePlace.IsReal : {K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Prod
/-- A variant of `differentiableWithinAt_finCons` where the derivative variables are free on the RHS
instead.  -/
differentiableWithinAt_finCons' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) s x ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- The elements in `spinGroup Q` embed into (CliffordAlgebra Q)ˣ.  -/
spinGroup.toUnits : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → ↥(spinGroup Q) →* (CliffordAlgebra Q)ˣ
-- Mathlib.Topology.Separation.Hausdorff
image_closure_of_isCompact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {s : Set X},
  IsCompact (closure s) → ∀ {f : X → Y}, ContinuousOn f (closure s) → f '' closure s = closure (f '' s)
-- Init.Notation
/-- The conditional function.

`cond c x y` is the same as `if c then x else y`, but optimized for a Boolean condition rather than
a decidable proposition. It can also be written using the notation `bif c then x else y`.

Just like `ite`, `cond` is declared `@[macro_inline]`, which causes applications of `cond` to be
unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and
only the selected branch is evaluated.
 -/
boolIfThenElse : Lean.ParserDescr
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toLinearEquiv_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V) (v : V), (SpecialLinearGroup.toLinearEquiv A) v = (fun x => ↑A x) v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ} (h : t.WF),
  (Std.TreeMap.Raw.filterMap f t).getD k fallback = (t[k]?.pbind fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Init.Data.Fin.Fold
Fin.foldr.loop.eq_def : ∀ {α : Sort u_1} (n : ℕ) (f : Fin n → α → α) (i : ℕ) (a : i ≤ n) (a_1 : α),
  Fin.foldr.loop n f i a a_1 =
    match i, a, a_1 with
    | 0, x, x_1 => x_1
    | i.succ, h, x => Fin.foldr.loop n f i ⋯ (f ⟨i, h⟩ x)
-- Mathlib.Data.Set.Insert
Set.forall_insert_of_forall : ∀ {α : Type u_1} {P : α → Prop} {a : α} {s : Set α}, (∀ x ∈ s, P x) → P a → ∀ x ∈ insert a s, P x
-- Mathlib.RingTheory.Jacobson.Radical
Ring.coe_jacobson_quotient : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided],
  ↑(Ring.jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ}
  {g : β → γ} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving g μb μc →
    MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → MeasureTheory.Measure.QuasiMeasurePreserving (g ∘ f) μa μc
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
        (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k (Std.Internal.List.insertEntry k v l) = true
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasBiproductsOfShape_of_equiv : ∀ {J : Type w} (C : Type uC) [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} [CategoryTheory.Limits.HasBiproductsOfShape K C]
  (e : J ≃ K), CategoryTheory.Limits.HasBiproductsOfShape J C
-- Mathlib.Analysis.Calculus.MeanValue
is_const_of_fderiv_eq_zero : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace 𝕜 G] {E : Type u_5} [inst_4 : NormedAddCommGroup E]
  [inst_5 : NormedSpace 𝕜 E] {f : E → G}, Differentiable 𝕜 f → (∀ (x : E), fderiv 𝕜 f x = 0) → ∀ (x y : E), f x = f y
-- Mathlib.Data.Rel
SetRel.empty_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : SetRel β γ), ∅.comp S = ∅
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).getKey! k = if (f (t.get? k)).isSome = true then k else default
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.prelude.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `Differentiable.add_iff_left` -/
Differentiable.fun_add_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 g → ((Differentiable 𝕜 fun i => f i + g i) ↔ Differentiable 𝕜 f)
-- Mathlib.Algebra.Lie.Subalgebra
/-- The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the
codomain.  -/
LieSubalgebra.map : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {L₂ : Type w} →
            [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → (L →ₗ⁅R⁆ L₂) → LieSubalgebra R L → LieSubalgebra R L₂
-- Std.Internal.Do.ExceptPost
Std.Internal.Do.EPost.Nil.mk : EPost⟨⟩
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instIsAddCommutative : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α] [IsAddCommutative α], IsAddCommutative (Matrix m n α)
-- Mathlib.Order.Irreducible
IsMin.not_supIrred : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, IsMin a → ¬SupIrred a
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.mk' : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} →
                      {σ : Representation A G W} →
                        (toIntertwiningMap : ρ.IntertwiningMap σ) →
                          (invFun : W → V) →
                            autoParam (Function.LeftInverse invFun toIntertwiningMap.toFun) Equiv.left_inv._autoParam →
                              autoParam (Function.RightInverse invFun toIntertwiningMap.toFun)
                                  Equiv.right_inv._autoParam →
                                ρ.Equiv σ
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.neg.injEq : ∀ (a a_1 : Int.Internal.Linear.Expr), (a.neg = a_1.neg) = (a = a_1)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- Curried `C^n` functions are `C^n` in the second coordinate.  -/
ContMDiffWithinAt.curry_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {y : M'} {s : Set (M × M')},
  ContMDiffWithinAt (I.prod I') J n (Function.uncurry f) s (x, y) →
    ContMDiffWithinAt I' J n (fun y => f x y) {y | (x, y) ∈ s} y
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.notMem_of_lt_hittingAfter : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} {k : ι}, ↑k < MeasureTheory.hittingAfter u s n ω → n ≤ k → u k ω ∉ s
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.instIsDenseSubsiteFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D)
  [CategoryTheory.Functor.IsDenseSubsite K J e.inverse], CategoryTheory.Functor.IsDenseSubsite J K e.functor
-- Lean.Util.Diff
/-- How many times the element occurs in the left array  -/
Lean.Diff.Histogram.Entry.leftCount : {α : Type u} → {lsize rsize : ℕ} → Lean.Diff.Histogram.Entry α lsize rsize → ℕ
-- Mathlib.Algebra.Polynomial.CoeffMem
/-- For polynomials `p q : R[X]`, the coefficients of `p /ₘ q` can be written as sums of products of
coefficients of `p` and `q`.

Precisely, each summand needs at most one coefficient of `p` and `deg p` coefficients of `q`.  -/
Polynomial.coeff_divByMonic_mem_pow_natDegree_mul : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (p q : Polynomial S)
  (Mp : Submodule R S),
  (∀ (i : ℕ), p.coeff i ∈ Mp) →
    1 ∈ Mp →
      ∀ (Mq : Submodule R S), (∀ (i : ℕ), q.coeff i ∈ Mq) → 1 ∈ Mq → ∀ (i : ℕ), (p /ₘ q).coeff i ∈ Mq ^ p.natDegree * Mp
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubMulAction.closure_mono : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul R M] {s t : Set M},
  s ⊆ t → SubMulAction.closure R s ≤ SubMulAction.closure R t
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.trans_P : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsFibrant A] (P P' : HomotopicalAlgebra.PathObject A) [inst_3 : P'.IsGood],
  (P.trans P').P = CategoryTheory.Limits.pullback P.p₁ P'.p₀
-- Mathlib.Order.Antichain
IsAntichain.image_relIso_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ≃r r'},
  IsAntichain r' (⇑φ '' s) ↔ IsAntichain r s
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Auxiliary definition for `Functor.Monoidal.transport`
 -/
CategoryTheory.Functor.Monoidal.coreMonoidalTransport : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F G : CategoryTheory.Functor C D} → [F.Monoidal] → (F ≅ G) → G.CoreMonoidal
-- Mathlib.Algebra.CharP.Basic
/-- The characteristic of the product of two rings of the same characteristic
is the same as the characteristic of the rings  -/
Prod.charP : ∀ (R : Type u_1) (S : Type u_2) [inst : AddMonoidWithOne R] [inst_1 : AddMonoidWithOne S] (p : ℕ) [CharP R p]
  [CharP S p], CharP (R × S) p
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over ranges in the index type
`β`, the ranges being closed.

The type of the resulting slices is `γ`.
 -/
Std.Rcc.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.RingTheory.Perfection
Perfection.pthRootMonoidHom_eq_symm_frobeniusEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  ⇑(Perfection.pthRootMonoidHom R p) = ⇑↑(frobeniusEquiv (Perfection R p) p).symm
-- Mathlib.Algebra.Group.Submonoid.Finite
Submonoid.closure_pi : ∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → MulOneClass (f i)] [Finite η] {s : (i : η) → Set (f i)},
  (∀ (i : η), 1 ∈ s i) →
    Submonoid.closure (Set.univ.pi fun i => s i) = Submonoid.pi Set.univ fun i => Submonoid.closure (s i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- The yoneda embedding of `AddGrp_C` into presheaves of additive groups.  -/
CategoryTheory.yonedaAddGrp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.AddGrp C) (CategoryTheory.Functor Cᵒᵖ AddGrpCat)
-- Init.Meta.Defs
Lean.NameGenerator.next : Lean.NameGenerator → Lean.NameGenerator
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (m₁ : Z₁₂ ⟶ Z₁₃) (m₃ : Z₁₃ ⟶ Z₂₃) (comm₁ : CategoryTheory.CategoryStruct.comp m₁ v₁₃ = v₁₂)
  (comm₂ :
    CategoryTheory.CategoryStruct.comp w₁₂ ((CategoryTheory.shiftFunctor C 1).map m₁) =
      CategoryTheory.CategoryStruct.comp u₂₃ w₁₃)
  (comm₃ : CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map m₃) = w₂₃)
  (comm₄ : CategoryTheory.CategoryStruct.comp m₃ v₂₃ = CategoryTheory.CategoryStruct.comp v₁₃ u₁₂)
  (mem :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃ (CategoryTheory.CategoryStruct.comp v₂₃ w₁₂) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (m₁_1 : Z₁₂ ⟶ Z₁₃) (m₃_1 : Z₁₃ ⟶ Z₂₃) (comm₁_1 : CategoryTheory.CategoryStruct.comp m₁_1 v₁₃ = v₁₂)
  (comm₂_1 :
    CategoryTheory.CategoryStruct.comp w₁₂ ((CategoryTheory.shiftFunctor C 1).map m₁_1) =
      CategoryTheory.CategoryStruct.comp u₂₃ w₁₃)
  (comm₃_1 : CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map m₃_1) = w₂₃)
  (comm₄_1 : CategoryTheory.CategoryStruct.comp m₃_1 v₂₃ = CategoryTheory.CategoryStruct.comp v₁₃ u₁₂)
  (mem_1 :
    CategoryTheory.Pretriangulated.Triangle.mk m₁_1 m₃_1 (CategoryTheory.CategoryStruct.comp v₂₃ w₁₂) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles),
  ({ m₁ := m₁, m₃ := m₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃, comm₄ := comm₄, mem := mem } =
      { m₁ := m₁_1, m₃ := m₃_1, comm₁ := comm₁_1, comm₂ := comm₂_1, comm₃ := comm₃_1, comm₄ := comm₄_1,
        mem := mem_1 }) =
    (m₁ = m₁_1 ∧ m₃ = m₃_1)
-- Mathlib.Data.Num.Lemmas
PosNum.succ'_pred' : ∀ (n : PosNum), n.pred'.succ' = n
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eraseKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.containsKey k (Std.Internal.List.eraseKey k l) = false
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1NormedCommRing : {R : Type u_3} →
  {M : Type u_4} →
    [inst : NormedCommRing R] →
      [inst_1 : NormedAddCommGroup M] →
        [inst_2 : Module R M] →
          [inst_3 : Module Rᵐᵒᵖ M] → [IsCentralScalar R M] → [IsBoundedSMul R M] → NormedCommRing (TrivSqZeroExt R M)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_aeval : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  (P : Polynomial R) (x : A), D ((Polynomial.aeval x) P) = (Polynomial.aeval x) (Polynomial.derivative P) • D x
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsSymm.mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, (∀ (x y : M), (B x) y = (B y) x) → B.IsSymm
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_δ_self' : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)},
  j = i.castSucc →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ j) =
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ i.succ)
-- Mathlib.Data.Finset.Insert
Finset.Nonempty.subset_singleton_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, s.Nonempty → (s ⊆ {a} ↔ s = {a})
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrArgKind.heq.sizeOf_spec : sizeOf Lean.Meta.CongrArgKind.heq = 1
-- Mathlib.Algebra.Group.Action.Defs
/-- Associativity of `•` and `*`  -/
SemigroupAction.mul_smul : ∀ {α : Type u_9} {β : Type u_10} {inst : Semigroup α} [self : SemigroupAction α β] (x y : α) (b : β),
  (x * y) • b = x • y • b
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.ringEquivOfRingEquiv_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {T : Submonoid P}
  {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q] {j : R ≃+* P}
  (H : Submonoid.map j.toMonoidHom M = T) (x : R) (y : ↥M),
  (IsLocalization.ringEquivOfRingEquiv S Q j H) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (j x) ⟨j ↑y, ⋯⟩
-- Std.Time.Format
/-- The ISO 8601 format, used for representing date and time in a standardized
format. The format follows the pattern `uuuu-MM-dd'T'HH:mm:ssXXX`.
 -/
Std.Time.Formats.iso8601 : Std.Time.GenericFormat Std.Time.Awareness.any
-- Lean.Meta.Tactic.Ext
/-- Priority of the extensionality theorem.  -/
Lean.Meta.Ext.ExtTheorem.priority : Lean.Meta.Ext.ExtTheorem → ℕ
-- Init.Data.Nat.Lemmas
Nat.lt_iff_add_one_le : ∀ {m n : ℕ}, m < n ↔ m + 1 ≤ n