mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_lt : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommGroup α] [inst_1 : PartialOrder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α}
  {a₁ a₂ : α} {i : ι} [L.NeBot] [L.LeAtTop], f ≤ g → f i < g i → HasSum f a₁ L → HasSum g a₂ L → a₁ < a₂
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `MulAction.isBlock_iff_smul_eq_smul_of_nonempty`. -/
MulAction.IsBlock.smul_eq_smul_of_nonempty : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X},
  MulAction.IsBlock G B → ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.refl : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u : α → β} {l : Filter α}, Asymptotics.IsEquivalent l u u
-- Mathlib.AlgebraicGeometry.Gluing
/-- A family of gluing data consists of
1. An index type `J`
2. A scheme `U i` for each `i : J`.
3. A scheme `V i j` for each `i j : J`.
  (Note that this is `J × J → Scheme` rather than `J → J → Scheme` to connect to the
  limits library easier.)
4. An open immersion `f i j : V i j ⟶ U i` for each `i j : ι`.
5. A transition map `t i j : V i j ⟶ V j i` for each `i j : ι`.

such that
6. `f i i` is an isomorphism.
7. `t i i` is the identity.
8. `V i j ×[U i] V i k ⟶ V i j ⟶ V j i` factors through `V j k ×[U j] V j i ⟶ V j i` via some
    `t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i`.
9. `t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _`.

We can then glue the schemes `U i` together by identifying `V i j` with `V j i`, such
that the `U i`'s are open subschemes of the glued space.
 -/
AlgebraicGeometry.Scheme.GlueData : Type (u_1 + 1)
-- Mathlib.Algebra.Group.Defs
/-- A `Semigroup` which `IsMulCommutative` is a `CommSemigroup`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instCommSemigroup : {M : Type u_2} → [inst : Semigroup M] → [IsMulCommutative M] → CommSemigroup M
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p f n : ℕ} {P : Polynomial K},
  Fintype.card K = p ^ f →
    ∀ (hn : p.Coprime n) [hp : Fact (Nat.Prime p)] [inst_2 : DecidableEq K],
      P ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.cyclotomic n K) →
        P.natDegree = orderOf (ZMod.unitOfCoprime (p ^ f) ⋯)
-- Qq.MetaM
/-- A version of `Lean.Meta.isLevelDefEq` which returns a strongly-typed witness rather than a bool.  -/
Qq.isLevelDefEqQ : (u v : Lean.Level) → Lean.MetaM (Qq.MaybeLevelDefEq u v)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signBijAux_injOn : ∀ {n : ℕ} {f : Equiv.Perm (Fin n)}, Set.InjOn f.signBijAux ↑(Equiv.Perm.finPairsLT n)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `f : M × S → M × S → α` respects the equivalence relation `LocalizedModule.r`, then
`f` descents to a map `LocalizedModule M S → LocalizedModule M S → α`.
 -/
LocalizedModule.liftOn₂ : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} →
      {M : Type v} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {α : Type u_3} →
              LocalizedModule S M →
                LocalizedModule S M →
                  (f : M × ↥S → M × ↥S → α) → (∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q') → α
-- Init.Data.SInt.Lemmas
Int64.toInt_toInt32 : ∀ (x : Int64), x.toInt32.toInt = x.toInt.bmod (2 ^ 32)
-- Mathlib.Data.Real.Basic
Real.instCommMonoidWithZero : CommMonoidWithZero ℝ
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j),
  d.transitionCocone hij = (CategoryTheory.Limits.Cocone.precompose (d.trans hij)).obj (d.cocone j)
-- Mathlib.Algebra.Group.Submonoid.Operations
MulEquiv.ofLeftInverse'_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) {g : N → M}
  (h : Function.LeftInverse g ⇑f) (a : ↥(MonoidHom.mrange f)), (MulEquiv.ofLeftInverse' f h).symm a = g ↑a
-- Mathlib.Data.Finsupp.Multiset
/-- Given `f : α →₀ ℕ`, `f.toMultiset` is the multiset with multiplicities given by the values of
`f` on the elements of `α`. We define this function as an `AddMonoidHom`.

Under the additional assumption of `[DecidableEq α]`, this is available as
`Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ)`; the two declarations are separate as this assumption
is only needed for one direction.  -/
Finsupp.toMultiset : {α : Type u_1} → (α →₀ ℕ) →+ Multiset α
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.return : Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.Code
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.unitsHasCoeToFun : CoeFun CircleDeg1Liftˣ fun x => ℝ → ℝ
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- `e : Edge x y` is a composition of `e` with `Edge.id y`.  -/
SSet.Truncated.Edge.CompStruct.compId : {X : SSet.Truncated 2} →
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    (e : SSet.Truncated.Edge x y) → e.CompStruct (SSet.Truncated.Edge.id y) e
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ProjectiveSpectrum 𝒜), x.asHomogeneousIdeal.toIdeal.IsPrime
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_comm : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, a / b ≤ c ↔ a / c ≤ b
-- Init.Core
decide_false : ∀ (h : Decidable False), decide False = false
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = (m.getKey? a).isSome
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.prod_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] [inst_6 : TopologicalSpace N] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N']
  [inst_9 : TopologicalSpace N'] (f : M [⋀^ι]→L[R] N) (g : M [⋀^ι]→L[R] N') (m : (i : ι) → (fun x => M) i),
  (f.prod g) m = (f m, g m)
