mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Presheaf
/-- The morphism of sheaves of rings corresponding to a morphism of schemes.  -/
AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    Y.ringCatSheaf ⟶
      ((TopologicalSpace.Opens.map f.base).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥Y)
            (Opens.grothendieckTopology ↥X)).obj
        X.ringCatSheaf
-- Init.Data.List.Basic
/-- Alternates the elements of `l` with `sep`.

`O(|l|)`.

`List.intercalate` is a similar function that alternates a separator list with elements of a list of
lists.

Examples:
* `List.intersperse "then" [] = []`
* `List.intersperse "then" ["walk"] = ["walk"]`
* `List.intersperse "then" ["walk", "run"] = ["walk", "then", "run"]`
* `List.intersperse "then" ["walk", "run", "rest"] = ["walk", "then", "run", "then", "rest"]`
 -/
List.intersperse : {α : Type u} → α → List α → List α
-- Lean.Message
Lean.instToMessageDataName : Lean.ToMessageData Lean.Name
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.cancelByCancelRequest : Lean.Server.RequestCancellationToken → BaseIO Unit
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.exists_of_isUnit_sum : ∀ {R : Type u_1} [inst : Semiring R] [IsLocalRing R] {ι : Type u_3} {s : Finset ι} {f : ι → R},
  IsUnit (∑ i ∈ s, f i) → ∃ i ∈ s, IsUnit (f i)
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
AlgebraicTopology.DoldKan.hσ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q n : ℕ),
  AlgebraicTopology.DoldKan.hσ q n = if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩
-- Mathlib.Order.Cover
/-- A characterisation of the `WCovBy` relation in products of preorders. See `Pi.wcovBy_iff` for the
(more common) version in products of partial orders.
 -/
Pi.wcovBy_iff_antisymmRel : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] {a b : (i : ι) → α i} [Nonempty ι],
  a ⩿ b ↔ ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 => x1 ≤ x2) (a j) (b j)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesToE.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂), X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.constantsOn_Relations : ∀ (α : Type u') (x : ℕ), (FirstOrder.Language.constantsOn α).Relations x = Empty
-- Mathlib.Topology.Order.OrderClosed
le_of_tendsto_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {f g : β → α}
  {b : Filter β} {a₁ a₂ : α} [hb : b.NeBot],
  Filter.Tendsto f b (nhds a₁) → Filter.Tendsto g b (nhds a₂) → f ≤ᶠ[b] g → a₁ ≤ a₂
-- Mathlib.RingTheory.Polynomial.Selmer
Polynomial.X_pow_sub_X_sub_one_irreducible_aux : ∀ {n : ℕ} (z : ℂ), ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.instAddCommMonoidAEval : (R : Type u_2) →
  (M : Type u_1) →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] → [inst_6 : IsScalarTower R A M] → (x : A) → AddCommMonoid (Module.AEval R M x)
-- Init.Grind.Lemmas
Lean.Grind.Nat.or_congr : ∀ {a b k₁ k₂ k : ℕ}, a = k₁ → b = k₂ → (k == k₁ ||| k₂) = true → a ||| b = k
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.homEquivOfIsLeftKanExtension.congr_simp : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α α_1 : F ⟶ L.comp F') (e_α : α = α_1) [inst_3 : F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H),
  F'.homEquivOfIsLeftKanExtension α G = F'.homEquivOfIsLeftKanExtension α_1 G
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `FunLike.coe_neg`. -/
QuadraticMap.coeFn_neg : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isDetector_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : Cᵒᵖ),
  CategoryTheory.IsDetector (Opposite.unop G) ↔ CategoryTheory.IsCodetector G
-- Mathlib.Computability.Primrec.Basic
Primrec.comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : γ → σ} {g : α → β → γ},
  Primrec f → Primrec₂ g → Primrec₂ fun a b => f (g a b)
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.val_unitsLift_apply_apply : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : Monoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousMul M] (f : C(X, Mˣ)) (x : X), ↑(ContinuousMap.unitsLift f) x = ↑(f x)
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
/-- If `X` is geometrically irreducible and universally open over `S` and `Y` is irreducible,
then `X ×ₛ Y` is irreducible.

The universally open assumption in particular holds when it is flat and locally of finite
presentation, or when `S` is a field.  -/
AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyIrreducible f]
  [AlgebraicGeometry.UniversallyOpen f] [IrreducibleSpace ↥Y], IrreducibleSpace ↥(CategoryTheory.Limits.pullback f g)
