mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
cocone morphism from `t`.  -/
CategoryTheory.Limits.IsColimit : {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.Cocone F → Type (max (max u₁ u₃) v₃)
-- Mathlib.RingTheory.SimpleRing.DivisionRing
IsSimpleModule.obj_of_isEquivalence : ∀ {R : Type u_3} {S : Type u_4} [inst : Ring R] [inst_1 : Ring S]
  (e : CategoryTheory.Functor (ModuleCat R) (ModuleCat S)) [e.IsEquivalence] (M : ModuleCat R) [IsSimpleModule R ↑M],
  IsSimpleModule S ↑(e.obj M)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.size_eq_match_rci : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.Rxi.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [Std.Rxi.LawfulHasSize α],
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some next => next...*.size
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
/-- [Stacks Tag 0310](https://stacks.math.columbia.edu/tag/0310) ((3)) -/
Module.associatedPrimes.preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (R' : Type u_2) [inst_1 : CommRing R'] [inst_2 : Algebra R R']
  [hSR' : IsLocalization S R'] {M : Type u_3} {M' : Type u_4} [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  [inst_5 : AddCommGroup M'] [inst_6 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [inst_8 : Module R' M']
  [IsScalarTower R R' M'] [IsNoetherianRing R],
  Ideal.comap (algebraMap R R') ⁻¹' associatedPrimes R M = associatedPrimes R' M'
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  {X Y Z : C} (e : Y ⟶ Z) [CategoryTheory.IsIso e] (f : X ⟶ Y), P f → P (CategoryTheory.CategoryStruct.comp f e)
-- Mathlib.RingTheory.PiTensorProduct
Commute.tprod : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] [inst_2 : (i : ι) → Module R (A i)]
  [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)]
  {a₁ a₂ : (i : ι) → A i}, Commute a₁ a₂ → Commute ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (t.modify k f).isEmpty = false → (t.modify k f).minKey! = if cmp t.minKey! k = Ordering.eq then k else t.minKey!
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_fun_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, ∫ᶜ (x : E) in γ, -ω x = -∫ᶜ (x : E) in γ, ω x
-- Std.Sync.CancellationToken
Std.CancellationReason.custom.injEq : ∀ (msg msg_1 : String), (Std.CancellationReason.custom msg = Std.CancellationReason.custom msg_1) = (msg = msg_1)
-- Mathlib.Order.Bounds.Basic
bddAbove_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, BddAbove (Set.Ioo a b)
-- Lean.Meta.Diagnostics
Lean.Meta.collectAboveThreshold : {α : Type u_1} →
  [inst : BEq α] → [inst_1 : Hashable α] → Lean.PHashMap α ℕ → ℕ → (α → Bool) → (α → α → Bool) → Array (α × ℕ)
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements_eq : ∀ {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} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  {i : ι} {Z : CategoryTheory.Over (X i)} (g : Z ⟶ CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (X i)))
  ⦃j : ι'⦄ (a : Z.left ⟶ X' j)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp a (f' j) = CategoryTheory.CategoryStruct.comp Z.hom (f i))
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements_eq._auto_1✝),
  CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements✝ w φ i g ⋯ =
    CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ Z.hom a fac
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {v : β}, (k, v) ∈ Std.DTreeMap.Const.toArray t ↔ Std.DTreeMap.Const.get? t k = some v
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.readLspMessage : IO.FS.Stream → IO Lean.JsonRpc.Message
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.allM_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.allM p it = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' x => do
        let __do_lift ← p x
        if __do_lift.down = true then Std.IterM.allM p it' else pure { down := false }
      | Std.IterStep.skip it' => Std.IterM.allM p it'
      | Std.IterStep.done => pure { down := true }
-- Mathlib.Algebra.Ring.NegOnePow
Int.cast_negOnePow_natCast : ∀ (R : Type u_1) [inst : Ring R] (n : ℕ), ↑↑(↑n).negOnePow = (-1) ^ n
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- Negation in the `Language.ring.Structure` is the same as the negation given by the
`Neg` instance  -/
FirstOrder.Ring.CompatibleRing.funMap_neg : ∀ {R : Type u_2} {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R}
  [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 1 → R),
  FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc x = -x 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.lift_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : D ⟶ (CategoryTheory.Functor.const J).obj X) {X_1 Y : J} (f : X_1 ⟶ Y),
  (CategoryTheory.Over.lift D s).map f = CategoryTheory.Over.homMk (D.map f) ⋯
