mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff : ∀ {G : Type u_1} [inst : AddCommGroup G] {x y : WithTop G}, x - y = ⊤ ↔ x = ⊤ ∨ y = ⊤
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- For `f : u ⟶ v` a morphism in `Arrow V`, this is the morphism `v ⟶ cokernel f` from `v` to
the "candidate cokernel" of `f`, whose image in `RightFreyd V` will be the projection to
the cokernel of the image of `f`.  -/
CategoryTheory.Preadditive.RightFreyd.Candidate.π : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts V] →
        {u v : CategoryTheory.Arrow V} → (f : u ⟶ v) → v ⟶ CategoryTheory.Preadditive.RightFreyd.Candidate.cokernel f
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.create : Lean.Lsp.CreateFile → Lean.Lsp.DocumentChange
-- Mathlib.CategoryTheory.Comma.Final
/-- Let `A` and `B` be filtered categories, `R : B ⥤ T` be final and `R : A ⥤ T`. Then, the
projection `snd L R : Comma L R ⥤ B` is final.  -/
CategoryTheory.Comma.final_snd : ∀ {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) [CategoryTheory.IsFiltered A] [CategoryTheory.IsFiltered B] [R.Final],
  (CategoryTheory.Comma.snd L R).Final
-- Init.Data.String.Slice
/-- Interprets a string as the decimal representation of an integer, returning it. Panics if the string
does not contain a decimal integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally `-` in front. Leading `+` characters are not allowed.

Use `Slice.isInt` to check whether `Slice.toInt!` would return a value.
`Slice.toInt?` is a safer alternative that returns `none` instead of panicking when the
string is not an integer.

Examples:

* `"0".toSlice.toInt! = 0`

* `"5".toSlice.toInt! = 5`

* `"587".toSlice.toInt! = 587`

* `"-587".toSlice.toInt! = -587`
 -/
String.Slice.toInt! : String.Slice → ℤ
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.toFractionRing_smul : ∀ {K : Type u} [inst : CommRing K] {R : Type u_1} [inst_1 : SMul R (FractionRing (Polynomial K))] (c : R)
  (p : RatFunc K), (c • p).toFractionRing = c • p.toFractionRing
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvalue_neg_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, (-f).HasEigenvalue μ ↔ f.HasEigenvalue (-μ)
-- Mathlib.CategoryTheory.Sites.Over
/-- The equivalence `Presieve Y ≃ Presieve Y.left` for all `Y : Over X`.  -/
CategoryTheory.Presieve.overEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → (Y : CategoryTheory.Over X) → CategoryTheory.Presieve Y ≃o CategoryTheory.Presieve Y.left
-- Mathlib.Geometry.Euclidean.Projection
/-- Reflecting a vector plus a point in the subspace produces the
negation of that vector plus the point if the vector is a multiple of
the result of subtracting a point's orthogonal projection from that
point.  -/
EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (r : 𝕜),
  p₁ ∈ s →
    (EuclideanGeometry.reflection s) (r • (p₂ -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p₂)) +ᵥ p₁) =
      -(r • (p₂ -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p₂))) +ᵥ p₁
-- Mathlib.RingTheory.Kaehler.Basic
/-- Given the commutative diagram
```
A --→ B
↑     ↑
|     |
R --→ S
```
The kernel of the presentation `⊕ₓ B dx ↠ Ω_{B/S}` is spanned by the image of the
kernel of `⊕ₓ A dx ↠ Ω_{A/R}` and all `ds` with `s : S`.
See `kerTotal_map'` for the special case where `R = S`.
 -/
KaehlerDifferential.kerTotal_map : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2)
  (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B]
  [inst_7 : Algebra S B] [inst_8 : Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B],
  Function.Surjective ⇑(algebraMap A B) →
    Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B))
          (KaehlerDifferential.kerTotal R A) ⊔
        Submodule.span A (Set.range fun x => fun₀ | (algebraMap S B) x => 1) =
      Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameConstructors : Lean.ParserDescr