-- Init.Data.String.Basic
String.Slice.Pos.offset_le_offset_str : ∀ {s : String.Slice} {pos : s.Pos}, pos.offset ≤ pos.str.offset
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.transitive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C} (X : C)
  (S R : CategoryTheory.Sieve X),
  J.Saturate X S →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (CategoryTheory.Sieve.pullback f R)) → J.Saturate X R
-- Mathlib.Data.WSeq.Defs
/-- Remove the `n`th element of `s`.  -/
Stream'.WSeq.removeNth : {α : Type u} → Stream'.WSeq α → ℕ → Stream'.WSeq α
-- Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FieldSimp.DenomCondition.nonzero.sizeOf_spec : ∀ {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)},
  sizeOf Mathlib.Tactic.FieldSimp.DenomCondition.nonzero = 1
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- To prove something for an arbitrary `MemLp` function a.e. strongly measurable with respect
to a sub-σ-algebra `m` in a normed space, it suffices to show that
* the property holds for (multiples of) characteristic functions which are measurable w.r.t. `m`;
* is closed under addition;
* the set of functions in the `Lᵖ` space strongly measurable w.r.t. `m` for which the property
  holds is closed.
* the property is closed under the almost-everywhere equal relation.
 -/
MeasureTheory.MemLp.induction_stronglyMeasurable : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : Fact (1 ≤ p)] [inst_2 : NormedSpace ℝ F],
  m ≤ m0 →
    p ≠ ⊤ →
      ∀ (P : (α → F) → Prop),
        (∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)) →
          (∀ ⦃f g : α → F⦄,
              Disjoint (Function.support f) (Function.support g) →
                MeasureTheory.MemLp f p μ →
                  MeasureTheory.MemLp g p μ →
                    MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → P f → P g → P (f + g)) →
            IsClosed {f | P ↑↑↑f} →
              (∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MeasureTheory.MemLp f p μ → P f → P g) →
                ∀ ⦃f : α → F⦄, MeasureTheory.MemLp f p μ → MeasureTheory.AEStronglyMeasurable f μ → P f
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.HeightOneSpectrum.adicAbv_def : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] {x : K},
  (NumberField.HeightOneSpectrum.adicAbv K v) x =
    ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))
-- Mathlib.NumberTheory.Ostrowski
_private.Mathlib.NumberTheory.Ostrowski.0.Rat.AbsoluteValue.expr_pos : ∀ {f : AbsoluteValue ℚ ℝ} {m : ℕ}, 1 < m → (¬∀ (n : ℕ), f ↑n ≤ 1) → 0 < ↑m * f ↑m / (f ↑m - 1)
-- Init.Data.Vector.Zip
Vector.zipWith_map_right : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} {as : Vector α n} {bs : Vector β n} {f : β → β'}
  {g : α → β' → γ}, Vector.zipWith g as (Vector.map f bs) = Vector.zipWith (fun a b => g a (f b)) as bs
-- Std.Time.Time.PlainTime
/-- Creates a `PlainTime` value from a total number of hours.
 -/
Std.Time.PlainTime.ofHours : Std.Time.Hour.Offset → Std.Time.PlainTime
-- Mathlib.Data.Set.Card.Arithmetic
Set.ncard_iUnion_le_of_fintype : ∀ {α : Type u_1} {ι : Type u_2} [inst : Fintype ι] (s : ι → Set α), (⋃ i, s i).ncard ≤ ∑ i, (s i).ncard
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- Let `u` be a unit in `(𝓞 K)ˣ`, then `u ∈ [1, -1, η, -η, η^2, -η^2]`.  -/
IsCyclotomicExtension.Rat.Three.Units.mem : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (u : (NumberField.RingOfIntegers K)ˣ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K], u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.symm_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A), P.symm.i₁ = P.i₀
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.LaxTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (F.obj a)) (self.app a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).inv h))
-- Mathlib.Data.Set.NAry
Set.image2_congr : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f f' : α → β → γ} {s : Set α} {t : Set β},
  (∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) → Set.image2 f s t = Set.image2 f' s t
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- The functor `(C₁ ⥤ C₂ ⥤ C₁₂) ⥤ (C₁₂ ⥤ C₃ ⥤ C₄) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` which
sends `F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂` and `G : C₁₂ ⥤ C₃ ⥤ C₄` to the functor
`bifunctorComp₁₂ F₁₂ G : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄`.  -/
CategoryTheory.bifunctorComp₁₂Functor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [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} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    CategoryTheory.Functor (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
                      (CategoryTheory.Functor (CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄))
                        (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))))
