mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The **left-translation shift** on configurations, in additive notation.

We call *configuration* an element of `G → A`.

Given a configuration `x : G → A` and an element `g : G` of the additive monoid,
the shifted configuration `shift g x` is defined by `(shift g x) h = x (g + h)`.

Intuitively, this moves the whole configuration "in the direction of `g`": the value
at position `h` in the shifted configuration is the value that was at position
`g + h` in the original one.

For example, if `G = ℤ` and `A = {0, 1}`, then
`shift 1 x` is the sequence obtained from `x` by shifting every symbol one
step to the left.  -/
SymbolicDynamics.FullShift.shift : {A : Type u_1} → {G : Type u_2} → [AddMonoid G] → G → (G → A) → G → A
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The Legendre symbol depends only on `a` mod `p`.  -/
legendreSym.mod : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a : ℤ), legendreSym p a = legendreSym p (a % ↑p)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_sup_pow_eq_top : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [I.IsTwoSided] {m n : ℕ}, I ⊔ J = ⊤ → I ^ m ⊔ J ^ n = ⊤
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHomClass.toBoundedLatticeHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [CompleteLatticeHomClass F α β], BoundedLatticeHomClass F α β
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto_comp_subtype : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), p.projectionOnto q h ∘ₗ p.subtype = LinearMap.id
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- If `α` has some multiplicative structure and coerces to a function,
then `Additive α` should also coerce to the same function.

This allows `Additive` to be used on bundled function types with a multiplicative structure, which
is often used for composition, without affecting the behavior of the function itself.
 -/
Additive.coeToFun : {α : Type u_1} → {β : α → Sort u_2} → [CoeFun α β] → CoeFun (Additive α) fun a => β (Additive.toMul a)
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C}
  {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (hY : J.CoversTop Y)
  (hF : CategoryTheory.Presheaf.IsSheaf J F) (i : I), ↑(hx.section_ hY hF) (Opposite.op (Y i)) = x i
-- Mathlib.Order.Minimal
not_minimal_iff_exists_lt : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : Preorder α], P x → (¬Minimal P x ↔ ∃ y < x, P y)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.instInhabited : {α : Type u_2} → [inst : Preorder α] → [Inhabited α] → Inhabited (OmegaCompletePartialOrder.Chain α)
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A union of a finite family of sets is totally bounded
if and only if each set of the family is totally bounded.  -/
totallyBounded_sUnion : ∀ {α : Type u} [uniformSpace : UniformSpace α] {S : Set (Set α)},
  S.Finite → (TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s)
-- Mathlib.Analysis.InnerProductSpace.Subspace
_private.Mathlib.Analysis.InnerProductSpace.Subspace.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Monoid
Continuous.pow : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M}, Continuous f → ∀ (n : ℕ), Continuous (f ^ n)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_cases : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (P : A → Prop) (a : A)
  (f : R → R),
  P 0 →
    (∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
        P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })) →
      P (cfc f a)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffWithinAt.smul_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {f : M → 𝕜} {s : (x : M) → V x} {u : Set M} {x₀ : M},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 𝕜) n f u x₀ →
    ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u x₀ →
      ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (f • s) x⟩) u x₀
-- Mathlib.Algebra.Lie.SerreConstruction
_private.Mathlib.Algebra.Lie.SerreConstruction.0.CartanMatrix.Relations.termAd : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves finite limits, then `F.rightOp : C ⥤ Dᵒᵖ` preserves finite
colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteColimits F.rightOp
-- Init.Data.String.Iterator
/-- Checks whether the iterator is after the beginning of the string.
 -/
String.Legacy.Iterator.hasPrev : String.Legacy.Iterator → Bool
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_cos_add_sin_mul_I_eq_toIocMod : ∀ (θ : ℝ), (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg = toIocMod Real.two_pi_pos (-Real.pi) θ
-- Mathlib.Algebra.GradedMulAction
GradedMonoid.mk_smul_mk : ∀ {ιA : Type u_1} {ιM : Type u_3} (A : ιA → Type u_4) (M : ιM → Type u_5) [inst : VAdd ιA ιM]
  [inst_1 : GradedMonoid.GSMul A M] {i : ιA} {j : ιM} (a : A i) (b : M j),
  GradedMonoid.mk i a • GradedMonoid.mk j b = GradedMonoid.mk (i +ᵥ j) (GradedMonoid.GSMul.smul a b)
-- Mathlib.Data.Nat.Fib.Basic
Nat.fastFibAux_bit_false : ∀ (n : ℕ),
  (Nat.bit false n).fastFibAux =
    have p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.IsIrreducible.nontrivial : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} (P : RootPairing ι R M N)
  [self : P.IsIrreducible], Nontrivial M