-- Std.Do.SPred.Laws
Std.Do.SPred.down_pure : ∀ {φ : Prop}, ⌜φ⌝.down = φ
-- Std.Sync.Broadcast
Std.Broadcast.instReprError.repr : Std.Broadcast.Error → ℕ → Std.Format
-- Mathlib.Data.Nat.Squarefree
Nat.prod_primeFactors_invOn_squarefree : Set.InvOn (fun n => n.factorization.support) (fun s => ∏ p ∈ s, p) {s | ∀ p ∈ s, Nat.Prime p} {n | Squarefree n}
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing_succ : ∀ (o : ONote) {a : ONote}, o.fundamentalSequence = Sum.inl (some a) → o.fastGrowing = fun i => a.fastGrowing^[i] i
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  ∏ w,
      NumberField.mixedEmbedding.fundamentalCone.deriv_expMap_single w
        ((NumberField.mixedEmbedding.fundamentalCone.completeBasis K).equivFun.symm x w) =
    Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) ^ Module.finrank ℚ K *
        (∏ w, ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x ↑w)⁻¹ *
      2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K
-- Mathlib.Analysis.Polynomial.Fourier
Polynomial.toAddCircle.integrable : ∀ (p : Polynomial ℂ), MeasureTheory.Integrable (⇑(Polynomial.toAddCircle p)) AddCircle.haarAddCircle
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instHasShiftInt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.HasShift (DerivedCategory C) ℤ
-- Lean.CoreM
Lean.Core.instMonadResolveNameCoreM : Lean.MonadResolveName Lean.CoreM
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
_private.Std.Data.Iterators.Lemmas.Equivalence.Basic.0.Std.quotMk_eq_quotOfQuot_comp : ∀ {α : Sort u_1} {R S : α → α → Prop} (h : ∀ (a b : α), R a b → S a b), Quot.mk S = Std.quotOfQuot✝ h ∘ Quot.mk R
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instIsCentralVAdd : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [inst_1 : (i : ι) → VAdd Mᵃᵒᵖ (α i)]
  [∀ (i : ι), IsCentralVAdd M (α i)], IsCentralVAdd M ((i : ι) × α i)
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.inferFVarType : Lean.FVarId → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- **Alias** of `le_mul_of_le_left`. -/
le_mul_right : ∀ {α : Type u} [inst : Mul α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] {a b c : α}, a ≤ b → a ≤ b * c
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `AddAction.isBlock_iff_vadd_eq_vadd_or_disjoint`. -/
AddAction.IsBlock.vadd_eq_vadd_or_disjoint : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X},
  AddAction.IsBlock G B → ∀ (g₁ g₂ : G), g₁ +ᵥ B = g₂ +ᵥ B ∨ Disjoint (g₁ +ᵥ B) (g₂ +ᵥ B)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    t.isEmpty = false →
      ∀ {k fallback : α}, (compare k (t.minKeyD fallback)).isLE = true ↔ ∀ k' ∈ t, (compare k k').isLE = true
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomologyMapData.add_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₁ h₂),
  (γ.add γ').right = γ.right.add γ'.right
-- Init.Data.String.Slice
String.Slice.toStringToString_eq : toString = String.Slice.copy
-- Mathlib.Data.Multiset.Count
Multiset.nodup_iff_count_le_one : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.Nodup ↔ ∀ (a : α), Multiset.count a s ≤ 1
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq.sizeOf_spec : ∀ (lhs : ℕ) (rhs : Lean.Meta.Grind.CnstrRHS),
  sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq lhs rhs) = 1 + sizeOf lhs + sizeOf rhs
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyPToId.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (q : ℕ),
  AlgebraicTopology.DoldKan.homotopyPToId X q.succ =
    (Homotopy.ofEq ⋯).trans
      (((AlgebraicTopology.DoldKan.homotopyPToId X q).add
            ((AlgebraicTopology.DoldKan.homotopyHσToZero q).compLeft (AlgebraicTopology.DoldKan.P q))).trans
        (Homotopy.ofEq ⋯))
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.basis.eq_1 : ∀ (R : Type u_7) (k : Type u_8) [inst : Semiring k],
  AddMonoidAlgebra.basis R k = { repr := AddMonoidAlgebra.coeffLinearEquiv k }
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.mk_lt_mk : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α}
  {a₁ b₁ : α} {a₂ b₂ : ↥s}, Localization.mk a₁ a₂ < Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ < ↑a₂ * b₁
