mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- In an ordered additive commutative monoid, if each summand `f i` of one nontrivial finite sum is
strictly less than the corresponding summand `g i` of another nontrivial finite sum, then
`s.sum f < s.sum g`.  -/
Finset.sum_lt_sum_of_nonempty : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {f g : ι → M} {s : Finset ι} [AddLeftStrictMono M], s.Nonempty → (∀ i ∈ s, f i < g i) → ∑ i ∈ s, f i < ∑ i ∈ s, g i
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback
-- Lean.Class
Lean.ClassState.mk.injEq : ∀ (outParamMap outLevelParamMap outParamMap_1 outLevelParamMap_1 : Lean.SMap Lean.Name (Array ℕ)),
  ({ outParamMap := outParamMap, outLevelParamMap := outLevelParamMap } =
      { outParamMap := outParamMap_1, outLevelParamMap := outLevelParamMap_1 }) =
    (outParamMap = outParamMap_1 ∧ outLevelParamMap = outLevelParamMap_1)
-- Mathlib.Data.Ineq
Mathlib.Ineq.ofNat_ctorIdx : ∀ (x : Mathlib.Ineq), Mathlib.Ineq.ofNat x.ctorIdx = x
-- Mathlib.RingTheory.RingHomProperties
RingHom.IsStableUnderBaseChange.tensorProduct : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ {R S : Type u} (T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
      [inst_4 : Algebra R T], P (algebraMap R S) → P (algebraMap T (TensorProduct R T S))
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.restrict₂_apply : ∀ {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {I J : Finset ι'} (hIJ : I ⊆ J) (x : EuclideanSpace 𝕜 ↥J) (i : ↥I),
  ((EuclideanSpace.restrict₂ hIJ) x).ofLp i = x.ofLp ⟨↑i, ⋯⟩
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_div_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a / x) ⁻¹' Set.Ico b c = Set.Ioc (a / c) (a / b)
-- Mathlib.Geometry.Euclidean.Projection
/-- Subtracting `p` from its `orthogonalProjection` produces a result
in the orthogonal direction.  -/
EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  ↑((EuclideanGeometry.orthogonalProjection s) p) -ᵥ p ∈ s.directionᗮ
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionDisabled.reason : Lean.Lsp.CodeActionDisabled → String
-- Mathlib.Algebra.TrivSqZeroExt.Ideal
TrivSqZeroExt.kerIdeal_sq : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [inst_4 : IsCentralScalar R M], TrivSqZeroExt.kerIdeal R M ^ 2 = ⊥
-- Mathlib.Logic.Basic
exists_of_exists_mem : ∀ {α : Sort u_1} {p q : α → Prop}, (∃ x, ∃ (_ : p x), q x) → ∃ x, q x
-- Mathlib.Control.Traversable.Lemmas
Traversable.traverse_map' : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {G : Type u → Type u} [inst_2 : Applicative G]
  [LawfulApplicative G] {α β γ : Type u} (g : α → β) (h : β → G γ), traverse (h ∘ g) = traverse h ∘ Functor.map g
-- Mathlib.Algebra.Group.Basic
div_div_self' : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a / (a / b) = b
-- Mathlib.Data.Fin.Fin2
_private.Mathlib.Data.Fin.Fin2.0.Fin2.toNat.match_1.eq_2 : ∀ (motive : (x : ℕ) → Fin2 x → Sort u_1) (n : ℕ) (i : Fin2 n) (h_1 : (n : ℕ) → motive (n + 1) Fin2.fz)
  (h_2 : (n : ℕ) → (i : Fin2 n) → motive (n + 1) i.fs),
  (match n + 1, i.fs with
    | .(n + 1), Fin2.fz => h_1 n
    | .(n + 1), i.fs => h_2 n i) =
    h_2 n i
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_add_measure : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] {ν : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E),
  MeasureTheory.Integrable (⇑f) (μ + ν) →
    MeasureTheory.SimpleFunc.integral (μ + ν) f =
      MeasureTheory.SimpleFunc.integral μ f + MeasureTheory.SimpleFunc.integral ν f
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHomClass.toMulHomClass : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {inst : NonUnitalNonAssocSemiring α}
  {inst_1 : NonUnitalNonAssocSemiring β} {inst_2 : FunLike F α β} [self : NonUnitalRingHomClass F α β],
  MulHomClass F α β
-- Mathlib.Analysis.Normed.MulAction
/-- Mixin class for scalar-multiplication actions with a strictly multiplicative norm, i.e.
`‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ`.  -/
ENormSMulClass : (α : Type u_3) → (β : Type u_4) → [ENorm α] → [ENorm β] → [SMul α β] → Prop
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.mem_specialUnitaryGroup_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  {A : Matrix n n α}, A ∈ Matrix.specialUnitaryGroup n α ↔ A ∈ Matrix.unitaryGroup n α ∧ A.det = 1
-- Mathlib.RingTheory.Noetherian.Basic
/-- If `M / S / R` is a scalar tower, and `M / R` is Noetherian, then `M / S` is
also Noetherian.  -/
isNoetherian_of_tower : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R S] [inst_4 : Module S M] [inst_5 : Module R M] [IsScalarTower R S M],
  IsNoetherian R M → IsNoetherian S M
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Extend a family of elements to the sieve generated by an arrow set.
This is the construction described as "easy" in Lemma C2.1.3 of [Elephant].
 -/
