mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSomeM?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Order.Hom.Basic
OrderHom.mk_le_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {hf : Monotone f}
  {hg : Monotone g}, { toFun := f, monotone' := hf } ≤ { toFun := g, monotone' := hg } ↔ f ≤ g
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformLeft_snd : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformLeft e x).2 = x.2 ∪ e⁻¹ • x.2
-- Init.Data.UInt.Bitwise
UInt64.neg_eq_not_add : ∀ (a : UInt64), -a = ~~~a + 1
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_iff_final_comp : ∀ {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) [F.Final], G.Final ↔ (F.comp G).Final
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.regularTopology.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C],
  CategoryTheory.regularTopology C = CategoryTheory.regularTopology C
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.finrank_ratFunc_ratFunc : ∀ (k : Type u_3) (K : Type u_4) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [Algebra.IsAlgebraic k K],
  Module.finrank (RatFunc k) (RatFunc K) = Module.finrank k K
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- An object admits an injective resolution.  -/
CategoryTheory.HasInjectiveResolution : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.pairing_p_symm_equivI : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (x : h.ι), h.pairing.p.symm (h.equivI x) = h.equivII x
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toFun_eq_coe : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  (↑e).toFun = ⇑e
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
tendsto_logDeriv_euler_sin_div : ∀ {x : ℂ},
  x ∈ Complex.integerComplement →
    Filter.Tendsto (fun n => logDeriv (fun z => ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) Filter.atTop
      (nhds (logDeriv (fun t => Complex.sin (↑Real.pi * t) / (↑Real.pi * t)) x))
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabLink.mk.injEq : ∀ (name name_1 : Lean.StrLit), ({ name := name } = { name := name_1 }) = (name = name_1)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_mul_of_right_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.leadingCoeff g ∈ nonZeroDivisors R → m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
-- Init.Data.Nat.Power2.Basic
/-- A natural number `n` is a power of two if there exists some `k : Nat` such that `n = 2 ^ k`.
 -/
Nat.isPowerOfTwo : ℕ → Prop
-- Init.Data.Fin.Lemmas
Fin.castLT_castAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), (Fin.castAdd m i).castLT ⋯ = i
-- Mathlib.CategoryTheory.Monoidal.Arrow
/-- The braided category instance induced by the pushout-product.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braidedCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        [inst_3 : CategoryTheory.CartesianMonoidalCategory C] →
          [inst_4 : CategoryTheory.MonoidalClosed C] →
            [inst_5 : CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory (CategoryTheory.Arrow C)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.mk.inj : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂} {inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂}
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {weightMap : M →ₗ[R] M₂} {coweightMap : N₂ →ₗ[R] N}
  {indexEquiv : ι ≃ ι₂}
  {weight_coweight_transpose : weightMap.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ coweightMap}
  {root_weightMap : ⇑weightMap ∘ ⇑P.root = ⇑Q.root ∘ ⇑indexEquiv}
  {coroot_coweightMap : ⇑coweightMap ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑indexEquiv.symm} {weightMap_1 : M →ₗ[R] M₂}
  {coweightMap_1 : N₂ →ₗ[R] N} {indexEquiv_1 : ι ≃ ι₂}
  {weight_coweight_transpose_1 : weightMap_1.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ coweightMap_1}
  {root_weightMap_1 : ⇑weightMap_1 ∘ ⇑P.root = ⇑Q.root ∘ ⇑indexEquiv_1}
  {coroot_coweightMap_1 : ⇑coweightMap_1 ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑indexEquiv_1.symm},
  { weightMap := weightMap, coweightMap := coweightMap, indexEquiv := indexEquiv,
        weight_coweight_transpose := weight_coweight_transpose, root_weightMap := root_weightMap,
        coroot_coweightMap := coroot_coweightMap } =
      { weightMap := weightMap_1, coweightMap := coweightMap_1, indexEquiv := indexEquiv_1,
        weight_coweight_transpose := weight_coweight_transpose_1, root_weightMap := root_weightMap_1,
        coroot_coweightMap := coroot_coweightMap_1 } →
    weightMap = weightMap_1 ∧ coweightMap = coweightMap_1 ∧ indexEquiv = indexEquiv_1
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- A Lie-Rinehart ring is a pair consisting of a commutative ring `A` and a Lie ring `L` such that
`A` and `L` are each a module over the other, satisfying compatibility conditions.  -/
LieRinehartRing : (A : Type u_1) → (L : Type u_2) → [inst : CommRing A] → [inst_1 : LieRing L] → [Module A L] → [LieRingModule L A] → Prop
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Submodule.baseChange_inj : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [Module.FaithfullyFlat R A] [inst_4 : AddCommGroup M] [inst_5 : Module R M] {p q : Submodule R M},
  Submodule.baseChange A p = Submodule.baseChange A q ↔ p = q
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.toGlueData : AlgebraicGeometry.Scheme.GlueData → CategoryTheory.GlueData AlgebraicGeometry.Scheme
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instMax : {G : Type u_1} →
  [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousAdd G] → Max (OpenAddSubgroup G)
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- The fiber functor on categories of presheaves that is given by a point of a site.  -/
CategoryTheory.GrothendieckTopology.Point.presheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      J.Point →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) A
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearEquiv.ofInjectiveEndo_right_inv : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f),
  f * ↑(LinearEquiv.ofInjectiveEndo f h_inj).symm = 1
