mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by `i + j` is the same as shifting by `i` and then shifting by `j`.  -/
CategoryTheory.shiftAdd : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (X : C) →
            (i j : A) →
              (CategoryTheory.shiftFunctor C (i + j)).obj X ≅
                (CategoryTheory.shiftFunctor C j).obj ((CategoryTheory.shiftFunctor C i).obj X)
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionCyclesIso_hom_iCycles_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (j k : ι) (hk : c.next j = k) {j' k' : ι'}
  (hj' : e.f j = j') (hk' : e.f k = k') (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j] {Z : C} (h : K.X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom
      (CategoryTheory.CategoryStruct.comp (K.iCycles j') h) =
    CategoryTheory.CategoryStruct.comp ((K.restriction e).iCycles j)
      (CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').hom h)
-- Mathlib.Algebra.Order.Star.Basic
instZeroLEOneClass : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R],
  ZeroLEOneClass R
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.node : {α : Type u} → ℕ → Ordnode α → α → Ordnode α → Ordnode α
-- Init.Notation
/-- `!p` parses the negation of `p`. That is, it fails if `p` succeeds, and
otherwise parses nothing. It has arity 0.
 -/
stx!_ : Lean.ParserDescr
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.sum_mem : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : ContinuousConstSMul 𝕜 E]
  [inst_10 : ContinuousConstSMul 𝕜 F] {S : Type u_6} {s : S} [inst_11 : SetLike S F] [AddSubmonoidClass S F],
  IsClosed ↑s → ∀ (p : FormalMultilinearSeries 𝕜 E F) (x : E), (∀ (k : ℕ), ((p k) fun x_1 => x) ∈ s) → p.sum x ∈ s
-- Mathlib.Logic.Equiv.Option
Equiv.optionIsSomeEquiv_apply : ∀ (α : Type u_4) (o : { x // x.isSome = true }), (Equiv.optionIsSomeEquiv α) o = (↑o).get ⋯
-- Mathlib.Order.RelClasses
/-- Set notation form of `ne_of_not_le` -/
ne_of_not_subset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, ¬a ⊆ b → a ≠ b
-- Mathlib.Topology.List
List.tendsto_eraseIdx : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {l : List α},
  Filter.Tendsto (fun x => x.eraseIdx n) (nhds l) (nhds (l.eraseIdx n))
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.cauchyBound_smul : ∀ {K : Type u_1} [inst : NormedDivisionRing K] {x : K},
  x ≠ 0 → ∀ (p : Polynomial K), (x • p).cauchyBound = p.cauchyBound
-- Init.Omega.IntList
Lean.Omega.IntList.dot_nil_right : ∀ {xs : Lean.Omega.IntList}, xs.dot [] = 0
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.prodMultiplicative_apply : ∀ (G : Type u_2) (H : Type u_3) [inst : Add G] [inst_1 : Add H] (x : Multiplicative (G × H)),
  (MulEquiv.prodMultiplicative G H) x =
    (Multiplicative.ofAdd (Multiplicative.toAdd x).1, Multiplicative.ofAdd (Multiplicative.toAdd x).2)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.leftInverse_exp_arg : Function.LeftInverse (⇑Circle.exp) (Complex.arg ∘ Subtype.val)
-- Std.Data.DHashMap.Internal.HashesTo
Std.DHashMap.Internal.List.hashesTo_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {i size : ℕ} {l : List ((a : α) × β a)} {k : α}
  {v : β k},
  (∀ (h' : 0 < size), (↑(Std.DHashMap.Internal.mkIdx size h' (hash k))).toNat = i) →
    Std.DHashMap.Internal.List.HashesTo l i size → Std.DHashMap.Internal.List.HashesTo (⟨k, v⟩ :: l) i size
-- Mathlib.MeasureTheory.MeasurableSpace.NCard
measurable_ncard : ∀ {α : Type u_1} [Countable α], Measurable Set.ncard
-- Init.Data.UInt.Lemmas
USize.mod_eq_of_lt : ∀ {a b : USize}, a < b → a % b = a
-- Init.Data.Nat.Compare
Nat.compare_eq_eq : ∀ {a b : ℕ}, compare a b = Ordering.eq ↔ a = b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    (∀ a ∈ m, (List.map Sigma.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Continuous f
-- Init.Data.FloatArray.Basic
FloatArray : Type
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.instInhabited : (α : Type u_2) → [inst : Preorder α] → [inst_1 : Add α] → Inhabited (α ≃+o α)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.range_zpow : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α}, f.IsCycleOn s → a ∈ s → (Set.range fun n => (f ^ n) a) = s
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- The coercion from `ℤ_[p]` to `ℚ_[p]` as a ring homomorphism.  -/
PadicInt.Coe.ringHom : {p : ℕ} → [hp : Fact (Nat.Prime p)] → ℤ_[p] →+* ℚ_[p]
-- Init.Data.UInt.Lemmas
USize.le_trans : ∀ {a b c : USize}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- The **Stone-Weierstrass Approximation Theorem**,
that a subalgebra `A` of `C(X, ℝ)`, where `X` is a compact topological space,
is dense if it separates points.
 -/
ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
  A.SeparatesPoints → A.topologicalClosure = ⊤
-- Mathlib.Data.List.Sigma
List.exists_of_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)},
  a ∈ l.keys → ∃ b l₁ l₂, a ∉ l₁.keys ∧ l = l₁ ++ ⟨a, b⟩ :: l₂ ∧ List.kerase a l = l₁ ++ l₂
-- Mathlib.Geometry.Polygon.Basic
Polygon.mk.injEq : ∀ {P : Type u_1} {n : ℕ} (vertices vertices_1 : Fin n → P),
  ({ vertices := vertices } = { vertices := vertices_1 }) = (vertices = vertices_1)
-- Mathlib.Algebra.Field.Defs
Field.toNontrivial : ∀ {K : Type u} [self : Field K], Nontrivial K
-- Init.Meta.Defs
Lean.Syntax.instBEqPreresolved : BEq Lean.Syntax.Preresolved
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.aux_tendsto_tsum_cexp_pnat : ∀ (z : UpperHalfPlane),
  Filter.Tendsto (fun N => ∑' (n : ℕ+), Complex.exp (2 * ↑Real.pi * Complex.I * (-↑↑N / ↑z)) ^ ↑n) Filter.atTop (nhds 0)
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.seminormedGroup.eq_1 : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F],
  Prod.seminormedGroup =
    { toNorm := Prod.toNorm, toGroup := Prod.instGroup, toPseudoMetricSpace := Prod.pseudoMetricSpaceMax, dist_eq := ⋯ }
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [inst_3 : TopologicalSpace E] {s : Set E},
  WithSeminorms p → (Bornology.IsVonNBounded 𝕜 s ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The homotopy category of bifibrant objects.  -/
HomotopicalAlgebra.BifibrantObject.HoCat : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [HomotopicalAlgebra.ModelCategory C] → Type u
-- Mathlib.Algebra.Group.Action.Prod
Prod.addAction.eq_1 : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α] [inst_2 : AddAction M β],
  Prod.addAction = { toVAdd := Prod.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.GroupTheory.Finiteness
AddMonoid.FG.fg_top : ∀ {M : Type u_3} {inst : AddMonoid M} [self : AddMonoid.FG M], ⊤.FG
-- Mathlib.Analysis.Normed.Order.Lattice
instHasSolidNormReal : HasSolidNorm ℝ
-- Init.Data.SInt.Bitwise
ISize.toInt32_and : ∀ (a b : ISize), (a &&& b).toInt32 = a.toInt32 &&& b.toInt32
-- Mathlib.RingTheory.LaurentSeries
/-- For every Laurent series `f` and every `γ : ℤᵐ⁰` one can find a rational function `Q` such
that the `X`-adic valuation `v` satisfies `v (f - Q) < γ`.  -/
LaurentSeries.exists_ratFunc_val_lt : ∀ {K : Type u_2} [inst : Field K] (f : LaurentSeries K) (γ : (WithZero (Multiplicative ℤ))ˣ),
  ∃ Q, Valued.v (f - (algebraMap (RatFunc K) (LaurentSeries K)) Q) < ↑γ
-- Lean.Parser.Module
_private.Lean.Parser.Module.0.Lean.Parser.consumeInput : Lean.Parser.InputContext → Lean.Parser.ParserModuleContext → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Geometry.Euclidean.Altitude
/-- Altitudes are perpendicular to the faces containing their foot.  -/
Affine.Simplex.inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {i j : Fin (n + 1)} (h : i ≠ j),
  have this := ⋯;
  inner ℝ (s.points j -ᵥ s.altitudeFoot i) (s.points i -ᵥ s.altitudeFoot i) = 0
-- Mathlib.Algebra.Order.Kleene
/-- **Alias** of the reverse direction of `add_eq_left_iff_le`. -/
LE.le.add_eq_left : ∀ {α : Type u_1} [inst : IdemSemiring α] {a b : α}, b ≤ a → a + b = a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (p₁.mulC p₂ c) =
    Lean.Grind.CommRing.Poly.denote ctx p₁ * Lean.Grind.CommRing.Poly.denote ctx p₂
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsMatchingFree.mono : ∀ {V : Type u_1} {G G' : SimpleGraph V}, G ≤ G' → G'.IsMatchingFree → G.IsMatchingFree
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. A measurable function is greater than its integral on a set f
positive measure.  -/
MeasureTheory.measure_lintegral_le_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  [MeasureTheory.IsProbabilityMeasure μ], ∫⁻ (a : α), f a ∂μ ≠ ⊤ → 0 < μ {x | ∫⁻ (a : α), f a ∂μ ≤ f x}
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The isomorphism between the fiber product of two schemes `Spec S` and `Spec T`
over a scheme `Spec R` and the `Spec` of the tensor product `S ⊗[R] T`.

This is a version of `pullbackSpecIso` stated in terms of `specOverSpec`.
TODO: Unify with `pullbackSpecIso` once `OverClass` is refactored to not bundle the morphism.  -/
AlgebraicGeometry.pullbackSpecIso' : (R S T : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      [inst_2 : CommRing T] →
        [inst_3 : Algebra R S] →
          [inst_4 : Algebra R T] →
            CategoryTheory.Limits.pullback
                (AlgebraicGeometry.Spec (CommRingCat.of S) ↘ AlgebraicGeometry.Spec (CommRingCat.of R))
                (AlgebraicGeometry.Spec (CommRingCat.of T) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) ≅
              AlgebraicGeometry.Spec (CommRingCat.of (TensorProduct R S T))
-- Mathlib.Analysis.Quaternion
Quaternion.coeComplex_one : ↑1 = 1
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.IsComplex.zero'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n},
  S.IsComplex →
    ∀ (i j k : ℕ) (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_1)
      (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_3)
      (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_5) {Z : C} (h : S.obj ⟨k, ⋯⟩ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (S.map' i j ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (S.map' j k ⋯ hk) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- An additive subsemigroup of an additive magma `M` is a subset closed under addition.  -/
AddSubsemigroup : (M : Type u_3) → [Add M] → Type u_3
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionSemiHomClass.toDistribMulActionSemiHomClass : ∀ {F : Type u_15} {M : outParam (Type u_16)} {N : outParam (Type u_17)} {inst : Monoid M} {inst_1 : Monoid N}
  {φ : outParam (M → N)} {R : outParam (Type u_18)} {S : outParam (Type u_19)} {inst_2 : Semiring R}
  {inst_3 : Semiring S} {inst_4 : DistribMulAction M R} {inst_5 : DistribMulAction N S} {inst_6 : FunLike F R S}
  [self : MulSemiringActionSemiHomClass F φ R S], DistribMulActionSemiHomClass F φ R S
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Return all applicable hypothesis rewrites of `e`. Similar to `getImportRewrites`.  -/
Mathlib.Tactic.LibraryRewrite.getHypothesisRewrites : Lean.Expr → Option Lean.FVarId → Lean.MetaM (Array (Array (Mathlib.Tactic.LibraryRewrite.Rewrite × Lean.FVarId)))
-- Init.Control.Lawful.Instances
controlAt.eq_1 : ∀ (m : Type u → Type v) {n : Type u → Type w} [inst : MonadControlT m n] [inst_1 : Bind n] {α : Type u}
  (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)), controlAt m f = liftWith f >>= restoreM
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalExprTransparencyMode.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.TransparencyMode
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.hasFiniteMulSupport_of_discreteTopology : ∀ {α : Type u_5} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α),
  Multipliable f → Function.HasFiniteMulSupport f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_eq_head?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey? = t.keys.head?
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_ne_endPos : ∀ {s : String} {p : s.Pos} {h : p ≠ s.startPos}, p.prev h ≠ s.endPos
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.NonnegCoeffs.below.nil : ∀ {motive : (a : Lean.Grind.Linarith.Poly) → a.NonnegCoeffs → Prop},
  Lean.Grind.Linarith.Poly.NonnegCoeffs.below Lean.Grind.Linarith.Poly.NonnegCoeffs.nil
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Truncated simplicial objects.  -/
CategoryTheory.SimplicialObject.Truncated : (C : Type u) → [CategoryTheory.Category.{v, u} C] → ℕ → Type (max v u)
-- Mathlib.Topology.Algebra.UniformRing
/-- The dense inducing extension as a ring homomorphism.  -/
IsDenseInducing.extendRingHom : {α : Type u_1} →
  [inst : UniformSpace α] →
    [inst_1 : Semiring α] →
      {β : Type u_2} →
        [inst_2 : UniformSpace β] →
          [inst_3 : Semiring β] →
            [IsTopologicalSemiring β] →
              {γ : Type u_3} →
                [inst_5 : UniformSpace γ] →
                  [inst_6 : Semiring γ] →
                    [IsTopologicalSemiring γ] →
                      [T2Space γ] →
                        [CompleteSpace γ] →
                          {i : α →+* β} →
                            {f : α →+* γ} → IsUniformInducing ⇑i → DenseRange ⇑i → UniformContinuous ⇑f → β →+* γ
-- Init.Conv
/-- `right` traverses into the right argument. Synonym for `rhs`.  -/
Lean.Parser.Tactic.Conv.convRight : Lean.ParserDescr
-- Init.Data.Nat.Lemmas
Nat.pow_add' : ∀ (a m n : ℕ), a ^ (m + n) = a ^ n * a ^ m
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A monoid homomorphism `f : M →* N` with a left-inverse `g : N → M` defines a multiplicative
equivalence between `M` and `f.mrange`.
This is a bidirectional version of `MonoidHom.mrangeRestrict`.  -/
MulEquiv.ofLeftInverse' : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] → (f : M →* N) → {g : N → M} → Function.LeftInverse g ⇑f → M ≃* ↥(MonoidHom.mrange f)
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing : ∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] (M : Type v)
  [inst_3 : AddCommGroup M] [inst_4 : Module R₀ M] [inst_5 : Module R M] [inst_6 : IsScalarTower R₀ R M]
  [IsSemisimpleModule R M] [Module.Finite R M],
  ∃ n D d x x_1,
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.addRight_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.AddGrpObj A],
  CategoryTheory.AddGrpObj.addRight CategoryTheory.AddMonObj.zero = CategoryTheory.Iso.refl A
-- Init.Data.UInt.Basic
/-- The power operation, raising an 8-bit unsigned integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
UInt8.pow : UInt8 → ℕ → UInt8
-- Mathlib.Topology.Algebra.Algebra
/-- Restrict codomain of a continuous algebra morphism.  -/
ContinuousAlgHom.codRestrict : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] →
                  [inst_6 : Algebra R B] → (f : A →A[R] B) → (p : Subalgebra R B) → (∀ (x : A), f x ∈ p) → A →A[R] ↥p
-- 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 : α → β → 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.CategoryTheory.Bicategory.Monad.Basic
/-- The comultiplication 2-morphism of the comonad.  -/
CategoryTheory.Bicategory.«termΔ[_]» : Lean.ParserDescr
-- Mathlib.Data.Finsupp.Single
Finsupp.support_update_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) {b : M} [inst_1 : DecidableEq α],
  b ≠ 0 → (f.update a b).support = insert a f.support
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Given a t-structure `t` on a pretriangulated category `C` and `n : ℤ`, this
is the `≥ n`-truncation functor. See also the natural transformation `truncGEπ`.  -/
CategoryTheory.Triangulated.TStructure.truncGE : {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] →
              CategoryTheory.Triangulated.TStructure C → ℤ → CategoryTheory.Functor C C
