mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t),
  CategoryTheory.CategoryStruct.comp (P.lift r) (P.conePointUniqueUpToIso Q).hom = Q.lift r
-- Mathlib.Order.Heyting.Basic
/-- `p → q → r ↔ q → p → r`  -/
himp_left_comm : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇨ c = b ⇨ a ⇨ c
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_rio : ∀ {α : Type u_1} {xs : List α} {hi : ℕ}, Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi xs
-- Mathlib.Algebra.GroupWithZero.Semiconj
Commute.zpow_self₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (n : ℤ), Commute (a ^ n) a
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.scalarRestriction.eq_1 : ∀ {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.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsAddMonHom f] (M : D) [inst_7 : CategoryTheory.AddModObj B M],
  CategoryTheory.AddMod.scalarRestriction f M =
    {
      vadd :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M)
          CategoryTheory.AddModObj.vadd,
      zero_vadd := ⋯, add_vadd := ⋯ }
-- Mathlib.Data.List.Chain
List.attachWith.hcongr_4 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (l : List α) (l' : List α'),
      l ≍ l' →
        ∀ (P : α → Prop) (P' : α' → Prop),
          P ≍ P' → ∀ (H : ∀ x ∈ l, P x) (H' : ∀ x ∈ l', P' x), H ≍ H' → l.attachWith P H ≍ l'.attachWith P' H'
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv_assoc : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D) {y z : C} (f : y ≅ z) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f.hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f.inv) h) =
    h
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.tr.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ)
  (motive : Turing.TM1to0.Λ' M → Γ → Sort u_4) (snd : σ) (x : Γ) (h_1 : (snd : σ) → (x : Γ) → motive (none, snd) x)
  (h_2 : (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (s : Γ) → motive (some q, v) s),
  (match (none, snd), x with
    | (none, snd), x => h_1 snd x
    | (some q, v), s => h_2 q v s) =
    h_1 snd x
-- Mathlib.Algebra.Ring.Identities
/-- Sophie Germain's identity, see <https://www.cut-the-knot.org/blue/SophieGermainIdentity.shtml>.
 -/
pow_four_add_four_mul_pow_four' : ∀ {R : Type u_1} [inst : CommRing R] {a b : R},
  a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
sigmaAntidiagonalEquivProd_symm_apply_snd : ∀ (x : ℕ+ × ℕ+), ↑(sigmaAntidiagonalEquivProd.symm x).snd = (↑x.1, ↑x.2)
-- Mathlib.Algebra.Order.Quantale
Quantale.mk : {α : Type u_1} → [inst : Semigroup α] → [inst_1 : CompleteLattice α] → [inst_2 : IsQuantale α] → Quantale α
-- Mathlib.Data.List.Sigma
List.Perm.kinsert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)},
  l₁.NodupKeys → l₁.Perm l₂ → (List.kinsert a b l₁).Perm (List.kinsert a b l₂)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubalgebra_injective : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Function.Injective IntermediateField.toSubalgebra
-- Init.Grind.Module.Basic
/-- Scalar multiplication by natural numbers.  -/
Lean.Grind.NatModule.nsmul : {M : Type u} → [self : Lean.Grind.NatModule M] → SMul ℕ M
-- Mathlib.Order.Quotient
Quotient.instIsTransLe : ∀ {α : Type u_1} {s : Setoid α} [inst : LE α], IsTrans (Quotient s) fun x1 x2 => x1 ≤ x2
-- Std.Do.WP.SimpLemmas
Except.mapError.eq_1 : ∀ {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') (err : ε),
  Except.mapError f (Except.error err) = Except.error (f err)
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `upperSemicontinuous_iff_limsup_le`. -/
UpperSemicontinuous.limsup_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  UpperSemicontinuous f → ∀ (x : α), Filter.limsup f (nhds x) ≤ f x
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongMono.of_arrow_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B A' B' : C} {f : B ⟶ A} {g : B' ⟶ A'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) [h : CategoryTheory.StrongMono f],
  CategoryTheory.StrongMono g