-- Init.Data.String.Basic
/-- Advances the position `p` `n` times.

If this would move `p` past the end of `s`, the result is `s.endPos`.
 -/
String.Pos.nextn : {s : String} → s.Pos → ℕ → s.Pos
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.of_measure_le_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {μ' : MeasureTheory.Measure α} {c : ENNReal},
  c ≠ ⊤ → μ' ≤ c • μ → ∀ {f : α → ε}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable f μ'
-- Mathlib.Data.Nat.Factorization.Basic
/-- Any nonzero natural number is the product of an odd part `m` and a power of
two `2 ^ k`.  -/
Nat.exists_eq_two_pow_mul_odd : ∀ {n : ℕ}, n ≠ 0 → ∃ k m, Odd m ∧ n = 2 ^ k * m
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
/-- A functor `LF : D ⥤ H` is a left derived functor of `F : C ⥤ H`
if it is equipped with a natural transformation `α : L ⋙ LF ⟶ F`
which makes it a right Kan extension of `F` along `L`,
where `L : C ⥤ D` is a localization functor for `W : MorphismProperty C`.  -/
CategoryTheory.Functor.IsLeftDerivedFunctor : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (LF : CategoryTheory.Functor D H) →
              {F : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (L.comp LF ⟶ F) → (W : CategoryTheory.MorphismProperty C) → [L.IsLocalization W] → Prop
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roc_eq_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toList[i]! = 0 ↔ (n - m).toNat ≤ i ∨ m + ↑i = -1
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'_submatrix : ∀ {R : Type u_1} [inst : CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5}
  [inst_1 : DecidableEq n] [inst_2 : Fintype n] [inst_3 : Fintype l] [inst_4 : DecidableEq l] (f₁ : m → k) (e₂ : n ≃ l)
  (M : Matrix k l R),
  Matrix.toLin' (M.submatrix f₁ ⇑e₂) = LinearMap.funLeft R R f₁ ∘ₗ Matrix.toLin' M ∘ₗ LinearMap.funLeft R R ⇑e₂.symm
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.constSMul_toEquiv : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [inst_3 : IsIsometricSMul G X] (c : G), (IsometryEquiv.constSMul c).toEquiv = MulAction.toPerm c
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `+` is an additive commutative semigroup, if it admits
a surjective map that preserves `+` from an additive commutative semigroup.  -/
Function.Injective.addCommMagma : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : AddCommMagma M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddCommMagma M₁
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_le_of_le_directed : ∀ {α : Type u_7} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Set α),
  s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → ∀ (t : Finset α), (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.floor.eq_1 : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (x : ι → ℕ)
  (i : ↑(IsProperLinearSet.basisSet✝ hs)),
  IsProperLinearSet.floor✝ hs x i =
    ⌊((IsProperLinearSet.basis✝ hs).repr (toRatVec✝ x - toRatVec✝ (IsProperLinearSet.base✝ hs))) i⌋
-- Mathlib.Order.Minimal
/-- If `P y` holds, and everything satisfying `P` is below `y`, then `y` is the unique maximal
element satisfying `P`.  -/
maximal_iff_eq : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : PartialOrder α],
  P y → (∀ ⦃x : α⦄, P x → x ≤ y) → (Maximal P x ↔ x = y)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Given a diagram
```
a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S
```
such that `φ` is strongly Cartesian, and morphisms `ψ ψ' : a' ⟶ a` such that
`g ≫ ψ = φ' = g ≫ ψ'`. Then we have that `ψ = ψ'`.  -/
CategoryTheory.Functor.IsStronglyCartesian.ext : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮}
  {a' : 𝒳} (g : R' ⟶ R) {ψ ψ' : a' ⟶ a} [p.IsHomLift g ψ] [p.IsHomLift g ψ'],
  CategoryTheory.CategoryStruct.comp ψ φ = CategoryTheory.CategoryStruct.comp ψ' φ → ψ = ψ'
-- Lean.Compiler.IR.Basic
Lean.IR.Expr : Type
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instBEqTag : BEq Mathlib.CrossRef.Tag
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.hom_inv_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C}
  (h : X ⟶ Z), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) h) = h
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.pairwise_toList_le : ∀ {α : Type u} {r : Std.Rio α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α] [inst_3 : Std.PRange.Least? α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_9 : Std.Rxo.IsAlwaysFinite α],
  List.Pairwise (fun a b => a ≤ b) r.toList