-- Mathlib.Data.List.Sym
List.mk_mem_sym2 : ∀ {α : Type u_1} {xs : List α} {a b : α}, a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_one : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [Nontrivial R], m.withBotDegree 1 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.opParallelPairIso_hom_app_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Limits.opParallelPairIso f g).hom.app (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.parallelPair f g).op.obj (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero))
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasDerivWithinAt_Iio_iff_Iic`. -/
HasDerivWithinAt.Iic_of_Iio : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : PartialOrder 𝕜],
  HasDerivWithinAt f f' (Set.Iio x) x → HasDerivWithinAt f f' (Set.Iic x) x
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapWhiskerRight_id : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (H : CategoryTheory.Functor D E'),
  CategoryTheory.Join.mapWhiskerRight (CategoryTheory.CategoryStruct.id Fₗ) H =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.mapPair Fₗ H)
-- Mathlib.Data.EReal.Inv
_private.Mathlib.Data.EReal.Inv.0.EReal.exists_mul_right_lt : ∀ {a b c : EReal}, 0 < a ∨ b ≠ ⊤ → a ≠ ⊤ ∨ b ≠ 0 → a * b < c → ∃ b' ∈ Set.Ioo b ⊤, a * b' < c
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {fallback : β k} {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.spine_spineToSimplex_apply : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path n), X.spine n (sx.spineToSimplex f) = f
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
CompactConvergenceCLM.piEquivL_apply : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜₁ E]
  [inst_3 : TopologicalSpace E] {ι : Type u_7} (F : ι → Type u_8) [inst_4 : (i : ι) → AddCommGroup (F i)]
  [inst_5 : (i : ι) → Module 𝕜₁ (F i)] [inst_6 : (i : ι) → TopologicalSpace (F i)]
  [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜₁ (F i)]
  (T : (i : ι) → CompactConvergenceCLM (RingHom.id 𝕜₁) E (F i)) (e : E) (i : ι),
  ((CompactConvergenceCLM.piEquivL 𝕜₁ E F) T) e i = (T i) e
-- Mathlib.Logic.Basic
Ne.ite_eq_left_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b : α}, a ≠ b → ((if P then a else b) = a ↔ P)
-- Mathlib.Data.List.Cycle
Cycle.mem_coe_iff : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ ↑l ↔ a ∈ l
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (s s_1 : aig.RefVec len),
  s = s_1 → ∀ (idx idx_1 : ℕ) (e_idx : idx = idx_1) (hidx : idx < len), s.get idx hidx = s_1.get idx_1 ⋯
-- Mathlib.Data.Nat.Prime.Basic
Nat.dvd_prime_pow : ∀ {p : ℕ}, Nat.Prime p → ∀ {m i : ℕ}, i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k
-- Mathlib.RepresentationTheory.Basic
/-- A `k`-linear representation of `G` on `V` can be thought of as a module over `k[G]`.
 -/
Representation.instModuleMonoidAlgebraAsModule : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module k V] → (ρ : Representation k G V) → Module (MonoidAlgebra k G) ρ.asModule
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (x : Std.DTreeMap.Internal.Impl α β)
  (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getEntryGT k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      if hkky : compare k ky = Ordering.lt then Std.DTreeMap.Internal.Impl.getEntryGTD k l ⟨ky, y⟩
      else Std.DTreeMap.Internal.Impl.getEntryGT k r ⋯ ⋯
-- Mathlib.Data.Sign.Basic
/-- We can decompose a sum of absolute value less than `n` into a sum of at most `n` signs.  -/
exists_signed_sum' : ∀ {α : Type u} [Nonempty α] [inst : DecidableEq α] (s : Finset α) (f : α → ℤ) (n : ℕ),
  ∑ i ∈ s, (f i).natAbs ≤ n →
    ∃ β x sgn g,
      (∀ (b : β), g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i, if g i = a then ↑(sgn i) else 0) = f a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rcc_eq_add : ∀ {m n i : ℕ}, i < n + 1 - m → (m...=n).toArray[i]! = m + i
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- An auxiliary equality useful to prove the **Cauchy–Schwarz inequality**. Here we use the
standard argument involving the discriminant of quadratic form.  -/
InnerProductSpace.Core.cauchy_schwarz_aux' : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F) (t : ℝ),
  0 ≤ InnerProductSpace.Core.normSq x * t * t + 2 * RCLike.re (inner 𝕜 x y) * t + InnerProductSpace.Core.normSq y
-- Init.Prelude
/-- Checks whether syntax has the given kind or pseudo-kind.

“Pseudo-kinds” are kinds that are assigned by convention to non-`Syntax.node` values:
`identKind` for `Syntax.ident`, `` `missing `` for `Syntax.missing`, and the atom's string literal
for atoms.
 -/
