mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.zero_def : ∀ {K : Type u_1} [inst : CommRing K], RatFunc.zero = { toFractionRing := 0 }
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.image_coe_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some '' Set.Iic a = Set.Iic ↑a
-- Mathlib.Analysis.Analytic.Basic
/-- Analogue of `HasFPowerSeriesOnBall` where convergence is required only on a set `s`. We also
require convergence at `x` as the behavior of this notion is very bad otherwise.  -/
HasFPowerSeriesWithinOnBall : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → (E → F) → FormalMultilinearSeries 𝕜 E F → Set E → E → ENNReal → Prop
-- Mathlib.Tactic.GRewrite.Core
/-- The new side goals  -/
Mathlib.Tactic.GRewrite.GRewriteResult.mvarIds : Mathlib.Tactic.GRewrite.GRewriteResult → List Lean.MVarId
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed : Type
-- Mathlib.Logic.Function.OfArity
Function.OfArity.const_succ_apply : ∀ (α : Type u) {β : Type u} (b : β) (n : ℕ) (x : α), Function.OfArity.const α b n.succ x = Function.OfArity.const α b n
-- Mathlib.GroupTheory.Nilpotent
/-- The range of a surjective homomorphism from a nilpotent additive group is
nilpotent.  -/
AddGroup.nilpotent_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {G' : Type u_2} [inst_1 : AddGroup G'] [h : AddGroup.IsNilpotent G] (f : G →+ G'),
  Function.Surjective ⇑f → AddGroup.IsNilpotent G'
-- Mathlib.CategoryTheory.Sums.Basic
/-- The sum of two functors that land in a given category `C`.  -/
CategoryTheory.Functor.sum' : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            CategoryTheory.Functor A C → CategoryTheory.Functor B C → CategoryTheory.Functor (A ⊕ B) C
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_closure : ∀ {M : Type u_2} [inst : AddZeroClass M] (s : Set Mᵃᵒᵖ),
  (AddSubmonoid.closure s).unop = AddSubmonoid.closure (AddOpposite.op ⁻¹' s)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
/-- `Over X` is braided w.r.t. the Cartesian monoidal structure given by `Limits.pullback`.  -/
CategoryTheory.Over.braidedCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → (X : C) → CategoryTheory.BraidedCategory (CategoryTheory.Over X)
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
MeasurableEquiv.IicProdIoc.eq_1 : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] [inst_4 : (i : ι) → MeasurableSpace (X i)] {a b : ι} (hab : a ≤ b),
  MeasurableEquiv.IicProdIoc hab =
    { toFun := fun x i => if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
      invFun := fun x => (fun i => x ⟨↑i, ⋯⟩, fun i => x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯, measurable_toFun := ⋯,
      measurable_invFun := ⋯ }
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveFunYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i))
  [CategoryTheory.Presheaf.IsLocallySurjective AlgebraicGeometry.Scheme.zariskiTopology
      (CategoryTheory.Limits.Sigma.desc f)],
  CategoryTheory.Sheaf.IsLocallySurjective (AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf)
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.minView!.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k' : α) →
                (v' : β k') →
                  (l' r' : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')) →
            motive l
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.alterKey_cons_perm.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} {k : α} (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.Data.Nat.Bits
Nat.bodd_eq_bits_head : ∀ (n : ℕ), n.bodd = n.bits.headI
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Integration by parts on (-∞, ∞).**
With respect to a general bilinear form. For the specific case of multiplication, see
`integral_mul_deriv_eq_deriv_mul`.  -/
MeasureTheory.integral_bilinear_hasDerivAt_right_eq_sub : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {L : E →L[ℝ] F →L[ℝ] G} {u : ℝ → E} {v : ℝ → F} {u' : ℝ → E} {v' : ℝ → F} {m n : G} [CompleteSpace G],
  (∀ x ∈ tsupport v, HasDerivAt u (u' x) x) →
    (∀ x ∈ tsupport u, HasDerivAt v (v' x) x) →
      MeasureTheory.Integrable (fun x => (L (u x)) (v' x)) MeasureTheory.volume →
        MeasureTheory.Integrable (fun x => (L (u' x)) (v x)) MeasureTheory.volume →
          Filter.Tendsto (fun x => (L (u x)) (v x)) Filter.atBot (nhds m) →
            Filter.Tendsto (fun x => (L (u x)) (v x)) Filter.atTop (nhds n) →
              ∫ (x : ℝ), (L (u x)) (v' x) = n - m - ∫ (x : ℝ), (L (u' x)) (v x)
-- Std.Sync.Broadcast
Std.Broadcast.instHashableError.hash : Std.Broadcast.Error → UInt64
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.instMeasureSpacePUnit : MeasureTheory.MeasureSpace PUnit.{u_4 + 1}
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.commaFromOver_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {X_1 Y : CategoryTheory.Functor J (CategoryTheory.Over X)} (f : X_1 ⟶ Y),
  (CategoryTheory.WithTerminal.commaFromOver.map f).left =
    CategoryTheory.Functor.whiskerRight f (CategoryTheory.Over.forget X)
-- Std.Sync.Channel
/-- Tried to send to a closed channel.
 -/
Std.CloseableChannel.Error.closed : Std.CloseableChannel.Error
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_minKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).minKey?.isSome = true
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.singleR.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll lr r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.singleR k v lk lv ll lr r =
    Std.DTreeMap.Internal.Impl.bin lk lv ll (Std.DTreeMap.Internal.Impl.bin k v lr r)
-- Init.Data.List.Lemmas
List.exists_mem_of_length_eq_add_one : ∀ {α : Type u_1} {n : ℕ} {l : List α}, l.length = n + 1 → ∃ a, a ∈ l
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map_id_apply : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal]
  (h : optParam (N ≤ Subgroup.comap (MonoidHom.id G) N) ⋯) (x : G ⧸ N), (QuotientGroup.map N N (MonoidHom.id G) h) x = x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank function `f : P.RankFunction ι` for a
proper pairing `P` of a subcomplex `A` of simplicial set `X`,
the inclusion `A.ι` is a relative cell complex with basic cells
given by horn inclusions.  -/
SSet.Subcomplex.Pairing.RankFunction.relativeCellComplex : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) →
            [inst_1 : P.IsProper] →
              [inst_2 : SuccOrder ι] →
                [inst_3 : OrderBot ι] →
                  [NoMaxOrder ι] → [inst_5 : WellFoundedLT ι] → HomotopicalAlgebra.RelativeCellComplex f.basicCell A.ι
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.mem_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β} {x : β},
  x ∈ s +ᵥ t ↔ ∃ y ∈ s, ∃ z ∈ t, y +ᵥ z = x
-- Mathlib.Analysis.Calculus.Deriv.Comp
fderivWithin_comp_derivWithin_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F} (x : 𝕜)
  {s : Set 𝕜} {l : F → E} {y : F} {t : Set F},
  DifferentiableWithinAt 𝕜 l t y →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t → y = f x → derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- **Alias** of `Left.one_le_pow_of_le`. -/
one_le_pow_of_one_le' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M}, 1 ≤ a → ∀ (n : ℕ), 1 ≤ a ^ n
-- Init.Data.List.Erase
List.eraseP_cons : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.eraseP p (a :: l) = bif p a then l else a :: List.eraseP p l
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.indexNeg_neg : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  -i = (P.reflectionPerm i) i
-- Mathlib.CategoryTheory.Comma.Final
CategoryTheory.Comma.initial_snd_of_isConnected_costructuredArrow : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T)
  [∀ (b : B), CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow L (R.obj b))],
  (CategoryTheory.Comma.snd L R).Initial
-- Batteries.Classes.Order
Std.TransCmp.lt_of_le_of_lt : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {x y z : α},
  cmp x y ≠ Ordering.gt → cmp y z = Ordering.lt → cmp x z = Ordering.lt
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_div_pow_of_dvd : ∀ (k : ℕ) {x p : ℕ}, Nat.Prime p → p ^ k ∣ x → x / p ^ k / p ^ (x / p ^ k).factorization p = x / p ^ x.factorization p
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instOneQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : MulOneClass R] → (c : RingCon R) → One c.Quotient
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_base_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : B),
  φ.rightUnitor.inv.base.app X = CategoryTheory.CategoryStruct.id (φ.base.obj X)
