mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.liftCover_restrict' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {A : Set (Set α)}
  {F : (s : Set α) → s ∈ A → C(↑s, β)}
  {hF :
    ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
      (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩}
  {hA : ∀ (x : α), ∃ i ∈ A, i ∈ nhds x} {s : Set α} {hs : s ∈ A},
  ContinuousMap.restrict s (ContinuousMap.liftCover' A F hF hA) = F s hs
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
Polynomial.image_comap_C_basicOpen : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R),
  PrimeSpectrum.comap Polynomial.C '' ↑(PrimeSpectrum.basicOpen f) = (PrimeSpectrum.zeroLocus (Set.range f.coeff))ᶜ
-- Mathlib.ModelTheory.Basic
/-- Any element of an injective `StrongHomClass` can be realized as a first order embedding.  -/
FirstOrder.Language.StrongHomClass.toEmbedding : {L : FirstOrder.Language} →
  {F : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : L.Structure M] →
          [inst_1 : L.Structure N] →
            [inst_2 : FunLike F M N] → [EmbeddingLike F M N] → [L.StrongHomClass F M N] → F → L.Embedding M N
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.PComp.mk.sizeOf_spec : ∀ (c : Mathlib.Tactic.Linarith.Comp) (src : Mathlib.Tactic.Linarith.CompSource)
  (history effective implicit vars : Std.TreeSet ℕ compare),
  sizeOf { c := c, src := src, history := history, effective := effective, implicit := implicit, vars := vars } =
    1 + sizeOf c + sizeOf src + sizeOf history + sizeOf effective + sizeOf implicit + sizeOf vars
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rii.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxi.IsAlwaysFinite α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rii α}, r.toList = (Std.Rii.Internal.iter r).toList
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometry.rTensor_def : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →ₗᵢ[𝕜] F),
  LinearIsometry.rTensor G f = TensorProduct.mapIsometry f LinearIsometry.id
