mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_below_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.IsPrime] [r.LiesOver q] [Module.Finite R T], q.inertiaDeg R ≤ r.inertiaDeg R
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.comp_assoc : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  {V4 : Type u_8} {P4 : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2]
  [inst_7 : AddCommGroup V3] [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] [inst_10 : AddCommGroup V4]
  [inst_11 : Module k V4] [inst_12 : AddTorsor V4 P4] (f₃₄ : P3 →ᵃ[k] P4) (f₂₃ : P2 →ᵃ[k] P3) (f₁₂ : P1 →ᵃ[k] P2),
  (f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂)
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.compLeft_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : Mul α] [inst_1 : Mul β] (f : α →ₙ* β) (I : Type u_7) (h : I → α) (a : I),
  (f.compLeft I) h a = (⇑f ∘ h) a
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.desc_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {W : C} (k : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f k = 0) [CategoryTheory.Epi k],
  CategoryTheory.Epi (CategoryTheory.Limits.cokernel.desc f k h)
-- Mathlib.Computability.Language
Language.reverse_kstar : ∀ {α : Type u_1} (l : Language α), (KStar.kstar l).reverse = KStar.kstar l.reverse
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.gammaSet_div_gcd_to_gammaSet10_bijection : ∀ (r : ℕ) [NeZero r],
  Set.BijOn (EisensteinSeries.divIntMap ↑r) (EisensteinSeries.gammaSet 1 r 0) (EisensteinSeries.gammaSet 1 1 0)
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.uncurry_mulSingle_mulSingle : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : One M] [inst_2 : DecidableEq ι']
  (i : ι) (i' : ι') (b : M), Function.uncurry (Pi.mulSingle i (Pi.mulSingle i' b)) = Pi.mulSingle (i, i') b
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toHom_apply : ∀ {α : Type u_1} (a : α), Quiver.SingleObj.toHom a = a
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.toIsCancelAdd : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α], IsCancelAdd α
-- Mathlib.RingTheory.Multiplicity
/-- `emultiplicity a b` returns the largest natural number `n` such that
`a ^ n ∣ b`, as an `ℕ∞`. If `∀ n, a ^ n ∣ b` then it returns `⊤`.  -/
emultiplicity : {α : Type u_1} → [Monoid α] → α → α → ℕ∞
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.digits.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((b : ℕ) → motive b.succ.succ) → motive x
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_X_add_C : ∀ (z : ℂ), (Polynomial.X + Polynomial.C z).mahlerMeasure = max 1 ‖z‖
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.isQuasicoherent_pushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D}
  {S : CategoryTheory.Sheaf K RingCat} [inst_4 : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat]
  [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_6 : ∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C)
  [inst_7 : G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R)
  (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S)
  [inst_9 : ∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))],
  (∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
      CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂,
          max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
        (SheafOfModules.pushforward
          (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) →
    ∀ {M : SheafOfModules R} [M.IsQuasicoherent], ((SheafOfModules.pushforward φ).obj M).IsQuasicoherent
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.zero_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [inst_2 : CategoryTheory.Limits.HasZeroObject D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C}
  (f : X ⟶ Y), CategoryTheory.Functor.map 0 f = 0
-- Mathlib.Topology.Algebra.Support
mulTSupport_pow : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : Monoid α] (f : X → α) (n : ℕ),
  (mulTSupport fun x => f x ^ n) ⊆ mulTSupport f
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.hasHomology_of_preserves' : ∀ {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 : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [S.HasHomology] [F.PreservesLeftHomologyOf S]
  [F.PreservesRightHomologyOf S], (F.mapShortComplex.obj S).HasHomology
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instDecidableEqOrdinal : DecidableEq Std.Time.Hour.Ordinal
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.isTotallyUnimodular_iff_fintype : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] (A : Matrix m n R),
  A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast
-- Mathlib.Order.Filter.Basic
Filter.Eventually.ne_bot_of_gt : ∀ {α : Type u} {β : Type v} [inst : Preorder β] [inst_1 : OrderBot β] {l : Filter α} {f g : α → β},
  (∀ᶠ (x : α) in l, g x < f x) → ∀ᶠ (x : α) in l, f x ≠ ⊥
-- Mathlib.ModelTheory.Complexity
/-- An atomic formula is either equality or a relation symbol applied to terms.
Note that `⊥` and `⊤` are not considered atomic in this convention.  -/
FirstOrder.Language.BoundedFormula.IsAtomic : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_congr : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF →
    ∀ {a b : α},
      compare a b = Ordering.eq → Std.DTreeMap.Internal.Impl.Const.get! t a = Std.DTreeMap.Internal.Impl.Const.get! t b
