mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- A morphism respecting addition, multiplication, and scalar multiplication
(denoted as `A →ₛₙₐ[φ] B`, or `A →ₙₐ[R] B` when `φ` is the identity on `R`).
When these arise from algebra structures, this is the same
as a not-necessarily-unital morphism of algebras.  -/
«term_→ₙₐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Group.Arithmetic
AddSubmonoid.instMeasurableVAdd : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : MeasurableSpace α] [inst_2 : AddMonoid M]
  [inst_3 : AddAction M α] [MeasurableVAdd M α] (s : AddSubmonoid M), MeasurableVAdd (↥s) α
-- Init.Data.Nat.Lcm
Nat.instCommutativeLcm : Std.Commutative Nat.lcm
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.foldl_eq_foldl_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  [inst : Std.TransCmp cmp] {f : δ → (a : α) → β a → δ} {init : δ},
  Std.ExtDTreeMap.foldl f init t = List.foldl (fun a b => f a b.fst b.snd) init t.toList
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.match_1.congr_eq_6 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (x : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (a b : Lean.Grind.Linarith.Expr),
  x = a.add b →
    (match x with
      | a.sub b => h_1 a b
      | a.neg => h_2 a
      | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
      | Lean.Grind.Linarith.Expr.zero => h_4 ()
      | Lean.Grind.Linarith.Expr.var v => h_5 v
      | a.add b => h_6 a b
      | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) ≍
      h_6 a b
-- Init.Sym.Simp.SimprocDSL
Lean.Parser.Category.sym_simproc : Lean.Parser.Category
-- Std.Internal.Do.PredTrans
/-- Monotonicity property for a predicate transformer: if both `post` and `epost` grow,
then the resulting precondition grows.  -/
Std.Internal.Do.PredTrans.monotone : {Pred : Type u_1} →
  {EPred : Type u_2} →
    {α : Type u_3} →
      [Lean.Order.PartialOrder Pred] → [Lean.Order.PartialOrder EPred] → Std.Internal.Do.PredTrans Pred EPred α → Prop
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.Nonsingular.of_leftRegular : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {A : Matrix n n R}, IsLeftRegular A → A.Nonsingular
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.instIsSplitMonoRightIArrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : Y ⟶ X} {g : W ⟶ Z}
  (h : CategoryTheory.RetractArrow f g), CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right h.i)
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.one_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C), CategoryTheory.MonObj.one = M.η
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.simprocCore : Bool → Lean.Meta.Simp.SimprocTree → Lean.PHashSet Lean.Name → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.subset_smul_self_of_ne_zero : ∀ {α : Type u_1} (s : Multiset α) {n : ℕ}, n ≠ 0 → s ⊆ n • s
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pushouts_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {A B X Y : C}
  {f : A ⟶ X} {q : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}, CategoryTheory.IsPushout f q p g → P q → P.pushouts p
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.add_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂), (f + g).hom₃ = f.hom₃ + g.hom₃
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The edist to a set depends continuously on the point  -/
Metric.continuous_infEDist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Continuous fun x => Metric.infEDist x s
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {V : (x : M') → TangentSpace I' x} {c : 𝕜}, VectorField.mpullback I I' f (c • V) = c • VectorField.mpullback I I' f V
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.IsPrincipal.iterate_lt : ∀ {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  a < o → Ordinal.IsPrincipal op o → ∀ (n : ℕ), (op a)^[n] a < o
-- Std.Data.HashMap.Raw
/-- Computes the intersection of the given hash maps. The result will only contain entries from the first map.

This function always merges the smaller map into the larger map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashMap.Raw.inter : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → Std.HashMap.Raw α β → Std.HashMap.Raw α β
-- Init.Data.SInt.Lemmas
Int32.ofNat_bitVecToNat : ∀ (n : BitVec 32), Int32.ofNat n.toNat = Int32.ofBitVec n
-- Lean.Meta.Tactic.Simp.Arith.Util
Lean.Meta.Simp.Arith.isLinearCnstr : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- If `C` has all colimits of diagrams `span f g`, then it has all pushouts  -/
CategoryTheory.Limits.hasPushouts_of_hasColimit_span : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)],
  CategoryTheory.Limits.HasPushouts C
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.contMDiff : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] (s : ContMDiffSection I F n V),
  ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, s x⟩
