mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Topology
/-- If we dilate a convex set about a point in its interior by a scale `t > 1`, the interior of
the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about `x`.  -/
Convex.subset_interior_image_homothety_of_one_lt : ∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {s : Set E},
  Convex ℝ s → ∀ {x : E}, x ∈ interior s → ∀ (t : ℝ), 1 < t → s ⊆ interior (⇑(AffineMap.homothety x t) '' s)
-- Mathlib.Analysis.Normed.Lp.Matrix
/-- `Matrix.toLin'` adapted for `PiLp R _`.  -/
Matrix.toLpLin : {m : Type u_1} →
  {n : Type u_2} →
    {R : Type u_4} →
      [Fintype n] →
        [DecidableEq n] →
          [inst : CommRing R] → (p q : ENNReal) → Matrix m n R ≃ₗ[R] WithLp p (n → R) →ₗ[R] WithLp q (m → R)
-- Mathlib.Order.RelSeries
/-- In ℕ, the head and tail of an `LTSeries` differ at least by the length of the series  -/
LTSeries.head_add_length_le_nat : ∀ (p : LTSeries ℕ), RelSeries.head p + p.length ≤ RelSeries.last p
-- Mathlib.ModelTheory.Semantics
/-- Two structures are elementarily equivalent when they satisfy the same sentences.  -/
FirstOrder.«term_≅[_]_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hurwitzOddFEPair_k : ∀ (a : UnitAddCircle), (HurwitzZeta.hurwitzOddFEPair a).k = 3 / 2
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The (reflexive) reachability relation for the TM2 model.  -/
Turing.TM2.Reaches : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        [DecidableEq K] → (Λ → Turing.TM2.Stmt Γ Λ σ) → Turing.TM2.Cfg Γ Λ σ → Turing.TM2.Cfg Γ Λ σ → Prop
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.ofSnowflaking_comp_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1},
  ⇑Metric.Snowflaking.ofSnowflaking ∘ ⇑Metric.Snowflaking.toSnowflaking = id
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.diff! m₂) = true},
  (m₁.diff! m₂).getKey k h_contains = m₁.getKey k ⋯
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instZPow.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : IsTopologicalGroup β],
  ContinuousMap.instZPow = { pow := fun f z => { toFun := ⇑f ^ z, continuous_toFun := ⋯ } }
-- Mathlib.Algebra.Ring.Units
Units.map_neg_one : ∀ {α : Type u} {β : Type v} [inst : Ring α] {F : Type u_1} [inst_1 : Ring β] [inst_2 : FunLike F α β]
  [inst_3 : RingHomClass F α β] (f : F), (Units.map ↑f) (-1) = -1
-- Mathlib.Order.Basic
exists_between' : ∀ {α : Type u_2} [inst : LT α] [DenselyOrdered α] {a₁ a₂ : α}, a₂ < a₁ → ∃ a < a₁, a₂ < a
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.invariantCardinalRank_comap : ∀ {α : Type u} {β : Type v} (M : Matroid β) [M.InvariantCardinalRank] (f : α → β), (M.comap f).InvariantCardinalRank
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.range_pair : ∀ {α : Type u_2} [inst : Preorder α] (a b : α) (hab : a ≤ b),
  Set.range ⇑(OmegaCompletePartialOrder.Chain.pair a b hab) = {a, b}
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'_hom_app : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) (X : ModuleCat R),
  (ModuleCat.restrictScalarsId' f hf).hom.app X = (ModuleCat.restrictScalarsId'App f hf X).hom
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.mul_inv_le_one`. -/
Units.le_of_mul_inv_le_one : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a : M} (u : Mˣ), a * ↑u⁻¹ ≤ 1 → a ≤ ↑u
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toArray_mapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  [LawfulMonad m] [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m γ},
  (Std.Iter.mapWithPostcondition f it).toArray = Array.mapM (fun x => (f x).run) it.toArray
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.bind_pure : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {x : Std.Iterators.HetT m α},
  x.bind Std.Iterators.HetT.pure = x
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_pos_of_pos_of_dvd : ∀ {a b : ℤ}, 0 < a → 0 ≤ b → b ∣ a → 0 < a.tdiv b
-- Mathlib.Order.Monotone.Defs
/-- A function `f` is strictly monotone on `s` if, for all `a, b ∈ s`, `a < b` implies
`f a < f b`.  -/
StrictMonoOn : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Set α → Prop
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPSnd_comp_swap : pointedToTwoPSnd.comp TwoP.swap = pointedToTwoPFst
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Refl.ne_imp_iff`.

---

