mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- The canonical diffeomorphism `M ⊕ ∅ → M`  -/
Diffeomorph.sumEmpty : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_5} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_9) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      (n : WithTop ℕ∞) →
                        {M' : Type u_13} →
                          [inst_6 : TopologicalSpace M'] →
                            [inst_7 : ChartedSpace H M'] → [IsEmpty M'] → Diffeomorph I I (M ⊕ M') M n
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂], Function.Injective fun f => ⇑f
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.sieveOfUliftSubfunctor_uliftFunctorInclusion : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X},
  CategoryTheory.Sieve.sieveOfUliftSubfunctor S.uliftFunctorInclusion = S
-- Mathlib.Algebra.Order.Field.Basic
one_div_pow_lt_one_div_pow_of_lt : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  1 < a → ∀ {m n : ℕ}, m < n → 1 / a ^ n < 1 / a ^ m
-- Mathlib.Order.Interval.Set.Basic
Set.left_notMem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∉ Set.Ioo a b
-- Batteries.Data.Vector.Lemmas
Vector.idRun_scanlM : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → Id β} {as : Vector α n},
  (Vector.scanlM f init as).run = Vector.scanl (fun x1 x2 => (f x1 x2).run) init as
-- Init.Data.Array.Basic
/-- Replaces the element at the given index, if it exists, with the result of applying the monadic
function `f` to it. If the index is invalid, the array is returned unmodified and `f` is not called.

Examples:
```lean example
#eval #[1, 2, 3, 4].modifyM 2 fun x => do
  IO.println s!"It was {x}"
  return x * 10
```
```output
It was 3
```
```output
#[1, 2, 30, 4]
```

```lean example
#eval #[1, 2, 3, 4].modifyM 6 fun x => do
  IO.println s!"It was {x}"
  return x * 10
```
```output
#[1, 2, 3, 4]
```
 -/
Array.modifyM : {α : Type u} → {m : Type u → Type u_1} → [Monad m] → Array α → ℕ → (α → m α) → m (Array α)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.semivariation_le_variation : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s : Set X}, μ.semivariation s ≤ μ.variation s
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.one_lt_top : ∀ {α : Type u} [inst : One α] [inst_1 : LT α], 1 < ⊤
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.natDegree_freeMonic : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ) [Nontrivial R], (Polynomial.freeMonic R n).natDegree = n
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.one_comul_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.orderHomOfSimplex.congr_simp : ∀ {p q n : ℕ}
  (x x_1 :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n })),
  x = x_1 →
    ∀ {m : ℕ} (hm : p + q = m),
      SSet.prodStdSimplex.orderHomOfSimplex x hm = SSet.prodStdSimplex.orderHomOfSimplex x_1 hm
-- Mathlib.Tactic.NormNum.BigOperators
/-- `norm_num` plugin for evaluating products of finsets.

If your finset is not supported, you can add it to the match in `Finset.proveEmptyOrCons`.
 -/
Mathlib.Meta.NormNum.evalFinsetProd : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.RingTheory.Localization.Algebra
/-- The canonical linear map from the kernel of `g` to the kernel of its localization
is localizing. In other words, localization commutes with taking kernels.  -/
RingHom.toKerIsLocalization_isLocalizedModule : ∀ {R : Type u_1} {S : Type u_2} {P : Type u_3} (Q : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring P] [inst_3 : CommSemiring Q] {M : Submonoid R} {T : Submonoid P} [inst_4 : Algebra R S]
  [inst_5 : Algebra P Q] [inst_6 : IsLocalization M S] [inst_7 : IsLocalization T Q] (g : R →+* P)
  (hT : Submonoid.map g M = T), IsLocalizedModule M (RingHom.toKerIsLocalization S Q g ⋯)
-- Mathlib.Data.Set.NAry
Set.exists_mem_image2 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {p : γ → Prop},
  (∃ z ∈ Set.image2 f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) [F.IsEquivalence],
  ((CategoryTheory.Functor.whiskeringRight E C D).obj F).IsEquivalence
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.extend_eq_at : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α},
  ContinuousAt f a → di.extend f (i a) = f a