-- Init.MetaTypes
/-- If true (default: false), extract lets from subterms that are implicit arguments.  -/
Lean.Meta.ExtractLetsConfig.implicits : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.Analysis.Normed.Group.Uniform
SeminormedCommGroup.toIsTopologicalGroup : ∀ {E : Type u_2} [inst : SeminormedCommGroup E], IsTopologicalGroup E
-- Init.Grind.Interactive
/-- `done` succeeds iff there are no remaining goals.  -/
Lean.Parser.Tactic.Grind.done : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.isometryEquivMap.toAffineMap_eq : ∀ {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁'] [inst_2 : NormedSpace 𝕜 V₁'] [inst_3 : MetricSpace P₁']
  [inst_4 : NormedAddTorsor V₁' P₁'] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁')
  [inst_9 : Nonempty ↥E],
  ↑(AffineSubspace.isometryEquivMap φ E).toAffineEquiv = ↑(E.equivMapOfInjective φ.toAffineMap ⋯)
-- Init.Data.UInt.Bitwise
UInt32.ne_not_self : ∀ {a : UInt32}, a ≠ ~~~a
-- Mathlib.Data.Set.Prod
Set.graphOn_prod_graphOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → γ) (g : β → δ),
  Set.graphOn f s ×ˢ Set.graphOn g t = ⇑(Equiv.prodProdProdComm α γ β δ) ⁻¹' Set.graphOn (Prod.map f g) (s ×ˢ t)
-- Mathlib.Topology.Order.LeftRightNhds
nhds_basis_mabs_div_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α]
  [OrderTopology α] [NoMaxOrder α] (a : α), (nhds a).HasBasis (fun ε => 1 < ε) fun ε => {b | |b / a|ₘ < ε}
-- Mathlib.RingTheory.Polynomial.HilbertPoly
_private.Mathlib.RingTheory.Polynomial.HilbertPoly.0.Polynomial.hilbertPoly.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (d : ℕ) → motive d.succ),
  (match 0 with
    | 0 => h_1 ()
    | d.succ => h_2 d) =
    h_1 ()
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α}, t.isEmpty = true → t.getKey! a = default
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.minKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.Equiv t₂ → t₁.minKey! = t₂.minKey!
-- Mathlib.Topology.ContinuousOn
/-- A function is continuous at a point `x` if `x` is isolated.  -/
continuousAt_of_not_accPt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α},
  ¬AccPt x (Filter.principal {x}ᶜ) → ContinuousAt f x
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.succ.match_1.eq_1 : ∀ (motive : PosNum → Sort u_1) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit1)
  (h_3 : (n : PosNum) → motive n.bit0),
  (match PosNum.one with
    | PosNum.one => h_1 ()
    | n.bit1 => h_2 n
    | n.bit0 => h_3 n) =
    h_1 ()
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_one : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), a ^ 1 = a
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.apply_mem_rootsOfUnity_orderOf : ∀ {F : Type u_1} [inst : Field F] [Finite F] {R : Type u_2} [inst_2 : CommRing R] (χ : MulChar F R) {a : F},
  a ≠ 0 → ∃ ζ ∈ rootsOfUnity (orderOf χ) R, ↑ζ = χ a
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂ : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCompIso G).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₂))
-- Init.Data.List.Control
List.findSomeM?_cons : ∀ {m : Type u → Type u_1} [inst : Monad m] {α : Type w} {β : Type u} {f : α → m (Option β)} {a : α} {as : List α},
  List.findSomeM? f (a :: as) = do
    let __do_lift ← f a
    match __do_lift with
      | some b => pure (some b)
      | none => List.findSomeM? f as
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse_apply_self : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → ∀ (y : M), f.inverse (f y) = y
-- Mathlib.Topology.Algebra.MulAction
ContinuousAt.vadd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {b : Y},
  ContinuousAt f b → ContinuousAt g b → ContinuousAt (f +ᵥ g) b
