mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsPathGraph3Compl.ne_fst : ∀ {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α}, G.IsPathGraph3Compl v w₁ w₂ → v ≠ w₁
-- Mathlib.Algebra.Group.Basic
conj_eq_one_iff : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a * b * a⁻¹ = 1 ↔ b = 1
-- Mathlib.Data.Sym.Sym2
Sym2.rel_iff' : ∀ {α : Type u_1} {p q : α × α}, Sym2.Rel α p q ↔ p = q ∨ p = q.swap
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.symm_baseSupp : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι],
  b.symm.baseSupp = -b.baseSupp
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.isoOfComponents_hom_hom_app : ∀ {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]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f))
      CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_1)
  (unit :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor)
          (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
        CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor)
      CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_3)
  (tensor :
    autoParam
      (∀ (X Y : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
            (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom)
            (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y))
      CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_5)
  (X : C), (CategoryTheory.LaxMonoidalFunctor.isoOfComponents e naturality unit tensor).hom.hom.app X = (e X).hom
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- Return the infinite place defined by a complex embedding `φ`.  -/
NumberField.InfinitePlace.mk : {K : Type u_1} → [inst : Field K] → (K →+* ℂ) → NumberField.InfinitePlace K
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_vsub_self_rev : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p q : P), ((signedDist (p -ᵥ q)) p) q = -dist p q
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.partialOrder.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α},
  Localization.partialOrder =
    { toLE := Localization.le, toLT := Localization.lt, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
      le_antisymm := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.setOfPred_symm_apply : ∀ {α : Type u_8} (s : Set α) (a : α), MeasurableEquiv.setOfPred.symm s a = (a ∈ s)
-- Mathlib.Order.Interval.Set.Monotone
antitone_Ici : ∀ {α : Type u_1} [inst : Preorder α], Antitone Set.Ici
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.seq.injEq : ∀ (action : Lean.Syntax) (k : Lean.Elab.Term.Do.Code) (action_1 : Lean.Syntax) (k_1 : Lean.Elab.Term.Do.Code),
  (Lean.Elab.Term.Do.Code.seq action k = Lean.Elab.Term.Do.Code.seq action_1 k_1) = (action = action_1 ∧ k = k_1)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_div_two_pow : ∀ {n : ℕ} (x i : ℕ), (x / 2 ^ n).testBit i = x.testBit (i + n)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.const_zsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f : β → α}, UniformContinuous f → ∀ (n : ℤ), UniformContinuous fun x => n • f x
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmooth_isStableUnderBaseChange : RingHom.IsStableUnderBaseChange @RingHom.IsStandardSmooth
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.exists_prop_of_containsZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero],
  ∃ Z, CategoryTheory.Limits.IsZero Z ∧ P Z
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.mul_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) [inst_2 : MulZeroClass β]
  [inst_3 : ContinuousMul β] (f g : ZeroAtInftyContinuousMap α β), (f * g) x = f x * g x
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.prettyParameterSet : Array Lean.Name →
  Array Lean.Expr → Array Lean.Expr → Array Lean.Elab.Structural.RecArgInfo → Lean.MetaM Lean.MessageData
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.mk.injEq : ∀ {𝕜 : 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] (toPartialEquiv : PartialEquiv H E)
  (source_eq : toPartialEquiv.source = Set.univ)
  (convex_range' :
    if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv) else Set.range ↑toPartialEquiv = Set.univ)
  (nonempty_interior' : (interior (Set.range ↑toPartialEquiv)).Nonempty)
  (continuous_toFun : autoParam (Continuous ↑toPartialEquiv) ModelWithCorners.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toPartialEquiv.invFun) ModelWithCorners.continuous_invFun._autoParam)
  (toPartialEquiv_1 : PartialEquiv H E) (source_eq_1 : toPartialEquiv_1.source = Set.univ)
  (convex_range'_1 :
    if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv_1)
    else Set.range ↑toPartialEquiv_1 = Set.univ)
  (nonempty_interior'_1 : (interior (Set.range ↑toPartialEquiv_1)).Nonempty)
  (continuous_toFun_1 : autoParam (Continuous ↑toPartialEquiv_1) ModelWithCorners.continuous_toFun._autoParam)
  (continuous_invFun_1 : autoParam (Continuous toPartialEquiv_1.invFun) ModelWithCorners.continuous_invFun._autoParam),
  ({ toPartialEquiv := toPartialEquiv, source_eq := source_eq, convex_range' := convex_range',
        nonempty_interior' := nonempty_interior', continuous_toFun := continuous_toFun,
        continuous_invFun := continuous_invFun } =
      { toPartialEquiv := toPartialEquiv_1, source_eq := source_eq_1, convex_range' := convex_range'_1,
        nonempty_interior' := nonempty_interior'_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 }) =
    (toPartialEquiv = toPartialEquiv_1)
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instMulZeroClass : {α : Type u₁} → {β : Type u₂} → [inst : MulZeroClass β] → MulZeroClass (α →₀ β)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ofInjective.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f),
  AddMonoidHom.ofInjective hf = AddEquiv.ofBijective (f.codRestrict f.range ⋯) ⋯
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.ShortComplex.Exact.gIsCokernel.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact)
  [inst_3 : CategoryTheory.Epi S.g], hS.gIsCokernel = hS.gIsCokernel
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.instEquivLike : {α : Type u} → {β : Type u_1} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → EquivLike (α ≃ᵤ β) α β
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.partition.loop.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α × List α → Sort u_2) (a : α) (as bs cs : List α)
  (h_1 : (bs cs : List α) → motive [] (bs, cs)) (h_2 : (a : α) → (as bs cs : List α) → motive (a :: as) (bs, cs)),
  (match a :: as, (bs, cs) with
    | [], (bs, cs) => h_1 bs cs
    | a :: as, (bs, cs) => h_2 a as bs cs) =
    h_2 a as bs cs
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.isLocalRing_pullback : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Semiring T] [IsLocalRing R]
  (f : R →+* T) (g : S →+* T) [IsLocalHom g], IsLocalRing ↥(f.pullback g)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.dual_map : ∀ {X Y : FinBddDistLat} (f : X ⟶ Y),
  FinBddDistLat.dual.map f = FinBddDistLat.ofHom (BoundedLatticeHom.dual (FinBddDistLat.Hom.hom f))
