mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.imageFactorisation_F_m : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  (f : X ⟶ Y) (x : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.imageFactorisation f x).F.m = ((CategoryTheory.Subobject.exists f).obj x).arrow
-- Mathlib.Data.Int.Log
Int.log_of_one_le_right : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (b : ℕ) {r : R},
  1 ≤ r → Int.log b r = ↑(Nat.log b ⌊r⌋₊)
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe : ∀ {n : ℕ} [inst : NeZero n] {K : Type u} {L : Type v} [inst_1 : Field K] [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (C : Type u_1)
  [inst_6 : CommRing C] [inst_7 : IsDomain C] [inst_8 : Algebra K C] (hirr : Irreducible (Polynomial.cyclotomic n K))
  (φ' : L →ₐ[K] C), ↑((hζ.embeddingsEquivPrimitiveRoots C hirr) φ') = φ' ζ
-- Mathlib.Analysis.Asymptotics.TVS
Filter.HasBasis.isLittleOTVS_iff : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} {ιE : Sort u_7}
  {ιF : Sort u_8} {pE : ιE → Prop} {pF : ιF → Prop} {sE : ιE → Set E} {sF : ιF → Set F},
  (nhds 0).HasBasis pE sE →
    (nhds 0).HasBasis pF sF →
      (f =o[𝕜; l] g ↔
        ∀ (i : ιE),
          pE i →
            ∃ j, pF j ∧ ∀ (ε : NNReal), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ ↑ε * egauge 𝕜 (sF j) (g x))
-- Batteries.Data.List.Lemmas
List.idxsOf_eq_nil_iff : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α], List.idxsOf x xs s = [] ↔ ∀ y ∈ xs, (y == x) = false
-- Init.Data.Nat.Div.Basic
/-- An induction principle customized for reasoning about the recursion pattern of `Nat.mod`.
 -/
Nat.mod.inductionOn : {motive : ℕ → ℕ → Sort u} →
  (x y : ℕ) →
    ((x y : ℕ) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) →
      ((x y : ℕ) → ¬(0 < y ∧ y ≤ x) → motive x y) → motive x y
-- Mathlib.Algebra.Module.ULift
ULift.moduleEquiv_apply : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (self : ULift.{w, v} M), ULift.moduleEquiv self = self.down
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.preimage_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F), G.preimage (CategoryTheory.CategoryStruct.id F) = G
-- Mathlib.Data.Seq.Basic
Stream'.Seq.get?_zip : ∀ {α : Type u} {β : Type v} (s : Stream'.Seq α) (t : Stream'.Seq β) (n : ℕ),
  (s.zip t).get? n = Option.map₂ Prod.mk (s.get? n) (t.get? n)
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.support.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] (μ : MeasureTheory.Measure X),
  μ.support = {x | ∃ᶠ (u : Set X) in (nhds x).smallSets, 0 < μ u}
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.isGE_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ),
  X.IsGE n ↔ ∀ i < n, CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor C i).obj X)
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.FindModelResult.mk.sizeOf_spec : ∀ (model : Lean.Expr) (normedSpaceInfo? : Option Manifold.Elab.NormedSpaceInfo),
  sizeOf { model := model, normedSpaceInfo? := normedSpaceInfo? } = 1 + sizeOf model + sizeOf normedSpaceInfo?
