mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toList_eq_match_rcc : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.succ? r.lower with
    | none => []
    | some next => (next...=r.upper).toList
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of a set of points in a projective space is equal to the infimum of the collection of
subspaces which contain the set.  -/
Projectivization.Subspace.span_eq_sInf : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)}, Projectivization.Subspace.span S = sInf {W | S ⊆ ↑W}
-- Mathlib.Algebra.BigOperators.Finprod
hasFiniteSupport_of_finsum_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M}, ∑ᶠ (i : α), f i ≠ 0 → Function.HasFiniteSupport f
-- Mathlib.Data.Nat.Digits.Defs
/-- The core implementation of `Nat.repr` returns a String with length less than or equal to the
number of digits in the decimal number (represented by `e`). For example, the decimal string
representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3.  -/
Nat.repr_length : ∀ (n e : ℕ), 0 < e → n < 10 ^ e → n.repr.length ≤ e
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqJoinPointId.beq : Lean.IR.JoinPointId → Lean.IR.JoinPointId → Bool
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
instCategorySimplexCategoryGenRel : CategoryTheory.Category.{0, 0} SimplexCategoryGenRel
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The sheaf `sheaf data G₀` extends `G₀`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.sheafIso : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        (G₀ : CategoryTheory.Sheaf J₀ A) →
                          (F.sheafPushforwardContinuous A J₀ J).obj
                              (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.sheaf data G₀) ≅
                            G₀
-- Mathlib.NumberTheory.SelbergSieve
/-- The weight of all the elements that are a multiple of `d`.  -/
BoundingSieve.multSum : {s : BoundingSieve} → ℕ → ℝ
-- Mathlib.CategoryTheory.Galois.Basic
/-- `C` has quotients by finite groups (G2).  -/
CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.PreGaloisCategory C] (G : Type u₂)
  [inst_1 : Group G] [Finite G], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_asympBound_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∀ᶠ (n : ℕ) in Filter.atTop, 0 < AkraBazziRecurrence.asympBound g a b n
-- Mathlib.RingTheory.Multiplicity
emultiplicity_sub_of_gt : ∀ {α : Type u_1} [inst : Ring α] {p a b : α},
  emultiplicity p b < emultiplicity p a → emultiplicity p (a - b) = emultiplicity p b
-- Mathlib.Data.List.TakeDrop
List.take_self_eq_iff : ∀ {α : Type u} (x : List α) {n : ℕ}, x = List.take n x ↔ x.length ≤ n
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The distance is symmetric.

This holds independent of `p` and does not require `[Fact (1 ≤ p)]`. We keep it separate
from `WithLp.instProdPseudoEMetricSpace` so it can be used also for `p < 1`.  -/
WithLp.prod_edist_comm : ∀ (p : ENNReal) {α : Type u_2} {β : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  (f g : WithLp p (α × β)), edist f g = edist g f
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.bcount.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)] (p : { a // Irreducible a }),
  Associates.bcount p none = 0
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.union : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  Topology.IsLocallyConstructible s → Topology.IsLocallyConstructible t → Topology.IsLocallyConstructible (s ∪ t)
-- Init.Data.String.Defs
/-- Returns the byte at a position in a slice that is not the end position.  -/
String.Slice.Pos.byte : {s : String.Slice} → (pos : s.Pos) → pos ≠ s.endPos → UInt8
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s t : Set Ω} {_m0 : MeasurableSpace Ω},
  MeasurableSet s →
    MeasurableSet t →
      ∀ (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
        ProbabilityTheory.Kernel.IndepSet s t κ μ ↔ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
-- Init.Data.Int.DivMod.Lemmas
Int.eq_zero_of_fdiv_eq_zero : ∀ {d n : ℤ}, d ∣ n → n.fdiv d = 0 → n = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConstC.induct_unfolding : ∀ (k : ℤ) (c : ℕ) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k_1 : ℤ), motive (Lean.Grind.CommRing.Poly.num k_1) (Lean.Grind.CommRing.Poly.num ((k_1 + k) % ↑c))) →
    (∀ (k_1 : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (p.addConstC k c) →
          motive (Lean.Grind.CommRing.Poly.add k_1 m p) (Lean.Grind.CommRing.Poly.add k_1 m (p.addConstC k c))) →
      ∀ (p : Lean.Grind.CommRing.Poly), motive p (p.addConstC k c)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_pow : ∀ {R : Type u} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Submonoid R}
  (n : ℕ) (a : A) (s : ↥S), LocalizedModule.mk a s ^ n = LocalizedModule.mk (a ^ n) (s ^ n)
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_inter_Ioc_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ c → Set.Iic a ∩ Set.Ioc b c = Set.Ioc b a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.reduceNatOp : Lean.Name → ℕ → (f : ℕ → ℕ) → ((n : ℕ) → Fin (f n)) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Analysis.Fourier.Notation
/-- A `FourierPair` is a pair of spaces `E` and `F` such that `𝓕⁻ ∘ 𝓕 = id` on `E`.  -/
FourierPair : (E : Type u_5) → (F : Type u_6) → [FourierTransform E F] → [FourierTransformInv F E] → Prop
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- If a map `f : α → β` sends any two distinct points to point that are **not** related by a fixed
`s ∈ 𝓤 β`, then `f` is a uniform embedding with respect to the discrete uniformity on `α`.  -/
isUniformEmbedding_of_spaced_out : ∀ {β : Type v} [inst : UniformSpace β] {α : Type u_1} {f : α → β} {s : Set (β × β)},
  s ∈ uniformity β → (Pairwise fun x y => (f x, f y) ∉ s) → IsUniformEmbedding f
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.toLp_coeFn : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)) (hf : MeasureTheory.MemLp (↑↑f) p μ),
  MeasureTheory.MemLp.toLp (↑↑f) hf = f
