mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Special case of `inner_smul_left_eq_star_smul` when the acting ring has a trivial star
(e.g. `ℕ`, `ℤ`, `ℚ≥0`, `ℚ`, `ℝ`).  -/
inner_smul_left_eq_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {𝕝 : Type u_4} [inst_3 : CommSemiring 𝕝] [inst_4 : StarRing 𝕝] [inst_5 : Algebra 𝕝 𝕜] [inst_6 : Module 𝕝 E]
  [IsScalarTower 𝕝 𝕜 E] [StarModule 𝕝 𝕜] [TrivialStar 𝕝] (x y : E) (r : 𝕝), inner 𝕜 (r • x) y = r • inner 𝕜 x y
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.const_inj : ∀ {n₁ n₂ : ℕ}, Nat.Partrec.Code.const n₁ = Nat.Partrec.Code.const n₂ → n₁ = n₂
-- Mathlib.Order.RelClasses
/-- **Alias** of `Std.Asymm.swap`. -/
IsAsymm.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Asymm r], Std.Asymm (Function.swap r)
-- Mathlib.Algebra.Group.Defs
/-- A mixin for right cancellative multiplication.  -/
IsRightCancelMul : (G : Type u) → [Mul G] → Prop
-- Batteries.Data.List.Lemmas
List.nil_diff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l : List α), [].diff l = []
-- Init.Coe
boolToProp : Coe Bool Prop
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- The real power function `x^y` on extended nonnegative reals, defined for `x : ℝ≥0∞` and
`y : ℝ` as the restriction of the real power function if `0 < x < ⊤`, and with the natural values
for `0` and `⊤` (i.e., `0 ^ x = 0` for `x > 0`, `1` for `x = 0` and `⊤` for `x < 0`, and
`⊤ ^ x = 1 / 0 ^ x`).  -/
ENNReal.rpow : ENNReal → ℝ → ENNReal
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- The mulAntidiagonal of an element `n` is the finset of pairs `(i, j)` such that
`i * j = n`.  -/
Finset.HasMulAntidiagonal.mulAntidiagonal : {A : Type u_1} → {inst : Monoid A} → [self : Finset.HasMulAntidiagonal A] → A → Finset (A × A)
-- Mathlib.Data.Nat.Sqrt
Nat.succ_le_succ_sqrt : ∀ (n : ℕ), n + 1 ≤ (n.sqrt + 1) * (n.sqrt + 1)
-- Mathlib.Analysis.Calculus.Deriv.Add
HasStrictDerivAt.sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F},
  (∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x) → HasStrictDerivAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x
-- Mathlib.CategoryTheory.Yoneda
/-- Alternative constructor for `F.IsRepresentable`, which takes as an input an
isomorphism `yoneda.obj X ≅ F`.  -/
CategoryTheory.Functor.IsRepresentable.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {X : C}
  (e : CategoryTheory.yoneda.obj X ≅ F), F.IsRepresentable
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.BifibrantObject C} {f g : X ⟶ Y},
  HomotopicalAlgebra.BifibrantObject.homRel C f g ↔ HomotopicalAlgebra.RightHomotopyRel f.hom g.hom
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.ofCocone_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  [inst_2 : CategoryTheory.IsFiltered I] {F : CategoryTheory.Functor I C}
  (c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)) (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).isColimit = hc
-- Mathlib.Data.NNReal.Defs
NNReal.iInf_const_zero : ∀ {α : Sort u_2}, ⨅ x, 0 = 0
-- Init.Data.Array.Basic
/-- Checks whether an array is empty.

An array is empty if its size is `0`.

Examples:
* `(#[] : Array String).isEmpty = true`
* `#[1, 2].isEmpty = false`
* `#[()].isEmpty = false`
 -/