Lean.Syntax.isOfKind : Lean.Syntax → Lean.SyntaxNodeKind → Bool
-- Mathlib.Data.String.Lemmas
/-- The length of the String returned by `String.leftpad n a c` is equal
to the larger of `n` and `s.length`  -/
String.length_leftpad : ∀ (n : ℕ) (c : Char) (s : String), (String.leftpad n c s).length = max n s.length
-- Mathlib.NumberTheory.NumberField.Basic
/-- The algebraMap between ring of integers is injective.  -/
NumberField.RingOfIntegers.algebraMap.injective : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Function.Injective ⇑(algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L))
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage : ∀ {β : Type u_2} [inst : TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U → ∀ {s : Set β}, IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' s)
-- Lean.Linter.Init
Lean.Linter.LinterOptions.get : {α : Type} → [Lean.KVMap.Value α] → Lean.Linter.LinterOptions → Lean.Name → α → α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Constructor for isomorphisms in `CategoricalPullback F G`.  -/
CategoryTheory.Limits.CategoricalPullback.mkIso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {x y : CategoryTheory.Limits.CategoricalPullback F G} →
                  (eₗ : x.fst ≅ y.fst) →
                    (eᵣ : x.snd ≅ y.snd) →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp (F.map eₗ.hom) y.iso.hom =
                            CategoryTheory.CategoryStruct.comp x.iso.hom (G.map eᵣ.hom))
                          CategoryTheory.Limits.CategoricalPullback.mkIso._auto_1 →
                        (x ≅ y)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (self : X.Hom Y) (U : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.f U) (Y.snd.β U).hom =
    CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U self.f)
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.mk.inj : ∀ {method : Aesop.ScriptGenerated.Method} {perfect hasMVar : Bool} {method_1 : Aesop.ScriptGenerated.Method}
  {perfect_1 hasMVar_1 : Bool},
  { method := method, perfect := perfect, hasMVar := hasMVar } =
      { method := method_1, perfect := perfect_1, hasMVar := hasMVar_1 } →
    method = method_1 ∧ perfect = perfect_1 ∧ hasMVar = hasMVar_1
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.comp : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [h₁ : Algebra.EssFiniteType R S] [h₂ : Algebra.EssFiniteType S T], Algebra.EssFiniteType R T
-- Lean.Util.Trace
Lean.traceM : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadTrace m] →
      [Lean.MonadRef m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Name → m Lean.MessageData → m Unit
-- Mathlib.MeasureTheory.Integral.Gamma
Complex.integral_exp_neg_rpow : ∀ {p : ℝ}, 1 ≤ p → ∫ (x : ℂ), Real.exp (-‖x‖ ^ p) = Real.pi * Real.Gamma (2 / p + 1)
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
panicking if no such element exists.
 -/
Std.ExtTreeSet.getGT! : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeSet α cmp → α → α
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_lineMap_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P} (y : P), x ∈ s → ∀ {t : R}, t ≤ 0 → s.WOppSide ((AffineMap.lineMap x y) t) y
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
Equiv.Perm.stabilizer_ne_top_of_nonempty_of_nonempty_compl : ∀ {α : Type u_2} {s : Set α}, s.Nonempty → sᶜ.Nonempty → MulAction.stabilizer (Equiv.Perm α) s ≠ ⊤
-- Mathlib.Condensed.Light.Basic
LightCondensed.hom_ext : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] {X Y : LightCondensed C} (f g : X ⟶ Y),
  (∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S) → f = g