-- Mathlib.Analysis.Calculus.DiffContOnCl
DifferentiableOn.diffContOnCl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  DifferentiableOn 𝕜 f (closure s) → DiffContOnCl 𝕜 f s
-- Mathlib.Data.Sum.Order
OrderIso.sumLexCongr_symm : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [inst : LE α₁] [inst_1 : LE α₂] [inst_2 : LE β₁]
  [inst_3 : LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂), (ea.sumLexCongr eb).symm = ea.symm.sumLexCongr eb.symm
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- Tilde of direct sums of `R` as an `R`-module is isomorphic to the free sheaf.  -/
AlgebraicGeometry.tildeFinsupp : {R : CommRingCat} → (ι : Type u) → AlgebraicGeometry.tilde (ModuleCat.of (↑R) (ι →₀ ↑R)) ≅ SheafOfModules.free ι
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- The set of elements of the `fundamentalCone` of `norm ≤ 1`.
 -/
NumberField.mixedEmbedding.fundamentalCone.normLeOne : (K : Type u_1) → [inst : Field K] → [NumberField K] → Set (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeUnivEquiv_symm_apply : ∀ {α : Sort u_9} {p : α → Prop} (h : ∀ (x : α), p x) (x : α), (Equiv.subtypeUnivEquiv h).symm x = ⟨x, ⋯⟩
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instNontrivialLeft : ∀ {𝕜 : Type u_3} {A : Type u_4} [Nontrivial 𝕜] [Nonempty A], Nontrivial (Unitization 𝕜 A)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.ofHom_apply : ∀ {X Y : Type u} [inst : Group X] [inst_1 : Finite X] [inst_2 : Group Y] [inst_3 : Finite Y] (f : X →* Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (FiniteGrp.ofHom f)) x = f x
-- Mathlib.Data.List.ModifyLast
_private.Mathlib.Data.List.ModifyLast.0.List.modifyLast.go_concat : ∀ {α : Type u_1} (f : α → α) (a : α) (tl : List α) (r : Array α),
  List.modifyLast.go f (tl ++ [a]) r = r.toListAppend (List.modifyLast.go f (tl ++ [a]) #[])
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.sub : ∀ {𝕜 : 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 𝕜 f → Differentiable 𝕜 g → Differentiable 𝕜 (f - g)
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.Iio_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio ↑a = WithTop.some '' Set.Iio a
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.mk.inj : ∀ {R : Type u_1} {inst : Ring R} {toSubsemiring : Subsemiring R}
  {eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0}
  {toSubsemiring_1 : Subsemiring R}
  {eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → -a ∈ toSubsemiring_1.carrier → a = 0},
  { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem' } =
      { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'_1 } →
    toSubsemiring = toSubsemiring_1
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.weylGroup_apply_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (g : ↥P.weylGroup)
  (i : ι), g • P.root i = P.root ((P.weylGroupToPerm g) i)
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor `(L, F ⋙ R) ⥤ (L, R)`  -/
CategoryTheory.Comma.preRight : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {C : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C] →
                (L : CategoryTheory.Functor A T) →
                  (F : CategoryTheory.Functor C B) →
                    (R : CategoryTheory.Functor B T) →
                      CategoryTheory.Functor (CategoryTheory.Comma L (F.comp R)) (CategoryTheory.Comma L R)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The direction of the affine span of adding a point to a finite-dimensional subspace is
finite-dimensional.  -/
finiteDimensional_direction_affineSpan_insert : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P) [FiniteDimensional k ↥s.direction] (p : P),
  FiniteDimensional k ↥(affineSpan k (insert p ↑s)).direction
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Multiplication on the right by a nonzero element of a normed division ring tends to infinity at
infinity.  -/
Filter.tendsto_mul_right_cobounded : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {a : α},
  a ≠ 0 → Filter.Tendsto (fun x => x * a) (Bornology.cobounded α) (Bornology.cobounded α)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.mk.inj : ∀ {X : Type u_3} {as as_1 : X}, { as := as } = { as := as_1 } → as = as_1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.pairwise_toList_le : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxo.IsAlwaysFinite α],
  List.Pairwise (fun a b => a ≤ b) r.toList
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.lift_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃) (r : R) (x : QuaternionAlgebra R c₁ c₂ c₃), q.lift (r • x) = r • q.lift x
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.subset_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Subsemiring R}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Init.Data.Array.InsertIdx
Array.insertIdx_size_self : ∀ {α : Type u} {xs : Array α} {x : α}, xs.insertIdx xs.size x ⋯ = xs.push x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.liftCycles_comp_cyclesMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} {i : ι} [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j)
  (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (φ : K ⟶ L),
  CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (HomologicalComplex.cyclesMap φ i) =
    L.liftCycles (CategoryTheory.CategoryStruct.comp k (φ.f i)) j hj ⋯
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instDecidableLe : {rel : ℤ → ℤ → Prop} → {a b : ℤ} → {x y : Std.Time.Internal.Bounded rel a b} → Decidable (x ≤ y)
-- Mathlib.Analysis.Convex.StdSimplex
/-- The vertex corresponding to `x : X` in `stdSimplex S X`.  -/
stdSimplex.vertex : {S : Type u_1} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {X : Type u_2} → [inst_2 : Fintype X] → [IsOrderedRing S] → [DecidableEq X] → X → ↑(stdSimplex S X)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of two weighted sums, where the weights in each
sum add to 0, in terms of the norms of pairwise differences.  -/
inner_sum_smul_sum_smul_of_sum_eq_zero : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {ι₁ : Type u_4} {s₁ : Finset ι₁}
  {w₁ : ι₁ → ℝ} (v₁ : ι₁ → F),
  ∑ i ∈ s₁, w₁ i = 0 →
    ∀ {ι₂ : Type u_5} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (v₂ : ι₂ → F),
      ∑ i ∈ s₂, w₂ i = 0 →
        inner ℝ (∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁) (∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂) =
          (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.isoMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g g_1 : f.left ≅ f'.left)
  (e_g : g = g_1) (w : CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom),
  CategoryTheory.CostructuredArrow.isoMk g w = CategoryTheory.CostructuredArrow.isoMk g_1 ⋯
-- Mathlib.Algebra.Category.Ring.Limits
SemiRingCat.sectionsSemiring : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) → Semiring ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.im_neg : ∀ (z : Complex.UnitDisc), (-z).im = -z.im
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.skipped.sizeOf_spec : sizeOf Aesop.SafeRulesResult.skipped = 1
-- Init.Data.String.Iterator
/-- Iterates over a string, updating a state at each character using the provided function `f`, until
`f` returns `none`. Begins with the state `init`. Returns the state and character for which `f`
returns `none`.
 -/
String.Legacy.Iterator.foldUntil : {α : Type u_1} → String.Legacy.Iterator → α → (α → Char → Option α) → α × String.Legacy.Iterator
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
Std.IterM.map_unattach_toList_attachWith : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α m]
  [LawfulMonad m], List.unattach <$> (it.attachWith P hP).toList = it.toList
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.instReprRCasesPatt : Repr Lean.Elab.Tactic.RCases.RCasesPatt
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats : Type
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.Q_apply : ∀ (r : ℝ), CliffordAlgebraComplex.Q r = -(r * r)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_ofVar : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (x : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.ofVar x) = Lean.Grind.CommRing.Var.denote ctx x
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.of_isRestriction : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {N : Matroid α}, N.IsBasis I X → N.IsRestriction M → M.IsBasis I X
-- Mathlib.Order.InitialSeg
InitialSeg.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : InitialSeg r s},
  f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.f'_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {Z : C} (h_1 : h.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.f' (CategoryTheory.CategoryStruct.comp h.π h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_neg : ∀ {α : Type u_1} [inst : Neg α] (a : Colex α), ofColex (-a) = -ofColex a
-- Std.Async.Basic
/-- Converts `IO (IO.Promise α)` to `Async`.
 -/
Std.Async.Async.ofPurePromise : {α : Type} → IO (IO.Promise α) → optParam String "the promise linked to the Async was dropped" → Std.Async.Async α
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Extension for the `positivity` tactic: `p.firstReturn` is positive if `p` is nonzero.  -/
Mathlib.Meta.Positivity.evalDyckWordFirstReturn : Mathlib.Meta.Positivity.PositivityExt
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSliceData.range : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RioSliceData α → Std.Rio α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- If `c` is a limiting binary product cone, and we have a terminal object,
then we have `IsPullback c.fst c.snd 0 0`
(where each `0` is the unique morphism to the terminal object).  -/
CategoryTheory.IsPullback.of_is_product : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {c : CategoryTheory.Limits.BinaryFan X Y}
  (h : CategoryTheory.Limits.IsLimit c) (t : CategoryTheory.Limits.IsTerminal Z),
  CategoryTheory.IsPullback c.fst c.snd
    (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }))
    (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (k : ℕ) (u v : V),
  G.IsEdgeReachable k u v = ∀ ⦃s : Set (Sym2 V)⦄, s.encard < ↑k → (G.deleteEdges s).Reachable u v
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} (self : D₁.Hom D₂)
  (i₁ i₂ : ι) {Z : ↑(F.obj { as := Opposite.op (X i₁) }).obj}
  (h : (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (D₂.obj i₂)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
      (CategoryTheory.CategoryStruct.comp
        ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (self.hom i₂))) h) =
    CategoryTheory.CategoryStruct.comp (self.hom i₁) (CategoryTheory.CategoryStruct.comp (D₂.hom i₁ i₂) h)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, (Std.HashMap.map f m).getKey? k = m.getKey? k