-- Mathlib.Data.Fin.Basic
/-- Assume `k = l` and `k' = l'`.
If two functions `Fin k → Fin k' → α` and `Fin l → Fin l' → α` are equal on each pair,
then they coincide (in the heq sense).  -/
Fin.heq_fun₂_iff : ∀ {α : Sort u_1} {k l k' l' : ℕ} (h : k = l) (h' : k' = l') {f : Fin k → Fin k' → α} {g : Fin l → Fin l' → α},
  f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
lebesgue_number_lemma_of_metric : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {s : Set α} {ι : Sort u_3} {c : ι → Set α},
  IsCompact s → (∀ (i : ι), IsOpen (c i)) → s ⊆ ⋃ i, c i → ∃ δ > 0, ∀ x ∈ s, ∃ i, Metric.ball x δ ⊆ c i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_q : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (assign : α → Bool)
  (lhs rhs : BitVec w) (n d : aig.RefVec w) (wn wr : ℕ) (q r : aig.RefVec w) (qbv rbv : BitVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
      (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
        (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
          ∀ (idx : ℕ) (hidx : idx < w),
            ⟦assign,
                { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig,
                  ref :=
                    (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).q.get idx
                      hidx }⟧ =
              (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Bound.0.SzemerediRegularity.Positivity.eps_pos : ∀ {ε : ℝ} {n : ℕ}, 100 ≤ 4 ^ n * ε ^ 5 → 0 < ε
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from commutative groups to types creates all limits.
 -/
CommGrpCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommGrpCat)
-- Init.Data.String.FindPos
/-- Obtains the largest valid position that is strictly less than the given byte position.
 -/
String.Slice.posLT : (s : String.Slice) → (offset : String.Pos.Raw) → 0 < offset → s.Pos
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
mem_compactlySupported : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ]
  {f : BoundedContinuousFunction α γ}, f ∈ compactlySupported α γ ↔ HasCompactSupport ⇑f
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.instSMulZeroClassOfDistribSMul : {M : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} → [inst : AddZeroClass A] → [inst_1 : AddZeroClass B] → [DistribSMul M B] → SMulZeroClass M (A →+ B)
-- Mathlib.LinearAlgebra.Ray
/-- The ray of `someVector`.  -/
Module.Ray.someVector_ray : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (x : Module.Ray R M), rayOfNeZero R x.someVector ⋯ = x
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.coe_id : ∀ (X : TopCat), ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : CategoryTheory.Cat) (x : CategoryTheory.Join C ↑D),
  ((CategoryTheory.Join.pseudofunctorRight C).mapId D).hom.toNatTrans.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)
-- Mathlib.Data.PFun
/-- Partial function extensionality  -/
PFun.ext' : ∀ {α : Type u_1} {β : Type u_2} {f g : α →. β},
  (∀ (a : α), a ∈ f.Dom ↔ a ∈ g.Dom) → (∀ (a : α) (p : a ∈ f.Dom) (q : a ∈ g.Dom), f.fn a p = g.fn a q) → f = g
-- Mathlib.Algebra.Order.Group.Synonym
toColex_div : ∀ {α : Type u_1} [inst : Div α] (a b : α), toColex (a / b) = toColex a / toColex b
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The centroid of a simplex is the `Finset.centroid` of the set of all its vertices.  -/
Affine.Simplex.centroid : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : DivisionRing k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → {n : ℕ} → Affine.Simplex k P n → P
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.AddMagmaCat.Hom.mk.sizeOf_spec : ∀ {A B : AddMagmaCat} (hom' : ↑A →ₙ+ ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Order.SymmDiff
symmDiff_left_injective : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a : α), Function.Injective fun x => symmDiff x a
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.val_le_val : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] {a b : AddUnits α}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.boundaryless : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_2} {H : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} (self : SingularManifold X k I),
  BoundarylessManifold I self.M
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.mem_cylinder : ∀ {A : Type u_1} {G : Type u_2} {U : Finset G} {x y : G → A},
  y ∈ SymbolicDynamics.FullShift.cylinder U x ↔ ∀ i ∈ U, y i = x i
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.content : Lean.VersoModuleDocs.DocContext✝ → Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)
-- Mathlib.Topology.Algebra.MulAction
instContinuousVAddForall : ∀ {M : Type u_1} [inst : TopologicalSpace M] {ι : Type u_5} {γ : ι → Type u_6}
  [inst_1 : (i : ι) → TopologicalSpace (γ i)] [inst_2 : (i : ι) → VAdd M (γ i)] [∀ (i : ι), ContinuousVAdd M (γ i)],
  ContinuousVAdd M ((i : ι) → γ i)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore_simplex : ∀ {m : ℕ} (k : Fin (m + 1)) (n : ℕ) (s : SSet.prodStdSimplex.pairingCore.Type₁ k n),
  (SSet.prodStdSimplex.pairingCore k n).simplex s = (s.x.cast ⋯).simplex