-- Mathlib.Topology.Algebra.Module.Star
starL'_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A] [inst_8 : TrivialStar R] (x : A), (starL' R) x = star x
-- Std.Do.PostCond
Std.Do.PostShape.arg.sizeOf_spec : ∀ (σ : Type u) (a : Std.Do.PostShape), sizeOf (Std.Do.PostShape.arg σ a) = 1 + sizeOf σ + sizeOf a
-- Mathlib.Data.Fintype.Card
/-- **Alias** of `Finset.card_univ_sdiff`. -/
Finset.card_univ_diff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α),
  (Finset.univ \ s).card = Fintype.card α - s.card
-- Mathlib.Analysis.Normed.Group.Constructions
MulOpposite.instNormedAddCommGroup : {E : Type u_2} → [NormedAddCommGroup E] → NormedAddCommGroup Eᵐᵒᵖ
-- Aesop.Util.Basic
Aesop.PersistentHashSet.filter : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → (α → Bool) → Lean.PHashSet α → Lean.PHashSet α
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_image2_eq_csInf_csSup : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) →
    (∀ (a : α), GaloisConnection (l a) (u₂ a)) →
      s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (Set.image2 l s t) = l (sInf s) (sSup t)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.norm_map' : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {E : Type u_11}
  {E₂ : Type u_12} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (self : E →ₛₗᵢ[σ₁₂] E₂) (x : E), ‖self.toLinearMap x‖ = ‖x‖
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [CategoryTheory.IsFiltered J]
  {D : CategoryTheory.Limits.Cocone F} {i j : J} (hD : CategoryTheory.Limits.IsColimit D)
  (x : CategoryTheory.ToType (F.obj i)) (y : CategoryTheory.ToType (F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (D.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (D.ι.app j)) y ↔
    ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) y
-- Mathlib.Order.Lattice
inf_le_sup : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊓ b ≤ a ⊔ b
-- Init.PropLemmas
exists_or_eq_left' : ∀ {α : Sort u_1} (y : α) (p : α → Prop), ∃ x, y = x ∨ p x
-- Mathlib.Testing.Plausible.Functions
/-- Shrink a permutation of a list, slicing a segment in the middle.

The sizes of the slice being removed start at `n` (with `n` the length
of the list) and then `n / 2`, then `n / 4`, etc. down to 1. The slices
will be taken at index `0`, `n / k`, `2n / k`, `3n / k`, etc.
 -/
Plausible.InjectiveFunction.shrinkPerm : {α : Type} →
  [DecidableEq α] →
    (xs : List α) ×' (ys : List α) ×' xs.Perm ys ∧ ys.Nodup →
      List ((xs : List α) ×' (ys : List α) ×' xs.Perm ys ∧ ys.Nodup)
-- Mathlib.GroupTheory.Congruence.Defs
/-- A congruence relation on a type with an addition is an equivalence relation which
preserves addition.  -/
AddCon : (M : Type u_1) → [Add M] → Type u_1
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for multiplicative (on coprime arguments) functions.

If `f : ℕ → R`, where `R` is a complete normed commutative ring, `f 0 = 0`, `f 1 = 1`, `f` is
multiplicative on coprime arguments, and `‖f ·‖` is summable, then
`∏' p : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n`. This version is stated using `HasProd`.  -/
EulerProduct.eulerProduct_hasProd : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  f 1 = 1 →
    (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
      (Summable fun x => ‖f x‖) → f 0 = 0 → HasProd (fun p => ∑' (e : ℕ), f (↑p ^ e)) (∑' (n : ℕ), f n)
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.IsLocallyFaithful.of_faithful : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  {K : CategoryTheory.GrothendieckTopology D} (G : CategoryTheory.Functor C D) [G.Faithful], G.IsLocallyFaithful K
-- Mathlib.Order.CompleteLattice.Basic
iInf_comm : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : CompleteLattice α] {f : ι → ι' → α},
  ⨅ i, ⨅ j, f i j = ⨅ j, ⨅ i, f i j
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.OrdSet.mk : {α : Type} → [inst : Hashable α] → [inst_1 : BEq α] → Array α → Std.HashSet α → Lean.Meta.Try.Collector.OrdSet α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).maxKey?.isSome = true
-- Batteries.Tactic.Alias
/-- Updates the `deprecated` declaration to point to `target` if no target is provided.  -/
Batteries.Tactic.Alias.setDeprecatedTarget : Lean.Name → Array Lean.Elab.Attribute → Array Lean.Elab.Attribute × Bool
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instFinitaryExtensiveScheme : CategoryTheory.FinitaryExtensive AlgebraicGeometry.Scheme
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.Context.mk.injEq : ∀ (level₂ level₁ : Lean.Level) (C : Q(Type level₁)) (instCat : Q(CategoryTheory.Category.{level₂, level₁} «$C»))
  (instMonoidal? : Option Q(CategoryTheory.MonoidalCategory «$C»)) (level₂_1 level₁_1 : Lean.Level)
  (C_1 : Q(Type level₁_1)) (instCat_1 : Q(CategoryTheory.Category.{level₂_1, level₁_1} «$C_1»))
  (instMonoidal?_1 : Option Q(CategoryTheory.MonoidalCategory «$C_1»)),
  ({ level₂ := level₂, level₁ := level₁, C := C, instCat := instCat, instMonoidal? := instMonoidal? } =
      { level₂ := level₂_1, level₁ := level₁_1, C := C_1, instCat := instCat_1, instMonoidal? := instMonoidal?_1 }) =
    (level₂ = level₂_1 ∧ level₁ = level₁_1 ∧ C = C_1 ∧ instCat = instCat_1 ∧ instMonoidal? = instMonoidal?_1)
-- Mathlib.Probability.ProductMeasure
MeasureTheory.integral_restrict_infinitePi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {E : Type u_3} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {s : Finset ι} {f : ((i : ↥s) → X ↑i) → E},
  MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.pi fun i => μ ↑i) →
    ∫ (y : (i : ι) → X i), f (s.restrict y) ∂MeasureTheory.Measure.infinitePi μ =
      ∫ (y : (i : ↥s) → X ↑i), f y ∂MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Precomposition with a linear isometry preserves the operator norm.  -/