If a reflexive relation `r : α → α → Prop` holds over `x y : α`,
then it holds whether or not `x ≠ y`.  -/
Reflexive.ne_imp_iff : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {x y : α}, x ≠ y → r x y ↔ r x y
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsBigOWith.rpow : ∀ {α : Type u_1} {r c : ℝ} {l : Filter α} {f g : α → ℝ},
  Asymptotics.IsBigOWith c l f g →
    0 ≤ c → 0 ≤ r → 0 ≤ᶠ[l] g → Asymptotics.IsBigOWith (c ^ r) l (fun x => f x ^ r) fun x => g x ^ r
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Given `x = f * g` with `g` homogeneous of positive degree,
this is the map `A_{(f)} → A_{(x)}` taking `a/f^i` to `ag^i/(fg)^i`.  -/
HomogeneousLocalization.awayMapₐ : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                (𝒜 : ι → σ) →
                  [inst_5 : GradedRing 𝒜] →
                    {e : ι} →
                      {f g : A} →
                        g ∈ 𝒜 e →
                          {x : A} →
                            x = f * g → HomogeneousLocalization.Away 𝒜 f →ₐ[↥(𝒜 0)] HomogeneousLocalization.Away 𝒜 x
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.maxKey? l = some k ↔
      Std.Internal.List.getKey? k l = some k ∧
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT : {α : Type u} →
  [Std.PRange.UpwardEnumerable α] → [inst : LT α] → [DecidableLT α] → Std.Iterator (Std.Rxo.Iterator α) Id α
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- **Alias** of `SimpleGraph.Walk.support_subset_support_append_right`. -/
SimpleGraph.Walk.subset_support_append_right : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w), q.support ⊆ (p.append q).support
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.gammaSet_eq_gcd_mul_divIntMap : ∀ {r : ℕ} {v : Fin 2 → ℤ}, v ∈ EisensteinSeries.gammaSet 1 r 0 → v = r • EisensteinSeries.divIntMap (↑r) v
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.Machine.mk : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Reader dir →
    Std.Http.Protocol.H1.Writer dir →
      Std.Http.Protocol.H1.Config →
        Array (Std.Http.Protocol.H1.Event dir) →
          Option Std.Http.Protocol.H1.Error →
            Option Std.Time.PlainDateTime → Bool → Bool → Bool → Std.Http.Protocol.H1.Machine dir
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.rnDeriv_neg : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ], (-s).rnDeriv μ =ᵐ[μ] -s.rnDeriv μ
-- Mathlib.Analysis.Fourier.AddCircle
/-- For each `1 ≤ p < ∞`, the linear span of the monomials `fourier n` is dense in
`Lp ℂ p haarAddCircle`.  -/
span_fourierLp_closure_eq_top : ∀ {T : ℝ} [hT : Fact (0 < T)] {p : ENNReal} [inst : Fact (1 ≤ p)],
  p ≠ ⊤ → (Submodule.span ℂ (Set.range (fourierLp p))).topologicalClosure = ⊤
-- Mathlib.Data.Set.Order
Antitone.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α},
  Antitone f → Antitone g → Antitone fun x => f x ∩ g x
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.lt_mul_inv_of_mul_lt : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, 0 < b → a * b < c → a < c * b⁻¹
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.alts.sizeOf_spec : ∀ (ref : Lean.Syntax) (a : List Lean.Elab.Tactic.RCases.RCasesPatt),
  sizeOf (Lean.Elab.Tactic.RCases.RCasesPatt.alts ref a) = 1 + sizeOf ref + sizeOf a
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.quasiIso_forget₂_εToSingle₀ : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  QuasiIso
    (((CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map
      (Rep.standardComplex.εToSingle₀ k G))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.IsLimit.fac_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F}
  (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) {Z : C} (h : F i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc f)
      (CategoryTheory.CategoryStruct.comp (c.proj i) h) =
    CategoryTheory.CategoryStruct.comp (f i) h
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- There are as many `U`s as `D`s  -/
DyckWord.count_U_eq_count_D : ∀ (self : DyckWord), List.count DyckStep.U ↑self = List.count DyckStep.D ↑self
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.DHashMap α β),
  m = m_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → m.getThenInsertIfNew? a b = m_1.getThenInsertIfNew? a b_1
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Construct a morphism `M ⟶ N` of `AddMon C` from a map `f : M ⟶ N` and
compatibilities with the zero and the addition.  -/
CategoryTheory.AddMon.Hom.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.AddMon C} →
        (f : M.X ⟶ N.X) →
          autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero)
              CategoryTheory.AddMon.Hom.mk'._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
                    CategoryTheory.AddMonObj.add)
                CategoryTheory.AddMon.Hom.mk'._auto_3 →
              M.Hom N
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.toIsometry_inv_rightUnitor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {M : QuadraticModuleCat R},
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv =
    M.form.tensorRId.symm.toIsometry