-- Mathlib.Util.Superscript
/-- Map from "normal" text to "special" (e.g. superscript) characters.  -/
Mathlib.Tactic.Superscript.Mapping.toSpecial : Mathlib.Tactic.Superscript.Mapping → Std.HashMap Char Char
-- Mathlib.Topology.Algebra.InfiniteSum.Field
Multipliable.norm : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedCommRing E] [NormMulClass E] [NormOneClass E] {f : α → E},
  Multipliable f → Multipliable fun x => ‖f x‖
-- Init.Data.SInt.Lemmas
Int32.left_eq_add : ∀ {a b : Int32}, a = a + b ↔ b = 0
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.π₀_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.ι K) (HomologicalComplex.pathObject.π₀ K) =
    CategoryTheory.CategoryStruct.id K
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.range_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {s : Set α} (hs : MeasurableSet s),
  s.Nonempty →
    s ≠ Set.univ →
      ∀ (x y : β),
        (MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α x)
              (MeasureTheory.SimpleFunc.const α y)).range =
          {x, y}
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationSingleWeights_apply_of_ne : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] {i j : ι},
  j ≠ i → Finset.affineCombinationSingleWeights k i j = 0
-- Batteries.Data.List.Scan
List.partialProds_nil : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α], [].partialProds = [1]
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorph_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  ↑e.toPartialHomeomorph = ⇑e
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isValidEq.eq_2 : ∀ (p : Int.Internal.Linear.Poly), (∀ (k : ℤ), p = Int.Internal.Linear.Poly.num k → False) → p.isValidEq = false
-- Lean.Server.FileWorker.Utils
/-- Amount of diagnostics reported in `publishDiagnostics` so far.  -/
Lean.Server.FileWorker.DiagnosticsState.publishedDiagsAmount : Lean.Server.FileWorker.DiagnosticsState → ℕ
-- Init.Data.Range.Polymorphic.NatLemmas
List.range_eq_toList_rco : ∀ {n : ℕ}, List.range n = (0...n).toList
-- Mathlib.Data.PNat.Xgcd
/-- `r = a % b`: remainder  -/
PNat.XgcdType.r : PNat.XgcdType → ℕ
-- Lean.Elab.PreDefinition.WF.Unfold
_private.Lean.Elab.PreDefinition.WF.Unfold.0.Lean.Elab.WF.mkUnfoldProof : Lean.Name → Lean.MVarId → Lean.MetaM Unit