-- Mathlib.Algebra.Algebra.RestrictScalars
instCommRingRestrictScalars : (R : Type u_1) → (S : Type u_2) → (A : Type u_4) → [I : CommRing A] → CommRing (RestrictScalars R S A)
-- Mathlib.Analysis.Calculus.TaylorIntegral
/-- *Taylor's theorem with remainder in integral form*. If `f` is `n + 1` times continuously
differentiable, then `f (x + y)` is given by
`∑ k in 0..n, D^k f(x; y,..,y) / k! + 1/n! ∫ t in 0..1, (1 - t) ^ n • D^{n+1}f (x + t • y; y,..,y)`,
where `D^k f` denotes the iterated derivative of `f`.

In the case that `n = 1`, this is a reformulation of the fundamental theorem of calculus, namely
`f (x + y) = f x + ∫ t in 0..1, D f(x + t • y; y)`.  -/
map_add_eq_sum_add_integral_iteratedFDeriv : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {x y : E} {n : ℕ} [CompleteSpace F],
  (∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑n + 1) f (x + t • y)) →
    f (x + y) =
      (∑ k ∈ Finset.range (n + 1), (↑k.factorial)⁻¹ • (iteratedFDeriv ℝ k f x) fun x => y) +
        (↑n.factorial)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x => y
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_const_add_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable Y μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance X (fun ω => c + Y ω) μ = ProbabilityTheory.covariance X Y μ
-- Mathlib.Data.Set.Image
/-- The preimage of a subsingleton under an injective map is a subsingleton.  -/
Set.Subsingleton.preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, s.Subsingleton → Function.Injective f → (f ⁻¹' s).Subsingleton
-- Std.Sat.AIG.CNF
/-- The node that we started CNF conversion at will always be marked as visited in the CNF cache.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go_marks : ∀ {aig : Std.Sat.AIG ℕ} {start : ℕ} {h : start < aig.decls.size} {state : Std.Sat.AIG.toCNF.State✝ aig},
  (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ ↑(Std.Sat.AIG.toCNF.go✝ aig start h state)))[start] =
    true
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.baseChangeMkQ_surjective : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type w}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] {B : Type w} [inst_5 : CommRing B] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : IsScalarTower R A B] (N : Submodule A (TensorProduct R A M)),
  Function.Surjective ⇑(Module.Grassmannian.baseChangeMkQ B N)
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.norm_lt_iff : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} {x : M ⧸ S} {r : ℝ}, ‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
-- Init.Meta.Defs
Lean.TSyntax.instCoeNumLitTerm : Coe Lean.NumLit Lean.Term
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_lipschitzWith_ofLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], LipschitzWith 1 WithLp.ofLp
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid contains the monoid's 1.  -/
Submonoid.one_mem : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), 1 ∈ S
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.norm_constOfIsEmpty : ∀ (𝕜 : Type u) (E : Type wE) {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : IsEmpty ι] (x : F),
  ‖ContinuousAlternatingMap.constOfIsEmpty 𝕜 E ι x‖ = ‖x‖