-- Mathlib.Data.Finset.Card
Finset.card_filter_eq_zero_iff : ∀ {α : Type u_1} {s : Finset α} {p : α → Prop} [inst : DecidablePred p], (Finset.filter p s).card = 0 ↔ ∀ x ∈ s, ¬p x
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientEquivProdOfLE_apply : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (a : α ⧸ s),
  (AddSubgroup.quotientEquivProdOfLE h_le) a =
    (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨-(Quotient.mk'' g).out + g, ⋯⟩) ⋯ a)
-- Batteries.Control.Nondet.Basic
Nondet.instInhabited : {σ : Type} → {m : Type → Type} → [inst : Lean.MonadBacktrack σ m] → {α : Type} → Inhabited (Nondet m α)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasStrictFDerivAt_exp_smul_const' : ∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedCommRing 𝕊] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝕊] [inst_4 : NormedAlgebra 𝕂 𝔸] [inst_5 : Algebra 𝕊 𝔸] [inst_6 : ContinuousSMul 𝕊 𝔸]
  [inst_7 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  HasStrictFDerivAt (fun u => NormedSpace.exp (u • x))
    ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp (t • x))) t
-- Init.Data.List.Sublist
List.flatten_sublist_iff : ∀ {α : Type u_1} {L : List (List α)} {l : List α},
  L.flatten.Sublist l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : ℕ) (x : i < L.length), L[i].Sublist (L'[i]?.getD [])
-- Mathlib.LinearAlgebra.JordanChevalley
/-- **Jordan-Chevalley-Dunford decomposition**: an endomorphism of a finite-dimensional vector space
over a perfect field may be written as a sum of nilpotent and semisimple endomorphisms. Moreover
these nilpotent and semisimple components are polynomial expressions in the original endomorphism.
 -/
Module.End.exists_isNilpotent_isSemisimple : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : Module.End K V}
  [FiniteDimensional K V] [PerfectField K], ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
-- Mathlib.Algebra.Order.Group.Cone
/-- Construct a linear order by designating a maximal cone in an abelian group.  -/
LinearOrder.mkOfGroupCone : {S : Type u_1} →
  {G : Type u_2} →
    [inst : CommGroup G] →
      [inst_1 : SetLike S G] →
        (C : S) → [GroupConeClass S G] → [HasMemOrInvMem C] → [DecidablePred fun x => x ∈ C] → LinearOrder G
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.of.inj : ∀ {carrier : Type u} {str : MeasurableSpace carrier} {carrier_1 : Type u} {str_1 : MeasurableSpace carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Init.Data.String.Basic
/-- Returns the character at the position `pos` of a string, or `none` if the position is the
past-the-end position.

This function is overridden with an efficient implementation in runtime code.
 -/
String.Pos.get? : {s : String} → s.Pos → Option Char
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
roots_mem_integralClosure : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra R S]
  {f : Polynomial R}, f.Monic → ∀ {a : S}, a ∈ f.aroots S → a ∈ integralClosure R S
-- Mathlib.Data.Sigma.Lex
Sigma.lex_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : (i : ι) × α i},
  Sigma.Lex r s a b ↔ r a.fst b.fst ∨ ∃ (h : a.fst = b.fst), s b.fst (h ▸ a.snd) b.snd
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.comp_base_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : TopCat} (h : ↑Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).base h =
    CategoryTheory.CategoryStruct.comp f.base (CategoryTheory.CategoryStruct.comp g.base h)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskeringLeft_preservesLimits : ∀ {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] [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} D]
  (F : CategoryTheory.Functor C E),
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', max u₃ v₂, max u₁ v₂, max (max (max u₂ u₃) v₂) v₃,
      max (max (max u₁ u₂) v₁) v₂}
    ((CategoryTheory.Functor.whiskeringLeft C E D).obj F)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan.0.MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real_nonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (r : ℝ),
  0 ≤ r → (r • s).toJordanDecomposition = r • s.toJordanDecomposition
