mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E}
  {x : E}, AnalyticWithinAt 𝕜 f s x → AnalyticWithinAt 𝕜 g s x → AnalyticWithinAt 𝕜 (f + g) s x
-- Mathlib.Data.Opposite
/-- The type of objects of the opposite of `α`; used to define the opposite category.

Now that Lean 4 supports definitional eta equality for records,
both `unop (op X) = X` and `op (unop X) = X` are definitional equalities.
 -/
Opposite : Sort u → Sort (max 1 u)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- The left inclusion in the constructed pushout `Pushout f g`.  -/
CategoryTheory.Limits.Types.Pushout.inl : {S X₁ X₂ : Type u} → (f : S ⟶ X₁) → (g : S ⟶ X₂) → X₁ ⟶ CategoryTheory.Limits.Types.Pushout f g
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [inst_4 : F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.ι (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i)
      (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv =
    F.map
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biproduct.ι (fun i => (CategoryTheory.Mat_.embedding C).obj (M.X i)) i)
        M.isoBiproductEmbedding.inv)
-- Mathlib.GroupTheory.Index
/-- A subgroup has index two if and only if there exists `a` such that for all `b`, exactly one
of `b * a` and `b` belong to `H`.  -/
Subgroup.index_eq_two_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 ↔ ∃ a, ∀ (b : G), Xor (b * a ∈ H) (b ∈ H)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.instRespectsIsoFunctorCoequifibered : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C], CategoryTheory.NatTrans.Coequifibered.RespectsIso
-- Mathlib.Order.SymmDiff
bihimp_bihimp_cancel_right : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp (bihimp b a) a = b
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom : Mathlib.Tactic.BicategoryLike.CoherenceHom → Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_div_left : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
  (a b c : G), dist (a / b) (a / c) = dist b c
