mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndInclusion_obj_left_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)),
  ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).left.right = b
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.nextCoeff_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionName.mk.sizeOf_spec : ∀ (value : String)
  (isValidExtensionName :
    autoParam (Std.Http.Chunk.IsValidExtensionName value) Std.Http.Chunk.ExtensionName.isValidExtensionName._autoParam),
  sizeOf { value := value, isValidExtensionName := isValidExtensionName } =
    1 + sizeOf value + sizeOf isValidExtensionName
-- Std.Time.Date.Basic
Std.Time.instHSubOffset : HSub Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.DocM.mk : {α : Type} →
  (Lean.Doc.Context → IO.Ref Lean.Doc.InternalState → IO.Ref Lean.Doc.State → Lean.Elab.TermElabM α) → Lean.Doc.DocM α
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.atTop_countable_basis : ∀ {α : Type u_1} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] [Countable α],
  Filter.atTop.HasCountableBasis (fun x => True) Set.Ici
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_of_fintype : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V], G.Colorable (Fintype.card V)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The residue of `ζ(s)` at `s = 1` is equal to 1, expressed using `tsum`.  -/
tendsto_sub_mul_tsum_nat_cpow : Filter.Tendsto (fun s => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) (nhdsWithin 1 {s | 1 < s.re}) (nhds 1)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pushforward_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {U : ι → C} {X Y : C} (g : (i : ι) → U i ⟶ X)
  (f : X ⟶ Y),
  CategoryTheory.Presieve.pushforward f (CategoryTheory.Presieve.ofArrows U g) =
    CategoryTheory.Presieve.ofArrows U fun x => CategoryTheory.CategoryStruct.comp (g x) f
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.associator_hom_inv : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c)
  (h : CategoryTheory.FreeBicategory.Hom c d), CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Data.Set.Image