ContinuousLinearMap.opNNNorm_comp_linearIsometryEquiv : ∀ {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜₁] [inst_4 : NormedSpace 𝕜₁ E] [inst_5 : NontriviallyNormedField 𝕜₂]
  [inst_6 : NormedSpace 𝕜₂ F] [inst_7 : NontriviallyNormedField 𝕜₃] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜₁} [inst_9 : RingHomInvPair σ₁₂ σ₂₁] [inst_10 : RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜₁ →+* 𝕜₃} [inst_11 : RingHomIsometric σ₁₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  [inst_13 : RingHomIsometric σ₂₃] (f : F →SL[σ₂₃] G) (e : E ≃ₛₗᵢ[σ₁₂] F), ‖f ∘SL ↑↑e‖₊ = ‖f‖₊
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIoc : {α : Type u_1} →
  [inst : Preorder α] → {a b x : α} → [Decidable (a < x)] → [Decidable (x ≤ b)] → Decidable (x ∈ Set.Ioc a b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey?_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey? =
        Option.map (fun km => if compare km k = Ordering.eq then k else km) t.maxKey?
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iio_filter_lt : ∀ {α : Type u_3} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderBot α] (a b : α),
  {x ∈ Finset.Iio a | x < b} = Finset.Iio (min a b)
-- Mathlib.Data.Fin.SuccPred
Fin.le_castPred_iff : ∀ {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n), j ≤ i.castPred hi ↔ j.castSucc ≤ i
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α], addRothNumber ∅ = 0
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- Synonym for constructor of `Hom2` where the 1-morphisms `f` and `g` lie in `B` and not `Bᵒᵖ`.  -/
Bicategory.Opposite.op2 : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (f.op ⟶ g.op)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.Associative.ε₂_ε₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃}
  {c : ComplexShape J} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c}
  {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) =
    c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