-- Aesop.Tree.TreeM
Aesop.mkInitialTree : Lean.MVarId → Aesop.LocalRuleSet → Aesop.BaseM Aesop.Tree
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.exists_eq_mul_self : ∀ {k : Type u} [inst : Field k] [IsSepClosed k] (x : k) [h2 : NeZero 2], ∃ z, x = z * z
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_mul_X_pow : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] (n : ℕ),
  (p * Polynomial.X ^ n).smeval x = p.smeval x * x ^ n
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.get_eq_of_lt_skipWhile_char : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos}, pos ≤ pos' → ∀ (h₂ : pos' < pos.skipWhile c), pos'.get ⋯ = c
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.pullback_χ_obj_mk_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (𝒞 : CategoryTheory.Subobject.Classifier C) {Z X : C} (i : Z ⟶ X) [inst_2 : CategoryTheory.Mono i],
  (CategoryTheory.Subobject.pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject = CategoryTheory.Subobject.mk i
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.Int.toNat.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (a : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.negSucc a with
    | Int.ofNat n => h_1 n
    | Int.negSucc a => h_2 a) =
    h_2 a
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W)
  (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Q Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Q W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inr)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (hP.desc h k w)) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q k) h_1
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.get : ∀ {l m₁ : List Char} {c : Char} {m₂ r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l (m₁ ++ c :: m₂) r s → s.get { byteIdx := String.utf8Len m₁ } = c
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_of_characteristic : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [h : H.Characteristic], H.Normal
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.natCast_toNat_le : ∀ (a : Cardinal.{u_1}), ↑(Cardinal.toNat a) ≤ a
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.isStrongTriangulatedGenerator_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.IsStrongTriangulatedGenerator ↔ ∃ n, P.triangEnvelopeIter n = ⊤
-- Mathlib.Topology.Maps.Proper.Basic
/-- A proper map `f : X → Y` is **universally closed**: for any topological space `Z`, the map
`Prod.map f id : X × Z → Y × Z` is closed. We will prove in `isProperMap_iff_universally_closed`
that proper maps are exactly continuous maps which have this property, but this result should be
easier to use because it allows `Z` to live in any universe.  -/
IsProperMap.universally_closed : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} (Z : Type u_6)
  [inst_2 : TopologicalSpace Z], IsProperMap f → IsClosedMap (Prod.map f id)
-- Mathlib.Algebra.Order.SuccPred
SuccAddOrder.mk : {α : Type u_1} →
  [inst : Preorder α] →
    [inst_1 : Add α] →
      [inst_2 : One α] → [toSuccOrder : SuccOrder α] → (∀ (x : α), SuccOrder.succ x = x + 1) → SuccAddOrder α
-- Std.Async.Signal
Std.Async.Signal.Waiter.native : Std.Async.Signal.Waiter → Std.Internal.UV.Signal
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- To check a polynomial over a field is irreducible, it suffices to check only for
divisors that have smaller degree.

See also: `Polynomial.Monic.irreducible_iff_natDegree`.
 -/
Polynomial.irreducible_iff_degree_lt : ∀ {R : Type u} [inst : Field R] (p : Polynomial R),
  p ≠ 0 → ¬IsUnit p → (Irreducible p ↔ ∀ (q : Polynomial R), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q)
-- Mathlib.Logic.Small.Set
small_biInter' : ∀ {α : Type u1} {ι : Type u4} (s : Set ι) [Nonempty ↑s] (f : (i : ι) → i ∈ s → Set α)
  [∀ (i : ι) (hi : i ∈ s), Small.{u, u1} ↑(f i hi)], Small.{u, u1} ↑(⋂ i, ⋂ (hi : i ∈ s), f i hi)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_eraseListₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {l : List α},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(m.eraseListₘ l)).buckets).Perm
      (Std.Internal.List.eraseList (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)),
  (∀ (i : ι),
      CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (f i) (CategoryTheory.CategoryStruct.id (X i))
          (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
        CategoryTheory.CategoryStruct.id
          ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (obj i))) →
    ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i)
      (hg :
        autoParam (CategoryTheory.CategoryStruct.comp g (f i) = q)
          CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self'._auto_1),
      CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q g g hg hg =
        CategoryTheory.CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (obj i))
-- Mathlib.SetTheory.ZFC.Rank
/-- For the rank of `⋃₀ x`, we only have `rank (⋃₀ x) ≤ rank x ≤ rank (⋃₀ x) + 1`.

This inequality is split into `rank_sUnion_le` and `le_succ_rank_sUnion`.  -/
PSet.rank_sUnion_le : ∀ (x : PSet.{u_1}), (⋃₀ x).rank ≤ x.rank
-- Mathlib.FieldTheory.KummerExtension
X_pow_sub_C_irreducible_of_odd : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  Odd n →
    ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (Polynomial.X ^ n - Polynomial.C a)
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `FunLike.coeAddMonoidHom_apply`. -/
ProbabilityTheory.Kernel.coeAddHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β] (f : F), (FunLike.coeAddMonoidHom F α β) f = ⇑f
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.adjunction_counit : ∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P],
  (CompHausLike.LocallyConstant.adjunction P hs).counit = CompHausLike.LocallyConstant.counit P hs