-- Mathlib.Data.Matrix.Mul
Matrix.diagonal_mul_diagonal : ∀ {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (d₁ d₂ : n → α), Matrix.diagonal d₁ * Matrix.diagonal d₂ = Matrix.diagonal fun i => d₁ i * d₂ i
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.algebraMap_eval_T : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Algebra R R'] (x : R) (n : ℤ),
  (algebraMap R R') (Polynomial.eval x (Polynomial.Chebyshev.T R n)) =
    Polynomial.eval ((algebraMap R R') x) (Polynomial.Chebyshev.T R' n)
-- Std.Tactic.BVDecide.Syntax
Lean.Elab.Tactic.BVDecide.BVDecideConfig.mk.sizeOf_spec : ∀ (timeout : ℕ)
  (trimProofs binaryProofs acNf andFlattening embeddedConstraintSubst structures fixedInt enums graphviz : Bool)
  (maxSteps : ℕ) (shortCircuit : Bool) (solverMode : Lean.Elab.Tactic.BVDecide.SolverMode),
  sizeOf
      { timeout := timeout, trimProofs := trimProofs, binaryProofs := binaryProofs, acNf := acNf,
        andFlattening := andFlattening, embeddedConstraintSubst := embeddedConstraintSubst, structures := structures,
        fixedInt := fixedInt, enums := enums, graphviz := graphviz, maxSteps := maxSteps, shortCircuit := shortCircuit,
        solverMode := solverMode } =
    1 + sizeOf timeout + sizeOf trimProofs + sizeOf binaryProofs + sizeOf acNf + sizeOf andFlattening +
                    sizeOf embeddedConstraintSubst +
                  sizeOf structures +
                sizeOf fixedInt +
              sizeOf enums +
            sizeOf graphviz +
          sizeOf maxSteps +
        sizeOf shortCircuit +
      sizeOf solverMode
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The proposed colimit cocone over `coyoneda.obj X` is a colimit cocone.
 -/
CategoryTheory.Coyoneda.colimitCoconeIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : Cᵒᵖ) → CategoryTheory.Limits.IsColimit (CategoryTheory.Coyoneda.colimitCocone X)
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the forward direction of `Asymptotics.isTheta_norm_right`. -/
Asymptotics.IsTheta.of_norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =Θ[l] fun x => ‖g' x‖) → f =Θ[l] g'
-- Mathlib.MeasureTheory.Group.Measure
/-- A nonzero left-invariant inner regular measure gives positive mass to any open set.  -/
MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_innerRegular : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.InnerRegular] [NeZero μ], μ.IsOpenPosMeasure
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.fpqcTopology_eq_propQCTopology : AlgebraicGeometry.Scheme.fpqcTopology = AlgebraicGeometry.Scheme.propQCTopology @AlgebraicGeometry.Flat
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Y' : C}
  (f f_1 : X ⟶ Y'),
  f = f_1 →
    ∀ (s s_1 : Y ⟶ Y') (e_s : s = s_1) (hs : W s),
      { Y' := Y', f := f, s := s, hs := hs } = { Y' := Y', f := f_1, s := s_1, hs := ⋯ }
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.le_one_of_extendedHom_le_one : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [inst_12 : Algebra K L]
  [inst_13 : Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsIntegrallyClosed A]
  [IsIntegrallyClosed B], (FractionalIdeal.extendedHom L B) I ≤ 1 → I ≤ 1
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instReprRingMode : Repr Mathlib.Tactic.RingNF.RingMode
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGE? : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.instDecidableRelRelDown' : (α : Type u_1) →
  [inst : AddRightCancelSemigroup α] →
    [DecidableEq α] → (a : α) → DecidableRel fun a_1 a_2 => (ComplexShape.down' a).Rel a_2 a_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (↑(t.insertMany l ⋯)).getKeyD k fallback = t.getKeyD k fallback
-- Lean.ParserCompiler
Lean.ParserCompiler.Context.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (varName : Lean.Name) (categoryAttr : Lean.KeyedDeclsAttribute α)
  (combinatorAttr : Lean.ParserCompiler.CombinatorAttribute),
  sizeOf { varName := varName, categoryAttr := categoryAttr, combinatorAttr := combinatorAttr } =
    1 + sizeOf varName + sizeOf categoryAttr + sizeOf combinatorAttr
-- Mathlib.Tactic.FunProp.FunctionData
/-- Can't generate function data as function body has let binder.  -/
Mathlib.Meta.FunProp.MaybeFunctionData.letE : Lean.Expr → Mathlib.Meta.FunProp.MaybeFunctionData
-- Mathlib.Data.Sigma.Interval
Sigma.Ioc_mk_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a b : α i),
  Finset.Ioc ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioc a b)
-- Init.Data.List.Basic
/-- Returns the smallest element of the list if it is not empty, or `none` if it is empty.

Examples:
* `[].min? = none`
* `[4].min? = some 4`
* `[1, 4, 2, 10, 6].min? = some 1`
 -/
List.min? : {α : Type u} → [Min α] → List α → Option α
-- Mathlib.Data.Finmap
Finmap.lookup_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : Finmap β), Finmap.lookup a (Finmap.erase a s) = none
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Group.covconv : ∀ {N : Type u_2} {r : N → N → Prop} [inst : Group N] [CovariantClass N N (fun x1 x2 => x1 * x2) r],
  ContravariantClass N N (fun x1 x2 => x1 * x2) r
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff.injEq : ∀ {k : Type u_1} {G : Type u_2} [inst : Zero k] (coeff coeff_1 : G →₀ k),
  ({ coeff := coeff } = { coeff := coeff_1 }) = (coeff = coeff_1)
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.instInhabited : Inhabited Std.Time.PlainDate
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_iSup_of_disjoint : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω},
  (∀ (i : ι), m i ≤ mΩ) →
    ProbabilityTheory.iCondIndep m' hm' m μ →
      ∀ {S T : Set ι}, Disjoint S T → ProbabilityTheory.CondIndep m' (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) hm' μ