-- Mathlib.Logic.Function.Basic
Function.ne_update_self_iff : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a},
  f ≠ Function.update f a b ↔ f a ≠ b
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryFinFinset_symm_apply_const : ∀ {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k l : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : G [×k]→L[𝕜] G [×l]→L[𝕜] G') (x : G),
  (((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) fun x_1 => x) = (f fun x_1 => x) fun x_1 => x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- A `Functor.PushoutObjObj` structure for a functor `F : C₁ ⥤ C₂ ⥤ C₃` and
morphisms `f₁ : X₁ ⟶ Y₁` and `f₂ : X₂ ⟶ Y₂` when `X₂` is initial and both
`F.obj X₁` and `F.obj Y₁` preserve the initial object.  -/
CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              {X₁ Y₁ : C₁} →
                (f₁ : X₁ ⟶ Y₁) →
                  {X₂ Y₂ : C₂} →
                    (f₂ : X₂ ⟶ Y₂) →
                      [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj X₁)] →
                        [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
                              (F.obj Y₁)] →
                          CategoryTheory.Limits.IsInitial X₂ → F.PushoutObjObj f₁ f₂
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- If `it` is an iterator, then `it.filterMapM f` is another iterator that applies a monadic
function `f` to all values emitted by `it`. `f` is expected to return an `Option` inside the monad.
If `f` returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

The base iterator `it` being monadic in `m`, `f` can return values in any monad `n` for which a
`MonadLiftT m n` instance is available.

If `f` is pure, then the simpler variant `it.filterMap` can be used instead.

**Marble diagram (without monadic effects):**

```text
it                ---a --b--c --d-e--⊥
it.filterMapM     ---a'-----c'-------⊥
```

(given that `f a = pure (some a)'`, `f c = pure (some c')` and `f b = f d = d e = pure none`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then
this combinator will preserve productiveness. If `f` is an `ExceptT` monad and will always fail,
then `it.filterMapM` will be finite even if `it` isn't. In such cases, the termination proof needs
to be done manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
returned `Option` value.
 -/
Std.IterM.filterMapM : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [Std.Iterator α m β] →
        [Monad n] →
          [inst : MonadAttach n] → [inst_1 : MonadLiftT m n] → (f : β → n (Option γ)) → Std.IterM m β → Std.IterM n γ
-- Std.Time.Format.Basic
/-- Converts a format `f` into a string.
 -/
Std.Time.Format.format : {f : Type} → {typ : Type → f → Type} → [self : Std.Time.Format f typ] → (fmt : f) → typ String fmt
-- Init.Data.Fin.Fold
/-- Variant of `foldlM_succ` that splits off `Fin.last n` rather than `0`.  -/
Fin.foldlM_succ_last : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] (f : α → Fin (n + 1) → m α),
  Fin.foldlM (n + 1) f = fun x => do
    let x ← Fin.foldlM n (fun x j => f x j.castSucc) x
    f x (Fin.last n)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.instDistribLattice : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → DistribLattice (TopologicalSpace.OpenNhdsOf x)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Given a family of elements of a sieve `S` on `F(X)`, we can realize it as a family of elements of
`S.functorPullback F`.
 -/
CategoryTheory.Presieve.FamilyOfElements.functorPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (F : CategoryTheory.Functor D C) →
            {Z : D} →
              {T : CategoryTheory.Presieve (F.obj Z)} →
                CategoryTheory.Presieve.FamilyOfElements P T →
                  CategoryTheory.Presieve.FamilyOfElements (F.op.comp P) (CategoryTheory.Presieve.functorPullback F T)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k k' : α}
  {f : β → β}, k' ∈ Std.DTreeMap.Const.modify t k f ↔ k' ∈ t
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.LazyTraceChildren.mk.injEq : ∀ (indent : ℕ) (children : Array (Lean.Server.WithRpcRef Lean.MessageData)) (indent_1 : ℕ)
  (children_1 : Array (Lean.Server.WithRpcRef Lean.MessageData)),
  ({ indent := indent, children := children } = { indent := indent_1, children := children_1 }) =
    (indent = indent_1 ∧ children = children_1)
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- If there exists a sequence of compact closed balls with the same center
such that the radii tend to infinity, then the space is proper.  -/
ProperSpace.of_seq_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {l : Filter β} [l.NeBot] {x : α} {r : β → ℝ},
  Filter.Tendsto r l Filter.atTop → (∀ᶠ (i : β) in l, IsCompact (Metric.closedBall x (r i))) → ProperSpace α
-- Mathlib.RingTheory.WittVector.StructurePolynomial
/-- `wittPolynomial p R n` is the `n`-th Witt polynomial
with respect to a prime `p` with coefficients in a commutative ring `R`.
It is defined as:

`∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …]`.  -/
Witt.termW_1 : Lean.ParserDescr
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.instEsakiaHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β], EsakiaHomClass (EsakiaHom α β) α β
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsIntegral.isAlgebraic_iff : ∀ (R : Type u_1) (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsIntegral R S] [FaithfulSMul R S] {a : A}, IsAlgebraic R a ↔ IsAlgebraic S a
-- Mathlib.Order.Antisymmetrization
AntisymmRel.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (a b : α), AntisymmRel r a b = (r a b ∧ r b a)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.ext_iff : ∀ {R : Type u_1} {x y : PrimeSpectrum.BasicConstructibleSetData R}, x = y ↔ x.f = y.f ∧ x.n = y.n ∧ x.g ≍ y.g
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f g : M₁ →ₗ[R] M₁),
  (LinearMap.toMatrixAlgEquiv v₁) (f * g) = (LinearMap.toMatrixAlgEquiv v₁) f * (LinearMap.toMatrixAlgEquiv v₁) g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtDTreeMap.Const.ofList l cmp).getKeyD k' fallback = k
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.sliceTo_lt_sliceTo_iff : ∀ {s : String.Slice} {p₀ q r : s.Pos} {h₁ : q ≤ p₀} {h₂ : r ≤ p₀}, p₀.sliceTo q h₁ < p₀.sliceTo r h₂ ↔ q < r
-- Init.Data.Float.Model.Unpacked.Operations.Sign
/-- Negates the given float.  -/
Float.Model.UnpackedFloat.neg : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat
-- Mathlib.Algebra.Order.Module.Equiv
/-- `ofLex` as a linear equivalence  -/
ofLexLinearEquiv : (α : Type u_1) →
  (β : Type u_2) → [inst : Semiring α] → [inst_1 : AddCommMonoid β] → [inst_2 : Module α β] → Lex β ≃ₗ[α] β