CategoryTheory.Presieve.FamilyOfElements.sieveExtend : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R : CategoryTheory.Presieve X} →
          CategoryTheory.Presieve.FamilyOfElements P R →
            CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `s` is a set in a space `X` with second countable topology and `f : X → Y` is Hölder
continuous in a neighborhood within `s` of every point `x ∈ s` with the same positive exponent `r`
but possibly different coefficients, then the Hausdorff dimension of the image `f '' s` is at most
the Hausdorff dimension of `s` divided by `r`.  -/
dimH_image_le_of_locally_holder_on : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [SecondCountableTopology X]
  {r : NNReal} {f : X → Y},
  0 < r → ∀ {s : Set X}, (∀ x ∈ s, ∃ C, ∃ t ∈ nhdsWithin x s, HolderOnWith C r f t) → dimH (f '' s) ≤ dimH s / ↑r
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj.eq_1 : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) (i : ι),
  TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj U (CategoryTheory.Pairwise.single i) =
    { obj := U i, property := ⋯ }
-- Mathlib.Order.RelIso.Basic
RelEmbedding.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r ↪r s}, f = g ↔ ∀ (x : α), f x = g x
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_startPos : ∀ (s : String.Slice), s.startPos.Splits "" s.copy
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_cpow_real : ∀ (x : ℂ) (y : ℝ), ‖x ^ ↑y‖ = ‖x‖ ^ y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- All supported unary operators on `BVExpr`.
 -/
Std.Tactic.BVDecide.BVUnOp : Type
-- Mathlib.Algebra.Order.Module.Defs
Prod.instPosSMulStrictMono : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : PartialOrder β]
  [inst_3 : PartialOrder γ] [inst_4 : Zero β] [inst_5 : Zero γ] [inst_6 : SMulWithZero α β] [inst_7 : SMulWithZero α γ]
  [PosSMulStrictMono α β] [PosSMulStrictMono α γ], PosSMulStrictMono α (β × γ)
-- Mathlib.RepresentationTheory.Action
Representation.linearizeTrivialIso_symm_apply : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] {X : Type w} (f : MonoidAlgebra k X),
  (Representation.linearizeTrivialIso k G X).symm f = f