Subtype.preimage_coe_nonempty : ∀ {α : Type u_1} {s t : Set α}, (Subtype.val ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.LiftActionCoreResult.subgoals : Lean.Elab.Tactic.Grind.LiftActionCoreResult
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) (k i : ℕ), (PowerSeries.coeff i) (H.seq f (k + 1) - H.seq f k) ∈ I ^ k
-- Mathlib.RingTheory.Trace.Basic
/-- Trace of the generator of a simple adjoin equals negative of the next coefficient of
its minimal polynomial coefficient.  -/
trace_adjoinSimpleGen : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsIntegral K x → (Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x) = -(minpoly K x).nextCoeff
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).base =
    CategoryTheory.CategoryStruct.id X.base
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_one : ∀ {d : ℤ}, Zsqrtd.norm 1 = 1
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.eq_1 : ∀ (M : Type u_4) [inst : AddZero M], AddMonoid.End M = (M →+ M)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT?_eq_getEntryLT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  Std.DTreeMap.Internal.Impl.getKeyLT? k t = Option.map (fun x => x.fst) (Std.DTreeMap.Internal.Impl.getEntryLT? k t)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β ky)
  (l r : Std.DTreeMap.Internal.Impl α β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.getKeyLE k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    match hkky : compare k ky with
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyLED k r ky
    | Ordering.eq => ky
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyLE k l ⋯ ⋯
-- Mathlib.Geometry.Manifold.Metrizable
/-- A σ-compact Hausdorff topological manifold over a finite-dimensional real vector space is
metrizable.  -/
Manifold.metrizableSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [inst_3 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [inst : TopologicalSpace M]
  [ChartedSpace H M] [SigmaCompactSpace M] [T2Space M], TopologicalSpace.MetrizableSpace M
-- Lean.Widget.Diff
/-- Given a `diff` between `before` and `after : Expr`, and the rendered `infoAfter : CodeWithInfos` for `after`,
this function decorates `infoAfter` with tags indicating where the expression has changed.

If `useAfter == false` before and after are swapped.  -/
_private.Lean.Widget.Diff.0.Lean.Widget.addDiffTags : Bool → Lean.Widget.ExprDiff✝ → Lean.Widget.CodeWithInfos → Lean.MetaM Lean.Widget.CodeWithInfos
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] (x : MonoidAlgebra R M), MonoidAlgebra.map (AddMonoidHom.id R) x = x
-- Mathlib.Data.Int.Cast.Defs
AddCommGroupWithOne.toAddGroupWithOne : {R : Type u} → [self : AddCommGroupWithOne R] → AddGroupWithOne R
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Two linear maps are equal if they are equal on basis vectors.  -/
Module.Basis.ext : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {R₁ : Type u_13} [inst_3 : Semiring R₁] {σ : R →+* R₁} {M₁ : Type u_14}
  [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁] {f₁ f₂ : M →ₛₗ[σ] M₁}, (∀ (i : ι), f₁ (b i) = f₂ (b i)) → f₁ = f₂
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.e.congr_simp : ∀ {ι : 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] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  (i i_1 : ↥b.support),
  i = i_1 →
    ∀ (a a_1 : ↥b.support ⊕ ι),
      a = a_1 →
        ∀ (a_2 a_3 : ↥b.support ⊕ ι),
          a_2 = a_3 → RootPairing.GeckConstruction.e i a a_2 = RootPairing.GeckConstruction.e i_1 a_1 a_3
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.moduleEndSelfOp_symm_apply : ∀ (R : Type u_1) {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : Module.End Aᵐᵒᵖ A), (AlgEquiv.moduleEndSelfOp R).symm f = f 1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_neg : ∀ (x : ENNReal) (y : ℝ), x ^ (-y) = (x ^ y)⁻¹
-- Mathlib.Order.WellFoundedSet
Set.IsWF.min_union : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Set α} (hs : s.IsWF) (hsn : s.Nonempty) (ht : t.IsWF) (htn : t.Nonempty),
  ⋯.min ⋯ = min (hs.min hsn) (ht.min htn)
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValued`. -/
FunctionField.inftyValuedFqt : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → Valued (RatFunc F) (WithZero (Multiplicative ℤ))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.latticeBasis_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)),
  (NumberField.mixedEmbedding.latticeBasis K) i = (NumberField.mixedEmbedding K) ((NumberField.integralBasis K) i)
-- Lean.Data.NameMap.Basic
/-- The union of two `NameSet`s.  -/
Lean.NameSet.append : Lean.NameSet → Lean.NameSet → Lean.NameSet
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.ContainsIdentities] [P.RespectsIso],
  (AlgebraicGeometry.Scheme.precoverage P).HasIsos
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.comap_eq : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β),
  UniformSpace.comap (⇑h) inst_1 = inst
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.smartHCongr?.loop : Congr!.Config →
  Lean.MVarId → ℕ → Lean.Expr → Lean.Expr → List Lean.Expr → List Lean.Expr → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse_comp_of_left : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂},
  g.IsInvertible → (g ∘SL f).inverse = f.inverse ∘SL g.inverse
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_union_le_size_add_size : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.kleisliCatEquivKleisli_functor_map_of : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m] {X Y : CategoryTheory.KleisliCat m} (f : X ⟶ Y),
  ((CategoryTheory.kleisliCatEquivKleisli m).functor.map f).of = TypeCat.ofHom f
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.foldM_filterMapWithPostcondition.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (x : Option γ) (h_1 : (c : γ) → motive (some c))
  (h_2 : (x : Option γ) → motive x),
  (∀ (c : γ), x = some c → False) →
    (match x with
      | some c => h_1 c
      | x => h_2 x) =
      h_2 x
-- Lean.Elab.DefView
Lean.Elab.HeaderProcessedSnapshot.toSnapshot : Lean.Elab.HeaderProcessedSnapshot → Lean.Language.Snapshot
-- Mathlib.Data.Rel
SetRel.preimage_empty_right : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.preimage ∅ = ∅
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_of_isOpen : ∀ {𝕜 : 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}, IsOpen s → x ∈ s → fderivWithin 𝕜 f s x = fderiv 𝕜 f x
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.comm_comp_comul : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [Coalgebra.IsCocomm R A],
  ↑(TensorProduct.comm R A A) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.erase_single : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (a : α) (b : M),
  (SkewMonoidAlgebra.erase a) (SkewMonoidAlgebra.single a b) = 0
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_def : ∀ (n : ℕ),
  Polynomial.bernoulli n = ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (bernoulli (n - i) * ↑(n.choose i))
-- Init.Data.Nat.Lemmas
/-- Dependent variant of `exists_lt_succ_left`.  -/
Nat.exists_lt_succ_left' : ∀ {n : ℕ} {p : (m : ℕ) → m < n + 1 → Prop}, (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 ⋯ ∨ ∃ m, ∃ (h : m < n), p (m + 1) ⋯
-- Mathlib.Analysis.Complex.Basic
Complex.im_tsum : ∀ {α : Type u_1} {L : SummationFilter α} [L.NeBot] {f : α → ℂ},
  Summable f L → (∑'[L] (a : α), f a).im = ∑'[L] (a : α), (f a).im
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given `G`-representations on `k`-modules `V, W`, a linear map `V →ₗ[k] W` commuting with
the representations induces a `k`-linear map between the coinvariants.  -/
Representation.Coinvariants.map : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommRing k] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module k V] →
                [inst_4 : AddCommGroup W] →
                  [inst_5 : Module k W] →
                    (ρ : Representation k G V) →
                      (τ : Representation k G W) → ρ.IntertwiningMap τ → ρ.Coinvariants →ₗ[k] τ.Coinvariants
-- Mathlib.Data.Fintype.Order
Bool.completeBooleanAlgebra : CompleteBooleanAlgebra Bool
-- Mathlib.Data.List.DropRight
List.rdrop_concat_succ : ∀ {α : Type u_1} (l : List α) (n : ℕ) (x : α), (l ++ [x]).rdrop (n + 1) = l.rdrop n
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.im_zero : Complex.UnitClosedDisc.im 0 = 0
-- Mathlib.Topology.Sheaves.Skyscraper
/-- The unit in `Presheaf.stalkFunctor ⊣ skyscraperPresheafFunctor`
 -/
StalkSkyscraperPresheafAdjunctionAuxs.unit : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasColimits C] →
              CategoryTheory.Functor.id (TopCat.Presheaf C X) ⟶
                (TopCat.Presheaf.stalkFunctor C p₀).comp (skyscraperPresheafFunctor p₀)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- The chosen cone `TopCat.limitCone F` for a functor `F : J ⥤ TopCat` is a limit cone.
Generally you should just use `limit.isLimit F`, unless you need the actual definition
(which is in terms of `Types.limitConeIsLimit`).
 -/
TopCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J TopCat) → CategoryTheory.Limits.IsLimit (TopCat.limitCone F)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
cauchySeq_finset_iff_nat_tsum_vanishing : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] {f : ℕ → G},
  (CauchySeq fun s => ∑ n ∈ s, f n) ↔ ∀ e ∈ nhds 0, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
-- Mathlib.Combinatorics.Digraph.Orientation
Digraph.toSimpleGraphInclusive_mono : ∀ {V : Type u_1}, Monotone Digraph.toSimpleGraphInclusive
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.getSlotValue : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT (ST IO.RealWorld) m] →
        IO.Ref (Std.Slot✝ α) → ℕ → Std.AtomicT (Std.Bounded.State✝ α) m (Option α × Bool)
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.decidableMemCentralizer.eq_1 : ∀ {M : Type u_1} {S : Set M} [inst : Monoid M] (a : M) [inst_1 : Decidable (∀ b ∈ S, b * a = a * b)],
  Submonoid.decidableMemCentralizer a = decidable_of_iff' (∀ g ∈ S, g * a = a * g) ⋯
-- Init.Grind.Lemmas
Lean.Grind.eq_true_of_not_eq_false : ∀ {a : Prop}, (¬a) = False → a = True
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The functor `hoFunctor : SSet ⥤ Cat` preserves binary products of simplicial sets `X` and
`Y`.  -/
CategoryTheory.hoFunctor.preservesBinaryProduct : ∀ (X Y : SSet), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) SSet.hoFunctor
-- Std.Data.HashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashMap.getKey! : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [Inhabited α] → Std.HashMap α β → α → α
-- Init.Prelude
_private.Init.Prelude.0.Lean.extractMainModule : List Lean.MacroScope → Lean.Name → List Lean.Name → Lean.MacroScopesView
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
List.iInf_mem_map_of_exists_le_sInf_empty : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {l : List ι} (f : ι → α),
  (∃ x ∈ l, f x ≤ sInf ∅) → ⨅ x ∈ l, f x ∈ List.map f l
-- Init.Data.Vector.Basic
Vector.mk : {α : Type u} → {n : ℕ} → (toArray : Array α) → toArray.size = n → Vector α n
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- The left uniformity on a topological additive group (as opposed to the right
uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a
`IsUniformAddGroup` structure. Two important special cases where they _do_ coincide are for
commutative additive groups (see `isUniformAddGroup_of_addCommGroup`) and for compact
additive groups (see `IsUniformAddGroup.of_compactSpace`).  -/
IsTopologicalAddGroup.leftUniformSpace : (G : Type u_1) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [IsTopologicalAddGroup G] → UniformSpace G
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorph.mfderivToContinuousLinearEquiv_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N}
  (hf : IsLocalDiffeomorph I J n f) (hn : n ≠ 0) (x : M), ↑(hf.mfderivToContinuousLinearEquiv hn x) = mfderiv% f x
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.beq_iff_le_and_ge : ∀ {α : Type u} (self : Std.Packages.PreorderOfLEArgs α),
  let this := self.le;
  let this_1 := self.decidableLE;
  let this_2 := self.beq;
  ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a
-- Mathlib.Data.PNat.Find
PNat.find_comp_succ : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (h₂ : ∃ n, p (n + 1)), ¬p 1 → PNat.find h = PNat.find h₂ + 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Limits.Cocone.underPost_pt : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {D : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone D)
  (j : J), (c.underPost j).pt = CategoryTheory.Under.mk (c.ι.app j)
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourier_eq' : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : V → E) (w : V),
  FourierTransform.fourier f w = ∫ (v : V), Complex.exp (↑(-2 * Real.pi * inner ℝ v w) * Complex.I) • f v
-- Init.Data.String.Defs
String.Pos.Raw.isValidForSlice_of_eq_rawEndPos : ∀ {p : String.Pos.Raw} {s : String.Slice}, p = s.rawEndPos → String.Pos.Raw.IsValidForSlice s p
-- Lean.DocString.Links
/-- Computes the root of the Lean reference manual that should be used for targets.

If the environment variable `LEAN_MANUAL_ROOT` is set, it is used as the root. If not, but a manual
root is pre-configured for the current Lean executable (typically true for releases), then it is
used. If neither are true, then `https://lean-lang.org/doc/reference/latest/` is used.
 -/