-- Mathlib.Algebra.Group.Basic
mul_mul_mul_comm' : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c d : G), a * b * c * d = a * c * b * d
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core : Lean.Expr →
  Lean.Expr →
    Lean.Meta.Grind.Arith.Linear.LinExpr →
      Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.EqCnstrProof
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_5.eq_2 : ∀ {α₂ β : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m β) → Sort u_3) (it₂ : Std.IterM m β)
  (h_1 : Unit → motive none) (h_2 : (it₂ : Std.IterM m β) → motive (some it₂)),
  (match some it₂ with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_2 it₂
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.differentiable_fourierChar : Differentiable ℝ fun x => ↑(Real.fourierChar x)
-- Mathlib.Data.QPF.Univariate.Basic
/-- composition of qpfs gives another qpf  -/
QPF.comp : {F₂ : Type u → Type u} → [q₂ : QPF F₂] → {F₁ : Type u → Type u} → [q₁ : QPF F₁] → QPF (Functor.Comp F₂ F₁)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
LiouvilleNumber.aux_calc : ∀ (n : ℕ) {m : ℝ}, 2 ≤ m → (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1).factorial) ≤ 1 / (m ^ n.factorial) ^ n
-- Mathlib.RingTheory.LocalRing.NonLocalRing
/-- There exists a surjective ring homomorphism from a non-local commutative ring onto a product
of two fields.  -/
IsLocalRing.exists_surjective_of_not_isLocalRing : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R], ¬IsLocalRing R → ∃ K₁ K₂ x x_1 f, Function.Surjective ⇑f
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).left =
    CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc
-- Mathlib.Order.Filter.Defs
/-- This filter is characterized by `Filter.eventually_curry_iff`:
`(∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)`. Useful
in adding quantifiers to the middle of `Tendsto`s. See
`hasFDerivAt_of_tendstoUniformlyOnFilter`.  -/
Filter.curry : {α : Type u_1} → {β : Type u_2} → Filter α → Filter β → Filter (α × β)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.isInducing_toContinuousMap : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], Topology.IsInducing ContinuousMonoidHom.toContinuousMap
-- Init.Data.BitVec.Bitblast
BitVec.toInt_eq_neg_toNat_neg_of_nonpos : ∀ {w : ℕ} {x : BitVec w}, x = 0#w ∨ x.msb = true → x.toInt = -↑(-x).toNat
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- Given a right homology map data `ψ : RightHomologyMapData φ h₁ h₂` such that
both right homology data `h₁` and `h₂` are preserved by a functor `F`, this is
the induced right homology map data for the morphism `F.mapShortComplex.map φ`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S₁ S₂ : CategoryTheory.ShortComplex C} →
              {φ : S₁ ⟶ S₂} →
                {h₁ : S₁.RightHomologyData} →
                  {h₂ : S₂.RightHomologyData} →
                    CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ →
                      (F : CategoryTheory.Functor C D) →
                        [inst_4 : F.PreservesZeroMorphisms] →
                          [inst_5 : h₁.IsPreservedBy F] →
                            [inst_6 : h₂.IsPreservedBy F] →
                              CategoryTheory.ShortComplex.RightHomologyMapData (F.mapShortComplex.map φ) (h₁.map F)
                                (h₂.map F)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.isCentralScalar : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : SMulZeroClass N R]
  [inst_2 : SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R], IsCentralScalar N (MonoidAlgebra R M)
