mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- **Alias** of `CategoryTheory.Mod.trivialAction`.

---

Every object is a module over a monoid object via the trivial action.  -/
CategoryTheory.Mod_.trivialAction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → (M : CategoryTheory.Mon C) → C → CategoryTheory.Mod C M.X
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.Hom.ext_zero_left : ∀ {n : SimplexCategory} (f g : { len := 0 } ⟶ n),
  autoParam ((SimplexCategory.Hom.toOrderHom f) 0 = (SimplexCategory.Hom.toOrderHom g) 0)
      SimplexCategory.Hom.ext_zero_left._auto_1 →
    f = g
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.ofRingCon.sizeOf_spec : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : SizeOf R] (ringCon : RingCon R),
  sizeOf { ringCon := ringCon } = 1 + sizeOf ringCon
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : H.IsCartanSubalgebra] [IsNoetherian R L], LieAlgebra.zeroRootSubalgebra R L H = H
-- Mathlib.NumberTheory.Padics.Complex
/-- The `ℝ≥0`-valued norm on `ℂ_[p]` extends the norm on `ℚ_[p]`.  -/
PadicComplex.nnnorm_extends' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℚ_[p]), ‖↑((algebraMap ℚ_[p] (PadicAlgCl p)) x)‖₊ = ‖x‖₊
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsNonneg.smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Preorder R] [PosMulMono R] {B : LinearMap.BilinForm R M} {c : R}, B.IsNonneg → 0 ≤ c → (c • B).IsNonneg
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.map_mul : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β) (a b : α),
  f (a * b) = f a * f b
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator.step : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.RxoIterator α β → Std.IterStep (Std.IterM Id ((a : α) × β a)) ((a : α) × β a)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod_hom_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop
      CategoryTheory.Limits.prod.fst =
    CategoryTheory.Limits.coprod.inl.unop
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.Const.get? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → Option β
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_Except : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u_1} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε Std.Do.PostShape.pure)} [inst : Monad m] [Std.Do.WPMonad m ps],
  ⦃Q.2.1 e⦄ MonadExceptOf.throw e ⦃Q⦄
-- Init.Data.Int.Lemmas
Int.mul_left_comm : ∀ (a b c : ℤ), a * (b * c) = b * (a * c)
-- Std.Data.TreeMap.Raw.Basic
/-- Folds the given monadic function over the mappings in the map in descending order.  -/
Std.TreeMap.Raw.foldrM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (α → β → δ → m δ) → δ → Std.TreeMap.Raw α β cmp → m δ
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsPrestackFor.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {S : C}
  {R : CategoryTheory.Presieve S}, Nonempty (F.toDescentData fun f => f.obj.hom).FullyFaithful → F.IsPrestackFor R
-- Lean.Level
Lean.Level.PP.Context.lIndex? : Lean.Level.PP.Context → Lean.LMVarId → Option ℕ
-- Mathlib.Analysis.Convex.Quasiconvex
Convex.quasiconvexOn_of_convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LE β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  Convex 𝕜 s → (∀ (r : β), Convex 𝕜 {x | f x ≤ r}) → QuasiconvexOn 𝕜 s f
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.self_trans_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  h.trans h.symm = Homeomorph.refl X
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL.match_7.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size → Sort u_3)
  (r : Std.DTreeMap.Internal.Impl α β) (hrb : r.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size)
  (h_1 :
    (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hrb hlr)
  (h_2 :
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l_1 r : Std.DTreeMap.Internal.Impl α β) →
            (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r) hrb hlr)
  (hrb_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr_1 : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size),
  r = Std.DTreeMap.Internal.Impl.leaf →
    hrb ≍ hrb_1 →
      hlr ≍ hlr_1 →
        (match r, hrb, hlr with
          | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => h_1 hrb hlr
          | Std.DTreeMap.Internal.Impl.inner rs k v l_1 r, hrb, hlr => h_2 rs k v l_1 r hrb hlr) ≍
          h_1 hrb_1 hlr_1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (a c : M) (b d : ↥S),
  AddLocalization.mk a b + AddLocalization.mk c d = AddLocalization.mk (a + c) (b + d)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.ext : ∀ {R : Type u_1} {inst : CommRing R} {x y : IsDedekindDomain.HeightOneSpectrum R}, x.asIdeal = y.asIdeal → x = y
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.rootForm_self_sum_of_squares : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (x : M), IsSumSq ((P.RootForm x) x)
-- Lean.Util.Diff
/-- How many times the element occurs in the right array  -/
Lean.Diff.Histogram.Entry.rightCount : {α : Type u} → {lsize rsize : ℕ} → Lean.Diff.Histogram.Entry α lsize rsize → ℕ
-- Init.Data.Vector.Lemmas
Vector.any_push : ∀ {α : Type u_1} {n : ℕ} {as : Vector α n} {a : α} {p : α → Bool}, (as.push a).any p = (as.any p || p a)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Filter.totallyBounded_comap : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {F : Filter β},
  IsUniformInducing f → F.TotallyBounded → (Filter.comap f F).TotallyBounded