-- Lean.Data.DeclarationRange
Lean.instInhabitedDeclarationRanges : Inhabited Lean.DeclarationRanges
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBy_one : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Submodule.torsionBy R M 1 = ⊥
-- Mathlib.Analysis.MeanInequalities
/-- **Weighted Hölder inequality**.  -/
ENNReal.inner_le_weight_mul_Lp_of_nonneg : ∀ {ι : Type u} (s : Finset ι) {p : ℝ},
  1 ≤ p → ∀ (w f : ι → ENNReal), ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.image_add_right_Ico : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq α] (a b c : α),
  Finset.image (fun x => x + c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)
-- Lean.Elab.Match
Lean.Elab.Term.Discr.mk.injEq : ∀ (expr : Lean.Expr) (h? : Option Lean.Syntax) (expr_1 : Lean.Expr) (h?_1 : Option Lean.Syntax),
  ({ expr := expr, h? := h? } = { expr := expr_1, h? := h?_1 }) = (expr = expr_1 ∧ h? = h?_1)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instDistribMulAction : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        {ι : Type u_5} →
          [inst : Monoid R] →
            [inst_1 : Semiring A] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : TopologicalSpace N] →
                      [inst_6 : Module A M] →
                        [inst_7 : Module A N] →
                          [inst_8 : DistribMulAction R N] →
                            [ContinuousConstSMul R N] →
                              [SMulCommClass A R N] → [inst_11 : ContinuousAdd N] → DistribMulAction R (M [⋀^ι]→L[A] N)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_periodic : Function.Periodic Complex.exp (2 * ↑Real.pi * Complex.I)
-- Mathlib.Data.Set.Lattice
Set.nonempty_iInter₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α},
  (⋂ i, ⋂ j, s i j).Nonempty ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The element `.mk x s` in `ValueGroupWithZero R` is sent to `v x / v s` in the
image group of `v`.  -/
ValuativeRel.ValueGroupWithZero.embed_mk : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible] (x : R) (s : ↥(ValuativeRel.posSubmonoid R)),
  (ValuativeRel.ValueGroupWithZero.embed v) (ValuativeRel.ValueGroupWithZero.mk x s) =
    (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) x /
      (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) ↑s
-- Mathlib.Topology.Separation.Basic
continuousWithinAt_insert : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] {x y : X}
  {s : Set X} {f : X → Y}, ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
-- Mathlib.Analysis.Oscillation
/-- The oscillation within `D` of `f` at `x ∈ D` is 0 if and only if `ContinuousWithinAt f D x`.  -/
OscillationWithin.eq_zero_iff_continuousWithinAt : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : TopologicalSpace E] (f : E → F) {D : Set E} {x : E},
  x ∈ D → (oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x)
-- Mathlib.Topology.Instances.ENat
ContinuousWithinAt.enatSub : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f g : X → ℕ∞} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → f x ≠ ⊤ ∨ g x ≠ ⊤ → ContinuousWithinAt (fun x => f x - g x) s x
-- Mathlib.Algebra.Category.Ring.Basic
/-- Ring equivalences are isomorphisms in category of rings  -/
RingEquiv.toRingCatIso : {R S : Type u} → [inst : Ring R] → [inst_1 : Ring S] → R ≃+* S → (RingCat.of R ≅ RingCat.of S)