-- Mathlib.SetTheory.Cardinal.Free
instInfiniteFreeAddMonoidOfNonempty : ∀ (α : Type u) [Nonempty α], Infinite (FreeAddMonoid α)
-- Mathlib.Data.Set.Semiring
instPartialOrderSetSemiring : (α : Type u_1) → PartialOrder (SetSemiring α)
-- Init.Data.Float.Float32
/-- Obtains a `Float32` whose value is near the given `UInt32`.

It will be exactly the value of the given `UInt32` if such a `Float32` exists. If no such `Float32`
exists, the returned value will either be the smallest `Float32` that is larger than the given
value, or the largest `Float32` that is smaller than the given value.

This function has a logical model in terms of `Float32.Model`, but is overridden at runtime with an
efficient implementation.
 -/
UInt32.toFloat32 : UInt32 → Float32
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.dualTensorHom_invFun : ∀ {G : Type u_6} {k : Type u_7} {V : Type u_8} {W : Type u_9} [inst : Group G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : FiniteDimensional k V] (ρ : Representation k G V) (σ : Representation k G W) (a : V →ₗ[k] W),
  (Representation.Equiv.dualTensorHom ρ σ).invFun a = (LinearEquiv.ofBijective (dualTensorHom k V W) ⋯).symm a
-- Init.Data.BitVec.Lemmas
BitVec.umod_def : ∀ {n : ℕ} {x y : BitVec n}, x % y = BitVec.ofNat n (x.toNat % y.toNat)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.ihom_adjunction_unit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.Closed A], (CategoryTheory.ihom.adjunction A).unit = CategoryTheory.ihom.coev A
-- Lean.Server.Requests
Lean.Server.lookupLspRequestHandler : String → IO (Option Lean.Server.RequestHandler)
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.ofNNReal_finsetSum : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldrM_eq_foldrM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.DTreeMap.Raw.foldrM (fun a x d => f a d) init t = List.foldrM f init t.keys
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.iteratedDeriv_six_relation_mul_id_pow_six : ∀ (L : PeriodPair), iteratedDeriv 6 (PeriodPair.relation✝ L * id ^ 6) 0 = 0
-- Mathlib.Topology.SeparatedMap
IsSeparatedMap.isClosed_eqLocus : ∀ {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace A] {f : X → Y}
  {g₁ g₂ : A → X}, Continuous g₁ → Continuous g₂ → IsSeparatedMap f → f ∘ g₁ = f ∘ g₂ → IsClosed {a | g₁ a = g₂ a}
-- Mathlib.Order.Lattice
/-- Pointwise infimum of two monotone functions is a monotone function.  -/
Monotone.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β},
  Monotone f → Monotone g → Monotone (f ⊓ g)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.subset_normalizer_of_normal : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G} [hH : H.Normal], S ⊆ ↑(AddSubgroup.normalizer ↑H)
-- Lean.Meta.Basic
Lean.Meta.instBEqAbstractMVarsResult.beq : Lean.Meta.AbstractMVarsResult → Lean.Meta.AbstractMVarsResult → Bool
-- Mathlib.Data.Finset.Union
Finset.disjoint_biUnion_right : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset β) (t : Finset α) (f : α → Finset β),
  Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).isSome).getD fallback
-- Mathlib.Topology.Order.LiminfLimsup
eventually_liminf_le : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) eventually_liminf_le._auto_1 →
    ∀ᶠ (b : β) in f, Filter.liminf u f ≤ u b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_
/-- If `X` represents a presheaf of commutative monoids, then `X` is a commutative monoid object.  -/
CategoryTheory.IsCommMonObj.ofRepresentableBy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ CommMonCat)
  (α : (F.comp (CategoryTheory.forget CommMonCat)).RepresentableBy X), CategoryTheory.IsCommMonObj X
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.category.inj : ∀ {cat cat_1 : Lean.Name},
  Lean.Parser.ParserResolution.category cat = Lean.Parser.ParserResolution.category cat_1 → cat = cat_1
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.isSome_least?_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α], Std.PRange.least?.isSome = true ↔ Nonempty α
-- Init.Data.List.Basic
/-- Returns the last element in the list, or `none` if the list is empty.

Alternatives include `List.getLastD`, which takes a fallback value for empty lists, and
`List.getLast!`, which panics on empty lists.

Examples:
 * `["circle", "rectangle"].getLast? = some "rectangle"`
 * `["circle"].getLast? = some "circle"`
 * `([] : List String).getLast? = none`
 -/