-- Mathlib.Computability.Language
Language.notMem_zero : ∀ {α : Type u_1} (x : List α), x ∉ 0
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorZero_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n : ℤ),
  ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
-- Mathlib.Algebra.Star.Basic
/-- A additive monoid endowed with `star` is an additive star monoid if it admits an injective map
that preserves `star` and `+` to an additive star monoid.  See note [reducible non-instances].  -/
Function.Injective.starAddMonoid : {R : Type u} →
  {S : Type v} →
    (f : R → S) →
      [inst : Star R] →
        [inst_1 : AddMonoid R] →
          [inst_2 : AddMonoid S] →
            [inst_3 : StarAddMonoid S] →
              Function.Injective f →
                (∀ (x : R), f (star x) = star (f x)) → (∀ (x y : R), f (x + y) = f x + f y) → StarAddMonoid R
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
/-- In a normed vector space `E`, there can be no satellite configuration with `multiplicity E + 1`
points and the parameter `goodτ E`. This will ensure that in the inductive construction to get
the Besicovitch covering families, there will never be more than `multiplicity E` nonempty
families.  -/
Besicovitch.isEmpty_satelliteConfig_multiplicity : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  IsEmpty (Besicovitch.SatelliteConfig E (Besicovitch.multiplicity E) (Besicovitch.goodτ E))
-- Init.Data.String.Basic
String.size_bytes : ∀ {s : String}, s.toByteArray.size = s.utf8ByteSize
-- Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
/-- Given a pair of objects which are sent by a fully faithful functor to a pair of objects
with an exact pairing, we get an exact pairing.
 -/
CategoryTheory.ExactPairing.ofFullyFaithful : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] →
                [F.Full] →
                  [F.Faithful] →
                    (X Y : C) → [CategoryTheory.ExactPairing (F.obj X) (F.obj Y)] → CategoryTheory.ExactPairing X Y
-- Mathlib.AlgebraicGeometry.Scheme
/-- forgetful functor to `TopCat` is the same as coercion  -/
AlgebraicGeometry.Scheme.forgetToTop_obj_eq_coe : AlgebraicGeometry.Scheme → Prop
-- Mathlib.Tactic.NormNum.Inv
/-- Helper function to synthesize a typed `CharZero α` expression given `Ring α`, if it exists.  -/
Mathlib.Meta.NormNum.inferCharZeroOfRing? : {u : Lean.Level} →
  {α : Q(Type u)} →
    (_i : autoParam Q(Ring «$α») Mathlib.Meta.NormNum.inferCharZeroOfRing?._auto_1) →
      Lean.MetaM (Option Q(CharZero «$α»))
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.EvalTacticFailure.mk.injEq : ∀ (exception : Lean.Exception) (state : Lean.Elab.Tactic.Grind.SavedState) (exception_1 : Lean.Exception)
  (state_1 : Lean.Elab.Tactic.Grind.SavedState),
  ({ exception := exception, state := state } = { exception := exception_1, state := state_1 }) =
    (exception = exception_1 ∧ state = state_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₁_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.a₁ = 1
-- Mathlib.CategoryTheory.NatTrans
/-- `NatTrans.id F` is the identity natural transformation on a functor `F`.  -/
CategoryTheory.NatTrans.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C D) → CategoryTheory.NatTrans F F
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_neg_iff_infiniteNeg_inv : ∀ {x : ℝ*}, x⁻¹.InfiniteNeg ↔ x.Infinitesimal ∧ x < 0
-- Mathlib.Data.Fin.SuccPred
Fin.le_pred_iff : ∀ {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0), j ≤ i.pred hi ↔ j.succ ≤ i
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The "canonical" valuation associated to a valuative relation.  -/
ValuativeRel.valuation : (R : Type u_2) → [inst : Ring R] → [inst_1 : ValuativeRel R] → Valuation R (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_coe : ∀ {S : AlgebraicGeometry.Scheme} {Ω : Type u} [inst : Field Ω] [inst_1 : IsSepClosed Ω]
  (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) {s₀ : ↥S} (hs₀ : s default = s₀) {X : S.Etale}
  (t : (AlgebraicGeometry.Scheme.pointSmallEtale s).fiber.obj X),
  ↑(AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage s hs₀ t) = (CategoryTheory.Over.Hom.left t) default
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.isLocalHom_pullbackSnd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Semiring T] (f : R →+* T)
  (g : S →+* T) [IsLocalHom f], IsLocalHom (f.pullbackSnd g)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.pair_mul : ∀ {α : Type u_2} [inst : Mul α] (a b : α) (s : Set α), {a, b} * s = a • s ∪ b • s
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
GaloisConnection.l_ciSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {f : ι → α}, BddAbove (Set.range f) → l (⨆ i, f i) = ⨆ i, l (f i)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.tendsto_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α}
  {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β},
  la.HasBasis pa sa →
    lb.HasBasis pb sb → (Filter.Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib)