-- Batteries.Tactic.OpenPrivate
/-- finds private declarations `n ++ suff` where `n` resolves and `n ++ suff` realizes  -/
_private.Batteries.Tactic.OpenPrivate.0.Lean.Elab.Command.elabOpenPrivateLike.findAll : Lean.NameSet → Lean.Ident → Lean.Name → Lean.Name → Lean.Elab.Command.CommandElabM (List Lean.Name)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.exists_normAtPlace_ne_zero_iff : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.mixedEmbedding.mixedSpace K},
  (∃ w, (NumberField.mixedEmbedding.normAtPlace w) x ≠ 0) ↔ x ≠ 0
-- Mathlib.Algebra.Group.Action.Pretransitive
MulAction.exists_smul_eq : ∀ (M : Type u_1) {α : Type u_3} [inst : SMul M α] [MulAction.IsPretransitive M α] (x y : α), ∃ m, m • x = y
-- Mathlib.Data.Seq.Defs
/-- Enumerate a sequence by tagging each element with its index.  -/
Stream'.Seq.enum : {α : Type u} → Stream'.Seq α → Stream'.Seq (ℕ × α)
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the third commutative square of a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.comm₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂)
  {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj T₂.obj₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp T₁.mor₃
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.hom₁) h) =
    CategoryTheory.CategoryStruct.comp self.hom₃ (CategoryTheory.CategoryStruct.comp T₂.mor₃ h)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Convert a TryThis suggestion to tactic syntax for verification.  -/
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.parseSuggestionToTactic : Lean.Meta.Tactic.TryThis.Suggestion → Lean.Elab.Command.CommandElabM (Lean.TSyntax `tactic)
-- Lean.Parser.Tactic.Doc
_private.Lean.Parser.Tactic.Doc.0.Lean.Parser.Tactic.Doc.getTacticExtensionString.bullet : String → String
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.ConfigItem.mk.injEq : ∀ (ref : Lean.Syntax) (option : Lean.Ident) (value : Lean.Syntax) (bool? : Option Bool) (origOptionName : Lean.Name)
  (optionComps prevOptionComps : List Lean.Syntax) (ref_1 : Lean.Syntax) (option_1 : Lean.Ident) (value_1 : Lean.Syntax)
  (bool?_1 : Option Bool) (origOptionName_1 : Lean.Name) (optionComps_1 prevOptionComps_1 : List Lean.Syntax),
  ({ ref := ref, option := option, value := value, bool? := bool?, origOptionName := origOptionName,
        optionComps := optionComps, prevOptionComps := prevOptionComps } =
      { ref := ref_1, option := option_1, value := value_1, bool? := bool?_1, origOptionName := origOptionName_1,
        optionComps := optionComps_1, prevOptionComps := prevOptionComps_1 }) =
    (ref = ref_1 ∧
      option = option_1 ∧
        value = value_1 ∧
          bool? = bool?_1 ∧
            origOptionName = origOptionName_1 ∧ optionComps = optionComps_1 ∧ prevOptionComps = prevOptionComps_1)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- **Alias** of the reverse direction of `AddSubgroup.normal_op`. -/
AddSubgroup.Normal.op : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup G}, H.Normal → H.op.Normal
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enriched_comp_id : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₂],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
          (CategoryTheory.Enriched.FunctorCategory.enrichedId V F₂))
        (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₂)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
-- Mathlib.Data.Nat.Prime.Infinite
/-- Euclid's theorem on the **infinitude of primes**.
Here given in the form: for every `n`, there exists a prime number `p ≥ n`.  -/
Nat.exists_infinite_primes : ∀ (n : ℕ), ∃ p, n ≤ p ∧ Nat.Prime p
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ReducedWord.mk.congr_simp : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (head head_1 : G),
  head = head_1 →
    ∀ (toList toList_1 : List (ℤˣ × G)) (e_toList : toList = toList_1)
      (chain : List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) toList),
      { head := head, toList := toList, chain := chain } = { head := head_1, toList := toList_1, chain := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.comp_sum : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
  {J : Type u_1} (s : Finset J) (f : P ⟶ Q) (g : J → (Q ⟶ R)),
  CategoryTheory.CategoryStruct.comp f (∑ j ∈ s, g j) = ∑ j ∈ s, CategoryTheory.CategoryStruct.comp f (g j)
-- Mathlib.GroupTheory.Coset.Basic
zero_leftAddCoset : ∀ {α : Type u_1} [inst : AddMonoid α] (s : Set α), 0 +ᵥ s = s
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  (f : CompactlySupportedContinuousMap α β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualCoannihilator.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Φ : Submodule R (Module.Dual R M)), Φ.dualCoannihilator = Submodule.comap (Module.Dual.eval R M) Φ.dualAnnihilator