-- Mathlib.Analysis.Calculus.Deriv.Inv
deriv_fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 d x → d x ≠ 0 → deriv (fun x => c x / d x) x = (deriv c x * d x - c x * deriv d x) / d x ^ 2
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_sdiff_lt_of_lt_add`. -/
MeasureTheory.measure_diff_lt_of_lt_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → s ⊆ t → μ s ≠ ⊤ → ∀ {ε : ENNReal}, μ t < μ s + ε → μ (t \ s) < ε
-- Init.Data.List.Lemmas
/-- An induction principle for lists based on contiguous runs of identical elements.  -/
List.replicateRecOn : ∀ {α : Type u_1} {p : List α → Prop} (l : List α),
  p [] →
    (∀ (a : α) (n : ℕ), 0 < n → p (List.replicate n a)) →
      (∀ (a b : α) (n : ℕ) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (List.replicate n a ++ b :: l)) → p l
-- Mathlib.Data.DFinsupp.WellFounded
/-- This key lemma says that if a finitely supported dependent function `x₀` is obtained by merging
two such functions `x₁` and `x₂`, and if we evolve `x₀` down the `DFinsupp.Lex` relation one
step and get `x`, we can always evolve one of `x₁` and `x₂` down the `DFinsupp.Lex` relation
one step while keeping the other unchanged, and merge them back (possibly in a different way)
to get back `x`. In other words, the two parts evolve essentially independently under
`DFinsupp.Lex`. This is used to show that a function `x` is accessible if
`DFinsupp.single i (x i)` is accessible for each `i` in the (finite) support of `x`
(`DFinsupp.Lex.acc_of_single`).  -/
DFinsupp.lex_fibration : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] (r : ι → ι → Prop) (s : (i : ι) → α i → α i → Prop)
  [inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)],
  Relation.Fibration (InvImage (Prod.GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) Prod.snd) (DFinsupp.Lex r s)
    fun x => x.2.1.piecewise x.2.2 x.1
-- Init.Data.Float.Model.Unpacked.Operations.Status
/-- Returns `true` if the float is positive or negative infinity.
 -/
Float.Model.UnpackedFloat.isInf : Float.Model.UnpackedFloat → Bool
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inr.eq_1 : ∀ (x y : AugmentedSimplexCategory),
  x.inr y =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor y).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.WithInitial.starInitial.to x) y)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.nnnorm_rid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : TensorProduct 𝕜 E 𝕜), ‖(TensorProduct.rid 𝕜 E) x‖₊ = ‖x‖₊
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.trans_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Mul α] [inst_4 : Mul β] [inst_5 : Mul γ] (f : α ≃*o β) (g : β ≃*o γ) (a : α), (f.trans g) a = g (f a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, (m.getThenInsertIfNew? k v).1 = m.get? k
-- Std.Time.Time.Unit.Basic
/-- Converts a `Second.Offset` to a `Nanosecond.Offset`.
 -/
Std.Time.Nanosecond.Offset.ofSeconds : Std.Time.Second.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The inverse to a model with corners, only registered as a `PartialEquiv`.  -/
ModelWithCorners.symm : {𝕜 : 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] → ModelWithCorners 𝕜 E H → PartialEquiv E H
-- Mathlib.Topology.UrysohnsLemma
/-- By assumption, for each `c : CU P` there exists an open set `u`
such that `c.C ⊆ u` and `closure u ⊆ c.U`. `c.right` is the pair `(closure u, c.U)`.  -/
Urysohns.CU.right : {X : Type u_1} → [inst : TopologicalSpace X] → {P : Set X → Set X → Prop} → Urysohns.CU P → Urysohns.CU P
-- Mathlib.Geometry.Manifold.Immersion
/-- Given `C^n` manifolds `M` and `N` over the same model `I`,
`Sum.inl : M → M ⊕ N` is a `C^n` immersion with complement `Unit`  -/
Manifold.IsImmersionOfComplement.sumInl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_15}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'] [IsManifold I n M] [IsManifold I n M'],
  Manifold.IsImmersionOfComplement Unit I I n Sum.inl
-- Mathlib.Order.ModularLattice
/-- **Alias** of `inf_covBy_of_covBy_sup_left`. -/
CovBy.inf_of_sup_left : ∀ {α : Type u_1} [inst : Lattice α] [IsLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → a ⊓ b ⋖ b
-- Mathlib.Topology.Maps.Proper.Basic
isProperMap_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [h : CompactSpace X]
  [T1Space Y] (y : Y), IsProperMap fun x => y
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are field extensions of `F`, such that `A ⊗[F] B` is a domain, then there exists
a field extension of `F` that `A` and `B` embed into with linearly disjoint images.  -/
IntermediateField.LinearDisjoint.exists_field_of_isDomain : ∀ (F : Type u) [inst : Field F] (A : Type v) [inst_1 : Field A] (B : Type w) [inst_2 : Field B] [inst_3 : Algebra F A]
  [inst_4 : Algebra F B] [IsDomain (TensorProduct F A B)], ∃ K x x_1 fa fb, fa.fieldRange.LinearDisjoint ↥fb.fieldRange
-- Mathlib.Tactic.Ring.Common
/-- A ring instance on `α`, if available.  -/
Mathlib.Tactic.Ring.Common.Cache.rα : {u : Lean.Level} →
  {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → Mathlib.Tactic.Ring.Common.Cache sα → Option Q(CommRing «$α»)
-- Mathlib.RepresentationTheory.Action
/-- Every morphism between `G`-sets could be made into an intertwining map between
`Representation`s by the linear map induced on the indexing sets.  -/
Representation.linearizeMap : {k : Type u} →
  {G : Type v} →
    [inst : Monoid G] →
      [inst_1 : Semiring k] →
        {X Y : Action (Type w) G} →
          (X ⟶ Y) → (Representation.linearize k G X).IntertwiningMap (Representation.linearize k G Y)
-- Init.PropLemmas
ite_then_not_self : ∀ {p : Prop} [inst : Decidable p] {q : Prop}, (if p then ¬p else q) ↔ ¬p ∧ q
-- Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
_private.Mathlib.RingTheory.Polynomial.Eisenstein.Criterion.0.Polynomial.generalizedEisenstein_aux : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {K : Type u_2} [inst_2 : Field K] [inst_3 : Algebra R K]
  {q f g : Polynomial R} {p : ℕ},
  Irreducible (Polynomial.map (algebraMap R K) q) →
    q.Monic →
      (algebraMap R K) f.leadingCoeff ≠ 0 →
        f.IsPrimitive →
          Polynomial.map (algebraMap R K) f =
              Polynomial.C ((algebraMap R K) f.leadingCoeff) * Polynomial.map (algebraMap R K) q ^ p →
            g ∣ f →
              ∃ m r,
                g = Polynomial.C g.leadingCoeff * q ^ m + r ∧ Polynomial.map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)
-- Mathlib.Analysis.Convex.Basic
Antitone.convex_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Antitone f → ∀ (r : β), Convex 𝕜 {x | r ≤ f x}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (m.alter k f).getKey? k' =
        if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'
-- Mathlib.Data.Seq.Computation
/-- `head c` is the first step of computation, either `some a` if `c = pure a`
or `none` if `c = think c'`.  -/
Computation.head : {α : Type u} → Computation α → Option α
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
Submodule.quotientEquivOfIsTopCompl.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (p q : Submodule R M) [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q),
  p.quotientEquivOfIsTopCompl q h = p.quotientEquivOfIsTopCompl q h