-- Mathlib.Data.NNReal.Defs
Real.nnabs_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → Real.nnabs x = x.toNNReal
-- Init.Data.BitVec.Lemmas
BitVec.toInt_add : ∀ {w : ℕ} (x y : BitVec w), (x + y).toInt = (x.toInt + y.toInt).bmod (2 ^ w)
-- Mathlib.Analysis.Normed.Group.Uniform
OneHomClass.bound_of_antilipschitz : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) {K : NNReal},
  AntilipschitzWith K ⇑f → ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instNormal : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (H : OpenNormalAddSubgroup G),
  (↑H.toOpenAddSubgroup).Normal
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.comp_hom_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  {X Y Z : CategoryTheory.Abelian.SpectralObject C ι} (f : X.Hom Y) (g : Y.Hom Z) (n : ℤ)
  {Z_1 : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C} (h : Z.H n ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).hom n) h =
    CategoryTheory.CategoryStruct.comp (f.hom n) (CategoryTheory.CategoryStruct.comp (g.hom n) h)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.degree : Lean.Grind.CommRing.Mon → ℕ
-- Mathlib.RingTheory.Polynomial.ScaleRoots
/-- **Alias** of `Polynomial.scaleRoots_dvd_iff`. -/
IsUnit.scaleRoots_dvd_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) {r : R},
  IsUnit r → (p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q)
-- Mathlib.LinearAlgebra.Matrix.Module
LinearMap.mapMatrixModule_comp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Ring R] [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : AddCommGroup P] [inst_8 : Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P),
  LinearMap.mapMatrixModule ι (g ∘ₗ f) = LinearMap.mapMatrixModule ι g ∘ₗ LinearMap.mapMatrixModule ι f
-- Std.Time.Format.DateFormat
Std.Time.DayPeriodSymbols.mk.injEq : ∀ (am pm noon midnight am_1 pm_1 noon_1 midnight_1 : String),
  ({ am := am, pm := pm, noon := noon, midnight := midnight } =
      { am := am_1, pm := pm_1, noon := noon_1, midnight := midnight_1 }) =
    (am = am_1 ∧ pm = pm_1 ∧ noon = noon_1 ∧ midnight = midnight_1)
-- Mathlib.Data.Holor
/-- `CPRankMax1 x` means `x` has CP rank at most 1, that is,
it is the tensor product of 1-dimensional holors.  -/
Holor.CPRankMax1 : {α : Type} → [Mul α] → {ds : List ℕ} → Holor α ds → Prop
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionObj_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (d : D) (c : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (Opposite.op d) (Opposite.op c) =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_comap_eq : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'},
  f.IsIdealMorphism → LieIdeal.map f (LieIdeal.comap f J) = f.idealRange ⊓ J
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.projection_respects_measure : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α)))
  [i : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] {t : Set α},
  MeasureTheory.IsFundamentalDomain G t ν →
    μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict t)