-- Lean.Parser.Types
/-- Return character after position `pos`  -/
Lean.Parser.InputContext.getNext : Lean.Parser.InputContext → String.Pos.Raw → Char
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec_nil : ∀ {β : Type u_1} {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {f : β → Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl × β)} {b : β},
  f b = none →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec f b =
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Algebra.Order.Pi
Function.const_le_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : Preorder α] {a : α} [Nonempty β],
  Function.const β a ≤ 1 ↔ a ≤ 1
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_sub_left : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (a : G),
  IsOpenMap fun x => a - x
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.precomp : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι' : Type u_6} {g : ι' → ι}
  {β : ι → Type u_7} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  Function.Injective g → ProbabilityTheory.iIndepFun f μ → ProbabilityTheory.iIndepFun (fun i => f (g i)) μ
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Convert the heap to an array in increasing order.  -/
Batteries.BinomialHeap.toArray : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → Array α
-- Mathlib.Data.Sign.Defs
SignType.neg_eq_self_iff : ∀ {a : SignType}, -a = a ↔ a = 0
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comm₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂),
  CategoryTheory.CategoryStruct.comp sq₁.f₁₃ self.τ₃ = CategoryTheory.CategoryStruct.comp self.τ₁ sq₂.f₁₃
-- Mathlib.Analysis.Complex.Norm
Complex.dist_mk : ∀ (x₁ y₁ x₂ y₂ : ℝ), dist { re := x₁, im := y₁ } { re := x₂, im := y₂ } = √((x₁ - x₂) ^ 2 + (y₁ - y₂) ^ 2)
-- Init.Data.SInt.Lemmas
Int8.toUInt8_le : ∀ {a b : Int8}, 0 ≤ a → a ≤ b → a.toUInt8 ≤ b.toUInt8
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHom_single : ∀ {R : Type u_1} {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Monoid M] [inst_2 : Monoid N]
  (f : M →* N) (m : M) (r : R),
  (MonoidAlgebra.mapDomainBialgHom R f) (MonoidAlgebra.single m r) = MonoidAlgebra.single (f m) r
