mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.index_eq_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] [Subsingleton α], (alternatingGroup α).index = 1
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_lt_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftStrictMono M] [AddLeftMono M]
  [AddRightStrictMono M] [AddRightMono M] {l : List ι} (f g : ι → M),
  (∀ i ∈ l, f i ≤ g i) → (∃ i ∈ l, f i < g i) → (List.map f l).sum < (List.map g l).sum
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {t : CategoryTheory.Limits.Cone K}
  (t_1 : CategoryTheory.Limits.IsLimit t)
  (s : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)),
  (CategoryTheory.WithTerminal.isLimitEquiv.symm t_1).lift s =
    ((CategoryTheory.WithTerminal.coneEquiv.symm.toAdjunction.homEquiv s t)
        (t_1.liftConeMorphism (CategoryTheory.WithTerminal.coneEquiv.inverse.obj s))).hom
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.top : ∀ (S : Type u_5) [inst : Semiring S] (M : Type u_6) [inst_1 : AddCommMonoid M] [inst_2 : Module S M],
  LinearMap.IsProj ⊤ LinearMap.id
-- Mathlib.Data.NNRat.Defs
NNRat.bddAbove_coe : ∀ {s : Set ℚ≥0}, BddAbove (NNRat.cast '' s) ↔ BddAbove s
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.exists_ne_map_eq_of_mapsTo : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β},
  s.Infinite → Set.MapsTo f s t → t.Finite → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Every generalized eigenvector is a generalized eigenvector for exponent `finrank K V`.
(Lemma 8.20 of [axler2024])  -/
Module.End.genEigenspace_le_genEigenspace_finrank : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (f : Module.End K V) (μ : K) (k : ℕ∞), (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ↑(Module.finrank K V)
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.pullback.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : NormedAddCommGroup E] (f : CompactlySupportedContinuousMap B E) (b : B),
  H.pullback f b = CompactlySupportedContinuousMap.pullback_monoidHom ⋯ f b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.PreservesBinaryBiproduct.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C}
  {F : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms],
  (∀ {b : CategoryTheory.Limits.BinaryBicone X Y} (a : b.IsBilimit), Nonempty (F.mapBinaryBicone b).IsBilimit) →
    CategoryTheory.Limits.PreservesBinaryBiproduct X Y F