-- Mathlib.Data.Sigma.Order
/-- Disjoint sum of orders. `⟨i, a⟩ < ⟨j, b⟩` iff `i = j` and `a < b`.  -/
Sigma.LT : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → LT (α i)] → (i : ι) × α i → (i : ι) × α i → Prop
-- Mathlib.Tactic.GCongr.Core
/-- Index of the left varying argument.  -/
Mathlib.Tactic.GCongr.GCongrHyp.lhsIdx : Mathlib.Tactic.GCongr.GCongrHyp → ℕ
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  α ≠ 0 → LieModule.genWeightSpace M ((LieModule.chainTopCoeff α β + 1) • α + ⇑β) = ⊥
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendId_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F),
  s.extendId.hom.hom = CategoryTheory.CategoryStruct.id s.pt
-- Mathlib.RingTheory.Localization.Algebra
IsLocalization.ker_map : ∀ {R : Type u_1} {S : Type u_2} {P : Type u_3} (Q : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring P] [inst_3 : CommSemiring Q] {M : Submonoid R} {T : Submonoid P} [inst_4 : Algebra R S]
  [inst_5 : Algebra P Q] [inst_6 : IsLocalization M S] [inst_7 : IsLocalization T Q] (g : R →+* P)
  (hT : Submonoid.map g M = T), RingHom.ker (IsLocalization.map Q g ⋯) = Ideal.map (algebraMap R S) (RingHom.ker g)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.span_eq_rootSpan_int : ∀ {ι : 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} [P.IsG2] {b : P.Base}
  [Finite ι] [CharZero R] [IsDomain R] {i j : ι},
  i ∈ b.support → j ∈ b.support → i ≠ j → Submodule.span ℤ {P.root i, P.root j} = P.rootSpan ℤ
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_hadamard_ofNat : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] [inst_3 : NatCast α] (a : ℕ) [inst_4 : a.AtLeastTwo],
  (SimpleGraph.adjMatrix α G).hadamard (OfNat.ofNat a) = 0
-- Mathlib.CategoryTheory.Yoneda
/-- Unification hint for `(coyoneda.obj (op X)).obj Y = X ⟶ Y`.  -/
CategoryTheory.coyoneda_obj_obj_eq_hom : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → C → C → C → Prop
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- Algebra homomorphism from the tensor algebra over `M` to the symmetric algebra over `M`.  -/
SymmetricAlgebra.algHom : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorAlgebra R M →ₐ[R] SymmetricAlgebra R M
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_succ : ∀ {w acc n : ℕ} {x : BitVec w}, x.cpopNatRec (n + 1) acc = x.cpopNatRec n (acc + (x.getLsbD n).toNat)
-- Mathlib.Analysis.Fourier.LpSpace
SchwartzMap.toLp_fourier_eq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E] (f : SchwartzMap E F),
  FourierTransform.fourier (f.toLp 2 MeasureTheory.volume) = (FourierTransform.fourier f).toLp 2 MeasureTheory.volume
-- Mathlib.Algebra.Module.Torsion.Basic
Module.instQuotientIdealSpanSingletonSetSubmoduleHSMulTop : {R : Type u_1} →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (r : R) → Module (R ⧸ Ideal.span {r}) (M ⧸ r • ⊤)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.one_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : One β] (x : α),
  1 x = 1
-- Mathlib.Logic.Function.Iterate
Function.Semiconj₂.iterate : ∀ {α : Type u} {f : α → α} {op : α → α → α}, Function.Semiconj₂ f op op → ∀ (n : ℕ), Function.Semiconj₂ f^[n] op op
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.modification.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.modification = 1
-- Mathlib.NumberTheory.LSeries.PrimesInAP
ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one : ∀ {q : ℕ} (a : ZMod q), (LSeries.abscissaOfAbsConv fun n => ↑(ArithmeticFunction.vonMangoldt.residueClass a n)) ≤ 1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNthEquiv_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)),
  (Fin.insertNthEquiv α p) f j = p.insertNth f.1 f.2 j
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.mul_star_self_eq_zero_iff : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] (x : E), x * star x = 0 ↔ x = 0
-- Init.System.IO
/-- Waits for the task to finish, then returns its result.
 -/