-- Mathlib.Topology.Defs.Basic
/-- The coborder is defined as the complement of `closure s \ s`,
or the union of `s` and the complement of `∂(s)`.
This is the largest set in which `s` is closed, and `s` is locally closed if and only if
`coborder s` is open.

This is unnamed in the literature, and this name is due to the fact that `coborder s = (border sᶜ)ᶜ`
where `border s = s \ interior s` is the border in the sense of Hausdorff.
 -/
coborder : {X : Type u} → [TopologicalSpace X] → Set X → Set X
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instPartialOrder : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → PartialOrder (AffineSubspace k P)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.finsupport_subset_fintsupport : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M),
  ρ.finsupport x₀ ⊆ ρ.fintsupport x₀
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] [inst_5 : TopologicalSpace A]
  [inst_6 : IsSemitopologicalSemiring A] [inst_7 : ContinuousConstSMul R A] (x x_1 : A),
  x = x_1 → NonUnitalAlgebra.elemental R x = NonUnitalAlgebra.elemental R x_1
-- Mathlib.Tactic.MkIffOfInductiveProp
_private.Mathlib.Tactic.MkIffOfInductiveProp.0.Mathlib.Tactic.MkIff.updateLambdaBinderInfoD! : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `(S, F) ⥤ (G(S), F ⋙ G)`.  -/
CategoryTheory.StructuredArrow.post : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {B : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} B] →
            (S : C) →
              (F : CategoryTheory.Functor B C) →
                (G : CategoryTheory.Functor C D) →
                  CategoryTheory.Functor (CategoryTheory.StructuredArrow S F)
                    (CategoryTheory.StructuredArrow (G.obj S) (F.comp G))
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.mk_add_choose_mul_one_sub_pow_eq_one : ∀ (S : Type u_1) [inst : CommRing S] (d : ℕ),
  (PowerSeries.mk fun n => ↑((d + n).choose d)) * (1 - PowerSeries.X) ^ (d + 1) = 1
-- Init.Data.List.MinMaxOn
List.minOn_eq_get_minOn? : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.minOn f xs h = (List.minOn? f xs).get ⋯
-- Mathlib.Data.Set.Semiring
/-- If `α` is a monoid, the map that sends `a : α` to
the singleton set `{a}` is a monoid homomorphism.  -/
SetSemiring.singletonMonoidHom : {α : Type u_1} → [inst : Monoid α] → α →* SetSemiring α
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.symm_one : (CategoryTheory.ConcreteCategory.hom TopCat.I.symm) 1 = 0
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalarsSum_unop : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) [T2Space E] (x : Eᵐᵒᵖ),
  FormalMultilinearSeries.ofScalarsSum c (MulOpposite.unop x) =
    MulOpposite.unop (FormalMultilinearSeries.ofScalarsSum c x)
-- Mathlib.CategoryTheory.Limits.Creates
/-- When `F` is fully faithful, to show that `F` creates the colimit for `K` it suffices to show that
a colimit point is in the essential image of `F`.
 -/
CategoryTheory.createsColimitOfFullyFaithfulOfIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    {l : CategoryTheory.Limits.Cocone (K.comp F)} →
                      CategoryTheory.Limits.IsColimit l → (X : C) → (F.obj X ≅ l.pt) → CategoryTheory.CreatesColimit K F