-- Mathlib.Geometry.RingedSpace.Basic
/-- If the germ of a section `f` is zero in the stalk at `x`, then `f` is zero on some neighbourhood
around `x`.  -/
AlgebraicGeometry.RingedSpace.exists_res_eq_zero_of_germ_eq_zero : ∀ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
  (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U),
  (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0 →
    ∃ V i, ∃ (_ : ↑x ∈ V), (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) f = 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- `lpMeasSubgroup` and `Lp F p (μ.trim hm)` are isometric.  -/
MeasureTheory.lpMeasSubgroupToLpTrimIso : {α : Type u_1} →
  (F : Type u_2) →
    (p : ENNReal) →
      [inst : NormedAddCommGroup F] →
        {m m0 : MeasurableSpace α} →
          (μ : MeasureTheory.Measure α) →
            [inst_1 : Fact (1 ≤ p)] →
              (hm : m ≤ m0) → ↥(MeasureTheory.lpMeasSubgroup F m p μ) ≃ᵢ ↥(MeasureTheory.Lp F p (μ.trim hm))
-- Mathlib.Logic.Equiv.Defs
Equiv.equivPUnit_apply : ∀ (α : Sort u) [inst : Unique α] (a : α), (Equiv.equivPUnit α) a = PUnit.unit
-- Mathlib.Logic.Equiv.Basic
/-- Combines an `Equiv` between two subtypes with an `Equiv` between their complements to form a
permutation.  -/
Equiv.subtypeCongr : {α : Type u_9} →
  {p q : α → Prop} →
    [DecidablePred p] → [DecidablePred q] → { x // p x } ≃ { x // q x } → { x // ¬p x } ≃ { x // ¬q x } → Equiv.Perm α
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.convs'Aux.eq_2 : ∀ {K : Type u_2} [inst : DivisionRing K] (x : Stream'.Seq (GenContFract.Pair K)) (n : ℕ),
  GenContFract.convs'Aux x n.succ =
    match x.head with
    | none => 0
    | some gp => gp.a / (gp.b + GenContFract.convs'Aux x.tail n)
-- Std.Async.Process
/-- Returns the constrained memory limit in bytes.
 -/
Std.IO.Process.constrainedMemory : IO UInt64
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α) (v : β), (t₁.insert k v).Equiv (t₂.insert k v)
-- Mathlib.Algebra.Group.Submonoid.Defs
MonoidHom.eqLocusM_same : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N), f.eqLocusM f = ⊤
-- Mathlib.Algebra.Category.CommAlgCat.Basic
_private.Mathlib.Algebra.Category.CommAlgCat.Basic.0.CommAlgCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} [inst_1 : SizeOf R] (hom' : ↑A →ₐ[R] ↑B),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_iff_isLittleO : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : NormedField β] [inst_1 : LinearOrder β]
  [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop → (Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =o[l] fun a => k a ^ z)
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- The horizontal identity 2-square.  -/
CategoryTheory.TwoSquare.hId : {C₁ : Type u₁} →
  {C₃ : Type u₃} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C₃] →
        (L : CategoryTheory.Functor C₁ C₃) →
          CategoryTheory.TwoSquare (CategoryTheory.Functor.id C₁) L L (CategoryTheory.Functor.id C₃)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Naturality of the left unitor, commutativity of `𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y` and `𝟙_ C ⊗ X ⟶ X ⟶ Y`
 -/
CategoryTheory.MonoidalCategory.leftUnitor_naturality_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y)
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Data.List.TakeDrop
List.tail_take_eq_take_tail : ∀ {α : Type u} (l : List α) (n : ℕ), (List.take n l).tail = List.take (n - 1) l.tail
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.precomposeEquivalence`.

---

If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of
cocones.
 -/
CategoryTheory.Limits.Cocones.postcomposeEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} → (F ≅ G) → (CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone G)
-- Mathlib.Algebra.MvPolynomial.Funext
MvPolynomial.funext_iff : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {p q : MvPolynomial σ R},
  p = q ↔ ∀ (x : σ → R), (MvPolynomial.eval x) p = (MvPolynomial.eval x) q
-- Mathlib.Algebra.Group.Opposite
MulOpposite.unop_zpow : ∀ {α : Type u_1} [inst : DivInvMonoid α] (x : αᵐᵒᵖ) (z : ℤ), MulOpposite.unop (x ^ z) = MulOpposite.unop x ^ z
-- Mathlib.Topology.Category.Compactum
Compactum.instCoeSortType : CoeSort Compactum (Type u_1)
-- Mathlib.FieldTheory.Normal.Defs
AlgHom.normal_bijective : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] (E : Type u_3)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra K E] [IsScalarTower F K E] [h : Normal F E]
  (ϕ : E →ₐ[F] K), Function.Bijective ⇑ϕ
-- Mathlib.Geometry.Euclidean.SignedDist
Affine.Simplex.signedInfDist_apply_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {i j : Fin (n + 1)},
  j ≠ i → (s.signedInfDist i) (s.points j) = 0
-- Mathlib.SetTheory.ZFC.Basic
/-- Convert a ZFC set into a `Set` of ZFC sets  -/
ZFSet.toSet : ZFSet.{u_1} → Set ZFSet.{u_1}
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.homMk_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A B : CategoryTheory.Pretriangulated.Triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂)
  (hom₃ : A.obj₃ ⟶ B.obj₃)
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_3)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
        CategoryTheory.CategoryStruct.comp hom₃ B.mor₃)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_5),
  (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₂ = hom₂
-- Mathlib.Analysis.Calculus.FDeriv.Const
/-- If `f : E → F` has injective differential within `s` at `x`,
it is differentiable within `s` at `x`.  -/
differentiableWithinAt_of_fderivWithin_injective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  Function.Injective ⇑(fderivWithin 𝕜 f s x) → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Data.Rel
SetRel.core_mono : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, Monotone R.core
-- Init.Data.Nat.Lemmas
Nat.mul_lt_mul_pow_succ : ∀ {a b n : ℕ}, 0 < a → 1 < b → n * b < a * b ^ (n + 1)
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.right_id : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    CategoryTheory.BiconeHom J CategoryTheory.Bicone.right CategoryTheory.Bicone.right
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_bot_right : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ], ProbabilityTheory.Indep m' ⊥ μ
-- Aesop.Rule.Name
Aesop.PhaseName.safe : Aesop.PhaseName
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.multiples_zero : ∀ {M : Type u_1} [inst : AddMonoid M], AddSubmonoid.multiples 0 = ⊥
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.isCardinalAccessible_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular]
  [F.IsCardinalAccessible κ], G.IsCardinalAccessible κ
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_pos_iff_degree_pos : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 < p.natDegree ↔ 0 < p.degree
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_le : ∀ {f : Ordinal.{u} → Ordinal.{u}} {a b : Ordinal.{u}}, (∀ (n : ℕ), f^[n] a ≤ b) → Ordinal.nfp f a ≤ b
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_subset_uIcc : ∀ {α : Type u_1} [inst : Lattice α] {a₁ a₂ b₁ b₂ : α},
  a₁ ∈ Set.uIcc a₂ b₂ → b₁ ∈ Set.uIcc a₂ b₂ → Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_nat : ∀ (n : ℕ), ↑↑n = ↑n
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_inv_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_ Z X).inv =
    CategoryTheory.CategoryStruct.comp (β_ Y X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.PullbackCone.IsLimit.type_ext : ∀ {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : CategoryTheory.Limits.PullbackCone f g}
  (hc : CategoryTheory.Limits.IsLimit c) {x y : c.pt},
  (CategoryTheory.ConcreteCategory.hom c.fst) x = (CategoryTheory.ConcreteCategory.hom c.fst) y →
    (CategoryTheory.ConcreteCategory.hom c.snd) x = (CategoryTheory.ConcreteCategory.hom c.snd) y → x = y
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ofStarAlgHom_apply : ∀ {R : Type u_8} {A : Type u_9} {B : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B) (g : B →⋆ₐ[R] A)
  (h₁ : g.comp f = StarAlgHom.id R A) (h₂ : f.comp g = StarAlgHom.id R B) (a : A),
  (StarAlgEquiv.ofStarAlgHom f g h₁ h₂) a = f a
-- Mathlib.Order.Hom.WithTopBot
Function.Embedding.coeWithBot_apply : ∀ {α : Type u_1} (a : α), Function.Embedding.coeWithBot a = ↑a
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.group : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.Linter.Whitespace
/-- The length of the mismatch, as number of characters.  -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.length : Mathlib.Linter.FormatError✝ → ℕ
-- Mathlib.Analysis.Calculus.FDeriv.Congr
/-- In the case `y = x`, see also `hasFDerivWithinAt_congr_set_nhdsNE`,
which does not require the domain to be a T₁ space.  -/
hasFDerivWithinAt_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E} [T1Space E] (y : E),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → (HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x)
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.ofEq_inner : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} {k' : α} {v' : β k'}
  {h : ∀ [Std.OrientedOrd α], k k' = Ordering.eq}, (Std.DTreeMap.Internal.Cell.ofEq k' v' h).inner = some ⟨k', v'⟩
-- Mathlib.CategoryTheory.Limits.Cones
/-- Given a cocone morphism `c ⟶ c'`, construct a cocone morphism on the mapped cocones
functorially.  -/
CategoryTheory.Functor.mapCoconeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F : CategoryTheory.Functor J C} →
                {c c' : CategoryTheory.Limits.Cocone F} → (c' ⟶ c) → (H.mapCocone c' ⟶ H.mapCocone c)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.augmentedCechNerve.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom],
  CategoryTheory.SimplicialObject.augmentedCechNerve = CategoryTheory.SimplicialObject.augmentedCechNerve
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- `EuclideanSpace.single` forms an orthonormal family.  -/
EuclideanSpace.orthonormal_single : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι],
  Orthonormal 𝕜 fun i => EuclideanSpace.single i 1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_equivSentence_symm : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {α : Type u'} (φ : (L.withConstants α).Sentence)
  (v : α → M), (FirstOrder.Language.Formula.equivSentence.symm φ).Realize v ↔ M ⊨ φ
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_toList : ∀ {α : Type u_1} {x : α} {t : RBTree.RBNode α}, x ∈ t.toList ↔ x ∈ t
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Pi.isAffineMap_eval : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_3}
  {X : ι → Type u_4} [inst_3 : (i : ι) → Convexity.ConvexSpace R (X i)] {i : ι}, Convexity.IsAffineMap R fun x => x i