-- Mathlib.Data.List.NatAntidiagonal
List.Nat.antidiagonal_succ' : ∀ {n : ℕ}, List.Nat.antidiagonal (n + 1) = List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceClientCapabilities.applyEdit? : Lean.Lsp.WorkspaceClientCapabilities → Option Bool
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- An orthonormal basis of a finite-dimensional inner product space defines a measurable
equivalence between the space and the Euclidean space of the same dimension.  -/
OrthonormalBasis.measurableEquiv : {ι : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup F] →
      [inst_1 : InnerProductSpace ℝ F] →
        [inst_2 : MeasurableSpace F] →
          [BorelSpace F] → [inst_4 : Fintype ι] → OrthonormalBasis ι ℝ F → F ≃ᵐ EuclideanSpace ℝ ι
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subsemiring.copy.congr_simp : ∀ {R : Type u} [inst : NonAssocSemiring R] (S S_1 : Subsemiring R) (e_S : S = S_1) (s s_1 : Set R) (e_s : s = s_1)
  (hs : s = ↑S), S.copy s hs = S_1.copy s_1 ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_negDblY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).negDblY (⇑f ∘ P) = f ((W'.baseChange A).negDblY P)
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousWithinAt.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {x : α} {s : Set α}
  {z : Set β}, LowerHemicontinuousWithinAt (fun _x => z) s x
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- Constructor for elements in the module `(free R).obj X`.  -/
ModuleCat.freeMk : {R : Type u} → [inst : Ring R] → {X : Type u} → X → ↑((ModuleCat.free R).obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks.0.CategoryTheory.Limits.spanOp.match_1.eq_3 : ∀ (motive : CategoryTheory.Limits.WalkingSpan → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : Unit → motive (some CategoryTheory.Limits.WalkingPair.left))
  (h_3 : Unit → motive (some CategoryTheory.Limits.WalkingPair.right)),
  (match some CategoryTheory.Limits.WalkingPair.right with
    | none => h_1 ()
    | some CategoryTheory.Limits.WalkingPair.left => h_2 ()
    | some CategoryTheory.Limits.WalkingPair.right => h_3 ()) =
    h_3 ()
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.funIndInfoExt : Lean.MapDeclarationExtension Lean.Meta.FunIndInfo
-- Mathlib.Algebra.Category.BoolRing
_private.Mathlib.Algebra.Category.BoolRing.0.BoolRing.Hom.mk.sizeOf_spec : ∀ {R : BoolRing} {S : BoolRing} (hom' : ↑R →+* ↑S), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F] (K₁ : CochainComplex C₁ ℤ)
  (K₂ : CochainComplex C₂ ℤ) (n : ℤ),
  (CategoryTheory.Functor.commShiftIso (F.map₂CochainComplex.obj K₁) n).inv.app K₂ =
    (K₁.mapBifunctorShift₂Iso K₂ F n).inv
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      {n : ℕ} →
        {Z : C} →
          (X.obj (Opposite.op { len := n + 1 }) ⟶ Z) →
            (Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Z)) → AlgebraicTopology.DoldKan.MorphComponents X n Z
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instBracketSubtypeMem : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (L' : LieSubalgebra R L) → {M : Type w} → [inst_3 : AddCommGroup M] → [LieRingModule L M] → Bracket (↥L') M
-- Mathlib.Topology.UniformSpace.Defs
uniformity.neBot : ∀ {α : Type ua} [inst : UniformSpace α] [Nonempty α], (uniformity α).NeBot
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Obj.mk.sizeOf_spec : ∀ (e? : Option Lean.Expr), sizeOf { e? := e? } = 1 + sizeOf e?
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.card_le_cliqueNum : ∀ {α : Type u_3} {G : SimpleGraph α} [Finite α] {t : Finset α} {tc : G.IsClique ↑t}, t.card ≤ G.cliqueNum
-- Mathlib.NumberTheory.LSeries.ZetaZeros
/-- The zeros of Riemann's ζ-function.  -/
riemannZetaZeros : Set ℂ
-- Init.Data.List.Lemmas
List.length_tail : ∀ {α : Type u_1} {l : List α}, l.tail.length = l.length - 1
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.eval₂_primPart_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {S : Type u_2} [inst_2 : CommSemiring S]
  [IsDomain S] {f : R →+* S},
  Function.Injective ⇑f →
    ∀ {p : Polynomial R} {s : S}, p ≠ 0 → Polynomial.eval₂ f s p = 0 → Polynomial.eval₂ f s p.primPart = 0
-- Mathlib.Tactic.DefEqAbuse
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep.ascend.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (returning : optParam (Option α) none),
  sizeOf (Lean.MessageData.VisitStep.ascend✝ returning) = 1 + sizeOf returning
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.ofEpi_π : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N)
  [inst_3 : CategoryTheory.Epi p], (σ.ofEpi p).π = CategoryTheory.CategoryStruct.comp σ.π p
-- Mathlib.Combinatorics.Matroid.Basic
/-- `M` has a ground set `E`.  -/
Matroid.E : {α : Type u_1} → Matroid α → Set α
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.inst_isScalarTower : ∀ (k : Type u_3) (K : Type u_4) (L : Type u_5) [inst : Field k] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra k K] [inst_4 : Algebra k L] [inst_5 : Algebra K L] [IsScalarTower k K L],
  IsScalarTower (NumberField.RingOfIntegers k) (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.completeSpace_eqLocus : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₂ M₂] {M' : Type u_9}
  [inst_5 : UniformSpace M'] [CompleteSpace M'] [inst_7 : AddCommMonoid M'] [inst_8 : Module R₁ M'] [T2Space M₂]
  (f g : M' →SL[σ₁₂] M₂), CompleteSpace ↥((↑f).eqLocus ↑g)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.length_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.toList.length = t.size
-- Mathlib.Topology.Compactness.CompactSystem
/-- Inserting `∅` into a compact system gives a compact system.  -/
IsCompactSystem.insert_empty : ∀ {α : Type u_1} {S : Set (Set α)}, IsCompactSystem S → IsCompactSystem (insert ∅ S)
-- Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
CategoryTheory.instReflectsIsomorphismsForgetTypeFun : (CategoryTheory.forget (Type u_1)).ReflectsIsomorphisms
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.piPremeasure_pi_mono : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] {m : (i : ι) → MeasureTheory.OuterMeasure (α i)}
  {s t : Set ((i : ι) → α i)}, s ⊆ t → MeasureTheory.piPremeasure m s ≤ MeasureTheory.piPremeasure m t
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Assumes left covariance.  -/
Left.mul_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulStrictMono α], 0 < a → 0 < b → 0 < a * b
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- Given a measure upstairs (i.e., on `α`), and a choice `s` of additive
fundamental domain, there's always an artificial way to generate a measure downstairs such that
the pair satisfies the `AddQuotientMeasureEqMeasurePreimage` typeclass.  -/
MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α]
  {s : Set α},
  MeasureTheory.IsAddFundamentalDomain G s ν →
    MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν
      (MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s))