-- Aesop.Tree.Data
Aesop.MVarClusterData.mk.sizeOf_spec : ∀ {Goal Rapp : Type} [inst : SizeOf Goal] [inst_1 : SizeOf Rapp] (parent? : Option (IO.Ref Rapp))
  (goals : Array (IO.Ref Goal)) (isIrrelevant : Bool) (state : Aesop.NodeState),
  sizeOf { parent? := parent?, goals := goals, isIrrelevant := isIrrelevant, state := state } =
    1 + sizeOf parent? + sizeOf goals + sizeOf isIrrelevant + sizeOf state
-- Mathlib.RingTheory.Bialgebra.Hom
/-- The proposition that the function preserves multiplication  -/
BialgHom.map_mul' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (self : A →ₐc[R] B) (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Each element of the scalars defines an additive monoid homomorphism.  -/
DistribSMul.toAddMonoidHom : {M : Type u_1} → (A : Type u_7) → [inst : AddZeroClass A] → [DistribSMul M A] → M → A →+ A
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The functor `Set.Iio i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
when `i ≤ j`.  -/
CategoryTheory.SmallObject.restrictionLT : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : PartialOrder J] →
        {j : J} → CategoryTheory.Functor (↑(Set.Iic j)) C → {i : J} → i ≤ j → CategoryTheory.Functor (↑(Set.Iio i)) C
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The isomorphism `𝟙_ D ≅ F.obj (𝟙_ C)` when `F` is a monoidal functor.  -/
CategoryTheory.Functor.Monoidal.εIso : {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 : CategoryTheory.Functor C D) →
              [F.Monoidal] →
                CategoryTheory.MonoidalCategoryStruct.tensorUnit D ≅
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The group homomorphism on nonsingular points induced by the base change from `F` to `K`, where
`W` is defined over a subring of a ring `S`, and `F` and `K` are field extensions of `S`.  -/
WeierstrassCurve.Affine.Point.baseChange : {R : Type r} →
  (F : Type u) →
    (K : Type v) →
      [inst : CommRing R] →
        [inst_1 : Field F] →
          [inst_2 : Field K] →
            {W' : WeierstrassCurve.Affine R} →
              [inst_3 : DecidableEq F] →
                [inst_4 : DecidableEq K] →
                  [inst_5 : Algebra R F] →
                    [inst_6 : Algebra R K] →
                      [inst_7 : Algebra F K] →
                        [IsScalarTower R F K] → (W'.baseChange F).Point →+ (W'.baseChange K).Point
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Convolution unit on linear maps from a coalgebra to an algebra.  -/
LinearMap.convOne : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid C] → [inst_4 : Module R C] → [Coalgebra R C] → One (WithConv (C →ₗ[R] A))
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.ne`. -/
HasSSubset.SSubset.ne : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → a ≠ b
-- Init.Data.List.Perm
List.Perm.map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {l₁ l₂ : List α}, l₁.Perm l₂ → (List.map f l₁).Perm (List.map f l₂)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
/-- An integer `n` is divisible by `ζ - 1` in `𝓞 K` if and only if it is divisible by `p`,
where `ζ` is a primitive `p`-th root of unity.  -/
IsCyclotomicExtension.Rat.zeta_sub_one_dvd_intCast_iff' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) {n : ℤ}, hζ.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n