-- Mathlib.Topology.DiscreteSubset
/-- Helper lemma for `codiscreteWithin_iff_locallyFiniteComplementWithin`: A set `s` is
`codiscreteWithin U` iff every point `z ∈ U` has a punctured neighborhood that does not intersect
`U \ s`.  -/
codiscreteWithin_iff_locallyEmptyComplementWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s U : Set X},
  s ∈ Filter.codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ nhdsWithin z {z}ᶜ, t ∩ (U \ s) = ∅
-- Mathlib.Order.Birkhoff
/-- **Birkhoff's Representation Theorem**. Any finite distributive lattice can be embedded in a
powerset lattice.  -/
OrderEmbedding.birkhoffFinset : {α : Type u_1} → [inst : DistribLattice α] → [Fintype α] → [DecidablePred SupIrred] → α ↪o Finset { a // SupIrred a }
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- The isomorphism expressing that `ofCocone c` extends the functor `F`
when `c : Cocone F`.  -/
CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} →
          {F : CategoryTheory.Functor (↑(Set.Iio j)) C} →
            (c : CategoryTheory.Limits.Cocone F) →
              CategoryTheory.SmallObject.restrictionLT (CategoryTheory.SmallObject.SuccStruct.ofCocone c) ⋯ ≅ F
-- Lean.Meta.ForEachExpr
/-- Similar to `Expr.forEach'`, but creates free variables whenever going inside of a binder.
If the inner function returns `false`, deeper subexpressions will not be visited.
  -/