-- Mathlib.Topology.Order.MonotoneConvergence
isLUB_of_tendsto_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsDirectedOrder β] [Nonempty β] {f : β → α} {a : α},
  Monotone f → Filter.Tendsto f Filter.atTop (nhds a) → IsLUB (Set.range f) a
-- Mathlib.Tactic.IntervalCases
/-- Given `(z1, e1, p1)` a lower bound on `e` and `(z2, e2, p2)` an upper bound on `e`,
such that the distance between the bounds is negative, returns a proof of `False`.
 -/
Mathlib.Tactic.IntervalCases.Methods.inconsistentBounds : Mathlib.Tactic.IntervalCases.Methods →
  Mathlib.Tactic.IntervalCases.Bound →
    Mathlib.Tactic.IntervalCases.Bound →
      Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Control.Functor.Multivariate
TypeVec.append1.match_1.congr_eq_2 : ∀ {n : ℕ} (motive : Fin2 (n + 1) → Sort u_1) (x : Fin2 (n + 1)) (h_1 : (i : Fin2 n) → motive i.fs)
  (h_2 : Unit → motive Fin2.fz),
  x = Fin2.fz →
    (match x with
      | i.fs => h_1 i
      | Fin2.fz => h_2 ()) ≍
      h_2 ()
-- Std.Time.Date.Unit.Year
/-- Converts the `Year` offset to an `Int`.
 -/
Std.Time.Year.Offset.toInt : Std.Time.Year.Offset → ℤ
-- Mathlib.Data.List.Destutter
List.destutter.eq_1 : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (h : α) (l : List α),
  List.destutter R (h :: l) = List.destutter' R h l
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- The function `x ^ y` tends to `+∞` at `+∞` for any positive real `y`.  -/
tendsto_rpow_atTop : ∀ {y : ℝ}, 0 < y → Filter.Tendsto (fun x => x ^ y) Filter.atTop Filter.atTop
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPos_addNeg_eq_both : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  assignment.addNegAssignment.addPosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.neg : ∀ {G : Type u} [inst : AddGroup G] {B : AddGroupFilterBasis G} {U : Set G}, U ∈ B → ∃ V ∈ B, V ⊆ (fun x => -x) ⁻¹' U
-- Mathlib.Tactic.ModCases
/-- The first theorem we apply says that `∃ z, 0 ≤ z < n ∧ a ≡ z (mod n)`.
The actual mathematical content of the proof is here.
 -/
Mathlib.Tactic.ModCases.IntMod.onModCases_start : (p : Sort u_1) → (a : ℤ) → (n : ℕ) → Nat.ble 1 n = true → Mathlib.Tactic.ModCases.IntMod.OnModCases n a 0 p → p
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.mk.congr_simp : ∀ {G : Type u_6} [inst : AddGroup G] (toZeroHom toZeroHom_1 : ZeroHom G ℝ) (e_toZeroHom : toZeroHom = toZeroHom_1)
  (add_le_max' : ∀ (r s : G), toZeroHom.toFun (r + s) ≤ max (toZeroHom.toFun r) (toZeroHom.toFun s))
  (neg' : ∀ (r : G), toZeroHom.toFun (-r) = toZeroHom.toFun r),
  { toZeroHom := toZeroHom, add_le_max' := add_le_max', neg' := neg' } =
    { toZeroHom := toZeroHom_1, add_le_max' := ⋯, neg' := ⋯ }
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `cyclotomic n` is primitive.  -/
Polynomial.cyclotomic.isPrimitive : ∀ (n : ℕ) (R : Type u_1) [inst : CommRing R], (Polynomial.cyclotomic n R).IsPrimitive
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.locallyConnectedSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  LocallyConnectedSpace (TopologicalSpace.NonemptyCompacts α) ↔ LocallyConnectedSpace α
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.constantCoeff_log : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A], PowerSeries.constantCoeff (PowerSeries.log A) = 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isZero_truncLT_obj_of_isGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) [t.IsGE X n],
  CategoryTheory.Limits.IsZero ((t.truncLT n).obj X)
