mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.comp_reflectsFiniteCoproducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsFiniteCoproducts F]
  [CategoryTheory.Limits.ReflectsFiniteCoproducts G], CategoryTheory.Limits.ReflectsFiniteCoproducts (F.comp G)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instCoeSortType.eq_1 : CommGrpCat.instCoeSortType = { coe := CommGrpCat.carrier }
-- Mathlib.Algebra.Free
FreeAddSemigroup.instMonad.eq_1 : FreeAddSemigroup.instMonad =
  { map := fun {α β} f x => (fun {α β} x f => (FreeAddSemigroup.lift f) x) x ((fun {α} => FreeAddSemigroup.of) ∘ f),
    pure := fun {α} => FreeAddSemigroup.of,
    seq := fun {α β} f x =>
      (fun {α β} x f => (FreeAddSemigroup.lift f) x) f fun y =>
        (fun {α β} x f => (FreeAddSemigroup.lift f) x) (x ()) ((fun {α} => FreeAddSemigroup.of) ∘ y),
    seqLeft := fun {α β} x y =>
      (fun {α β} x f => (FreeAddSemigroup.lift f) x) x fun a =>
        (fun {α β} x f => (FreeAddSemigroup.lift f) x) (y ()) fun x => (fun {α} => FreeAddSemigroup.of) a,
    seqRight := fun {α β} x y => (fun {α β} x f => (FreeAddSemigroup.lift f) x) x fun x => y (),
    bind := fun {α β} x f => (FreeAddSemigroup.lift f) x }
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.endsWith_bool_eq_false_iff_get : ∀ {p : Char → Bool} {s : String.Slice},
  s.endsWith p = false ↔ ∀ (h : s.endPos ≠ s.startPos), p ((s.endPos.prev h).get ⋯) = false
-- Mathlib.Data.Set.SymmDiff
Set.union_symmDiff_subset : ∀ {α : Type u} {s t u : Set α}, symmDiff (s ∪ t) u ⊆ symmDiff s u ∪ symmDiff t u
-- Mathlib.Data.Multiset.Count
Multiset.count_le_of_le : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {s t : Multiset α}, s ≤ t → Multiset.count a s ≤ Multiset.count a t
-- Mathlib.Algebra.Group.Conj
IsAddConj.nsmul : ∀ {α : Type u} [inst : AddMonoid α] {a b : α} (n : ℕ), IsAddConj a b → IsAddConj (n • a) (n • b)
-- Mathlib.Data.List.Cycle
/-- Reverse a `s : Cycle α` by reversing the underlying `List`.  -/
Cycle.reverse : {α : Type u_1} → Cycle α → Cycle α
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite
on compacts and regular, they coincide up to a multiplicative constant.  -/
MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_regular : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : μ'.IsAddLeftInvariant] [μ.Regular] [inst_9 : μ'.Regular],
  μ' = μ'.addHaarScalarFactor μ • μ
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.toRangeSheafify_app_hom_apply_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  {F F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) (X : Cᵒᵖ) (a : F'.obj X),
  ↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Subfunctor.toRangeSheafify J f).app X)) a) =
    ↑(((CategoryTheory.Subfunctor.toRange f).app X).hom' a)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsUniversal.of_isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsUniversal
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instOneCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → One (CauSeq.Completion.Cauchy abv)
-- Mathlib.AlgebraicGeometry.Scheme
/-- **Alias** of `AlgebraicGeometry.Scheme.preimage_basicOpen_top`. -/
AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))),
  (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) =
    X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) r)
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.powerBasis_gen : ∀ {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),
  (IsPrimitiveRoot.powerBasis K hζ).gen = ζ