-- Mathlib.CategoryTheory.Center.Localization
/-- Given `r : CatCenter C` and `L : C ⥤ D` a localization functor with respect
to `W : MorphismProperty D`, this is the induced element in `CatCenter D`
obtained by localization.  -/
CategoryTheory.CatCenter.localization : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.CatCenter C →
          (L : CategoryTheory.Functor C D) →
            (W : CategoryTheory.MorphismProperty C) → [L.IsLocalization W] → CategoryTheory.CatCenter D
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tfst_comp_tfst : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ α₁ α₂ β : Type u}
  (f : α₀ → F α₁) (f' : α₁ → G α₂),
  Functor.Comp.mk ∘ Functor.map (Bitraversable.tfst f') ∘ Bitraversable.tfst f =
    Bitraversable.tfst (Functor.Comp.mk ∘ Functor.map f' ∘ f)
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
CommGrpCat.instBraidedForgetMonoidHomCarrier : (CategoryTheory.forget CommGrpCat).Braided
-- Mathlib.Topology.Algebra.Ring.Real
NNReal.instIsTopologicalSemiring : IsTopologicalSemiring NNReal
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal.privateConstInfo : Lean.Environment.ConstPromiseVal✝ → Lean.ConstantInfo
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.toList_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {f : (a : α) → β a → γ a} {l : Std.DHashMap.Internal.AssocList α β},
  (Std.DHashMap.Internal.AssocList.map f l).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l.toList)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι} {G : ι → α → β},
  TendstoLocallyUniformly F f p → (∀ (n : ι) (x : α), F n x = G n x) → TendstoLocallyUniformly G f p
-- Init.Data.Fin.Lemmas
Fin.pred_succ : ∀ {n : ℕ} (i : Fin n) {h : i.succ ≠ 0}, i.succ.pred h = i
-- Mathlib.Algebra.Group.End
MulAut.instInhabited : (M : Type u_2) → [inst : Mul M] → Inhabited (MulAut M)
-- Mathlib.Algebra.Order.Group.PosPart
/-- See also `leOnePart_eq_one`.  -/
leOnePart_eq_one' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, a⁻ᵐ = 1 ↔ a⁻¹ ≤ 1
-- Mathlib.Data.Fintype.Quotient
/-- `Quotient.finChoice` as an equivalence.  -/
Quotient.finChoiceEquiv : {ι : Type u_1} →
  [Fintype ι] →
    [DecidableEq ι] → {α : ι → Sort u_2} → {S : (i : ι) → Setoid (α i)} → ((i : ι) → Quotient (S i)) ≃ Quotient piSetoid
-- Mathlib.Topology.Algebra.FilterBasis
/-- `GroupFilterBasis` constructor in the commutative group case.  -/
groupFilterBasisOfComm : {G : Type u_1} →
  [inst : CommGroup G] →
    (sets : Set (Set G)) →
      sets.Nonempty →
        (∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) →
          (∀ U ∈ sets, 1 ∈ U) →
            (∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U) →
              (∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x => x⁻¹) ⁻¹' U) → GroupFilterBasis G
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.signAux.eq_1 : ∀ {n : ℕ} (a : Equiv.Perm (Fin n)), a.signAux = ∏ x ∈ Equiv.Perm.finPairsLT n, if a x.fst ≤ a x.snd then -1 else 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.homMonoidHom_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.MonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (a : X ⟶ M), F.homMonoidHom a = F.map a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_alter_eq_sub_one : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  k ∈ t → (f (Std.ExtDTreeMap.Const.get? t k)).isNone = true → (Std.ExtDTreeMap.Const.alter t k f).size = t.size - 1
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.categoryOfDifferentialObjects : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            CategoryTheory.Category.{v, max u v} (CategoryTheory.DifferentialObject S C)
-- Init.Data.BitVec.Bitblast
/-- the most significant bit of the signed division `x.sdiv y` can be computed
by the following cases:
(1) x nonneg, y nonneg: never neg.
(2) x nonneg, y neg: neg when result nonzero.
   We know that y is nonzero since it is negative, so we only check `|x| ≥ |y|`.
(3) x neg, y nonneg: neg when result nonzero.
  We check that `y ≠ 0` and `|x| ≥ |y|`.
(4) x neg, y neg: neg when `x = intMin, `y = -1`, since `intMin / -1 = intMin`.

The proof strategy is to perform a case analysis on the sign of `x` and `y`,
followed by unfolding the `sdiv` into `udiv`.
 -/
BitVec.msb_sdiv_eq_decide : ∀ {w : ℕ} {x y : BitVec w},
  (x.sdiv y).msb =
    (decide (0 < w) && (!x.msb && y.msb && decide (-y ≤ x)) ||
        x.msb && !y.msb && decide (y ≤ -x) && !decide (y = 0#w) ||
      x.msb && y.msb && decide (x = BitVec.intMin w) && decide (y = -1#w))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
/-- If `cons (exp, coef) tl` is trimmed, then `coef` is trimmed and is not zero.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.elim_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} {f : ℝ → ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f).Trimmed →
    coef.Trimmed ∧ ¬coef.IsZero
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.ofHom_apply : ∀ {R S : Type u} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (r : R),
  (CategoryTheory.ConcreteCategory.hom (CommSemiRingCat.ofHom f)) r = f r
-- Mathlib.Topology.Subpath
/-- The subpath of `γ` from `t₀` to `t₁`.  -/
Path.subpath : {X : Type u_1} → [inst : TopologicalSpace X] → {a b : X} → (γ : Path a b) → (t₀ t₁ : ↑unitInterval) → Path (γ t₀) (γ t₁)
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.TreeMap.maxEntry! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap α β cmp → α × β
-- Mathlib.RingTheory.Noetherian.Defs
wellFoundedGT : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [h : IsNoetherian R M], WellFoundedGT (Submodule R M)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldrM_eq_foldrM_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.DTreeMap.Raw.foldrM (fun a x d => f a d) init t = Array.foldrM f init t.keysArray
-- Mathlib.Order.Bounds.Basic
DirectedOn.of_isCofinalFor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) t → s ⊆ t → IsCofinalFor t s → DirectedOn (fun x1 x2 => x1 ≤ x2) s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isNone_minKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.minKey?.isNone = t.isEmpty
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousWithinAt.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {x : α} {s : Set α} {f : β → Prop},
  SemicontinuousWithinAt (fun _x => f) s x
-- Mathlib.Data.Int.Init
/-- Immediate successor of an integer: `succ n = n + 1`  -/
Int.succ : ℤ → ℤ
-- Mathlib.Algebra.GroupWithZero.Basic
/-- In a monoid with zero, either zero and one are nonequal, or zero is the only element.  -/
zero_ne_one_or_forall_eq_0 : ∀ {M₀ : Type u_1} [inst : MulZeroOneClass M₀], 0 ≠ 1 ∨ ∀ (a : M₀), a = 0
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of a set of points contains the set of points.  -/
Projectivization.Subspace.subset_span : ∀ {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)), S ⊆ ↑(Projectivization.Subspace.span S)
-- Mathlib.Order.Defs.Unbundled
IsPreorder.toIsTrans : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsPreorder α r], IsTrans α r
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {km : α},
  t.max? = some km → t.get? km = some km
-- Mathlib.Dynamics.Ergodic.Extreme
Ergodic.eq_of_absolutelyContinuous_measure_univ_eq : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  Ergodic f μ → MeasureTheory.MeasurePreserving f ν ν → ν.AbsolutelyContinuous μ → ν Set.univ = μ Set.univ → ν = μ
-- Mathlib.NumberTheory.ModularForms.DedekindEta
/-- The infinite product `∏ (1 - q^(n+1))` converges locally uniformly on the open unit disc,
with limit `q ↦ ∏' n, (1 - q^(n+1))`.  -/
ModularForm.multipliableLocallyUniformlyOn_one_sub_pow : MultipliableLocallyUniformlyOn (fun n q => 1 - q ^ (n + 1)) (Metric.ball 0 1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.one_def : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁], 1 = AffineEquiv.refl k P₁
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.ShiftTarget w → Std.Sat.AIG.RefVecEntry α w
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∈ m ↔ (m.getKey? a).isSome = true
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.not_nhds_le_map : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α}
  [inst_2 : TopologicalSpace β],
  IsLocalMaxOn f s a → ∀ [(nhdsWithin (f a) (Set.Ioi (f a))).NeBot], ¬nhds (f a) ≤ Filter.map f (nhdsWithin a s)
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- A symmetric projection is positive.  -/
LinearMap.IsSymmetricProjection.isPositive : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {p : E →ₗ[𝕜] E}, p.IsSymmetricProjection → p.IsPositive
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_neg_sub_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.U R (-n - 1) = -Polynomial.Chebyshev.U R (n - 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel_not_iso_of_nonzero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f],
  f ≠ 0 → CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι f) → False