-- Mathlib.Data.Multiset.MapFold
Multiset.nodup_map_iff_of_inj_on : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β},
  (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → ((Multiset.map f s).Nodup ↔ s.Nodup)
-- Mathlib.Data.Int.Interval
Finset.Ioo_succ_succ : ∀ (m n : ℕ), Finset.Ioo (-(↑m + 1)) (↑n + 1) = Finset.Ioo (-↑m) ↑n ∪ {-↑m, ↑n}
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.mk.injEq : ∀ (carrier : Type u) [str : AddCommMonoid carrier] (carrier_1 : Type u) (str_1 : AddCommMonoid carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatClamp n).toUSize = USize.ofNatLT n ⋯
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalPreprocessor.mk : Mathlib.Tactic.Linarith.PreprocessorBase →
  (List Lean.Expr → Lean.MetaM (List Lean.Expr)) → Mathlib.Tactic.Linarith.GlobalPreprocessor
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.congr_inseparable_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι} {g : α → β},
  TendstoUniformlyOn F f p s → (∀ x ∈ s, Inseparable (f x) (g x)) → TendstoUniformlyOn F g p s
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `H` is closed under conjugation  -/
Subgroup.Normal.conj_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H
-- Mathlib.Data.Part
Part.some_div_some : ∀ {α : Type u_1} [inst : Div α] (a b : α), Part.some a / Part.some b = Part.some (a / b)
-- Mathlib.Tactic.Translate.GuessName
Mathlib.Tactic.GuessName.instInhabitedGuessNameData : Inhabited Mathlib.Tactic.GuessName.GuessNameData
-- Mathlib.Algebra.Homology.Opposite
/-- Auxiliary definition for `opEquivalence`.  -/
HomologicalComplex.opInverse : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          CategoryTheory.Functor (HomologicalComplex Vᵒᵖ c.symm) (HomologicalComplex V c)ᵒᵖ
-- Lean.LocalContext
/-- Returns `true` if `LocalDecl.value?` is not `none`.
 -/
Lean.LocalDecl.hasValue : Lean.LocalDecl → optParam Bool false → Bool
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.getKey!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.getKey! ⟨{ size := size, buckets := buckets }, hm⟩ a =
    Std.DHashMap.Internal.AssocList.getKey! a buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.Data.Set.Prod
Set.subset_eval_image_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)},
  (s.pi t).Nonempty → ∀ (i : ι), t i ⊆ Function.eval i '' s.pi t
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.rem.eq_1 : ∀ {s : BoundingSieve} (d : ℕ), BoundingSieve.rem d = BoundingSieve.multSum d - s.nu d * s.totalMass
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.map_mul_intCast : ∀ {n : Type u_2} [inst : Fintype n] {α : Type u_3} [inst_1 : NonAssocRing α] (A B : Matrix n n ℤ),
  (A * B).map Int.cast = A.map Int.cast * B.map Int.cast
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey? k = m₂.getKey? k
-- Mathlib.Data.Sum.Order
Sum.instIsTransLiftRel : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTrans α r] [IsTrans β s],
  IsTrans (α ⊕ β) (Sum.LiftRel r s)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace_toPresheafedSpace : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : AlgebraicGeometry.PresheafedSpace C}
  (Y : AlgebraicGeometry.SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace Y f).toPresheafedSpace = X
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_functor_map_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) {Y X : CategoryTheory.Comma L R₁} (f : Y ⟶ X),
  ((CategoryTheory.Comma.mapRightIso L i).functor.map f).right = f.right
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_modify_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α} {f : β → β}, (t.modify k f).minKey? = t.minKey?
-- Mathlib.Combinatorics.Hindman
Hindman.FS.finsetSum : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : Stream' M) (s : Finset ℕ), s.Nonempty → ∑ i ∈ s, a.get i ∈ Hindman.FS a
-- Mathlib.RingTheory.LocalRing.NonLocalRing
/-- For an index type `ι` with at least two elements and an indexed family of (semi)rings
`R : ι → Type*`, the indexed product (semi)ring `Π i, R i` is not local.  -/
IsLocalRing.not_isLocalRing_of_nontrivial_pi : ∀ {ι : Type u_1} [Nontrivial ι] (R : ι → Type u_2) [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), Nontrivial (R i)],
  ¬IsLocalRing ((i : ι) → R i)