-- Mathlib.Algebra.Polynomial.Degree.Monomial
Polynomial.natDegree_le_pred : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.natDegree ≤ n → p.coeff n = 0 → p.natDegree ≤ n - 1
-- Mathlib.Algebra.Group.Hom.Defs
/-- The identity map from a monoid to itself.  -/
MonoidHom.id : (M : Type u_10) → [inst : MulOne M] → M →* M
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult.tacticInfo : Lean.Elab.GoalsAtResult → Lean.Elab.TacticInfo
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.foldl_eq_foldl_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  {f : δ → α → β → δ} {init : δ},
  Std.DTreeMap.foldl f init t = List.foldl (fun a b => f a b.1 b.2) init (Std.DTreeMap.Const.toList t)
-- Lean.Compiler.Specialize
Lean.Compiler.SpecializeAttributeKind.specialize : Lean.Compiler.SpecializeAttributeKind
-- Mathlib.Data.Setoid.Partition
IndexedPartition.mk.sizeOf_spec : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} [inst : SizeOf ι] [inst_1 : SizeOf α]
  [inst_2 : (a : ι) → (a_1 : α) → SizeOf (s a a_1)] (eq_of_mem : ∀ {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j)
  (some : ι → α) (some_mem : ∀ (i : ι), some i ∈ s i) (index : α → ι) (mem_index : ∀ (x : α), x ∈ s (index x)),
  sizeOf { eq_of_mem := eq_of_mem, some := some, some_mem := some_mem, index := index, mem_index := mem_index } = 1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite : {M N : ProfiniteGrp.{u}} → CoeFun (M ⟶ N) fun x => ↑M.toProfinite.toTop → ↑N.toProfinite.toTop
-- Mathlib.Order.GameAdd
Prod.GameAdd.fst : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a₁ a₂ : α} {b : β},
  rα a₁ a₂ → Prod.GameAdd rα rβ (a₁, b) (a₂, b)
-- Mathlib.Data.Fintype.Inv
/-- The inverse of an `hf : injective` function `f : α → β`, of the type `↥(Set.range f) → α`.
This is the computable version of `Function.invFun` that requires `Fintype α` and `DecidableEq β`,
or the function version of applying `(Equiv.ofInjective f hf).symm`.
This function should not usually be used for actual computation because for most cases,
an explicit inverse can be stated that has better computational properties.
This function computes by checking all terms `a : α` to find the `f a = b`, so it is O(N) where
`N = Fintype.card α`.
 -/