Array.isEmpty : {α : Type u} → Array α → Bool
-- Mathlib.Tactic.Translate.Reorder
/-- Decompose the permutation `map` into its disjoint cycle representation.  -/
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.decomposePerm : {n : ℕ} → Vector (Option (Fin n)) n → Mathlib.Tactic.Translate.Permutation
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_succ_right_eq_append : ∀ {m n : ℕ}, m ≤ n + 1 → (m...=n + 1).toList = (m...=n).toList ++ [n + 1]
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.preservesFiniteLimits_presheafToSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms]
  [inst_8 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ]
  [CategoryTheory.Limits.HasFiniteLimits D],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.plusPlusSheaf J D)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k fallback : α},
  k ∉ m → l.contains k = false → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKeyD k fallback = fallback
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.IsFiniteType.mk : ∀ {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] {M : SheafOfModules R},
  (∃ σ, σ.IsFiniteType) → M.IsFiniteType
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isEncodedChar_isAscii : ∀ {r : UInt8 → Bool} (c : UInt8), Std.Http.URI.isEncodedChar r c = true → Std.Http.Internal.Char.isAsciiByte c = true
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.set_smul_le : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (s : Set S) (N p : Submodule R M),
  (∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → s • N ≤ p
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.mk : (toSheafedSpace : AlgebraicGeometry.SheafedSpace CommRingCat) →
  (∀ (x : ↑↑toSheafedSpace.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace.presheaf.stalk x)) →
    AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Data.List.Cycle
Cycle.reverse_nil : ∀ {α : Type u_1}, Cycle.nil.reverse = Cycle.nil
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_withTheReader_ReaderT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ α : Type u}
  {post : α → ρ → Pred} {epost : EPred} (f : ρ → ρ) (x : ReaderT ρ m α),
  Std.Internal.Do.wp (withTheReader ρ f x) post epost = Std.Internal.Do.wp (MonadWithReaderOf.withReader f x) post epost
-- Mathlib.Topology.Gluing
TopCat.GlueData.image_inter : ∀ (D : TopCat.GlueData) (i j : D.J),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) =
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)))
-- Mathlib.Topology.Order.Monotone
/-- If a function is antitone in a second countable topological space, then there
are only countably many points that have several preimages.  -/
Antitone.countable_setOfPred_two_preimages : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [SecondCountableTopology α],
  Antitone f → {c | ∃ x y, x < y ∧ f x = c ∧ f y = c}.Countable
-- Init.Data.UInt.Lemmas
UInt32.instIsLinearOrder : Std.IsLinearOrder UInt32
-- Mathlib.Topology.Constructions.SumProd
Prod.instNeBotNhdsWithinIio : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder X]
  [inst_3 : Preorder Y] {x : X × Y} [hx₁ : (nhdsWithin x.1 (Set.Iio x.1)).NeBot]
  [hx₂ : (nhdsWithin x.2 (Set.Iio x.2)).NeBot], (nhdsWithin x (Set.Iio x)).NeBot
-- Lean.Meta.IndPredBelow
/-- Converts a pattern that matches on `h : ∀ x y z..., ABC ...` (where `ABC` is an inductive
predicate) into two patterns: One that still matches on the same type as before and
another that matches on `∀ x y z..., belowIndName ... (h x y z)`. This function assumes that
`belowIndName` corresponds to a `below` inductive for `ABC` (for nested inductive predicates this
may not be `ABC.below`).
The goal of this function is to get as many motive proofs (used for recursive applications) and
below proofs (used for further matches) as possible. In the default case, it will simply keep the
original pattern and introduce a new variable of type `∀ x y z..., belowIndName ... (h x y z)` as
the below pattern.
 -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowMatcher.convertToBelow : Array Lean.Expr →
  ℕ →
    Lean.Name →
      Lean.Meta.Match.Pattern →
        Option Lean.Expr →
          StateRefT' IO.RealWorld (Array Lean.Meta.IndPredBelow.NewDecl✝) Lean.MetaM
            (Lean.Meta.Match.Pattern × Lean.Meta.Match.Pattern)
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N : Submodule R M), N.annihilator = Module.annihilator R ↥N
-- Aesop.Forward.State
Aesop.VariableMap.map : Aesop.VariableMap → Lean.PHashMap Aesop.PremiseIndex Aesop.InstMap
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.dropn_nil : ∀ {α : Type u} (n : ℕ), Stream'.WSeq.nil.drop n = Stream'.WSeq.nil
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last : ∀ {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} {M₄ : Type u_6} [inst : CommRing R]
  [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : AddCommGroup M₄]
  [inst_5 : Module R M] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] {rs : List R}
  {f₁ : M →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {f₃ : M₃ →ₗ[R] M₄},
  Function.Exact ⇑f₁ ⇑f₂ →
    Function.Exact ⇑f₂ ⇑f₃ →
      Function.Surjective ⇑f₃ →
        RingTheory.Sequence.IsWeaklyRegular M₄ rs →
          Function.Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₁ ⋯)
            ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₂ ⋯)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The norm is submultiplicative.  -/
NormedRing.norm_mul_le : ∀ {α : Type u_5} [self : NormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) {Z : C}
  (h : ((TopCat.Presheaf.pullback C f).obj F).stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F U x hx)
      (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPullbackHom C f F x) h) =
    CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).germ U x hx) h
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel κ]
  [inst : ProbabilityTheory.IsFiniteKernel η] {a : α},
  (κ a).AbsolutelyContinuous (η a) → (η.withDensity (κ.rnDeriv η)) a = κ a