-- Init.Data.List.Sublist
List.eq_nil_of_infix_nil : ∀ {α : Type u_1} {l : List α}, l <:+: [] → l = []
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.coe_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : OneHom M N)
  (hmul : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y), ⇑{ toOneHom := f, map_mul' := hmul } = ⇑f
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.homotopicFrom : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  {p q : ↑(GenLoop N X x)}, Path.Homotopic (GenLoop.toLoop i p) (GenLoop.toLoop i q) → GenLoop.Homotopic p q
-- Lean.Server.References
/-- All references from within a module for all identifiers used in a single module.  -/
Lean.Server.ModuleRefs : Type
-- Init.Data.BitVec.Bitblast
BitVec.mulRec.eq_def : ∀ {w : ℕ} (x y : BitVec w) (s : ℕ),
  x.mulRec y s =
    have cur := if y.getLsbD s = true then x <<< s else 0;
    match s with
    | 0 => cur
    | s.succ => x.mulRec y s + cur
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.normal_ker : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M), f.ker.Normal
-- Mathlib.Data.Stream.Init
Stream'.take_succ' : ∀ {α : Type u} {s : Stream' α} (n : ℕ), Stream'.take (n + 1) s = Stream'.take n s ++ [s.get n]
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instQuasiSeparated : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsSeparated f], AlgebraicGeometry.QuasiSeparated f
-- Init.Data.Array.Subarray
Subarray.instInhabited : {α : Type u_1} → Inhabited (Subarray α)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.coe_dualBasis : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε) [inst_3 : DecidableEq ι] [inst_4 : Finite ι],
  ⇑h.basis.dualBasis = ε