-- Mathlib.Tactic.Core
/-- Given a local context and an array of `FVarIds` assumed to be in that local context, remove all
implementation details.  -/
Lean.Elab.Tactic.filterOutImplementationDetails : Lean.LocalContext → Array Lean.FVarId → Array Lean.FVarId
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.OplaxTrans F G) (a : B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a))
      (self.naturality (CategoryTheory.CategoryStruct.id a)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv
        (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)))
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piRing_apply : ∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] (S : Type u_4) [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : Module S M]
  [inst_7 : SMulCommClass R S M] (f : (ι → R) →ₗ[R] M) (i : ι), (LinearEquiv.piRing R M ι S) f i = f (Pi.single i 1)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.toIsLocalRing : ∀ {R : Type u} {inst : CommRing R} {inst_1 : IsDomain R} [self : IsDiscreteValuationRing R], IsLocalRing R
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
ModularForm.IsCuspForm.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : Γ.HasDetOne] (f f_1 : ModularForm Γ k),
  f = f_1 → f.IsCuspForm = f_1.IsCuspForm
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
continuous_barycentric_coord : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {P : Type u_4} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor E P]
  [FiniteDimensional 𝕜 E] (b : AffineBasis ι 𝕜 P) (i : ι), Continuous ⇑(b.coord i)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.gc_hull_coe : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M], GaloisConnection (ConvexCone.hull R) SetLike.coe
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
/-- The integral of `f (R • x)` with respect to an additive Haar measure is a multiple of the
integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
thanks to the convention that a non-integrable function has integral zero.  -/
MeasureTheory.Measure.integral_comp_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F] (f : E → F) (R : ℝ),
  ∫ (x : E), f (R • x) ∂μ = |(R ^ Module.finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.instPartialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder αᵃᵒᵖ
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.groupSMul_span_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_5} [inst_3 : Group G] [inst_4 : SMul G R] [inst_5 : MulAction G M] [IsScalarTower G R M] {v : ι → M},
  Submodule.span R (Set.range v) = ⊤ → ∀ {w : ι → G}, Submodule.span R (Set.range (w • v)) = ⊤
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getEntryGE? k = Std.DTreeMap.Internal.Impl.getEntryGE?.go k none
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_strictlyPositive : ∀ (R : Type u_2) (M : Type u_4) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : PartialOrder M] [inst_4 : IsOrderedAddMonoid M] [inst_5 : Module R M] [inst_6 : PosSMulStrictMono R M],
  ↑(ConvexCone.strictlyPositive R M) = Set.Ioi 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.inter_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ : Std.TreeMap.Raw α β cmp}, t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ ∩ t₃).Equiv (t₂ ∩ t₃)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.ι_colimitCompWhiskeringLeftIsoCompColimit_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j)
      (CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit F G).hom =
    G.whiskerLeft (CategoryTheory.Limits.colimit.ι F j)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l → ∀ {h : k' ∈ m.insertManyIfNewUnit l}, (m.insertManyIfNewUnit l).getKey k' h = k
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.not_lt_lt : ∀ {R : Type u_1} [inst : CommRing R] [Ring.DimensionLEOne R] (p₀ p₁ p₂ : Ideal R) [hp₁ : p₁.IsPrime] [hp₂ : p₂.IsPrime],
  ¬(p₀ < p₁ ∧ p₁ < p₂)
-- Mathlib.NumberTheory.ModularForms.NormTrace
ModularForm.norm_eq_zero_iff : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ℋ.HasDetPlusMinusOne] [inst_3 : ModularFormClass F 𝒢 k],
  ModularForm.norm ℋ f = 0 ↔ ⇑f = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The `MonoidHom` from a `Submonoid` to its image.
See `MulEquiv.SubmonoidMap` for a variant for `MulEquiv`s.  -/
MonoidHom.submonoidMap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] → [inst_1 : MulOneClass N] → (f : M →* N) → (M' : Submonoid M) → ↥M' →* ↥(Submonoid.map f M')
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaIsoCoyoneda_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ),
  CategoryTheory.shrinkCoyonedaIsoCoyoneda.inv.app X =
    (CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.shrinkCoyonedaObjObjEquiv.toIso) ⋯).inv
-- Lean.Meta.LetToHave
/-- Returns `true` if we need to do full typechecking due to `let` variables being in scope.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Context.check : Lean.Meta.LetToHave.Context✝ → Bool
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_ofNat_succ : ∀ {R : Type u_1} [inst : Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (a n : ℕ) [h : a.AtLeastTwo],
  (OfNat.ofNat a).coeff (n + 1) = 0
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
instSeparatingDual : ∀ {E : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E],
  SeparatingDual 𝕜 E
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.prod'CompSnd_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor A C) (X : A), (F.prod'CompSnd G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.mulHead.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w : Monoid.CoprodI.NeWord M i j)
  (x : M i) (hnotone : x * w.head ≠ 1), w.mulHead x hnotone = Monoid.CoprodI.NeWord.replaceHead (x * w.head) hnotone w
-- Lean.Elab.App
/-- Gets `s.fType` with all loose bvars instantiated.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.State.getFType : Lean.Elab.Term.ElabAppArgs.State → Lean.Expr
-- Mathlib.Data.Real.Pointwise
Real.sInf_smul_of_nonpos : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Module α ℝ]
  [IsOrderedModule α ℝ] {a : α}, a ≤ 0 → ∀ (s : Set ℝ), sInf (a • s) = a • sSup s