-- Mathlib.Algebra.Ring.Parity
Even.mul_left : ∀ {α : Type u_2} [inst : Add α] [inst_1 : Mul α] {a : α} [LeftDistribClass α], Even a → ∀ (b : α), Even (b * a)
-- Mathlib.Topology.Homotopy.TopCat.Basic
/-- The homotopy between compositions of morphisms in `TopCat`.  -/
TopCat.Homotopy.comp : {X Y Z : TopCat} →
  {f₀ f₁ : X ⟶ Y} →
    {g₀ g₁ : Y ⟶ Z} →
      TopCat.Homotopy g₀ g₁ →
        TopCat.Homotopy f₀ f₁ →
          TopCat.Homotopy (CategoryTheory.CategoryStruct.comp f₀ g₀) (CategoryTheory.CategoryStruct.comp f₁ g₁)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.descOpcycles_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
  [inst_2 : S.HasRightHomology] {A' : C} (α : A ⟶ A') {Z : C} (h : A' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.descOpcycles k hk) (CategoryTheory.CategoryStruct.comp α h) =
    CategoryTheory.CategoryStruct.comp (S.descOpcycles (CategoryTheory.CategoryStruct.comp k α) ⋯) h
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.instIteratorAccess : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LT α] →
      [inst_2 : DecidableLT α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLT α] → Std.IteratorAccess (Std.Rxo.Iterator α) Id