-- Mathlib.Tactic.Ring.Common
/-- Given a monomial expression `va`, splits off the leading coefficient `k` and the remainder
`e'`, stored in the `ExtractCoeff` structure.

* `c = 1 * c` (if `c` is a constant)
* `a * b = (a * b') * k` if `b = b' * k`
 -/
Mathlib.Tactic.Ring.Common.extractCoeff : Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
  {a : Q(ℕ)} → Mathlib.Tactic.Ring.Common.ExProdNat a → Mathlib.Tactic.Ring.Common.ExtractCoeff a
-- Lean.Meta.DecLevel
Lean.Meta.DecLevelContext : Type
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The unique map to the base from the pullback.  -/
CategoryTheory.Limits.WidePullback.base : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {B : C} →
        {objs : J → C} →
          (arrows : (j : J) → objs j ⟶ B) →
            [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] →
              CategoryTheory.Limits.widePullback B objs arrows ⟶ B
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.obj_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} (x y : CategoryTheory.CostructuredArrow S T) (hl : x.left = y.left),
  CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.eqToHom hl)) y.hom = x.hom → x = y
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instMax : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Max (LieSubmodule R L M)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.exists_finset_of_mem_iSup : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Type u_3}
  {f : ι → IntermediateField F E} {x : E}, x ∈ ⨆ i, f i → ∃ s, x ∈ ⨆ i ∈ s, f i