IO.wait : {α : Type} → Task α → BaseIO α
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_faceOpposite : ∀ {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 : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → ∀ (i : Fin (n + 1)), s.excenter signs ∉ affineSpan ℝ (Set.range (s.faceOpposite i).points)
-- Init.Prelude
/-- Returns the element at the provided index, counting from `0`.

In other words, for `i : Fin as.length`, `as.get i` returns the `i`'th element of the list `as`.
Because the index is a `Fin` bounded by the list's length, the index will never be out of bounds.

Examples:
 * `["spring", "summer", "fall", "winter"].get (2 : Fin 4) = "fall"`
 * `["spring", "summer", "fall", "winter"].get (0 : Fin 4) = "spring"`
 -/
List.get : {α : Type u} → (as : List α) → Fin as.length → α
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme_toLocallyRingedSpace : ∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f).toLocallyRingedSpace =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y.toLocallyRingedSpace f
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.homeomorph_symm : ∀ (x : ↑TopCat.I),
  TopCat.I.homeomorph ((CategoryTheory.ConcreteCategory.hom TopCat.I.symm) x) =
    unitInterval.symm (TopCat.I.homeomorph x)
-- Std.Http.Internal.Char
/-- OWS = *( SP / HTAB )  (character class only)
 -/
Std.Http.Internal.Char.ows : Char → Bool
-- Init.Prelude
Pure.mk : {f : Type u → Type v} → ({α : Type u} → α → f α) → Pure f
-- Mathlib.Data.Set.Lattice
Set.mem_iUnion₂_of_mem : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {a : α} {i : ι} (j : κ i),
  a ∈ s i j → a ∈ ⋃ i, ⋃ j, s i j
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.map_id : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  (Q₁ : QuadraticForm R M₁), CliffordAlgebra.map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)
-- Mathlib.LinearAlgebra.Ray
SameRay.zero_right : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (x : M), SameRay R x 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonColorInformation.toJson : Lean.Lsp.ColorInformation → Lean.Json
-- Lean.Attributes
Lean.mkAttributeImplOfConstantUnsafe : Lean.Environment → Lean.Options → Lean.Name → Except String Lean.AttributeImpl
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.oneMul_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n),
  (SSet.PtSimplex.MulStruct.oneMul f i).map = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.σ i.castSucc) f.map
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree.eq_1 : ∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.withBotDegree f = WithBot.map (⇑m.toSyn.symm) (Finset.image (⇑m.toSyn) f.support).max
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.piRingEquiv.eq_1 : ∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : Fintype ι],
  MultilinearMap.piRingEquiv =
    { toFun := fun z => MultilinearMap.mkPiRing R ι z, map_add' := ⋯, map_smul' := ⋯, invFun := fun f => f fun x => 1,
      left_inv := ⋯, right_inv := ⋯ }
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.instBEqEMatchTheoremPtr : BEq Lean.Meta.Grind.EMatchTheoremPtr
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- An unrolled version of the induction principle obtained in the previous lemma.  -/
SimplexCategoryGenRel.hom_induction : ∀ (P : CategoryTheory.MorphismProperty SimplexCategoryGenRel),
  (∀ {n : ℕ}, P (CategoryTheory.CategoryStruct.id (SimplexCategoryGenRel.mk n))) →
    (∀ {n m : ℕ} (u : SimplexCategoryGenRel.mk n ⟶ SimplexCategoryGenRel.mk m) (i : Fin (m + 2)),
        P u → P (CategoryTheory.CategoryStruct.comp u (SimplexCategoryGenRel.δ i))) →
      (∀ {n m : ℕ} (u : SimplexCategoryGenRel.mk n ⟶ SimplexCategoryGenRel.mk (m + 1)) (i : Fin (m + 1)),
          P u → P (CategoryTheory.CategoryStruct.comp u (SimplexCategoryGenRel.σ i))) →
        ∀ {a b : SimplexCategoryGenRel} (f : a ⟶ b), P f
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.Small.mk : ∀ {α : Type v}, Nonempty (Std.Internal.ComputableSmall α) → Std.Internal.Small α
-- Mathlib.Analysis.Convex.Strict
StrictConvex.sub : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s t : Set E} [IsTopologicalAddGroup E],
  StrictConvex 𝕜 s → StrictConvex 𝕜 t → StrictConvex 𝕜 (s - t)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {E : Type u₃}
  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] [inst_7 : CategoryTheory.MonoidalCategory E]
  [inst_8 : CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E}
  [inst_9 : F.LaxBraided] [inst_10 : G.LaxBraided] (X : CategoryTheory.CommMon C),
  (CategoryTheory.Functor.mapCommMonCompIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.sub_one_mul_conj : ∀ {p q : NNReal}, p.HolderConjugate q → (p - 1) * q = p