-- Mathlib.Tactic.NormNum.PowMod
/-- Invariants: `a ^ b₀ % m = c₀`, `depth > 0`, `b >>> depth = b₀`  -/
_private.Mathlib.Tactic.NormNum.PowMod.0.Mathlib.Meta.NormNum.evalNatPowMod.go : ℕ →
  (a m b₀ c₀ b : Q(ℕ)) →
    (p : Q(Prop)) →
      «$p» =Q ((«$a».pow «$b₀»).mod «$m» = «$c₀») →
        (c : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNatPowModT «$p» «$a» «$b» «$m» «$c»)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_comp_neg : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) (f : E →L[𝕜] E),
  (FormalMultilinearSeries.ofScalars E c).compContinuousLinearMap (-f) =
    (FormalMultilinearSeries.ofScalars E fun k => (-1) ^ k * c k).compContinuousLinearMap f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_union_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R), ((Polynomial.monomial n) a).mirror = (Polynomial.monomial n) a
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.isOffsetPattern? : Lean.Expr → Option (Lean.Expr × ℕ)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.not_isMarkovKernel_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α],
  ¬ProbabilityTheory.IsMarkovKernel 0
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instReprLambdaTheoremType : Repr Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polarBilin_comp : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {N' : Type u_8} [inst_5 : AddCommGroup N'] [inst_6 : Module R N']
  (Q : QuadraticMap R N' N) (f : M →ₗ[R] N'), (Q.comp f).polarBilin = LinearMap.compl₁₂ Q.polarBilin f f
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.Commute.zpow_zpow_self : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) (m n : ℤ), Commute (A ^ m) (A ^ n)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_add_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (f : ↥(MeasureTheory.Lp E 1 μ)),
  (MeasureTheory.L1.setToL1 ⋯) f = (MeasureTheory.L1.setToL1 hT) f + (MeasureTheory.L1.setToL1 hT') f
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.commute : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g} {x : B} {h : c ⟶ x}
  [self : CategoryTheory.Bicategory.Lan.CommuteWith f g h],
  Nonempty ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h).IsKan
-- Mathlib.Data.Part
Part.Dom.of_bind : ∀ {α : Type u_1} {β : Type u_2} {f : α → Part β} {a : Part α}, (a.bind f).Dom → a.Dom
-- Mathlib.Topology.Algebra.MetricSpace.Lipschitz
LipschitzWith.cauchySeq_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ {u : ℕ → α}, CauchySeq u → CauchySeq (f ∘ u)
-- Mathlib.FieldTheory.SeparableDegree
/-- A random bijection between `Field.Emb F E` and `E →ₐ[F] K` if `E = F(S)` such that every
element `s` of `S` is integral (= algebraic) over `F` and whose minimal polynomial splits in `K`.
Combined with `Field.instInhabitedEmb`, it can be viewed as a stronger version of
`IntermediateField.nonempty_algHom_of_adjoin_splits`.  -/
Field.embEquivOfAdjoinSplits : (F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (K : Type w) →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] →
                {S : Set E} →
                  IntermediateField.adjoin F S = ⊤ →
                    (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
                      Field.Emb F E ≃ (E →ₐ[F] K)
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.nonempty_antidiagonal : ∀ {M : Type u_2} [inst : AddMonoid M] [inst_1 : Finset.HasAntidiagonal M] (a : M),
  (Finset.HasAntidiagonal.antidiagonal a).Nonempty
-- Mathlib.Analysis.Calculus.ContDiff.Polynomial
/-- Polynomials are smooth  -/
Polynomial.contDiff_aeval : ∀ {R : Type u_1} {𝕜 : Type u_2} [inst : CommSemiring R] [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : Algebra R 𝕜]
  (f : Polynomial R) (n : WithTop ℕ∞), ContDiff 𝕜 n fun x => (Polynomial.aeval x) f
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsDecompositionField.ringEquiv.eq_1 : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (D : Type u_5) [inst_4 : Field D] [inst_5 : Algebra D L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (D' : Type u_8) [inst_7 : Field D'] [inst_8 : Algebra D' L]
  [inst_9 : IsDecompositionField K L P D] [inst_10 : IsDecompositionField K L P D'],
  IsDecompositionField.ringEquiv K L P D D' = IsGaloisGroup.ringEquiv (↥(MulAction.stabilizer Gal(L/K) P)) D D' L
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- An abbreviation for `HasColimit (Discrete.functor f)`.  -/
CategoryTheory.Limits.HasCoproduct : {β : Type w} → {C : Type u} → [CategoryTheory.Category.{v, u} C] → (β → C) → Prop
-- Mathlib.Data.Multiset.AddSub
Multiset.nodup_singleton : ∀ {α : Type u_1} (a : α), {a}.Nodup
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instLTOffset : LT Std.Time.Millisecond.Offset
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffAt_iff : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞} {f : M → M'} {x : M},
  ContMDiffAt I I' n f x ↔
    ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x)
-- Init.Data.SInt.Basic
instToStringInt64 : ToString Int64
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_mulVec : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalCommSemiring α] [inst_1 : Fintype m]
  [inst_2 : Fintype n] (A : Matrix m n α) (B : Matrix m o α) (x : n → α),
  Matrix.vecMul (A.mulVec x) B = Matrix.vecMul x (A.transpose * B)
-- Init.Core
ReflBEq.mk : ∀ {α : Type u_1} [inst : BEq α], (∀ {a : α}, (a == a) = true) → ReflBEq α
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.ofAbs_div : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Field R] (v : AbsoluteValue R S)
  (x y : WithAbs v), (x / y).ofAbs = x.ofAbs / y.ofAbs
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_inter_cancel_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (s ∪ t) ∩ t = t
-- Mathlib.Analysis.Normed.Group.Hom
/-- Associate to a group homomorphism a bounded group homomorphism under a norm control condition.

See `AddMonoidHom.mkNormedAddGroupHom` for a version that uses `ℝ` for the bound.  -/
AddMonoidHom.mkNormedAddGroupHom' : {V : Type u_1} →
  {W : Type u_2} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : SeminormedAddCommGroup W] →
        (f : V →+ W) → (C : NNReal) → (∀ (x : V), ‖f x‖₊ ≤ C * ‖x‖₊) → NormedAddGroupHom V W
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.isScalarTower : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) [inst_2 : SMul S R] [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M], IsScalarTower S R ↥p
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.universally_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C), P.universally ≤ P
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.instRespectsLeftSchemeOfIsStableUnderBaseChange : ∀ {W P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [W.IsStableUnderBaseChange]
  [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving W] [P.RespectsLeft Q] [Q.IsStableUnderBaseChange],
  (AlgebraicGeometry.sourceLocalClosure W P).RespectsLeft Q
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Tendsto.const_mul : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal},
  Filter.Tendsto m f (nhds b) → b ≠ 0 ∨ a ≠ ⊤ → Filter.Tendsto (fun b => a * m b) f (nhds (a * b))