Function.Injective.invOfMemRange : {α : Type u_1} →
  {β : Type u_2} → [Fintype α] → [DecidableEq β] → {f : α → β} → Function.Injective f → ↑(Set.range f) → α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_modifyKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} [inst_2 : Inhabited (β k)] {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast! k (Std.Internal.List.modifyKey k f l) =
      (Option.map f (Std.Internal.List.getValueCast? k l)).get!
-- Mathlib.Algebra.Group.Subsemigroup.Defs
isMulCommutative_iff_of_setLike : ∀ {S : Type u_3} {M : Type u_4} [inst : SetLike S M] [inst_1 : Mul M] [inst_2 : MulMemClass S M] {s : S},
  IsMulCommutative ↥s ↔ ∀ a ∈ s, ∀ b ∈ s, a * b = b * a
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegrable_def : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (c : ℂ) (R : ℝ),
  CircleIntegrable f c R ↔ IntervalIntegrable (fun θ => f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)
-- Mathlib.Topology.MetricSpace.Algebra
TendstoLocallyUniformly.mul₀ : ∀ {X : Type u_3} {M : Type u_4} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : PseudoMetricSpace M]
  [inst_2 : Zero M] [inst_3 : Mul M] [IsBoundedSMul M M] {F G : ι → X → M} {f g : X → M} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l → Continuous f → Continuous g → TendstoLocallyUniformly (F * G) (f * g) l
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.coe_ofSubmodule : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (S : Submodule R E), ↑↑S = ↑S
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_insertRupUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  (f.insertRupUnits units).1.assignments.size = f.assignments.size
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  (Std.ExtHashMap.unitOfList l)[k]? = if l.contains k = true then some () else none
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller.congr_simp : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] (I : Ideal R) [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R], Perfection.teichmuller p I = Perfection.teichmuller p I
-- Mathlib.Topology.Compactness.Compact
exists_subset_nhds_of_compactSpace : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] [Nonempty ι] {V : ι → Set X},
  Directed (fun x1 x2 => x1 ⊇ x2) V →
    (∀ (i : ι), IsClosed (V i)) → ∀ {U : Set X}, (∀ x ∈ ⋂ i, V i, U ∈ nhds x) → ∃ i, V i ⊆ U
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ENode.mk.sizeOf_spec : ∀ (self next root congr : Lean.Expr) (target? proof? : Option Lean.Expr) (flipped : Bool) (size : ℕ)
  (interpreted ctor hasLambdas heqProofs : Bool) (idx generation mt : ℕ) (sTerms : Lean.Meta.Grind.SolverTerms)
  (funCC : Bool) (ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource),
  sizeOf
      { self := self, next := next, root := root, congr := congr, target? := target?, proof? := proof?,
        flipped := flipped, size := size, interpreted := interpreted, ctor := ctor, hasLambdas := hasLambdas,
        heqProofs := heqProofs, idx := idx, generation := generation, mt := mt, sTerms := sTerms, funCC := funCC,
        ematchDiagSource := ematchDiagSource } =
    1 + sizeOf self + sizeOf next + sizeOf root + sizeOf congr + sizeOf target? + sizeOf proof? + sizeOf flipped +
                          sizeOf size +
                        sizeOf interpreted +
                      sizeOf ctor +
                    sizeOf hasLambdas +
                  sizeOf heqProofs +
                sizeOf idx +
              sizeOf generation +
            sizeOf mt +
          sizeOf sTerms +
        sizeOf funCC +
      sizeOf ematchDiagSource
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
noZeroDivisors_iff_forall_mem_nonZeroDivisorsLeft : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀], NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → x ∈ nonZeroDivisorsLeft M₀
-- Std.Http.Data.Body.Stream
Std.Http.Body.instForInContextAsyncStreamChunk : ForIn Std.Async.ContextAsync Std.Http.Body.Stream Std.Http.Chunk
-- Mathlib.Data.TypeVec
/-- arrow that rearranges the type of `Subtype_` to turn a vector of subtypes
into a subtype of vector  -/
TypeVec.ofSubtype : {n : ℕ} →
  {α : TypeVec.{u} n} →
    (p : α.Arrow (TypeVec.repeat n Prop)) → (TypeVec.Subtype_ p).Arrow fun i => { x // TypeVec.ofRepeat (p i x) }
-- Mathlib.Data.FinEnum
/-- create a `FinEnum` instance from an exhaustive list; duplicates are removed  -/
FinEnum.ofList : {α : Type u} → [DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → FinEnum α
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
AddAction.isMultiplyPreprimitive_congr : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {N : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup N] [inst_3 : AddAction N β] {φ : M → N},
  Function.Surjective φ →
    ∀ {f : α →ₑ[φ] β},
      Function.Bijective ⇑f → ∀ {n : ℕ}, AddAction.IsMultiplyPreprimitive M α n ↔ AddAction.IsMultiplyPreprimitive N β n
-- Lean.Expr
/-- Returns a natural number literal used in the frontend. It is a `OfNat.ofNat` application.
Recall that all theorems and definitions containing numeric literals are encoded using
`OfNat.ofNat` applications in the frontend.
 -/
Lean.mkNatLit : ℕ → Lean.Expr
-- Mathlib.RingTheory.RingHom.Smooth
/-- Helper lemma for the `algebraize` tactic  -/
RingHom.FormallySmooth.toAlgebra : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.FormallySmooth → Algebra.FormallySmooth R S
-- Batteries.Data.List.Perm
List.singleton_subperm_iff : ∀ {α : Type u_1} {l : List α} {a : α}, [a].Subperm l ↔ a ∈ l
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_ofBitVec : ∀ (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 32),
  { toBitVec := n }.toBitVec32 h = BitVec.cast h n
-- Std.Http.Data.Request
Std.Http.Request.instInhabitedHead.default : Std.Http.Request.Head
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.add_mem_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x y : G}, x ∈ H → (y + x ∈ H ↔ y ∈ H)
-- Mathlib.Algebra.Order.Module.Defs
smul_nonneg' : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosMono α β], 0 ≤ a → 0 ≤ b₁ → 0 ≤ a • b₁
-- Mathlib.Data.Finset.Card
Finset.card_empty : ∀ {α : Type u_1}, ∅.card = 0
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.base_smul_def' : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (h : H) (w : Monoid.PushoutI.NormalWord d),
  h • w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.ofFunction_eq : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α),
  (∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t) →
    (∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)) → (MeasureTheory.OuterMeasure.ofFunction m m_empty) s = m s
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Algebra.lmul_algebraMap : ∀ (R : Type u) {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : R),
  (Algebra.lmul R A) ((algebraMap R A) x) = (Algebra.lsmul R R A) x
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isIso₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.IsIso T.mor₁ → CategoryTheory.Limits.IsZero T.obj₃
-- Mathlib.Order.Notation
/-- Set / lattice complement  -/
HasCompl : Type u_1 → Type u_1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).incenter = s.incenter
-- Mathlib.Control.LawfulFix
LawfulFix.mk : {α : Type u_3} →
  [inst : OmegaCompletePartialOrder α] →
    [toFix : Fix α] →
      (∀ {f : α → α}, OmegaCompletePartialOrder.ωScottContinuous f → Fix.fix f = f (Fix.fix f)) → LawfulFix α
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.degreeOf_mul_eq : ∀ {R : Type u_1} {σ : Type u_2} {n : σ} [inst : CommSemiring R] {p q : MvPolynomial σ R} [NoZeroDivisors R],
  p ≠ 0 → q ≠ 0 → MvPolynomial.degreeOf n (p * q) = MvPolynomial.degreeOf n p + MvPolynomial.degreeOf n q