-- Mathlib.NumberTheory.Fermat
Nat.prod_fermatNumber : ∀ (n : ℕ), ∏ k ∈ Finset.range n, k.fermatNumber = n.fermatNumber - 2
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mk.sizeOf_spec : ∀ {M : Type u_3} [inst : Mul M] [inst_1 : SizeOf M] (carrier : Set M)
  (mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier),
  sizeOf { carrier := carrier, mul_mem' := mul_mem' } = 1
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_neg : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 → UpperHalfPlane.qExpansion h (-f) = -UpperHalfPlane.qExpansion h f
-- Mathlib.Data.Num.Lemmas
Num.add_toZNum : ∀ (m n : Num), (m + n).toZNum = m.toZNum + n.toZNum
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.mk.sizeOf_spec : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  [inst_1 : SizeOf B] (prop : (X : B) → CategoryTheory.ObjectProperty ↑(F.obj X)), sizeOf { prop := prop } = 1
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The binary coproduct cofan in `TopCat`.  -/
TopCat.binaryCofan : (X Y : TopCat) → CategoryTheory.Limits.BinaryCofan X Y
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.pow_left_iff : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} {m : ℕ}, 0 < m → (IsCoprime (x ^ m) y ↔ IsCoprime x y)
-- Mathlib.Data.Finset.Basic
Finset.disjoint_sdiff_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), Disjoint (s \ t) (s ∩ t)
-- Init.Data.BitVec.Lemmas
BitVec.not_neg : ∀ {w : ℕ} (x : BitVec w), ~~~(-x) = x - 1#w
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.IntFractPair.get?_seq1_eq_succ_get?_stream : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ},
  (GenContFract.IntFractPair.seq1 v).2.get? n = GenContFract.IntFractPair.stream v (n + 1)
-- Mathlib.Topology.EMetricSpace.Defs
Metric.nhdsWithin_basis_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α},
  (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.eball x ε ∩ s
-- Std.Http.Protocol.H1
/-- The pulled body chunk.
 -/
Std.Http.Protocol.H1.PulledChunk.chunk : Std.Http.Protocol.H1.PulledChunk → Std.Http.Chunk
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
/-- `minpolyDiv R x : S[X]` for `x : S` is the polynomial `minpoly R x / (X - C x)`.  -/
minpolyDiv : (R : Type u_1) → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → S → Polynomial S
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forgetToTop_obj : ∀ (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.forgetToTop.obj X = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).obj X.toSheafedSpace
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryLED : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → α × β → α × β
-- Init.Data.List.Nat.Perm
/-- Variant of `List.Perm.take` specifying that the permutation is constant after `i` elementwise.  -/
List.Perm.take_of_getElem? : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.Perm l₂ → ∀ {i : ℕ}, (∀ (j : ℕ), i ≤ j → l₁[j]? = l₂[j]?) → (List.take i l₁).Perm (List.take i l₂)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Tendsto.mul_const : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal},
  Filter.Tendsto m f (nhds a) → a ≠ 0 ∨ b ≠ ⊤ → Filter.Tendsto (fun x => m x * b) f (nhds (a * b))
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.l_sup : ∀ {α : Type u} {β : Type v} {a₁ a₂ : α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {l : α → β} {u : β → α},
  GaloisConnection l u → l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.singleton_inj : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {x y : α}, {x} = {y} ↔ x = y
-- Mathlib.Topology.Order
instTopologicalSpaceBool : TopologicalSpace Bool
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.eta.eq_1 : ∀ (G : GrpCat),
  ProfiniteGrp.ProfiniteCompletion.eta G =
    GrpCat.ofHom { toFun := ProfiniteGrp.ProfiniteCompletion.etaFn G, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- A congruence lemma for `mfderiv`, (ab)using the fact that `TangentSpace I' (f x)` is
definitionally equal to `E'`.  -/
mfderiv_congr : ∀ {𝕜 : 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'] {f : M → M'} {x : M} {f' : M → M'},
  f = f' → mfderiv% f x = mfderiv% f' x
-- Mathlib.Data.Nat.Factorization.Root
/-- Flooring root of a natural number. This divides the valuation of every prime number rounding
down.

Eg if `n = 2`, `a = 2^3 * 3^2 * 5`, then `floorRoot n a = 2 * 3`.

In order theory terms, this is the upper or right adjoint of the map `a ↦ a ^ n : ℕ → ℕ` where `ℕ`
is ordered by divisibility.

To ensure that the adjunction (`Nat.pow_dvd_iff_dvd_floorRoot`) holds in as many cases as possible,
we special-case the following values:
* `floorRoot 0 a = 0`
* `floorRoot n 0 = 0`
 -/
Nat.floorRoot : ℕ → ℕ → ℕ
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Lean.Environment
/-- Enables/disables kernel diagnostics.  -/
Lean.Kernel.enableDiag : Lean.Environment → Bool → Lean.Environment
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the reverse direction of `SimpleGraph.edgeSet_ssubset_edgeSet`. -/
SimpleGraph.edgeSet_strict_mono : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V}, G₁ < G₂ → G₁.edgeSet ⊂ G₂.edgeSet
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence of functions `Fₙ` converges uniformly to a limiting function `f` w.r.t.
filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ˢ ⊤` to the uniformity.
In other words: one knows nothing about the behavior of `x` in this limit.
 -/
tendstoUniformly_iff_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
  TendstoUniformly F f p ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (uniformity β)