-- Mathlib.Order.Hom.CompleteLattice
/-- The map `(a, b) ↦ a ⊔ b` as a `sSupHom`.  -/
supsSupHom : {α : Type u_2} → [inst : CompleteLattice α] → sSupHom (α × α) α
-- Mathlib.Order.Monotone.Basic
List.foldr_monotone : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β → β},
  (∀ (a : α), Monotone (f a)) → ∀ (l : List α), Monotone fun b => List.foldr f b l
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_id_eq_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.map (CategoryTheory.Functor.id C) = P.isoClosure
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getMatchRoot : {α : Type} → Lean.Meta.DiscrTree α → Lean.Meta.DiscrTree.Key → Array Lean.Expr → Array α → Lean.MetaM (Array α)
-- Mathlib.Algebra.BigOperators.Option
Finset.add_sum_eq_sum_insertNone : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → M) (x : M) (s : Finset α),
  x + ∑ i ∈ s, f i = ∑ i ∈ Finset.insertNone s, i.elim x f
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.coeFn_injective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂], Function.Injective DFunLike.coe
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.convMul_def : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R C] [inst_4 : Algebra R A] (f g : WithConv (C →ₐ[R] A)),
  f * g =
    WithConv.toConv
      ((Algebra.TensorProduct.lmul' R).comp
        ((Algebra.TensorProduct.map f.ofConv g.ofConv).comp (Bialgebra.comulAlgHom R C)))
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
_private.Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization.0.Polynomial.f_ne_zero : ∀ {K : Type u_1} [Field K] [inst : Fintype K] {p f : ℕ}, Fintype.card K = p ^ f → f ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.sup_support_coeff_finsetProd_le`. -/
AddMonoidAlgebra.sup_support_finsetProd_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} {ι : Type u_6} [inst : SemilatticeSup B] [inst_1 : OrderBot B]
  [inst_2 : CommSemiring R] [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid B] [AddLeftMono B] [AddRightMono B]
  {degb : A → B},
  degb 0 ≤ 0 →
    (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
      ∀ (s : Finset ι) (f : ι → AddMonoidAlgebra R A),
        (∏ i ∈ s, f i).coeff.support.sup degb ≤ ∑ i ∈ s, (f i).coeff.support.sup degb
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.FiniteIndex ↔ H.index ≠ 0
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The two fans on `i ↦ S ⊗[R] P i` agree if `ι` is finite.  -/
CommRingCat.Under.tensorProductFanIso : {R S : CommRingCat} →
  [inst : Algebra ↑R ↑S] →
    {ι : Type u} →
      (P : ι → CategoryTheory.Under R) →
        [Fintype ι] → [DecidableEq ι] → CommRingCat.Under.tensorProductFan S P ≅ CommRingCat.Under.tensorProductFan' S P
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.get_eq_of_singleton : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos} {t₁ t₂ : String} {c : Char},
  (p.next h).Splits (t₁ ++ String.singleton c) t₂ → p.get h = c
-- Mathlib.Data.Fintype.Order
Set.subset_sUnion_iff_of_directed : ∀ {α : Type u_2} {S : Set (Set α)} {s : Set α},
  S.Nonempty → S.Finite → DirectedOn (fun x1 x2 => x1 ⊆ x2) S → (s ⊆ sSup S ↔ ∃ t ∈ S, s ⊆ t)
-- Mathlib.Topology.Order.IntermediateValue
/-- If a closed interval is forward-invariant under a continuous map `f : α → α`,
then this map has a fixed point on this interval.  -/
exists_mem_Icc_isFixedPt_of_mapsTo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} {f : α → α},
  ContinuousOn f (Set.Icc a b) →
    a ≤ b → Set.MapsTo f (Set.Icc a b) (Set.Icc a b) → ∃ c ∈ Set.Icc a b, Function.IsFixedPt f c
-- Mathlib.Logic.Equiv.Finset
Denumerable.raise'.eq_2 : ∀ (x m : ℕ) (l : List ℕ), Denumerable.raise' (m :: l) x = (m + x) :: Denumerable.raise' l (m + x + 1)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.add_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {μ ν : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → ν.Integrable f → (μ + ν).Integrable f
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.restrict_mono : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}, π₁ ≤ π₂ → π₁.restrict J ≤ π₂.restrict J
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.hasInjectiveDimensionLT_of_enoughProjectives : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] [CategoryTheory.EnoughProjectives C] (X : C) (n : ℕ),
  (∀ (Y : C), Subsingleton (CategoryTheory.Abelian.Ext Y X n)) → CategoryTheory.HasInjectiveDimensionLT X n
-- Init.Data.Nat.Lemmas
Nat.sub_eq_of_eq_add' : ∀ {a b c : ℕ}, a = b + c → a - b = c
-- Init.System.Uri
/-- Decode %HH escapings in the given string. Note that sometimes a consecutive
sequence of multiple escapings can represent a utf-8 encoded sequence for
a single unicode code point and these will also be decoded correctly.  -/
System.Uri.UriEscape.decodeUri : String → String
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_inter_add_sdiff : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α} (t : Set α),
  s.Finite → ∑ᶠ (i : α) (_ : i ∈ s ∩ t), f i + ∑ᶠ (i : α) (_ : i ∈ s \ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_toENat : ∀ (a : Cardinal.{u_1}), (Cardinal.toENat a).toNat = Cardinal.toNat a
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_piEquivPiSubtypeProd : ∀ {ι : Type u_1} [inst : Fintype ι] (α : ι → Type u_4) [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] (p : ι → Prop) [inst_3 : DecidablePred p],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) MeasureTheory.volume
    MeasureTheory.volume
-- Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
/-- If `w` lies over `v`, then `w.Completion` is a `v.Completion`-algebra.  -/
NumberField.LiesOver.instAlgebraCompletion : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {v : NumberField.InfinitePlace K} →
            {w : NumberField.InfinitePlace L} → [w.LiesOver v] → Algebra v.Completion w.Completion
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The `GradedObject.BifunctorComp₁₂IndexData` which arises from complex shapes.  -/
ComplexShape.ρ₁₂ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {I₁₂ : Type u_4} →
        {J : Type u_6} →
          (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] →
                        CategoryTheory.GradedObject.BifunctorComp₁₂IndexData (c₁.r c₂ c₃ c₁₂ c)
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.IsTotallyUnimodular.reindex : ∀ {m : Type u_1} {m' : Type u_2} {n : Type u_3} {n' : Type u_4} {R : Type u_5} [inst : CommRing R] {A : Matrix m n R}
  (em : m ≃ m') (en : n ≃ n'), A.IsTotallyUnimodular → ((Matrix.reindex em en) A).IsTotallyUnimodular
-- Mathlib.Data.Set.Finite.Lattice
Finite.Set.finite_biUnion' : ∀ {α : Type u} {ι : Type u_1} (s : Set ι) [Finite ↑s] (t : ι → Set α) [∀ (i : ι), Finite ↑(t i)], Finite ↑(⋃ x ∈ s, t x)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesEpimorphisms.iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), F.PreservesEpimorphisms ↔ G.PreservesEpimorphisms
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.coe_con : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] (A : Set M) {a : ↑A}, ↑(L.con a) = ↑a
-- Std.Http.Data.Body.Basic
Std.Http.Body.instFromByteArrayString : Std.Http.Body.FromByteArray String
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- `K` as a valued field with the `v`-adic valuation.  -/
IsDedekindDomain.HeightOneSpectrum.adicValued : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type u_2} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → Valued K (WithZero (Multiplicative ℤ))
-- Mathlib.NumberTheory.Padics.Hensel
/-- We will construct a sequence of elements of `ℤ_p` satisfying successive values of `ih`.  -/
_private.Mathlib.NumberTheory.Padics.Hensel.0.ih_gen : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} → [inst_1 : CommSemiring R] → [Algebra R ℤ_[p]] → {F : Polynomial R} → {a : ℤ_[p]} → ℕ → ℤ_[p] → Prop