-- Init.SizeOf
Lean.Name.anonymous.sizeOf_spec : sizeOf Lean.Name.anonymous = 1
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_le_inf : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [I.IsTwoSided], I * J ≤ I ⊓ J
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.FunInfoEnvCacheKey.mk.injEq : ∀ (c : Lean.Name) (ls : List Lean.Level) (maxArgs? : Option ℕ) (c_1 : Lean.Name) (ls_1 : List Lean.Level)
  (maxArgs?_1 : Option ℕ),
  ({ c := c, ls := ls, maxArgs? := maxArgs? } = { c := c_1, ls := ls_1, maxArgs? := maxArgs?_1 }) =
    (c = c_1 ∧ ls = ls_1 ∧ maxArgs? = maxArgs?_1)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `s` is closed under inverses  -/
InvMemClass.inv_mem : ∀ {S : Type u_3} {G : outParam (Type u_4)} {inst : Inv G} {inst_1 : SetLike S G} [self : InvMemClass S G] {s : S}
  {x : G}, x ∈ s → x⁻¹ ∈ s
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.val : Std.Sat.AIG.Fanin → ℕ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Ideal.uniqueFactorizationMonoid : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A], UniqueFactorizationMonoid (Ideal A)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The type of functions from `α` to `β` equipped with the uniform structure and topology of
uniform convergence. We denote it `α →ᵤ β`.  -/
UniformFun : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding f → IsClosedMap f
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `right` co(ntra)variant.  -/
Right.one_le_inv_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a : α}, 1 ≤ a⁻¹ ↔ a ≤ 1
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.lift₃NatIso_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_13, u_13} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (L₃ : CategoryTheory.Functor C₃ D₃) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) (W₃ : CategoryTheory.MorphismProperty C₃) [inst_7 : L₁.IsLocalization W₁]
  [inst_8 : L₂.IsLocalization W₂] [inst_9 : L₃.IsLocalization W₃] [inst_10 : W₁.ContainsIdentities]
  [inst_11 : W₂.ContainsIdentities] [inst_12 : W₃.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)))
  [inst_13 : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁']
  [inst_14 : CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (e : F₁ ≅ F₂),
  (CategoryTheory.Localization.lift₃NatIso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e).hom =
    CategoryTheory.Localization.lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e.hom
-- Mathlib.Analysis.Normed.Order.UpperLower
closure_lowerClosure_comm_pi : ∀ {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)}, BddAbove s → closure ↑(lowerClosure s) = ↑(lowerClosure (closure s))
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.hausdorffMeasure_smul_right_image : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] (v : E) (s : Set ℝ),
  (MeasureTheory.Measure.hausdorffMeasure 1) ((fun r => r • v) '' s) =
    ‖v‖₊ • (MeasureTheory.Measure.hausdorffMeasure 1) s