-- Std.Do.PostCond
Std.Do.ExceptConds.snd_imp : ∀ {ps : Std.Do.PostShape} {ε : Type u} {x₁ x₂ : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)},
  (x₁ →ₑ x₂).2 = (x₁.2 →ₑ x₂.2)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryObjProdComp_hom_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2}
  [inst_3 : CategoryTheory.Category.{v_1, u_1} C'] [inst_4 : CategoryTheory.Category.{v_2, u_2} D']
  (F₁ : CategoryTheory.Functor C D) (F₂ : CategoryTheory.Functor C' D') (G : CategoryTheory.Functor (D × D') E) (X : C)
  (X_1 : C'),
  ((F₁.curryObjProdComp F₂ G).hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X_1))
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.mul_nc_NonnegCoeffs : ∀ {p₁ p₂ : Lean.Grind.CommRing.Poly}, p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.mul_nc p₂).NonnegCoeffs
-- Mathlib.Order.CompleteBooleanAlgebra
himp_le_iff : ∀ {α : Type u} [inst : Order.Frame α] {a b c : α}, a ⇨ b ≤ c ↔ ∀ (d : α), d ⊓ a ≤ b → d ≤ c
-- Mathlib.Lean.Name
_private.Mathlib.Lean.Name.0.Lean.Name.willRoundTrip.go : Lean.Name → Bool
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by adding a constant value to both the lower and upper bounds.
 -/
Std.Time.Internal.Bounded.LE.add : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → (num : ℤ) → Std.Time.Internal.Bounded.LE (n + num) (m + num)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_ε_η_assoc : ∀ {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] {C' : Type u₁'}
  [inst_4 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal]
  (G : CategoryTheory.Functor D C') {Z : C'} (h : G.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.η F)) h) =
    h
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchTypeAndDiscrs : Array Lean.Syntax →
  Lean.Syntax →
    Array Lean.Elab.Term.TermMatchAltView → Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Term.ElabMatchTypeAndDiscrsResult
-- Mathlib.Topology.MetricSpace.Gluing
Metric.instMetricSpaceGlueSpace : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : Nonempty Z] →
        [inst_1 : MetricSpace Z] →
          [inst_2 : MetricSpace X] →
            [inst_3 : MetricSpace Y] →
              {Φ : Z → X} → {Ψ : Z → Y} → (hΦ : Isometry Φ) → (hΨ : Isometry Ψ) → MetricSpace (Metric.GlueSpace hΦ hΨ)
-- Mathlib.Logic.Equiv.Fin.Basic
finSumFinEquiv_apply_right : ∀ {m n : ℕ} (i : Fin n), finSumFinEquiv (Sum.inr i) = Fin.natAdd m i
-- Init.Data.Int.Order
Int.le_total : ∀ (a b : ℤ), a ≤ b ∨ b ≤ a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
one_le_of_le_mul_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulRightReflectLE α] {a b : α}, b ≤ a * b → 1 ≤ a
-- Mathlib.Analysis.Convex.Intrinsic
/-- The intrinsic frontier of a set is its frontier considered as a set in its affine span.  -/
intrinsicFrontier : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring 𝕜] →
        [inst_1 : AddCommGroup V] → [Module 𝕜 V] → [TopologicalSpace P] → [AddTorsor V P] → Set P → Set P
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.instIsEquivalenceMonoOverRepresentative : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
  CategoryTheory.Subobject.representative.IsEquivalence
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDerivWithin_sum_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {ι : Type u_3} {f : ι → E → F} {u : Finset ι} {i : ℕ} {x : E},
  UniqueDiffOn 𝕜 s →
    x ∈ s →
      (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
        iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
-- Mathlib.Data.NNReal.Basic
NNReal.coe_prod : ∀ {ι : Type u_2} (s : Finset ι) (f : ι → NNReal), ↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- Constructor for `Type₁ k n`.  -/
SSet.prodStdSimplex.pairingCore.IsIndex.type₁ : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} →
        {d : ℕ} →
          {hd : x.dim = d + 1} →
            {i : Fin (d + 1)} →
              SSet.prodStdSimplex.pairingCore.IsIndex x hd i.succ → SSet.prodStdSimplex.pairingCore.Type₁ k n