List.getLast? : {α : Type u} → List α → Option α
-- Lean.Server.CodeActions.Basic
/-- A code action optionally supporting a lazy code action computation that is only run when the user clicks on
the code action in the editor.

If you want to use the lazy feature, make sure that the `edit?` field on the `eager` code action result is `none`.
  -/
Lean.Server.LazyCodeAction : Type
-- Mathlib.SetTheory.ZFC.Class
Class.coe_powerset : ∀ (x : ZFSet.{u}), ↑x.powerset = (↑x).powerset
-- Mathlib.Algebra.Ring.Defs
/-- **Alias** of `left_distrib`. -/
mul_add : ∀ {R : Type v} [inst : Mul R] [inst_1 : Add R] [LeftDistribClass R] (a b c : R), a * (b + c) = a * b + a * c
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Path.eq_cast_iff_heq : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v)
  (p' : Quiver.Path u' v'), p' = Quiver.Path.cast hu hv p ↔ p' ≍ p
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Real.differentiableAt_exp : ∀ {x : ℝ}, DifferentiableAt ℝ Real.exp x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.SupportsStmt.eq_7 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ),
  Turing.TM2.SupportsStmt S Turing.TM2.Stmt.halt = True
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial_one : Nat.superFactorial 1 = 1
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.mem_spanningSets_of_index_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (x : α)
  {n : ℕ}, MeasureTheory.spanningSetsIndex μ x ≤ n → x ∈ MeasureTheory.spanningSets μ n
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_subset_iff : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set α},
  ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The following statement says that summing over `s`-factored numbers such that
`s` contains `primesBelow N` for large enough `N` gets us arbitrarily close to the sum
over all natural numbers (assuming `f` is summable and `f 0 = 0`; the latter since
`0` is not `s`-factored).  -/
EulerProduct.norm_tsum_factoredNumbers_sub_tsum_lt : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  Summable f →
    f 0 = 0 →
      ∀ {ε : ℝ},
        0 < ε →
          ∃ N, ∀ (s : Finset ℕ), N.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m‖ < ε
-- Mathlib.Data.Finset.Fold
Finset.fold.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (op : β → β → β) [hc : Std.Commutative op] [ha : Std.Associative op] (b : β) (f : α → β)
  (s : Finset α), Finset.fold op b f s = Multiset.fold op b (Multiset.map f s.val)