-- Mathlib.LinearAlgebra.Multilinear.Finsupp
/-- When `freeFinsuppEquiv` is applied to a map with a single value the resulting multilinear
map sends inputs to a single value in the codomain, taking a product over images from each
component of the domain.
 -/
MultilinearMap.freeFinsuppEquiv_single : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {κ : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  [inst_2 : CommSemiring R] [inst_3 : DecidableEq R] [inst_4 : DecidableEq ι'] [inst_5 : (i : ι) → Fintype (κ i)]
  [inst_6 : (i : ι) → DecidableEq (κ i)] (p : ((i : ι) → κ i) × ι') (r : R) (x : (i : ι) → κ i →₀ R),
  (MultilinearMap.freeFinsuppEquiv fun₀ | p => r) x = r • fun₀ | p.2 => ∏ i, (x i) (p.1 i)
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the forward direction of `SimpleGraph.isCompleteBetween_comm`. -/
SimpleGraph.IsCompleteBetween.symm : ∀ {V : Type u} (G : SimpleGraph V) {s t : Set V}, G.IsCompleteBetween s t → G.IsCompleteBetween t s
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_subst : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_eq_subst_cert x p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ = 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ = 0 → Int.Internal.Linear.Poly.denote' ctx p₃ = 0
-- Mathlib.Data.SetLike.Basic
SetLike.setOfPred_mem_eq : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] (a : A), {b | b ∈ a} = ↑a
-- Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
/-- The open set `imageOfDf f` coincides with the image of `basicOpen f` under the
morphism `C⁺ : Spec R[x] → Spec R`.  -/
AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  AlgebraicGeometry.Polynomial.imageOfDf f = PrimeSpectrum.comap Polynomial.C '' (PrimeSpectrum.zeroLocus {f})ᶜ
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.isEquivalenceMap : ∀ {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] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full]
  [CategoryTheory.IsIso α] [CategoryTheory.IsIso β], (CategoryTheory.Comma.map α β).IsEquivalence
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.ofIso_source : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ≅ Y), (AlgebraicGeometry.Scheme.PartialIso.ofIso f).source = ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited β] {f : α → β → Bool} {k : α} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.filter f m) k =
    ((Std.DHashMap.Internal.Raw₀.Const.get? m k).pfilter fun x h' => f (m.getKey k ⋯) x).get!
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- For each `R₃`-module `M`, restriction of scalars of `M` by a composition of ring morphisms
identifies to successively restricting scalars.  -/
ModuleCat.restrictScalarsComp'App : {R₁ : Type u₁} →
  {R₂ : Type u₂} →
    {R₃ : Type u₃} →
      [inst : Ring R₁] →
        [inst_1 : Ring R₂] →
          [inst_2 : Ring R₃] →
            (f : R₁ →+* R₂) →
              (g : R₂ →+* R₃) →
                (gf : R₁ →+* R₃) →
                  gf = g.comp f →
                    (M : ModuleCat R₃) →
                      (ModuleCat.restrictScalars gf).obj M ≅
                        (ModuleCat.restrictScalars f).obj ((ModuleCat.restrictScalars g).obj M)
-- Init.Data.Nat.Lemmas
Nat.two_pow_pred_mod_two_pow : ∀ {w : ℕ}, 0 < w → 2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeEquivalence_functor : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  (CategoryTheory.Limits.Cone.postcomposeEquivalence α).functor = CategoryTheory.Limits.Cone.postcompose α.hom
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
/-- An upper bound on the Minkowski bound of a number field `K` with `|discr K| ≤ N`;
see `minkowskiBound_lt_boundOfDiscBdd`.  -/
NumberField.hermiteTheorem.boundOfDiscBdd : ℕ → NNReal