-- Std.Data.DTreeMap.Internal.Balancing
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.«term✓» : Lean.ParserDescr
-- Init.Data.List.Lemmas
List.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u_1} {xs : List α}, xs.isEmpty = false ↔ ∃ x, x ∈ xs
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_const : ∀ (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (p : P2), ⇑(AffineMap.const k P1 p) = Function.const P1 p
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_ne_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R} {m : M}, AddMonoidAlgebra.single m r ≠ 0 ↔ r ≠ 0
-- Std.Do.SPred.SVal
Std.Do.SVal.curry.eq_1 : ∀ {α : Type u} (f_2 : Std.Do.SVal.StateTuple [] → α), Std.Do.SVal.curry f_2 = f_2 PUnit.unit
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.Measure.isProbabilityMeasure_of_map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : α → β) [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ)], MeasureTheory.IsProbabilityMeasure μ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.diff_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp}, t₁.diff t₂ = t₁ \ t₂
-- Init.Data.Bool
Bool.cond_false : ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
addCommGroupOfAddCyclicCenterQuotient.eq_1 : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] [inst_2 : IsAddCyclic G'] (f : G →+ G')
  (hf : f.ker ≤ AddSubgroup.center G),
  addCommGroupOfAddCyclicCenterQuotient f hf = { toAddGroup := inst, add_comm := ⋯ }
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.IicSnd_univ : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ),
  (ρ.IicSnd r) Set.univ = ρ (Set.univ ×ˢ Set.Iic r)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.eval_homogenize : ∀ {K : Type u_1} [inst : Semifield K] {p : Polynomial K} {n : ℕ},
  p.natDegree ≤ n →
    ∀ (x : Fin 2 → K), x 1 ≠ 0 → (MvPolynomial.eval x) (p.homogenize n) = Polynomial.eval (x 0 / x 1) p * x 1 ^ n
-- Mathlib.Algebra.GroupWithZero.Hom
/-- Composition of `MonoidWithZeroHom`s as a `MonoidWithZeroHom`.  -/
MonoidWithZeroHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : MulZeroOneClass α] →
        [inst_1 : MulZeroOneClass β] → [inst_2 : MulZeroOneClass γ] → (β →*₀ γ) → (α →*₀ β) → α →*₀ γ
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix.eq_1 : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] (f : m ≃. n),
  f.toMatrix = Matrix.of fun i j => if j ∈ f i then 1 else 0