-- Batteries.Data.Array.Scan
Array.scanlM_eq_scanlM_toList : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] [LawfulMonad m] {f : β → α → m β}
  {as : Array α}, Array.scanlM f init as = List.toArray <$> List.scanlM f init as.toList
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.eval.eq_1 : Turing.ToPartrec.Cont.halt.eval = pure
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedMor₁.default : Mathlib.Tactic.BicategoryLike.Mor₁
-- Std.Data.DHashMap.Internal.AssocList.Iterator
_private.Std.Data.DHashMap.Internal.AssocList.Iterator.0.Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.IterStep (Std.IterM Id ((a : α) × β a)) ((a : α) × β a) → Sort u_3)
  (it : Std.IterM Id ((a : α) × β a))
  (h_1 : (it' : Std.IterM Id ((a : α) × β a)) → (out : (a : α) × β a) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM Id ((a : α) × β a)) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Mathlib.Data.PNat.Basic
instWellFoundedLTPNat : WellFoundedLT ℕ+
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀o β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = ↑f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverTerms.nil.sizeOf_spec : sizeOf Lean.Meta.Grind.SolverTerms.nil = 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : t[a]?.isSome = true}, t[a]?.get h = t[a]
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The empty set is a block.  -/
AddAction.IsBlock.empty : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X], AddAction.IsBlock G ∅
-- Mathlib.RingTheory.Support
Module.annihilator_le_of_mem_support : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PrimeSpectrum R}, p ∈ Module.support R M → Module.annihilator R M ≤ p.asIdeal
-- Mathlib.Algebra.Polynomial.Basic
/-- The map sending a collection of roots into a polynomial, as a morphism.  -/
Polynomial.ofMultiset : {R : Type u} → [inst : CommRing R] → AddChar (Multiset R) (Polynomial R)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- The coefficient is well-defined regardless of which `y` we pick in `evalCoeff`.  -/
HahnEmbedding.Partial.evalCoeff_eq : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] {x : M} {c : FiniteArchimedeanClass M} {y : ↥(↑f).domain},
  ↑y - x ∈ FiniteArchimedeanClass.ball K c → f.evalCoeff x c = (ofLex (↑↑f y)).coeff c
-- Mathlib.Topology.MetricSpace.Defs
Metric.sphere_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x : γ}, Metric.sphere x 0 = {x}
-- Lean.Util.Profile
Lean.profileitIOUnsafe : {ε α : Type} → String → Lean.Options → EIO ε α → optParam Lean.Name Lean.Name.anonymous → EIO ε α
-- Init.Data.UInt.Lemmas
UInt64.pow_succ : ∀ (x : UInt64) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Mathlib.Data.Nat.Choose.Central
Nat.centralBinom_zero : Nat.centralBinom 0 = 1