-- Mathlib.Algebra.Category.Grp.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
GrpCat.Hom.Simps.hom : (X Y : GrpCat) → X.Hom Y → ↑X →* ↑Y
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.Polynomial.quotQuotEquivComm_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.Polynomial.quotQuotEquivComm I f)
      ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}))
        (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f}))
      ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) p)
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1 : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] {𝕜 : Type u_5} [inst_5 : NormedRing 𝕜] [inst_6 : Module 𝕜 E]
  [inst_7 : IsBoundedSMul 𝕜 E], SMulCommClass Mᵈᵐᵃ 𝕜 ↥(MeasureTheory.Lp E p μ)
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.SparseCasesOnKey.mk.sizeOf_spec : ∀ (indName : Lean.Name) (ctors : Array Lean.Name) (isPrivate : Bool),
  sizeOf { indName := indName, ctors := ctors, isPrivate := isPrivate } =
    1 + sizeOf indName + sizeOf ctors + sizeOf isPrivate
-- Init.Prelude
/-- An opaque hash mixing operation, used to implement hashing for products.  -/
mixHash : UInt64 → UInt64 → UInt64
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.unique : ∀ {M : Type u_1} [inst : CommMonoid M] {k l : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → IsPrimitiveRoot ζ l → k = l
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.ExtDHashMap.Const.unitOfList l).getKey? k = none
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability at filter in both endpoints.

If `f` is a measurable function integrable on `a..b`, `(lb, lb')` is an `intervalIntegral.FTCFilter`
pair around `b`, and `f` has a finite limit `c` almost surely at `lb'`, then
`(∫ x in a..v, f x) - ∫ x in a..u, f x = (v - u) • c + o(‖v - u‖)` as `u` and `v` tend to `lb`.

This lemma could've been formulated using `HasStrictDerivAtFilter` if we had this definition.  -/
intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E}
  {c : E} {lb lb' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {u v : ι → ℝ} [intervalIntegral.FTCFilter b lb lb'],
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f lb' MeasureTheory.volume →
      Filter.Tendsto f (lb' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        Filter.Tendsto u lt lb →
          Filter.Tendsto v lt lb →
            (fun t => ((∫ (x : ℝ) in a..v t, f x) - ∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)
-- Mathlib.Data.UInt
UInt64.instNonUnitalCommRing : NonUnitalCommRing UInt64
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instAddSubgroupClass : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  AddSubgroupClass (LieSubalgebra R L) L
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological_relation : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (x : Module.Presentation.tautological.R A M),
  (Module.Presentation.tautological A M).relation x =
    match x with
    | Module.Presentation.tautological.R.add m₁ m₂ => ((fun₀ | m₁ => 1) + fun₀ | m₂ => 1) - fun₀ | m₁ + m₂ => 1
    | Module.Presentation.tautological.R.smul a m => (fun₀ | m => a) - fun₀ | a • m => 1
-- Init.Data.Range.Polymorphic.Map
/-- Compatibility class for `Map` and `Rxi.HasSize`.  -/
Std.PRange.UpwardEnumerable.Map.PreservesRxiSize : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.UpwardEnumerable β] →
        [Std.Rxi.HasSize α] → [Std.Rxi.HasSize β] → Std.PRange.UpwardEnumerable.Map α β → Prop
-- Mathlib.Topology.PartialHomeomorph.Basic
Set.InjOn.toPartialEquiv.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f f_1 : α → β) (e_f : f = f_1) (s s_1 : Set α) (e_s : s = s_1)
  (hf : Set.InjOn f s), Set.InjOn.toPartialEquiv f s hf = Set.InjOn.toPartialEquiv f_1 s_1 ⋯
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- **Alias** of `Ideal.hasFiniteMulSupport_inv`.

---

For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
`v^-(val_v(I))` is not the unit ideal.  -/
Ideal.finite_mulSupport_inv : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 →
    Function.HasFiniteMulSupport fun v => ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk I).factors))