Lean.manualRoot : String
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.comp.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P] (hnp : ZeroHom N P)
  (hmn : ZeroHom M N), hnp.comp hmn = { toFun := fun x => hnp (hmn x), map_zero' := ⋯ }
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a bi-Heyting homomorphism preserves the Heyting implication.  -/
BiheytingHom.map_himp' : ∀ {α : Type u_6} {β : Type u_7} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] (self : BiheytingHom α β)
  (a b : α), self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- seminormed group instance on the product of finitely many normed groups, using the `L^p`
norm.  -/
PiLp.seminormedAddCommGroup : (p : ENNReal) →
  {ι : Type u_2} →
    (β : ι → Type u_4) →
      [hp : Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → SeminormedAddCommGroup (β i)] → SeminormedAddCommGroup (PiLp p β)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity_empty_right : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (s : Finset α),
  Rel.edgeDensity r s ∅ = 0
-- Plausible.Arbitrary
Plausible.Array.Arbitrary : {α : Type u_1} → [Plausible.Arbitrary α] → Plausible.Arbitrary (Array α)
-- Init.Data.UInt.Lemmas
UInt8.toNat_lt_size : ∀ (a : UInt8), a.toNat < UInt8.size
-- Mathlib.Data.Finset.Empty
Finset.coe_nonempty : ∀ {α : Type u_1} {s : Finset α}, (↑s).Nonempty ↔ s.Nonempty
-- Lean.Meta.Basic
/-- If diagnostics are enabled, record that instance `declName` was used during TC resolution.  -/
Lean.Meta.recordInstance : Lean.Name → Lean.MetaM Unit
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairMap_of_snd_mem_fst : ∀ (σ : Type u_1) [inst : DecidableEq σ] {t : Finset σ × σ},
  t.2 ∈ t.1 → MvPolynomial.NewtonIdentities.pairMap✝ σ t = (t.1.erase t.2, t.2)
-- Mathlib.Combinatorics.Colex
Finset.Colex.le_def : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Colex (Finset α)},
  s ≤ t ↔ ∀ ⦃a : α⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b ∈ ofColex t, b ∉ ofColex s ∧ a ≤ b