-- Batteries.Data.Fin.Coding
Fin.encodePi.eq_2 : ∀ (n_2 : ℕ) (f_2 : Fin (n_2 + 1) → ℕ) (x_2 : (i : Fin (n_2 + 1)) → Fin (f_2 i)),
  Fin.encodePi f_2 x_2 =
    match
      Fin.encodePi (fun x => f_2 x.succ) fun x =>
        match x with
        | ⟨i, hi⟩ => x_2 ⟨i + 1, ⋯⟩ with
    | ⟨k, hk⟩ => ⟨f_2 0 * k + ↑(x_2 0), ⋯⟩
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.toAddEquiv_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), f.toAddEquiv = ↑f
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- For a prime ideal `q` in `A⁰_f`, the set `{a | aᵢᵐ/fⁱ ∈ q}` as a homogeneous ideal.
 -/
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdeal : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              {f : A} →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace →
                        HomogeneousIdeal 𝒜
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_pos_iff : ∀ {x : EReal}, 0 < x.toENNReal ↔ 0 < x
-- Mathlib.ModelTheory.Syntax
/-- The universal quantifier over bounded formulas.  -/
FirstOrder.«term∀'_» : Lean.ParserDescr
-- Std.Sat.CNF.Basic
Std.Sat.CNF.eval_append : ∀ {α : Type u_1} (a : α → Bool) (f1 f2 : Std.Sat.CNF α),
  Std.Sat.CNF.eval a (f1 ++ f2) = (Std.Sat.CNF.eval a f1 && Std.Sat.CNF.eval a f2)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_toArray_rco : ∀ {m n : ℕ}, (m...n).toArray.toList = (m...n).toList
-- Mathlib.CategoryTheory.Join.Opposites
_private.Mathlib.CategoryTheory.Join.Opposites.0.CategoryTheory.Join.opEquiv.match_1.eq_1 : ∀ (C : Type u_2) (D : Type u_1) [inst : CategoryTheory.Category.{u_3, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_1} D] (motive : (CategoryTheory.Join C D)ᵒᵖ → Sort u_5) (a : C)
  (h_1 : (a : C) → motive (Opposite.op (CategoryTheory.Join.left a)))
  (h_2 : (a : D) → motive (Opposite.op (CategoryTheory.Join.right a))),
  (match Opposite.op (CategoryTheory.Join.left a) with
    | Opposite.op (CategoryTheory.Join.left a) => h_1 a
    | Opposite.op (CategoryTheory.Join.right a) => h_2 a) =
    h_1 a
-- Mathlib.RingTheory.AdjoinRoot
/-- If `L / K` is an integral extension, `K` is a domain, `L` is a field, then any irreducible
polynomial over `L` divides some monic irreducible polynomial over `K`.  -/
Irreducible.exists_dvd_monic_irreducible_of_isIntegral : ∀ {K : Type u_6} {L : Type u_7} [inst : CommRing K] [IsDomain K] [inst_2 : Field L] [inst_3 : Algebra K L]
  [Algebra.IsIntegral K L] {f : Polynomial L},
  Irreducible f → ∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
-- Lean.Meta.Sym.Pattern
/-- If `unify` is `false`, it contains which variables can be assigned.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.mvarsNew : Lean.Meta.Sym.DefEqM.Context✝ → Array Lean.MVarId
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.copy_eq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
compContinuousLinearMap_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G]
  [inst_6 : NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G),
  p.compContinuousLinearMap 0 = constFormalMultilinearSeries 𝕜 E ((p 0) 0)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instNSMulQuotientNat : {M : Type u_4} → [inst : AddMonoid M] → (c : AddCon M) → SMul ℕ c.Quotient
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Relations.isUniversal_symmetric : ∀ {L : FirstOrder.Language} (r : L.Relations 2), FirstOrder.Language.BoundedFormula.IsUniversal r.symmetric
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.ext_iff : ∀ {X : Type u_3} {inst : MetricSpace X} {x y : Delone.DeloneSet X},
  x = y ↔ x.carrier = y.carrier ∧ x.packingRadius = y.packingRadius ∧ x.coveringRadius = y.coveringRadius