-- Lean.Data.KVMap
Lean.KVMap.instValueBool : Lean.KVMap.Value Bool
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.comp_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {γ : Type u_5} [inst_2 : TopologicalSpace γ] {f : β → γ},
  MeasureTheory.AEStronglyMeasurable f ν → MeasureTheory.AEStronglyMeasurable (fun z => f z.2) (μ.prod ν)
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.det_vandermonde_add : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R) (a : R),
  (Matrix.vandermonde fun i => v i + a).det = (Matrix.vandermonde v).det
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_append : ∀ {b : ℕ} {l1 l2 : List ℕ}, Nat.ofDigits b (l1 ++ l2) = Nat.ofDigits b l1 + b ^ l1.length * Nat.ofDigits b l2
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosedEmbedding_comap_of_surjective : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f → Topology.IsClosedEmbedding (PrimeSpectrum.comap f)
-- Mathlib.Data.List.Lattice
List.union_sublist_append : ∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α), (l₁ ∪ l₂).Sublist (l₁ ++ l₂)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_def : ∀ {R : Type u_2} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R],
  f.measure =
    let __OuterMeasure := f.outer;
    { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ }
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.fun_sum : ∀ {𝕜 : 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] {x : E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  (∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) → DifferentiableAt 𝕜 (fun y => ∑ i ∈ u, A i y) x
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.instFunLike : (R : Type u_1) →
  [inst : CommMonoid R] → (R' : Type u_2) → [inst_1 : CommMonoidWithZero R'] → FunLike (MulChar R R') R R'
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.le_pointwise_smul_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : AddMonoid A] [inst_1 : Group G] [inst_2 : DistribMulAction G A] {a : G}
  {S T : AddSubmonoid A}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Mathlib.Util.Qq
Qq.QuotedDefEq.rfl : ∀ {u : Lean.Level} {α : Q(Sort u)} {a : Q(«$α»)}, «$a» =Q «$a»
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balLeft.match_4.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α)
  (h_1 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b))
  (h_2 : (l : RBTree.RBNode α) → motive l),
  (match RBTree.RBNode.node RBTree.RBColor.red a x b with
    | RBTree.RBNode.node RBTree.RBColor.red a x b => h_1 a x b
    | l => h_2 l) =
    h_1 a x b
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.Exact.toIsComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n}, S.Exact → S.IsComplex
-- Mathlib.Data.PNat.Basic
PNat.natPred_injective : Function.Injective PNat.natPred
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- An isomorphism in `Cᴹᵒᵖ` gives an isomorphism in `C`.  -/
CategoryTheory.Iso.unmop : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : Cᴹᵒᵖ} → (X ≅ Y) → (X.unmop ≅ Y.unmop)
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.toPosMulStrictMono : ∀ {α : Type u_5} (self : ConditionallyCompleteLinearOrderedField α), PosMulStrictMono α
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- For a ring homomorphism `f : R →+* S` and open sets `U` and `V` of the prime spectra of `R` and
`S` such that `V ⊆ (comap f) ⁻¹ U`, the induced ring homomorphism from the structure sheaf of `R`
at `U` to the structure sheaf of `S` at `V`.

Explicitly, this map is given as follows: For a point `p : V`, if the section `s` evaluates on `p`
to the fraction `a / b`, its image on `V` evaluates on `p` to the fraction `f(a) / f(b)`.
 -/
AlgebraicGeometry.StructureSheaf.comapₗ : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        {S : Type u} →
          [inst_3 : CommRing S] →
            {N : Type u} →
              [inst_4 : AddCommGroup N] →
                [inst_5 : Module S N] →
                  {σ : R →+* S} →
                    (M →ₛₗ[σ] N) →
                      (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
                        (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) →
                          V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier →
                            (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U) →ₛₗ[σ]
                              (AlgebraicGeometry.structureSheafInType S N).obj.obj (Opposite.op V)
-- Init.Data.SInt.Lemmas
Int8.add_right_inj : ∀ {a b : Int8} (c : Int8), c + a = c + b ↔ a = b
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type u_1)
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n m : ℤ)
  (z : CochainComplex.HomComplex.Cochain F G n),
  (CochainComplex.HomComplex.δ_hom R F G n m) z = CochainComplex.HomComplex.δ n m z
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  IsFractionRing ↥(Algebra.adjoin F S) ↥(IntermediateField.adjoin F S)
-- Mathlib.AlgebraicTopology.ModelCategory.Transport
HomotopicalAlgebra.trivialCofibrations.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.trivialCofibrations C = HomotopicalAlgebra.cofibrations C ⊓ HomotopicalAlgebra.weakEquivalences C
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_trans : ∀ {R : Type u_1} {inst : Semiring R} [self : ValuativeRel R] {z y x : R}, x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z
-- Mathlib.Data.Finset.Basic
/-- A finset is equivalent to its coercion as a set.  -/
Finset.equivToSet : {α : Type u_1} → (s : Finset α) → ↥s ≃ ↑↑s