-- Mathlib.MeasureTheory.SetSemiring
/-- In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`,
`disjointOfDiffUnion` is a finite set of sets in `C` such that
`s \ ⋃₀ I = ⋃₀ (hC.disjointOfDiffUnion hs I hI)`.
`disjointOfDiff` is a special case of `disjointOfDiffUnion` where `I` is a
singleton.  -/
MeasureTheory.IsSetSemiring.disjointOfDiffUnion : {α : Type u_1} →
  {C : Set (Set α)} →
    {s : Set α} → {I : Finset (Set α)} → MeasureTheory.IsSetSemiring C → s ∈ C → ↑I ⊆ C → Finset (Set α)
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.const_eq_zero : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [Nonempty ι] {a : α}, Function.const ι a = 0 ↔ a = 0
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The function `HomotopyCategory₂.mk` taking a vertex of `A` and sending it to the corresponding
object of `HomotopyCategory₂ A` is surjective.
 -/
SSet.Truncated.HomotopyCategory₂.mk_surjective : ∀ {A : SSet.Truncated 2}, Function.Surjective SSet.Truncated.HomotopyCategory₂.mk
-- Mathlib.Analysis.InnerProductSpace.Trace
LinearMap.trace_eq_sum_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype ι] [inst_2 : NormedAddCommGroup E]
  [inst_3 : InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) (b : OrthonormalBasis ι 𝕜 E),
  (LinearMap.trace 𝕜 E) T = ∑ i, inner 𝕜 (b i) (T (b i))
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ofList_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  Std.ExtHashSet.ofList l = ∅ ↔ l = []
-- Mathlib.Topology.Order.LeftRightNhds
nhds_basis_one_mabs_lt : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α]
  [OrderTopology α] [NoMaxOrder α], (nhds 1).HasBasis (fun ε => 1 < ε) fun ε => {b | |b|ₘ < ε}
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zsmul_empty : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {n : ℤ}, n ≠ 0 → n • ∅ = ∅
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_lt : ∀ {a b : Cardinal.{u}}, Cardinal.lift.{v, u} a < Cardinal.lift.{v, u} b ↔ a < b
-- Mathlib.Data.NNRat.Floor
/-- `norm_num` extension for `Nat.ceil`  -/
Mathlib.Meta.NormNum.evalNatCeil : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryMidLinearEquiv_symm_apply : ∀ (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (p : Fin (n + 1))
  (f : M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂),
  (MultilinearMap.curryMidLinearEquiv R M M₂ p).symm f = LinearMap.uncurryMid p f
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoLeftHomology.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hf : S.f = 0),
  S.cyclesIsoLeftHomology hf = S.cyclesIsoLeftHomology hf
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.optionalNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRoiSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRoiSlice._auto_1) →
      Std.Roi.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RoiSlice α β)
-- Lean.Parser.Types
Lean.Parser.ParserInfo : Type
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.iso_apply_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M) (s : ↥S),
  (IsLocalizedModule.iso S f) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_snd_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀)
  {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.glueDataT'Aux U V W U₀ hU₀)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯))
        (CategoryTheory.CategoryStruct.comp (↑V ⊓ ↑U₀).ι h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))
        (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))
        (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (CategoryTheory.CategoryStruct.comp (↑U).ι h)))
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.span_iUnion : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {ι : Sort u_1}
  (s : ι → Set L), LieSubalgebra.lieSpan R L (⋃ i, s i) = ⨆ i, LieSubalgebra.lieSpan R L (s i)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.cancel_left : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : DecidableEq ι] [inst_8 : AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B}
  {𝒞 : ι → Submodule R C} [inst_9 : GradedAlgebra 𝒜] [inst_10 : GradedAlgebra ℬ] [inst_11 : GradedAlgebra 𝒞]
  {g₁ g₂ : 𝒜 →ₐᵍ[R] ℬ} {f : ℬ →ₐᵍ[R] 𝒞}, Function.Injective ⇑f → (f.comp g₁ = f.comp g₂ ↔ g₁ = g₂)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The sieves associated to each object must contain the top sieve.
Use `GrothendieckTopology.top_mem`.  -/
CategoryTheory.GrothendieckTopology.top_mem' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) (X : C),
  ⊤ ∈ self.sieves X
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.iterate_surjective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f' : Module.End R M}, Function.Surjective ⇑f' → ∀ (n : ℕ), Function.Surjective ⇑(f' ^ n)
-- Mathlib.Analysis.RCLike.Basic
_private.Mathlib.Analysis.RCLike.Basic.0.RCLike.termReR : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.endsWith_char_eq_getLast? : ∀ {c : Char} {s : String.Slice}, s.endsWith c = (s.copy.toList.getLast? == some c)
-- Batteries.Data.List.Lemmas
List.countPBefore_zero : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.countPBefore p xs 0 = 0
-- Init.System.IO
_private.Init.System.IO.0.IO.eprintAux : String → IO Unit
-- Mathlib.Topology.Separation.Basic
t0Space_iff_not_inseparable : ∀ (X : Type u) [inst : TopologicalSpace X], T0Space X ↔ Pairwise fun x y => ¬Inseparable x y
-- Batteries.Data.List.Basic
List.swapTR.go.eq_1 : ∀ {α : Type u_1} (l : List α) (a a_1 : ℕ) (a_2 : Array α), List.swapTR.go l [] a a_1 a_2 = l
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Internal.ext_iff : ∀ {α : Type u_1} {f1 f2 : Std.Sat.CNF α}, f1 = f2 ↔ f1.clauses = f2.clauses
-- Mathlib.Algebra.Order.Group.Synonym
isAddRegular_ofLex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : Lex α}, IsAddRegular (ofLex a) ↔ IsAddRegular a
-- Batteries.Data.UInt
UInt64.ext : ∀ {x y : UInt64}, x.toNat = y.toNat → x = y
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.vInv_iso_inv_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [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₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄)
  (B : CategoryTheory.Functor C₃ C₄) (x : CategoryTheory.CatCommSq T L.functor R.functor B) (X : C₃),
  (CategoryTheory.CatCommSq.iso B L.inverse R.inverse T).inv.app X =
    CategoryTheory.CategoryStruct.comp (R.unitIso.hom.app (T.obj (L.inverse.obj X)))
      (CategoryTheory.CategoryStruct.comp
        (R.inverse.map ((CategoryTheory.CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj X)))
        (R.inverse.map (B.map (L.counitIso.hom.app X))))
-- Lean.Data.KVMap
Lean.KVMap.instForInProdNameDataValueOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.KVMap (Lean.Name × Lean.DataValue)