-- Mathlib.RingTheory.MvPowerSeries.Equiv
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.coeff_coeff_optionFunLeft : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (p : MvPowerSeries (Option σ) R) (n : ℕ) (x : σ →₀ ℕ),
  (MvPowerSeries.coeff x) ((PowerSeries.coeff n) (MvPowerSeries.optionFunLeft✝ σ R p)) =
    (MvPowerSeries.coeff (Finsupp.optionElim n x)) p
-- Mathlib.Algebra.Group.Defs
eq_neg_of_add_eq_zero_left : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, a + b = 0 → a = -b
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.instIteratorOfPure.match_3.eq_1 : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ]
  {m : Type → Type u_1} {s : String.Slice} (motive : Std.IterM m String.Slice → Sort u_2) (currPos : s.Pos)
  (searcher : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (currPos : s.Pos) →
      (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.RevSplitIterator.operating currPos searcher })
  (h_2 : Unit → motive { internalState := String.Slice.RevSplitIterator.atEnd }),
  (match { internalState := String.Slice.RevSplitIterator.operating currPos searcher } with
    | { internalState := String.Slice.RevSplitIterator.operating currPos searcher } => h_1 currPos searcher
    | { internalState := String.Slice.RevSplitIterator.atEnd } => h_2 ()) =
    h_1 currPos searcher