-- Mathlib.Algebra.GroupWithZero.Basic
zero_pow_eq_zero : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {n : ℕ} [Nontrivial M₀], 0 ^ n = 0 ↔ n ≠ 0
-- Mathlib.Data.Part
Part.neg_def : ∀ {α : Type u_1} [inst : Neg α] (a : Part α), -a = Part.map (fun x => -x) a
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.convolution.eq_1 : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') (x : M),
  DiscreteConvolution.convolution L f g x = ∑' (ab : ↑(DiscreteConvolution.mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.vadd_of_comm : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} {G' : Type u_6} [inst_3 : AddGroup G'] [inst_4 : AddAction G' α]
  [MeasurableConstVAdd G' α] [MeasureTheory.VAddInvariantMeasure G' α μ] [VAddCommClass G' G α],
  MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (g : G'), MeasureTheory.IsAddFundamentalDomain G (g +ᵥ s) μ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.forallProp.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Grind.SplitSource.forallProp e) = 1 + sizeOf e
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X Y : P.FullSubcategory) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)),
  ((CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct X Y).lift t).hom =
    CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.Limits.BinaryFan.fst t).hom
      (CategoryTheory.Limits.BinaryFan.snd t).hom
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.instInfSet : {α : Type u_1} → [LE α] → [InfSet α] → InfSet (WithTop α)
-- Init.MetaTypes
/-- Configuration for the `extract_lets` tactic.
 -/
Lean.Meta.ExtractLetsConfig : Type
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.ground_eq_empty_iff : ∀ {α : Type u_1} {M : Matroid α}, M.E = ∅ ↔ M = Matroid.emptyOn α
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.stacksTagParser.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.commAlgEquiv_single_zero_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (m : M),
  (AddMonoidAlgebra.commAlgEquiv R) (AddMonoidAlgebra.single 0 (AddMonoidAlgebra.single m 1)) =
    AddMonoidAlgebra.single m 1
-- Init.PropLemmas
Decidable.imp_or' : ∀ {b : Prop} {a : Sort u_1} {c : Prop} [Decidable b], (∀ (a : a), b ∨ c) ↔ (∀ (a : a), b) ∨ ∀ (a : a), c
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles_assoc : ∀ {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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₀)
      (CategoryTheory.CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) h) =
    CategoryTheory.CategoryStruct.comp (X.δ f₁ f₂ n₀ n₁ hn₁) h
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.MonadGetStruct.mk : {m : Type → Type} → m Lean.Meta.Grind.Arith.Linear.Struct → Lean.Meta.Grind.Arith.Linear.MonadGetStruct m
-- Mathlib.Order.SuccPred.Relation
/-- `(n, m)` is in the reflexive-transitive closure of `~` if `i ~ succ i` and `succ i ~ i`
for all `i` between `n` and `m`.  -/
reflTransGen_of_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → Relation.ReflTransGen r n m
-- Mathlib.Data.Nat.PrimeFin
Nat.Prime.primeFactors : ∀ {p : ℕ}, Nat.Prime p → p.primeFactors = {p}
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.IsSeparated (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsSeparated f
-- Plausible.Sampleable
Plausible.NoShrink.get : {α : Type u_1} → Plausible.NoShrink α → α
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffOn.smulRight : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {n : WithTop ℕ∞} {f : E → StrongDual 𝕜 F}
  {g : E → G},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (fun x => ContinuousLinearMap.smulRight (f x) (g x)) s
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_top : ∀ {α : Type u_1} [inst : CoheytingAlgebra α], Coheyting.boundary ⊤ = ⊥
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_of_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → s ∪ t \ s = t
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.pentagon : ∀ {C : Type u} {W X Y Z : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    (((CategoryTheory.FreeMonoidalCategory.Hom.α_hom W X Y).whiskerRight Z).comp
      ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom W (X.tensor Y) Z).comp
        (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft W (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z))))
    ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom (W.tensor X) Y Z).comp
      (CategoryTheory.FreeMonoidalCategory.Hom.α_hom W X (Y.tensor Z)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insertMany!_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} {fallback : β k'},
      List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
        ⟨k, v⟩ ∈ l → (↑(t.insertMany! l)).getD k' fallback = cast ⋯ v
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofInt_of_two_pow_numBits : ∀ {n : ℤ},
  -2 ^ (System.Platform.numBits - 1) ≤ n →
    n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofInt n).toNatClampNeg = n.toNat