Lean.Meta.forEachExpr' : {m : Type → Type} →
  [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadControlT Lean.MetaM m] → Lean.Expr → (Lean.Expr → m Bool) → m Unit
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- A (random) homomorphism from an algebraic extension of R into an algebraically
closed extension of R.  -/
IsAlgClosed.lift : {M : Type w} →
  [inst : Field M] →
    [IsAlgClosed M] →
      {R : Type u} →
        [inst_2 : CommRing R] →
          [IsDomain R] →
            {S : Type v} →
              [inst_4 : CommRing S] →
                [IsDomain S] →
                  [inst_6 : Algebra R S] →
                    [inst_7 : Algebra R M] →
                      [Module.IsTorsionFree R S] → [Module.IsTorsionFree R M] → [Algebra.IsAlgebraic R S] → S →ₐ[R] M
-- Init.Data.Nat.Dvd
Nat.dvd_of_mod_eq_zero : ∀ {m n : ℕ}, n % m = 0 → m ∣ n
-- Init.Data.SInt.Basic
/-- Arithmetic right shift for 16-bit signed integers. Usually accessed via the `<<<` operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.shiftRight : Int16 → Int16 → Int16
-- Lean.Parser.Syntax
Lean.Parser.Syntax.sepBy1.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.nfpFamily_lt_ord_lift : ∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Ordinal.{max u v}},
  Cardinal.aleph0 < c.cof →
    Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof →
      (∀ (i : ι), ∀ b < c, f i b < c) → ∀ {a : Ordinal.{max u v}}, a < c → Ordinal.nfpFamily f a < c
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instSMulBase : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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] [LieModule R L M],
  LieDerivation.SMulBracketCommClass R L M
-- Mathlib.Analysis.Fourier.AddCircle
has_antideriv_at_fourier_neg : ∀ {T : ℝ},
  Fact (0 < T) →
    ∀ {n : ℤ},
      n ≠ 0 →
        ∀ (x : ℝ), HasDerivAt (fun y => ↑T / (-2 * ↑Real.pi * Complex.I * ↑n) * (fourier (-n)) ↑y) ((fourier (-n)) ↑x) x
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.decompose'.eq_1 : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : DecidableEq M] (φ : MvPolynomial σ R),
  MvPolynomial.decompose' R w φ =
    (DirectSum.mk (fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i))
        (Finset.image (⇑(Finsupp.weight w)) φ.support))
      fun m => ⟨(MvPolynomial.weightedHomogeneousComponent w ↑m) φ, ⋯⟩
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mk.sizeOf_spec : ∀ {K : Type u} [inst : DivisionRing K] [inst_1 : SizeOf K] (toSubring : Subring K)
  (inv_mem' : ∀ x ∈ toSubring.carrier, x⁻¹ ∈ toSubring.carrier),
  sizeOf { toSubring := toSubring, inv_mem' := inv_mem' } = 1 + sizeOf toSubring
-- Mathlib.Analysis.ConstantSpeed
HasConstantSpeedOnWith.ratio : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l l' : NNReal},
  l' ≠ 0 →
    ∀ {φ : ℝ → ℝ},
      MonotoneOn φ s →
        HasConstantSpeedOnWith (f ∘ φ) s l →
          HasConstantSpeedOnWith f (φ '' s) l' → ∀ ⦃x : ℝ⦄, x ∈ s → Set.EqOn φ (fun y => ↑l / ↑l' * (y - x) + φ x) s
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.sliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos →
    ∀ (p : s.Pos) (hp : pos ≤ p), String.Slice.Pattern.Model.IsLongestMatch pat (p.sliceTo pos hp)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- The subsemigroup generated by a set includes the set.  -/
Subsemigroup.subset_closure : ∀ {M : Type u_1} [inst : Mul M] {s : Set M}, s ⊆ ↑(Subsemigroup.closure s)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.comp_preservesLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {B : Type u₄} [inst_4 : CategoryTheory.Category.{v₄, u₄} B]
  {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.PreservesLimit G H],
  CategoryTheory.Limits.PreservesLimit (F.comp G) H
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_toType : ∀ (o : Ordinal.{u_1}), Order.cof o.ToType = o.cof
-- Mathlib.Order.Bounded
Set.unbounded_lt_univ : ∀ {α : Type u_1} [inst : Preorder α] [NoTopOrder α], Set.Unbounded (fun x1 x2 => x1 < x2) Set.univ
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.add_right' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν' : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν' → ∀ (ν : MeasureTheory.Measure α), μ.AbsolutelyContinuous (ν + ν')
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.closure : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsLinearSet s → IsSemilinearSet ↑(AddSubmonoid.closure s)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.piecewise_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [inst_2 : (x : X) → Decidable (x ∈ s)]
  [inst_3 : (y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t)
  (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)),
  ↑(e.piecewise e' s t H H' Hs Heq) = s.piecewise ↑e ↑e'