-- Mathlib.Probability.Decision.Risk.Basic
/-- See `avgRisk_le_mul` for the usual case in which `π` is a probability measure and the kernels
are Markov.  -/
ProbabilityTheory.avgRisk_le_mul' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} (P : ProbabilityTheory.Kernel Θ 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
  (π : MeasureTheory.Measure Θ) {C : NNReal},
  (∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C) → ProbabilityTheory.avgRisk ℓ P κ π ≤ ↑C * κ.bound * P.bound * π Set.univ
-- Init.Data.List.Lemmas
List.getLast_filterMap_of_eq_some : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (w : l ≠ []) {b : β} (h : f (l.getLast w) = some b),
  (List.filterMap f l).getLast ⋯ = b
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- Given the data of a basic constructible set `s = V(g₁, ..., gₙ) \ V(f)`, return `f`.  -/
PrimeSpectrum.BasicConstructibleSetData.f : {R : Type u_1} → PrimeSpectrum.BasicConstructibleSetData R → R
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_of_not_le`. -/
Ideal.ramificationIdx_of_not_le : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, ¬Ideal.map (algebraMap R S) p ≤ P → p.ramificationIdx' P = 0
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.PRange.UpwardEnumerable β}
  {toFun : α → β} {injective : Function.Injective toFun}
  {succ?_toFun : ∀ (a : α), Std.PRange.succ? (toFun a) = Option.map toFun (Std.PRange.succ? a)}
  {succMany?_toFun : ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun a) = Option.map toFun (Std.PRange.succMany? n a)}
  {toFun_1 : α → β} {injective_1 : Function.Injective toFun_1}
  {succ?_toFun_1 : ∀ (a : α), Std.PRange.succ? (toFun_1 a) = Option.map toFun_1 (Std.PRange.succ? a)}
  {succMany?_toFun_1 :
    ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun_1 a) = Option.map toFun_1 (Std.PRange.succMany? n a)},
  { toFun := toFun, injective := injective, succ?_toFun := succ?_toFun, succMany?_toFun := succMany?_toFun } =
      { toFun := toFun_1, injective := injective_1, succ?_toFun := succ?_toFun_1,
        succMany?_toFun := succMany?_toFun_1 } →
    toFun = toFun_1
-- Mathlib.LinearAlgebra.Pi
LinearMap.CompatibleSMul.pi : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) [inst : Semiring S]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : SMul R M] [inst_4 : SMul R N] [inst_5 : Module S M]
  [inst_6 : Module S N] [LinearMap.CompatibleSMul M N R S], LinearMap.CompatibleSMul M (ι → N) R S
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.instBEqReason : BEq Std.Time.Reason✝
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_some_iff : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k k' : α}, m.WF → (m.getKey? k = some k' ↔ ∃ (h : k ∈ m), m.getKey k h = k')
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P Q : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : P ⟶ Q) (g : Φ.presheafFiber.obj Q ⟶ M) {Z : CategoryTheory.Functor Cᵒᵖ A} (h : Φ.skyscraperPresheaf M ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (Φ.skyscraperPresheafHomEquiv (CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map f) g)) h =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv g) h)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
exists_linearIndepOn_extension : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s t : Set ι},
  LinearIndepOn K v s → s ⊆ t → ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ ↑(Submodule.span K (v '' b)) ∧ LinearIndepOn K v b
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.id_eq_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : T.Algebra),
  CategoryTheory.Monad.Algebra.Hom.id A = CategoryTheory.CategoryStruct.id A
-- Mathlib.Analysis.Quaternion
Quaternion.coeComplex_coe : ∀ (r : ℝ), ↑↑r = ↑r
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- If `s` is not in `-ℕ`, then `hurwitzZetaOdd a (1 - s)` is an explicit multiple of
`sinZeta s`.  -/
HurwitzZeta.hurwitzZetaOdd_one_sub : ∀ (a : UnitAddCircle) {s : ℂ},
  (∀ (n : ℕ), s ≠ -↑n) →
    HurwitzZeta.hurwitzZetaOdd a (1 - s) =
      2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.sin (↑Real.pi * s / 2) * HurwitzZeta.sinZeta a s