-- Init.Control.Except
instMonadExceptOfExceptTOfMonad : (m : Type u → Type v) → (ε : Type u) → [Monad m] → MonadExceptOf ε (ExceptT ε m)
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.cardQuot_pow_inertiaDeg`. -/
Ideal.cardQuot_pow_inertiaDeg' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [Module.Finite R S] [p.IsMaximal] [q.IsMaximal] [q.LiesOver p],
  Submodule.cardQuot p ^ q.inertiaDeg R = Submodule.cardQuot q
-- Init.Data.BitVec.Lemmas
BitVec.mul_def : ∀ {n : ℕ} {x y : BitVec n}, x * y = { toFin := x.toFin * y.toFin }
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of a monoid by a congruence relation is a monoid.  -/
Con.mulOneClass : {M : Type u_1} → [inst : MulOneClass M] → (c : Con M) → MulOneClass c.Quotient
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, k ∉ t₁ → Std.DTreeMap.Const.getD (t₁ ∩ t₂) k fallback = fallback
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_zero : ∀ {R : Type u_1} [inst : Semiring R], (Cubic.toPoly 0).degree = ⊥
-- Lean.Elab.Exception
Lean.Elab.isAbortException : Lean.Exception → Bool
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasProd.sigma_of_hasProd : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α] [T3Space α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α},
  HasProd g a → (∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)) → Multipliable f → HasProd f a
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.term_pos : ∀ {a : ℕ → ℂ} {n : ℕ}, n ≠ 0 → 0 < a n → ∀ (x : ℝ), 0 < LSeries.term a (↑x) n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapAddMon_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapAddMon.inverse = e.inverse.mapAddMon
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ._auto_1),
  CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀) (X.δ f₁ f₂₃ n₀ n₁ hn₁) =
    X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
-- Mathlib.RingTheory.Valuation.ValuationSubring
IsLocalRing.residue.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R],
  IsLocalRing.residue R = Ideal.Quotient.mk (IsLocalRing.maximalIdeal R)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Finpartition.ofSubset.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a b : α} (P P_1 : Finpartition a) (e_P : P = P_1)
  {parts parts_1 : Finset α} (e_parts : parts = parts_1) (subset : parts ⊆ P.parts) (sup_parts : parts.sup id = b),
  P.ofSubset subset sup_parts = P_1.ofSubset ⋯ ⋯
-- Init.Data.Rat.Lemmas
Rat.natCast_add : ∀ (a b : ℕ), ↑(a + b) = ↑a + ↑b
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalAssumption : Lean.Elab.Tactic.Tactic
-- Init.Coe
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
or by double type ascription `((x : α) : β)`.  -/
CoeHTCT.coe : {α : Sort u} → {β : Sort v} → [self : CoeHTCT α β] → α → β
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.toLp_norm_eq_toLp_norm_coe : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  [inst_6 : Fact (1 ≤ p)] {𝕜 : Type u_4} [inst_7 : NontriviallyNormedField 𝕜] [inst_8 : NormedSpace 𝕜 E],
  ‖ContinuousMap.toLp p μ 𝕜‖ = ‖BoundedContinuousFunction.toLp p μ 𝕜‖
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → Bool} {k : α},
  (Std.DHashMap.filter f m).getKey! k =
    ((m.getKey? k).pfilter fun x_2 h' => f x_2 (Std.DHashMap.Const.get m x_2 ⋯)).get!
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_eq_false_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = true → l.isEmpty = false
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldl_eq_foldl_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {f : δ → (a : α) → β a → δ} {init : δ},
  Std.DTreeMap.Raw.foldl f init t = Array.foldl (fun a b => f a b.fst b.snd) init t.toArray
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} (J : α → Type u')
  [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] [∀ (a : α), Nonempty (J a)], ⊥.limitsClosure J = ⊥
-- Lean.Environment
Lean.instInhabitedModuleData.default : Lean.ModuleData
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.mem_closure_of_mem : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {x : M}, x ∈ s → x ∈ Submonoid.closure s
-- Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
_private.Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Init.Data.Int.DivMod.Lemmas
Int.lt_tdiv_of_mul_lt : ∀ {a b c : ℤ}, 0 ≤ b → b ∣ c → a * b < c → a < c.tdiv b
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- Each set has to be measurable.  -/
MeasureTheory.Measure.MeasureDense.measurable : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  μ.MeasureDense 𝒜 → ∀ s ∈ 𝒜, MeasurableSet s
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.SpecΓIdentity_app : ∀ (R : CommRingCat), AlgebraicGeometry.Scheme.SpecΓIdentity.app R = AlgebraicGeometry.Scheme.ΓSpecIso R
-- Init.Data.Array.Lemmas
Array.filter_flatten : ∀ {α : Type u_1} {p : α → Bool} {xss : Array (Array α)} {stop : ℕ},
  stop = xss.flatten.size → Array.filter p xss.flatten 0 stop = (Array.map (fun as => Array.filter p as) xss).flatten
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_filterMap_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  (Std.DHashMap.filterMap f m).isEmpty = true ↔
    ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (Std.DHashMap.Const.get m k h) = none
-- Mathlib.Probability.Distributions.Uniform
/-- A random variable `X` has uniform distribution on `s` if its push-forward measure is
`(μ s)⁻¹ • μ.restrict s`.  -/
MeasureTheory.pdf.IsUniform : {E : Type u_1} →
  [inst : MeasurableSpace E] →
    {Ω : Type u_2} →
      {x : MeasurableSpace Ω} →
        (Ω → E) →
          Set E →
            MeasureTheory.Measure Ω → autoParam (MeasureTheory.Measure E) MeasureTheory.pdf.IsUniform._auto_1 → Prop
-- Init.Data.Rat.Lemmas
Rat.maybeNormalize.congr_simp : ∀ (num num_1 : ℤ) (e_num : num = num_1) (den den_1 : ℕ) (e_den : den = den_1) (g g_1 : ℕ) (e_g : g = g_1)
  (dvd_num : ↑g ∣ num) (dvd_den : g ∣ den) (den_nz : den / g ≠ 0) (reduced : (num / ↑g).natAbs.Coprime (den / g)),
  Rat.maybeNormalize num den g dvd_num dvd_den den_nz reduced = Rat.maybeNormalize num_1 den_1 g_1 ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_zero : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B}, AddMonoidAlgebra.supDegree D 0 = ⊥
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.dual_isCocircuit_iff : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M✶.IsCocircuit C ↔ M.IsCircuit C
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] [inst_2 : Fintype α], Finset.univ⁻¹ = Finset.univ