-- Init.Data.List.Lemmas
List.getD_getElem? : ∀ {α : Type u_1} {l : List α} {i : ℕ} {d : α}, l[i]?.getD d = if p : i < l.length then l[i] else d
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.mem_iff_fract_eq_and_floor_nonneg : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (x : ι → ℕ),
  x ∈ s ↔
    IsProperLinearSet.fract✝ hs x = IsProperLinearSet.base✝ hs ∧
      ∀ (i : ↑(IsProperLinearSet.basisSet✝ hs)),
        0 ≤ IsProperLinearSet.floor✝ hs x i ∧ (↑i ∉ IsProperLinearSet.periods✝ hs → IsProperLinearSet.floor✝ hs x i = 0)
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.colimit.toOver_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  (CategoryTheory.Limits.colimit.toOver F).pt =
    CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit F))
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_eq_one_iff : ∀ {α : Type u_1} [inst : One α] (a : α), SymAlg.sym a = 1 ↔ a = 1
-- Mathlib.SetTheory.Cardinal.Order
/-- The **well-ordering theorem** (or **Zermelo's theorem**): every type can be co-well-ordered.  -/
exists_wellFoundedGT : ∀ (α : Type u), ∃ x, WellFoundedGT α
-- Mathlib.Algebra.Lie.Abelian
LieModule.commute_toEnd_of_mem_center_right : ∀ {R : Type u} {L : Type v} (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {x : L},
  x ∈ LieAlgebra.center R L → ∀ (y : L), Commute ((LieModule.toEnd R L M) y) ((LieModule.toEnd R L M) x)
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 1 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₂ f₁ f₂).obj 1)
-- Mathlib.Combinatorics.Enumerative.Composition
instInhabitedCompositionAsSet : {n : ℕ} → Inhabited (CompositionAsSet n)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instContinuousSup : ∀ {α : Type u_1} [inst : TopologicalSpace α], ContinuousSup (TopologicalSpace.Compacts α)
-- Mathlib.RingTheory.Artinian.Module
/-- If `M / S / R` is a scalar tower, and `M / R` is Artinian, then `M / S` is also Artinian.  -/
isArtinian_of_tower : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R S] [inst_4 : Module S M] [inst_5 : Module R M] [IsScalarTower R S M], IsArtinian R M → IsArtinian S M
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestParenTac : Lean.Elab.Tactic.Try.TryTactic
-- Mathlib.LinearAlgebra.Dual.Defs
Dual.apply_one_mul_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (f : Module.Dual R R) (r : R), f 1 * r = f r
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.grindPatternCnstr.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.sum` -/
Meromorphic.fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {s : Finset ι} {G : ι → 𝕜 → E},
  (∀ σ ∈ s, Meromorphic (G σ)) → Meromorphic fun a => ∑ c ∈ s, G c a
-- Mathlib.FieldTheory.Normal.Basic
Normal.minpoly_eq_iff_mem_orbit : ∀ {F : Type u_1} [inst : Field F] (E : Type u_6) [inst_1 : Field E] [inst_2 : Algebra F E] [h : Normal F E] {x y : E},
  minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit Gal(E/F) y
-- Mathlib.Data.Bundle
Bundle.TotalSpace.ext : ∀ {B : Type u_1} {F : Type u_4} {E : B → Type u_5} {x y : Bundle.TotalSpace F E},
  x.proj = y.proj → x.snd ≍ y.snd → x = y
-- Lean.Meta.Basic
/-- Gets the current `zetaDeltaFVarIds` set.
If `Context.trackZetaDelta` is true, then `whnf` adds to this set
those local definitions that are unfolded ("zeta-delta reduced") .

See `withTrackingZetaDelta` and `withTrackingZetaDeltaSet`.
 -/
Lean.Meta.getZetaDeltaFVarIds : Lean.MetaM Lean.FVarIdSet
-- Mathlib.Data.Set.Sups
Set.infs_eq_empty : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α}, s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d_ofNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m : ℕ), h.d ↑n ↑m = L.d n m
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.bracket : (M : Type w) →
  {R : Type u_1} →
    {L : Type u_2} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (I : LieIdeal R L) → [Bracket L M] → Bracket (↥I) M
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Slice.Pos.find?_char_eq_none_iff_not_mem_of_splits : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} {t u : String}, pos.Splits t u → (pos.find? c = none ↔ c ∉ u.toList)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward₀.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor Dᵒᵖ RingCat),
  PresheafOfModules.pushforward₀ F R =
    { obj := fun M => PresheafOfModules.pushforward₀Obj F R M,
      map := fun {M₁ M₂} φ => { app := fun X => φ.app (F.op.obj X), naturality := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.prod_iso_invFun_left : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_2) [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] (L : Type u_3)
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (a : K × L),
  ((LieAlgebra.SemiDirectSum.prod_iso R K L).invFun a).left = a.1
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Whiskering a left exact functor by a left exact functor yields a left exact functor.  -/
CategoryTheory.LeftExactFunctor.whiskeringRight : (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] →
            CategoryTheory.Functor (D ⥤ₗ E) (CategoryTheory.Functor (C ⥤ₗ D) (C ⥤ₗ E))
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.Boundaryless.range_eq_univ : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {H : Type u_3} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H}
  [self : I.Boundaryless], Set.range ↑I = Set.univ
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The first cyclotomic polynomial is `X - 1`.  -/
Polynomial.cyclotomic_one : ∀ (R : Type u_1) [inst : Ring R], Polynomial.cyclotomic 1 R = Polynomial.X - 1
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_eq_top_iff : ∀ {x : EReal}, x.toENNReal = ⊤ ↔ x = ⊤