-- Mathlib.Order.Filter.Interval
Filter.Tendsto.Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {l₁ l₂ : Filter α} [Filter.TendstoIxxClass Set.Ico l₁ l₂]
  {lb : Filter β} {u₁ u₂ : β → α},
  Filter.Tendsto u₁ lb l₁ → Filter.Tendsto u₂ lb l₁ → Filter.Tendsto (fun x => Set.Ico (u₁ x) (u₂ x)) lb l₂.smallSets
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView.mk : Lean.Syntax → Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → Lean.Elab.WhereFinallyView
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_antisymm` -/
subset_antisymm : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → b ⊆ a → a = b
-- Mathlib.Data.Vector.Defs
List.Vector.pmap_nil : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (hp : ∀ x ∈ List.Vector.nil.toList, p x),
  List.Vector.pmap f List.Vector.nil hp = List.Vector.nil
-- Mathlib.Data.Nat.ModEq
Nat.left_modEq_add_iff : ∀ {n a b : ℕ}, a ≡ a + b [MOD n] ↔ n ∣ b
-- Lean.Meta.Tactic.Grind.Theorems
_private.Lean.Meta.Tactic.Grind.Theorems.0.Lean.Meta.Grind.Theorems.mk.injEq : ∀ {α : Type} (smap : Lean.PHashMap Lean.Name (List α)) (origins erased : Lean.PHashSet Lean.Meta.Grind.Origin)
  (omap : Lean.PHashMap Lean.Meta.Grind.Origin (List α)) (smap_1 : Lean.PHashMap Lean.Name (List α))
  (origins_1 erased_1 : Lean.PHashSet Lean.Meta.Grind.Origin) (omap_1 : Lean.PHashMap Lean.Meta.Grind.Origin (List α)),
  ({ smap := smap, origins := origins, erased := erased, omap := omap } =
      { smap := smap_1, origins := origins_1, erased := erased_1, omap := omap_1 }) =
    (smap = smap_1 ∧ origins = origins_1 ∧ erased = erased_1 ∧ omap = omap_1)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Integration by parts on (-∞, ∞).**
For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`.  -/
MeasureTheory.integral_mul_deriv_eq_deriv_mul : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] {a' b' : A} {u v u' v' : ℝ → A} [CompleteSpace A],
  (∀ x ∈ tsupport v, HasDerivAt u (u' x) x) →
    (∀ x ∈ tsupport u, HasDerivAt v (v' x) x) →
      MeasureTheory.Integrable (u * v') MeasureTheory.volume →
        MeasureTheory.Integrable (u' * v) MeasureTheory.volume →
          Filter.Tendsto (u * v) Filter.atBot (nhds a') →
            Filter.Tendsto (u * v) Filter.atTop (nhds b') → ∫ (x : ℝ), u x * v' x = b' - a' - ∫ (x : ℝ), u' x * v x
-- Mathlib.Order.Filter.Pointwise
Filter.semigroup.eq_1 : ∀ {α : Type u_2} [inst : Semigroup α], Filter.semigroup = { toMul := Filter.instMul, mul_assoc := ⋯ }
-- Mathlib.Analysis.Calculus.Gradient.Basic
Filter.EventuallyEq.hasGradientAtFilter_iff : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {x : F} {L : Filter F} {f₀ f₁ : F → 𝕜} {f₀' f₁' : F},
  f₀ =ᶠ[L] f₁ → f₀ x = f₁ x → f₀' = f₁' → (HasGradientAtFilter f₀ f₀' x L ↔ HasGradientAtFilter f₁ f₁' x L)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromRel_adj : ∀ {V : Type u} (r : V → V → Prop) (v w : V), (SimpleGraph.fromRel r).Adj v w ↔ v ≠ w ∧ (r v w ∨ r w v)
-- Mathlib.Topology.Separation.Basic
nhds_eq_nhds_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {a b : X}, nhds a = nhds b ↔ a = b
-- Mathlib.Algebra.Group.Action.Faithful
FaithfulVAdd.trans : ∀ (R : Type u_4) (S : Type u_5) (T : Type u_6) [inst : AddMonoid S] [inst_1 : AddZeroClass T] [inst_2 : VAdd R S]
  [VAddAssocClass R S S] [inst_4 : AddAction S T] [VAddAssocClass S T T] [inst_6 : VAdd R T] [VAddAssocClass R T T]
  [VAddAssocClass R S T] [FaithfulVAdd R S] [FaithfulVAdd S T], FaithfulVAdd R T
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.readMessage : IO.FS.Stream → ℕ → IO Lean.JsonRpc.Message
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (H : CategoryTheory.Functor C D)
  {X Y : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C} (α : X ⟶ Y) (X_1 : (SimplexCategory.Truncated n)ᵒᵖ),
  (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).obj H).map α).app X_1 = H.map (α.app X_1)