-- Init.Data.List.Attach
List.any_subtype : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → l.any f = l.unattach.any g
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulConst : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulConst k p) =
    ↑k * Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.Data.Sum.Order
Sum.Lex.inl_lt_inl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α}, toLex (Sum.inl a) < toLex (Sum.inl b) ↔ a < b
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
/-- Constructor for cycles of short complexes in a concrete category.  -/
CategoryTheory.ShortComplex.cyclesMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [inst_3 : CategoryTheory.HasForget₂ C Ab] →
              [inst_4 : CategoryTheory.Preadditive C] →
                [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] →
                  [(CategoryTheory.forget₂ C Ab).PreservesHomology] →
                    (S : CategoryTheory.ShortComplex C) →
                      [inst_7 : S.HasHomology] →
                        (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂)) →
                          (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.g)) x₂ = 0 →
                            ↑((CategoryTheory.forget₂ C Ab).obj S.cycles)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_eq_one : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α], G.ediam = 1 ↔ G = ⊤
-- Mathlib.Algebra.Algebra.Unitization
IsSelfAdjoint.inr : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarAddMonoid R] [inst_2 : Star A] {a : A},
  IsSelfAdjoint a → IsSelfAdjoint ↑a
-- Mathlib.NumberTheory.PrimesCongruentOne
/-- For any positive `k : ℕ` there exists an arbitrarily large prime `p` such that
`p ≡ 1 [MOD k]`.  -/
Nat.exists_prime_gt_modEq_one : ∀ {k : ℕ} (n : ℕ), k ≠ 0 → ∃ p, Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_eq_empty : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, s⁻¹ = ∅ ↔ s = ∅
-- Mathlib.Order.RelIso.Basic
/-- An increasing function is injective  -/
RelHom.injective_of_increasing : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous r] [Std.Irrefl s] (f : r →r s),
  Function.Injective ⇑f
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.upperBound?.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Option α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α) (y : α)
  (b : RBTree.RBNode α) (ub : Option α) (h_1 : (ub : Option α) → motive RBTree.RBNode.nil ub)
  (h_2 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) → (b : RBTree.RBNode α) → (ub : Option α) → motive (RBTree.RBNode.node c a y b) ub),
  (match RBTree.RBNode.node c a y b, ub with
    | RBTree.RBNode.nil, ub => h_1 ub
    | RBTree.RBNode.node c a y b, ub => h_2 c a y b ub) =
    h_2 c a y b ub
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.two_lt_lineCount : ∀ {P : Type u_1} (L : Type u_2) [inst : Membership P L] [Configuration.ProjectivePlane P L] [Finite P] [Finite L]
  (p : P), 2 < Configuration.lineCount L p
-- Mathlib.Order.Ideal
Order.IsIdeal.toIdeal.congr_simp : ∀ {P : Type u_1} [inst : LE P] {I I_1 : Set P} (e_I : I = I_1) (h : Order.IsIdeal I), h.toIdeal = ⋯.toIdeal
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_antitone : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x : E} {r : ℝ}
  {p q : Seminorm 𝕜 E}, q ≤ p → p.closedBall x r ⊆ q.closedBall x r
-- Mathlib.Algebra.Free
AddMagma.AssocRel.intro : ∀ {α : Type u} [inst : Add α] (x y z : α), AddMagma.AssocRel α (x + y + z) (x + (y + z))
-- Mathlib.Data.List.ProdSigma
List.sigma_cons : ∀ {α : Type u_1} {σ : α → Type u_3} (a : α) (l₁ : List α) (l₂ : (a : α) → List (σ a)),
  (a :: l₁).sigma l₂ = List.map (Sigma.mk a) (l₂ a) ++ l₁.sigma l₂
-- Init.Data.Vector.Lemmas
Vector.foldlM_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] {xs : Vector α n} {f : β → α → m β}
  {b : β}, Vector.foldlM f b xs.reverse = Vector.foldrM (fun x y => f y x) b xs