-- Mathlib.Order.InitialSeg
InitialSeg.le_iff_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a a' : α} [inst_1 : PartialOrder α] (f : α ≤i β),
  f a ≤ f a' ↔ a ≤ a'
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.ennrealToMeasure_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} {v : MeasureTheory.VectorMeasure α ENNReal} {s : Set α},
  MeasurableSet s → v.ennrealToMeasure s = v s
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_le_fst : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (j : ℕ) {a b : α},
  (∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b) → a ≤ (F.intervalGapsWithin h a b ↑j).1
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Subalgebra.finrank_eq_one_iff : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  {S : Subalgebra F E} [Nontrivial E] [Module.Free F ↥S], Module.finrank F ↥S = 1 ↔ S = ⊥
-- Lean.Server.GoTo
Lean.Server.locationLinksFromInstanceProjection : Lean.Expr → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.partialOrder.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α},
  AddLocalization.partialOrder =
    { toLE := AddLocalization.le, toLT := AddLocalization.lt, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
      le_antisymm := ⋯ }
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.of_linearOrderedField : ∀ {R : Type u} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R],
  (∀ {x : R}, 0 ≤ x → IsSquare x) → (∀ {f : Polynomial R}, Odd f.natDegree → ∃ x, f.IsRoot x) → IsRealClosed R
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.Semaphore.mk.inj : ∀ {lock lock_1 : Std.Mutex Std.SemaphoreState✝}, { lock := lock } = { lock := lock_1 } → lock = lock_1
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.type : Lean.Meta.Closure.MkValueTypeClosureResult → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The addition morphism of an additive monoid object.  -/
CategoryTheory.AddMonObj.termσ : Lean.ParserDescr
-- Mathlib.RingTheory.GradedAlgebra.FiniteType
GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous : ∀ {S : Type u_1} {σ : Type u_2} {ι : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing S]
  [inst_3 : SetLike σ S] [inst_4 : AddSubgroupClass σ S] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜]
  [Algebra.FiniteType (↥(𝒜 0)) S], ∃ s, Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_iInf : ∀ {ι : Sort u_1} (f : ι → ENNReal), (⨅ i, f i)⁻¹ = ⨆ i, (f i)⁻¹
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Same as `get?_zero_add_tail_sum`, but avoiding the `List.headI` garbage
complication by requiring the list to be nonempty.  -/
List.headI_add_tail_sum_of_ne_nil : ∀ {M : Type u_4} [inst : AddMonoid M] [inst_1 : Inhabited M] (l : List M), l ≠ [] → l.headI + l.tail.sum = l.sum
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPullbacks.hasPullback : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} [self : P.HasPullbacks]
  {X Y S : C} {f : X ⟶ S} (g : Y ⟶ S), P f → CategoryTheory.Limits.HasPullback f g
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- If `u` is a monotone function with linear ordered codomain and the range of `u` is not bounded
above, then `Tendsto u atTop atTop`.  -/
Filter.tendsto_atTop_atTop_of_monotone' : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : LinearOrder α] {u : ι → α},
  Monotone u → ¬BddAbove (Set.range u) → Filter.Tendsto u Filter.atTop Filter.atTop
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousMapClass.mk : ∀ {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [inst : TopologicalSpace α]
  [inst_1 : PseudoMetricSpace β] [inst_2 : FunLike F α β] [toContinuousMapClass : ContinuousMapClass F α β],
  (∀ (f : F), ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C) → BoundedContinuousMapClass F α β
-- Mathlib.Data.Nat.Choose.Lucas
/-- **Alias** of `Choose.choose_modEq_prod_range_choose_nat`.

---

**Lucas's Theorem**: For primes `p`, `choose n k` is congruent to the product of
`choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p)` over `i` modulo `p`.  -/
Choose.lucas_theorem_nat : ∀ {n k p : ℕ} [Fact (Nat.Prime p)] {a : ℕ},
  n < p ^ a → k < p ^ a → n.choose k ≡ ∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Translate configurations from TM1 to TM0.  -/
Turing.TM1to0.trCfg : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (M : Λ → Turing.TM1.Stmt Γ Λ σ) →
        [inst : Inhabited Γ] → Turing.TM1.Cfg Γ Λ σ → Turing.TM0.Cfg Γ (Turing.TM1to0.Λ' M)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.decl.sizeOf_spec : ∀ (xs : Array Lean.Elab.Term.Do.Var) (doElem : Lean.Syntax) (k : Lean.Elab.Term.Do.Code),
  sizeOf (Lean.Elab.Term.Do.Code.decl xs doElem k) = 1 + sizeOf xs + sizeOf doElem + sizeOf k
-- Mathlib.Logic.Equiv.Basic
Equiv.symm_swap : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), Equiv.symm (Equiv.swap a b) = Equiv.swap a b
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {α : Type u} [inst_2 : DecidableEq α]
  (x : ↑A) (i : α) (g : G) (r : k),
  (A.coinvariantsTensorFreeToFinsupp α)
      ((Representation.Coinvariants.mk (A.ρ.tprod (Representation.free k G α)))
        (x ⊗ₜ[k] fun₀ | i => MonoidAlgebra.single g r)) =
    fun₀ | i => r • (A.ρ g⁻¹) x
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_atTop_nsmul_iff_mem_topologicalClosure_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [inst_3 : IsTopologicalAddGroup G]
  {x y : G}, (MapClusterPt x Filter.atTop fun x => x • y) ↔ x ∈ (AddSubgroup.zmultiples y).topologicalClosure
-- Mathlib.Algebra.Group.Action.Basic
/-- Pushforward a multiplicative distributive multiplicative action along a surjective monoid
homomorphism.  -/
Function.Surjective.mulDistribMulAction : {M : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : Monoid M] →
        [inst_1 : Monoid A] →
          [inst_2 : MulDistribMulAction M A] →
            [inst_3 : Monoid B] →
              [inst_4 : SMul M B] →
                (f : A →* B) →
                  Function.Surjective ⇑f → (∀ (c : M) (x : A), f (c • x) = c • f x) → MulDistribMulAction M B
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.le_maximalRealSubfield : ∀ {K : Type u_2} [inst : Field K] (E : Subfield K) [NumberField.IsTotallyReal ↥E], E ≤ NumberField.maximalRealSubfield K
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none
-- Mathlib.GroupTheory.Subsemigroup.Center
Subsemigroup.center.commSemigroup.eq_1 : ∀ {M : Type u_1} [inst : Mul M],
  Subsemigroup.center.commSemigroup =
    { toMul := MulMemClass.mul (Subsemigroup.center M), mul_assoc := ⋯, mul_comm := ⋯ }
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} →
        (aig : Std.Sat.AIG α) →
          aig.RefVec len →
            (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) →
              [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func] → Std.Sat.AIG.Entrypoint α
-- Init.Data.String.Defs
/-- Appends the strings in a list of strings, placing the separator `s` between each pair.

Examples:
* `", ".intercalate ["red", "green", "blue"] = "red, green, blue"`
* `" and ".intercalate ["tea", "coffee"] = "tea and coffee"`
* `" | ".intercalate ["M", "", "N"] = "M |  | N"`
 -/
String.intercalate : String → List String → String