-- Mathlib.Analysis.Convex.Strong
UniformConvexOn.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (s : Set E) (φ : ℝ → ℝ) (f : E → ℝ),
  UniformConvexOn s φ f =
    (Convex ℝ s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y - a * b * φ ‖x - y‖)
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
AddSubgroup.discreteTopology_iff_of_isFiniteRelIndex : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  {H K : AddSubgroup G}, H ≤ K → ∀ [H.IsFiniteRelIndex K], DiscreteTopology ↥H ↔ DiscreteTopology ↥K
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- Turn a morphism in `TopRep` back into an `IntertwiningMap`.  -/
TopRep.Hom.hom : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] → [inst_2 : Monoid G] → {A B : TopRep k G} → A.Hom B → ContIntertwiningMap A.ρ B.ρ
-- Init.Data.Array.Erase
Array.eraseIdx_ne_empty_iff : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {h : i < xs.size}, xs.eraseIdx i h ≠ #[] ↔ 2 ≤ xs.size
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The morphism from `K.opcycles i` that is induced by an "opcycle", i.e. a morphism
from `K.X i` whose precomposition with the differential is zero.  -/
HomologicalComplex.descOpcycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            {i : ι} →
              [inst_2 : K.HasHomology i] →
                {A : C} →
                  (k : K.X i ⟶ A) →
                    (j : ι) → c.prev i = j → CategoryTheory.CategoryStruct.comp (K.d j i) k = 0 → (K.opcycles i ⟶ A)
-- Init.Data.Vector.Count
Vector.count_eq_countP : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} {a : α} {xs : Vector α n},
  Vector.count a xs = Vector.countP (fun x => x == a) xs
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- A morphism of SheafedSpaces is an open immersion if it is an open immersion as a morphism
of PresheafedSpaces
 -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : AlgebraicGeometry.SheafedSpace C} → (X ⟶ Y) → Prop
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.snd.injEq : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} (a a_1 : Std.IterM m β),
  (Std.Iterators.Types.Append.snd a = Std.Iterators.Types.Append.snd a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi'_ε : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).Monoidal] (i : I),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Functor.pi' F) i = CategoryTheory.Functor.LaxMonoidal.ε (F i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
derivWithin_sin : ∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → derivWithin (fun x => Real.sin (f x)) s x = Real.cos (f x) * derivWithin f s x
-- Mathlib.Algebra.Star.StarRingHom
/-- `α →⋆ₙ+* β` denotes the type of non-unital ring homomorphisms from `α` to `β`.  -/
«term_→⋆ₙ+*_» : Lean.TrailingParserDescr
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.mk.sizeOf_spec : ∀ {σ : Type} [inst : SizeOf σ] (id : ℕ) (mkInitial : IO σ), sizeOf { id := id, mkInitial := mkInitial } = 1 + sizeOf id
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The bipartite double cover of `G` is contained in the corresponding complete bipartite graph,
that is, the bipartite double cover of `G` is bipartite.  -/
SimpleGraph.bipartiteDoubleCover_le : ∀ {V : Type u_1} {G : SimpleGraph V}, G.bipartiteDoubleCover ≤ completeBipartiteGraph V V