-- Mathlib.Algebra.Group.Commute.Units
IsAddUnit.of_nsmul_eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] {n : ℕ} {a : M}, n • a = 0 → n ≠ 0 → IsAddUnit a
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.instRespectsIsoArrowArrow : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.RespectsIso],
  W.arrow.RespectsIso
-- Std.Sync.Channel
/-- Precondition: The channel must not be closed.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.trySend' : {α : Type} → α → Std.AtomicT (Std.CloseableChannel.Zero.State✝ α) BaseIO Bool
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearMap.setIntegral_compLp : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  {𝕜' : Type u_7} [inst_1 : RCLike 𝕜] [inst_2 : RCLike 𝕜'] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜' F] {p : ENNReal} [inst_7 : NormedSpace ℝ F] {σ : 𝕜 →+* 𝕜'}
  [inst_8 : RingHomIsometric σ] (L : E →SL[σ] F) (φ : ↥(MeasureTheory.Lp E p μ)) {s : Set X},
  MeasurableSet s → ∫ (x : X) in s, ↑↑(L.compLp φ) x ∂μ = ∫ (x : X) in s, L (↑↑φ x) ∂μ
-- Init.Data.SInt.Lemmas
ISize.neg_zero : -0 = 0
-- Mathlib.RingTheory.Valuation.Basic
Valuation.instFunLike : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : Ring R] → [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] → FunLike (Valuation R Γ₀) R Γ₀
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.costar_snd : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) (u : U) (a : Quiver.Costar u),
  (φ.costar u a).snd = φ.map a.snd
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.relation_mem_ker : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) (i : σ), P.relation i ∈ P.ker
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.notMem_right : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → v ∉ t
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cycles₁_eq_top_of_isTrivial : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [A.IsTrivial],
  groupHomology.cycles₁ A = ⊤
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.coe_iSup : ∀ {α : Type u_1} {ι : Sort u_3} (f : ι → MeasureTheory.OuterMeasure α), ⇑(⨆ i, f i) = ⨆ i, ⇑(f i)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- An injective measurable function from a standard Borel space to a
countably separated measurable space is a measurable embedding.  -/
Measurable.measurableEmbedding : ∀ {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace α] {f : γ → α} [MeasurableSpace.CountablySeparated α]
  [inst_2 : MeasurableSpace γ] [StandardBorelSpace γ], Measurable f → Function.Injective f → MeasurableEmbedding f
-- Mathlib.Algebra.Group.End
Equiv.mul_swap_eq_iff : ∀ {α : Type u_4} [inst : DecidableEq α] {i j : α} {σ : Equiv.Perm α}, σ * Equiv.swap i j = σ ↔ i = j
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprRUsage : Repr Std.Internal.UV.System.RUsage
-- Mathlib.Order.Category.LinOrd
LinOrd.Iso.mk_hom : ∀ {α β : LinOrd} (e : ↑α ≃o ↑β), (LinOrd.Iso.mk e).hom = LinOrd.ofHom ↑e
-- Mathlib.Data.Finset.Card
/-- See also `card_bij`.
TODO: consider deprecating, since this has been unused in mathlib for a long time and is just a
special case of `card_bij`.
 -/
Finset.card_eq_of_bijective : ∀ {α : Type u_1} {s : Finset α} {n : ℕ} (f : (i : ℕ) → i < n → α),
  (∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a) →
    (∀ (i : ℕ) (h : i < n), f i h ∈ s) → (∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) → s.card = n
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- If the left addition of `g` is ergodic
with respect to a measure which is positive on nonempty open sets,
then the integer multiples of `g` are dense in `G`.  -/
DenseRange.zsmul_of_ergodic_add_left : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [OpensMeasurableSpace G] {μ : MeasureTheory.Measure G} [μ.IsOpenPosMeasure] {g : G},
  Ergodic (fun x => g + x) μ → DenseRange fun x => x • g
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
minimalPrimes_eq_minimals : ∀ {R : Type u_1} [inst : CommSemiring R], minimalPrimes R = {x | Minimal Ideal.IsPrime x}