-- Mathlib.Logic.Relation
Relation.eqvGen_iff : ∀ {α : Type u_1} (r : α → α → Prop) (a a_1 : α),
  Relation.EqvGen r a a_1 ↔
    r a a_1 ∨ a_1 = a ∨ Relation.EqvGen r a_1 a ∨ ∃ y, Relation.EqvGen r a y ∧ Relation.EqvGen r y a_1
-- Mathlib.RingTheory.MvPolynomial.Localization
MvPolynomial.isLocalization_C_mk' : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] (M : Submonoid R) (S : Type u_3) [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (a : R) (m : ↥M),
  MvPolynomial.C (IsLocalization.mk' S a m) =
    IsLocalization.mk' (MvPolynomial σ S) (MvPolynomial.C a) ⟨MvPolynomial.C ↑m, ⋯⟩
-- Init.SizeOf
Lean.Name.num.sizeOf_spec : ∀ (p : Lean.Name) (n : ℕ), sizeOf (p.num n) = 1 + sizeOf p + sizeOf n
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.unop_neg : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : Cᵒᵖ}
  (f : X ⟶ Y), (-f).unop = -f.unop
-- Mathlib.Analysis.Normed.Order.UpperLower
IsLowerSet.mem_interior_of_forall_lt : ∀ {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} {x y : ι → ℝ},
  IsLowerSet s → x ∈ closure s → (∀ (i : ι), y i < x i) → y ∈ interior s
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.IsLocalization.height_under_eq_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsLocalization S A] (J : Ideal A) [J.IsPrime], (Ideal.comap (algebraMap R A) J).height = J.height
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The trivial seminorm on a ring `R` is the `MulRingSeminorm` taking value `0` at `0` and `1` at
every other element.  -/
MulRingSeminorm.instOne : {R : Type u_1} →
  [inst : NonAssocRing R] → [DecidableEq R] → [NoZeroDivisors R] → [Nontrivial R] → One (MulRingSeminorm R)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] F),
  ContinuousLinearMap.lTensor G (-f) = -ContinuousLinearMap.lTensor G f
-- Mathlib.RingTheory.Norm.Transitivity
/-- The upper-left block of `M * aux M k`.  -/
Algebra.Norm.Transitivity.termMulAuxMatBlock : Lean.ParserDescr