-- Mathlib.Order.Basic
/-- **Alias** of `lt_or_eq_of_le`. -/
LE.le.lt_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → a < b ∨ a = b
-- Mathlib.Analysis.Convex.Between
left_mem_affineSegment : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] (x y : P), x ∈ affineSegment R x y
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.mk.injEq : ∀ {G : Type u_6} [inst : Group G] (toGroupSeminorm : GroupSeminorm G)
  (eq_one_of_map_eq_zero' : ∀ (x : G), toGroupSeminorm.toFun x = 0 → x = 1) (toGroupSeminorm_1 : GroupSeminorm G)
  (eq_one_of_map_eq_zero'_1 : ∀ (x : G), toGroupSeminorm_1.toFun x = 0 → x = 1),
  ({ toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' } =
      { toGroupSeminorm := toGroupSeminorm_1, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'_1 }) =
    (toGroupSeminorm = toGroupSeminorm_1)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.nonempty_uIcc : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, (Set.uIcc a b).Nonempty
-- Mathlib.Order.Interval.Set.Image
Set.preimage_subtype_val_Ici : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a : { x // p x }), Subtype.val ⁻¹' Set.Ici ↑a = Set.Ici a
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Second.Offset` to a `PlainDateTime`, adjusting the minute, hour, and date if the seconds overflow.
 -/
Std.Time.PlainDateTime.addSeconds : Std.Time.PlainDateTime → Std.Time.Second.Offset → Std.Time.PlainDateTime
-- Mathlib.Algebra.Group.Center
Set.center.eq_1 : ∀ (M : Type u_1) [inst : Mul M], Set.center M = {z | IsMulCentral z}
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The information for computing the keys of a subexpression.  -/
Lean.Meta.RefinedDiscrTree.ExprInfo : Type
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℤ_[p]}, x ≠ 0 → y ≠ 0 → (x * y).valuation = x.valuation + y.valuation
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.order_log : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] [Nontrivial A], (PowerSeries.log A).order = 1
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_mul_add_pos : ∀ {b v : Ordinal.{u_1}}, b ≠ 0 → ∀ (u : Ordinal.{u_1}), v ≠ 0 → ∀ (w : Ordinal.{u_1}), 0 < b ^ u * v + w
-- Lean.Environment
Lean.PersistentEnvExtensionDescr.toPersistentEnvExtensionDescrCore : {α β σ : Type} → Lean.PersistentEnvExtensionDescr α β σ → Lean.PersistentEnvExtensionDescrCore α β σ
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSemisimple.isSimple_of_isAtom : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSemisimple R L] (I : LieIdeal R L), IsAtom I → LieAlgebra.IsSimple R ↥I
-- Mathlib.NumberTheory.ZetaValues
contDiff_bernoulliFun : ∀ (k : ℕ), ContDiff ℝ ⊤ (bernoulliFun k)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofIsInitial_pt : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj X₃)]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj Y₃)]
  (h : CategoryTheory.Limits.IsInitial X₁),
  (CategoryTheory.Functor.PullbackObjObj.ofIsInitial G f₁ f₃ h).pt = (G.obj (Opposite.op Y₁)).obj Y₃
-- Mathlib.Order.SymmDiff
bihimp_compl_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), bihimp a aᶜ = ⊥
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_lt_sum_of_subset : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M}
  {s t : Finset ι} [AddLeftStrictMono M],
  s ⊆ t → ∀ {i : ι}, i ∈ t → i ∉ s → 0 < f i → (∀ j ∈ t, j ∉ s → 0 ≤ f j) → ∑ j ∈ s, f j < ∑ j ∈ t, f j
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesLimitsOfSize.CreatesLimitsOfShape : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {F : CategoryTheory.Functor C D} →
          [self : CategoryTheory.CreatesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] →
            {J : Type w} → [inst_2 : CategoryTheory.Category.{w', w} J] → CategoryTheory.CreatesLimitsOfShape J F
-- Mathlib.Order.KrullDimension
Order.height_coe_withBot : ∀ {α : Type u_1} [inst : Preorder α] (x : α), Order.height ↑x = Order.height x + 1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.StrongCore.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η : F ⟶ G} →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (η.app a) (G.map f) ≅
                      CategoryTheory.CategoryStruct.comp (F.map f) (η.app b)) →
              autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
                  CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom._autoParam →
                CategoryTheory.Lax.LaxTrans.StrongCore η
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections],
  AddCommGrpCat.limitCone F =
    CategoryTheory.liftLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)))
-- Init.Data.Rat.Lemmas
Rat.lt_neg_iff : ∀ {a b : ℚ}, a < -b ↔ b < -a
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cocone on `F.unop : J ⥤ C`.  -/
CategoryTheory.Limits.coconeUnopOfCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} → CategoryTheory.Limits.Cone F → CategoryTheory.Limits.Cocone F.unop
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.Q.exact : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] {a b : α × α},
  Lean.Grind.IntModule.OfNatModule.Q.mk a = Lean.Grind.IntModule.OfNatModule.Q.mk b →
    Lean.Grind.IntModule.OfNatModule.r α a b
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0)
  (n : ℕ),
  ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
    { X₁ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
      X₃ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
      g := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_tail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.tail.length = p.length - 1
-- Mathlib.Analysis.Convex.Basic
Submodule.Convex.semilinear_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {𝕜' : Type u_5} [inst_4 : Semiring 𝕜'] {σ : 𝕜' →+* 𝕜} [inst_5 : RingHomSurjective σ]
  {F' : Type u_6} [inst_6 : AddCommMonoid F'] [inst_7 : Module 𝕜' F'] (f : F' →ₛₗ[σ] E), Convex 𝕜 ↑f.range
-- Init.Data.Order.LemmasExtra
Std.IsLinearPreorder.of_ord : ∀ {α : Type u} [inst : LE α] [inst_1 : Ord α] [Std.LawfulOrderOrd α] [Std.TransOrd α], Std.IsLinearPreorder α
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.HasCardinalFilteredColimits C Cardinal.aleph0 ↔ CategoryTheory.Limits.HasFilteredColimits C
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δ_pOpcycles : ∀ {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 : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_pOpcycles._auto_1),
  CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (X.pOpcycles f g n₁) = 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace),
  CategoryTheory.inv (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f U) =
    CategoryTheory.CategoryStruct.comp
      (f.hom.c.app (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U)))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_odd : ∀ (n : ℤ), Odd n → n.negOnePow = -1