mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piEquivPiSubtypeProd_symm_apply : ∀ {δ' : Type u_5} (π : δ' → Type u_6) [inst : (x : δ') → MeasurableSpace (π x)] (p : δ' → Prop)
  [inst_1 : DecidablePred p],
  ⇑(MeasurableEquiv.piEquivPiSubtypeProd π p).symm = fun f x => if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
-- Mathlib.GroupTheory.Perm.Support
/-- **Alias** of `Equiv.Perm.support_swap_mul_ge_support_sdiff`. -/
Equiv.Perm.support_swap_mul_ge_support_diff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) (x y : α),
  f.support \ {x, y} ⊆ (Equiv.swap x y * f).support
-- Mathlib.Topology.Semicontinuity.Basic
/-- The overlevel sets of an upper semicontinuous function on a compact set are compact.  -/
UpperSemicontinuousOn.isCompact_inter_preimage_Ici : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ] {f : α → γ},
  UpperSemicontinuousOn f s → IsCompact s → ∀ (c : γ), IsCompact (s ∩ f ⁻¹' Set.Ici c)
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : CommSemigroup α],
  MulOpposite.instCommSemigroup = { toSemigroup := MulOpposite.instSemigroup, mul_comm := ⋯ }
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.isOpen_def : ∀ {α : Type u_1} [inst : Preorder α] {T : Set (Topology.WithLawson α)},
  IsOpen T ↔ TopologicalSpace.IsOpen (⇑Topology.WithLawson.toLawson ⁻¹' T)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.symm_symm : ∀ {𝕜 : 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₂] (e : P ≃ᵃⁱ[𝕜] P₂), e.symm.symm = e
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.map_expand : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] {p : ℕ} {f : R →+* S} {q : Polynomial R},
  Polynomial.map f ((Polynomial.expand R p) q) = (Polynomial.expand S p) (Polynomial.map f q)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_theta_add_sum_theta' : ∀ {x : ℝ},
  2 ≤ x →
    ∀ {N : ℕ},
      ⌊Real.log x / Real.log 2⌋₊ ≤ N →
        Chebyshev.psi x = Chebyshev.theta x + ∑ n ∈ Finset.Icc 2 N, Chebyshev.theta (x ^ (1 / ↑n))
-- Lean.Declaration
Lean.instInhabitedQuotKind : Inhabited Lean.QuotKind
-- Mathlib.Tactic.NormNum.Inv
/-- Helper function to synthesize a typed `CharZero α` expression given `AddMonoidWithOne α`.  -/
Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne : {u : Lean.Level} →
  {α : Q(Type u)} →
    (_i : autoParam Q(AddMonoidWithOne «$α») Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne._auto_1) →
      Lean.MetaM Q(CharZero «$α»)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF →
    t₂.WF →
      ∀ {k : α} {fallback : β k},
        (t₁ \ t₂).getD k fallback = if t₂.contains k = true then fallback else t₁.getD k fallback
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, t.WF → (Std.TreeMap.Raw.map f t).getKey? k = t.getKey? k
-- Mathlib.Tactic.NormNum.BigOperators
/-- The set is Nil.  -/
Mathlib.Meta.List.ProveNilOrConsResult.nil : {u : Lean.Level} → {α : Q(Type u)} → {s : Q(List «$α»)} → Q(«$s» = []) → Mathlib.Meta.List.ProveNilOrConsResult s
-- Mathlib.Topology.Algebra.InfiniteSum.Order
le_hasProd_of_le_prod : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : Preorder α] [inst_1 : CommMonoid α]
  [inst_2 : TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIciTopology α] [L.NeBot],
  HasProd f a L → (∀ (s : Finset ι), c ≤ ∏ i ∈ s, f i) → c ≤ a
-- Mathlib.Order.Bounds.Basic
/-- If `s ⊆ t` and `t` is bounded above, then so is `s`.  -/
BddAbove.mono : ∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddAbove t → BddAbove s
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Given a local frame `s i ` on `u`, if a section `t` has differentiable coefficients on `u`
w.r.t. `s i`, then `t` is differentiable on `u`.  -/
IsLocalFrameOn.mdifferentiableOn_of_coeff : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {t : (x : M) → V x} [VectorBundle 𝕜 F V] (hs : IsLocalFrameOn I F 1 s u) [FiniteDimensional 𝕜 F],
  (∀ (i : ι), MDiff[u] ((LinearMap.piApply (hs.coeff i)) t)) → MDiff[u] (T% t)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the index type of the covering of `S`  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.I₀ : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} → {S : C} → F.PreOneHypercoverDenseData S → Type w
-- Mathlib.Data.Vector3
/-- The vector cons operation  -/
Vector3.«term_::_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Monoid
SeparatelyContinuousMul.to_continuousSMul_op : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M], ContinuousConstSMul Mᵐᵒᵖ M
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k k' : α} {f : β k → β k},
      (m.modify k f).get? k' = if h : (k == k') = true then cast ⋯ (Option.map f (m.get? k)) else m.get? k'
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.Agree'.trivial : ∀ {F : PFunctor.{uA, uB}} (x y : F.M), PFunctor.M.Agree' 0 x y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.PullbackCone.pasteVert.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁}
  (t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁) {i₂ : t₁.pt ⟶ X₂}
  (t₂ t₂_1 : CategoryTheory.Limits.PullbackCone i₂ f₂),
  t₂ = t₂_1 → ∀ (hi₂ : i₂ = t₁.snd), t₁.pasteVert t₂ hi₂ = t₁.pasteVert t₂_1 hi₂
-- Mathlib.FieldTheory.Normal.Defs
normal_self : ∀ (F : Type u_1) [inst : Field F], Normal F F
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- If `e : A ≃+* B` is an isomorphism of rings, then so is `map e`.  -/
MvPolynomial.mapEquiv : {S₁ : Type v} →
  {S₂ : Type w} →
    (σ : Type u_1) →
      [inst : CommSemiring S₁] → [inst_1 : CommSemiring S₂] → S₁ ≃+* S₂ → MvPolynomial σ S₁ ≃+* MvPolynomial σ S₂
-- Lean.Meta.Basic
/-- Given `e` of the form `∀ (p₁ : P₁) … (p₁ : P₁), B[p_1,…,p_n]` and `arg₁ : P₁, …, argₙ : Pₙ`, returns
* the names `p₁, …, pₙ`,
* the binder infos,
* the binder types `P₁, P₂[arg₁], …, P[arg₁,…,argₙ₋₁]`, and
* the type `B[arg₁,…,argₙ]`.

It uses `whnf` to reduce `e` if it is not a forall.

See also `Lean.Meta.instantiateForall`.
 -/
Lean.Meta.instantiateForallWithParamInfos : Lean.Expr → Array Lean.Expr → optParam Bool false → Lean.MetaM (Array Lean.Meta.ExprParamInfo × Lean.Expr)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_right_injective₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀}
  [ZeroLEOneClass M₀], 0 < a → a ≠ 1 → Function.Injective fun x => a ^ x
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.type.injEq : ∀ (next next_1 : Mathlib.Tactic.Conv.Path), (next.type = next_1.type) = (next = next_1)
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.selmerGroup.valuation_ker_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ},
  IsDedekindDomain.selmerGroup.valuation.ker = IsDedekindDomain.selmerGroup.subgroupOf IsDedekindDomain.selmerGroup
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.topCharacteristic : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.Characteristic
-- Mathlib.Logic.Equiv.Finset
Encodable.length_sortedUniv : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Encodable α], (Encodable.sortedUniv α).length = Fintype.card α
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.integrable_of_bilin_of_bdd_left : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F} (C : ℝ),
  MeasureTheory.AEStronglyMeasurable f μ →
    (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C) → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.inv.sizeOf_spec : ∀ {R : Type u} [inst : SizeOf R] (a : Rack.PreEnvelGroup R), sizeOf a.inv = 1 + sizeOf a
-- Init.Data.Range.Polymorphic.Char
Char.instLeast? : Std.PRange.Least? Char
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.sup_spanningCoe : ∀ {V : Type u} {G : SimpleGraph V} (H H' : G.Subgraph), (H ⊔ H').spanningCoe = H.spanningCoe ⊔ H'.spanningCoe
-- Mathlib.RingTheory.Derivation.Lie
Derivation.compAlgebraMapL.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : AddCommMonoid M] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Module A M] [inst_7 : Module B M] [inst_8 : Module R M] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] [inst_11 : IsScalarTower A B M] [inst_12 : IsScalarTower R B M],
  Derivation.compAlgebraMapL R A B M = Derivation.compAlgebraMapL R A B M
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `S` is finite and `IsCyclotomicExtension S K A`, then `finiteDimensional K A`.  -/
IsCyclotomicExtension.finiteDimensional : ∀ (S : Set ℕ) (K : Type w) [inst : Field K] (C : Type z) [Finite ↑S] [inst_2 : CommRing C] [inst_3 : Algebra K C]
  [IsDomain C] [IsCyclotomicExtension S K C], FiniteDimensional K C
-- Lean.Meta.Tactic.Backtrack
/-- Pretty print a list of goals.
 -/
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.ppMVarId : Lean.MVarId → Lean.MetaM Std.Format
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_inv_left : ∀ {G : Type u_1} [inst : Group G] (a b : G), ⁅a⁻¹, b⁆ = a⁻¹ * ⁅b, a⁆ * a
-- Mathlib.RingTheory.RingInvo
RingInvo.instCoeOutRingEquivMulOpposite : {R : Type u_2} → [inst : Semiring R] → CoeOut (RingInvo R) (R ≃+* Rᵐᵒᵖ)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_eq_self_of_le : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a : Ordinal.{u}},
  Order.IsNormal f → o₁ ≤ o₂ → Ordinal.veblenWith f o₂ a = a → Ordinal.veblenWith f o₁ a = a
-- Mathlib.Analysis.Calculus.TangentCone.Pi
/-- The product of a family of sets of unique differentiability is a set of unique
differentiability.  -/
UniqueDiffOn.univ_pi : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [inst_3 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)]
  [∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] {s : (i : ι) → Set (E i)},
  (∀ (i : ι), UniqueDiffOn 𝕜 (s i)) → UniqueDiffOn 𝕜 (Set.univ.pi s)
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- `annIdealGenerator 𝕜 a` is the monic generator of `annIdeal 𝕜 a`
if one exists, otherwise `0`.

Since `𝕜[X]` is a principal ideal domain there is a polynomial `g` such that
`span 𝕜 {g} = annIdeal a`. This picks some generator.
We prefer the monic generator of the ideal.  -/
Polynomial.annIdealGenerator : (𝕜 : Type u_1) → {A : Type u_2} → [inst : Field 𝕜] → [inst_1 : Ring A] → [Algebra 𝕜 A] → A → Polynomial 𝕜
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.snd_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C),
  (StarAlgHom.snd R B C).comp (f.prod g) = g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List ((a : α) × β a)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l →
        ∀ {h' : k' ∈ Std.ExtDTreeMap.ofList l cmp}, (Std.ExtDTreeMap.ofList l cmp).getKey k' h' = k
-- Mathlib.Data.Nat.Fib.Basic
Nat.fastFibAux_eq : ∀ (n : ℕ), n.fastFibAux = (Nat.fib n, Nat.fib (n + 1))
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.algebraMap_exp_comm_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CharZero 𝕂] [CompleteSpace 𝕂],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝕂).radius,
    (algebraMap 𝕂 𝔸) (NormedSpace.exp x) = NormedSpace.exp ((algebraMap 𝕂 𝔸) x)
-- Mathlib.Data.Part
Part.instAppend : {α : Type u_1} → [Append α] → Append (Part α)
-- Mathlib.Data.Finmap
/-- Lift a permutation-respecting function on 2 `AList`s to 2 `Finmap`s.  -/
Finmap.liftOn₂ : {α : Type u} →
  {β : α → Type v} →
    {γ : Type u_1} →
      Finmap β →
        Finmap β →
          (f : AList β → AList β → γ) →
            (∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries.Perm a₂.entries → b₁.entries.Perm b₂.entries → f a₁ b₁ = f a₂ b₂) → γ
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The identity transformation induces the identity endofunctor on the category of algebras.  -/
CategoryTheory.Endofunctor.Algebra.functorOfNatTransId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      CategoryTheory.Endofunctor.Algebra.functorOfNatTrans (CategoryTheory.CategoryStruct.id F) ≅
        CategoryTheory.Functor.id (CategoryTheory.Endofunctor.Algebra F)
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_eq_utf8ByteSize_beq_zero : ∀ {s : String}, s.isEmpty = (s.utf8ByteSize == 0)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : k' ∈ Std.DTreeMap.Raw.Const.ofList l cmp}, (Std.DTreeMap.Raw.Const.ofList l cmp).getKey k' h' = k
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.coe_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), ↑p.support = {u} + ↑p.support.tail
-- Mathlib.Data.List.Chain
List.IsChain.iff_of_mem_imp : ∀ {α : Type u_1} {R S : α → α → Prop} {l : List α},
  (∀ (a b : α), a ∈ l → b ∈ l → (R a b ↔ S a b)) → (List.IsChain R l ↔ List.IsChain S l)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOn.inv` -/
TendstoUniformlyOn.fun_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {g : β → α} {s : Set β},
  TendstoUniformlyOn f g l s → TendstoUniformlyOn (fun i i_1 => (f i i_1)⁻¹) (fun i => (g i)⁻¹) l s
-- Aesop.Options.Public
/-- Maximum total number of goals in the search tree. When this limit is exceeded,
the search ends. 0 means no limit.
 -/
Aesop.Options.maxGoals : Aesop.Options → ℕ
-- Init.Data.List.MinMax
_private.Init.Data.List.MinMax.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_exists : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E],
  ∃ u,
    ContDiff ℝ (↑⊤) u ∧ (∀ (x : E), u x ∈ Set.Icc 0 1) ∧ Function.support u = Metric.ball 0 1 ∧ ∀ (x : E), u (-x) = u x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
AEMeasurable.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] {_m : MeasurableSpace α} (f : α → β)
  (μ : MeasureTheory.Measure α), AEMeasurable f μ = ∃ g, Measurable g ∧ f =ᵐ[μ] g
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a covering of `X` by compact subsets,
`α` a uniform space, `F : ι → (X → α)` a family equicontinuous on each `K ∈ 𝔖`, and `ℱ` a filter
on `ι`. Then, `F` tends to `f : X → α` along `ℱ` *uniformly on each `K ∈ 𝔖`* iff it tends to `f`
*pointwise* along `ℱ`.

This is a specialization of `EquicontinuousOn.tendsto_uniformOnFun_iff_pi'` to the case
where `𝔖` covers `X`.  -/
EquicontinuousOn.tendsto_uniformOnFun_iff_pi : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    ⋃₀ 𝔖 = Set.univ →
      (∀ K ∈ 𝔖, EquicontinuousOn F K) →
        ∀ (ℱ : Filter ι) (f : X → α),
          Filter.Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (nhds ((UniformOnFun.ofFun 𝔖) f)) ↔ Filter.Tendsto F ℱ (nhds f)
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.card_le_card_mul_self₀ : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : DecidableEq α] {s : Finset α} [IsLeftCancelMulZero α],
  s.card ≤ (s * s).card
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.head_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl).head = some (exp, coef)
-- Mathlib.Order.Interval.Set.Defs
/-- `s : Set α` is `OrdConnected` if for all `x y ∈ s` it includes the interval `[[x, y]]`.  -/
Set.OrdConnected.out' : ∀ {α : Type u_1} {inst : Preorder α} {s : Set α} [self : s.OrdConnected] ⦃x : α⦄,
  x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s
-- Mathlib.Combinatorics.Colex
Finset.Colex.ofColex_bot : ∀ {α : Type u_1} [inst : PartialOrder α], ofColex ⊥ = ∅
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.insert.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (t : RBTree.RBNode α) (v : α),
  RBTree.RBNode.insert cmp t v =
    match t.isRed with
    | RBTree.RBColor.red => (RBTree.RBNode.ins cmp v t).setBlack
    | RBTree.RBColor.black => RBTree.RBNode.ins cmp v t
-- Mathlib.Order.Bounds.Basic
/-- If `a` is the greatest element of `s` and `b` is the greatest element of `t`,
then `max a b` is the greatest element of `s ∪ t`.  -/
IsGreatest.union : ∀ {γ : Type u_3} [inst : LinearOrder γ] {a b : γ} {s t : Set γ},
  IsGreatest s a → IsGreatest t b → IsGreatest (s ∪ t) (max a b)
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.BundledIterM.Equiv.congr_simp : ∀ (m : Type w → Type w') (β : Type w) [inst : Monad m] [inst_1 : LawfulMonad m] (ita ita_1 : Std.BundledIterM m β),
  ita = ita_1 →
    ∀ (itb itb_1 : Std.BundledIterM m β),
      itb = itb_1 → Std.BundledIterM.Equiv m β ita itb = Std.BundledIterM.Equiv m β ita_1 itb_1
-- Mathlib.Analysis.Normed.Module.Basic
/-- This is a shortcut instance, which was found to help with performance in
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Normed.20modules/near/516757412.

It is implied via `NormedSpace.toNormSMulClass`.  -/
NormedSpace.toIsBoundedSMul : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E],
  IsBoundedSMul 𝕜 E
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.nonsingularLift_negMap : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : WeierstrassCurve.Jacobian.PointClass F},
  W.NonsingularLift P → W.NonsingularLift (W.negMap P)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k =
        f (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_surjective : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (z : N), ∃ x y, f.mk' x y = z
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList_iter : ∀ {α : Type u_1} {β : α → Type u_2} {z : Std.DTreeMap.Internal.Zipper α β}, z.iter.toList = z.toList
-- Mathlib.Order.Lattice
sup_le_sup_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → ∀ (c : α), a ⊔ c ≤ b ⊔ c
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.Result.rfl.sizeOf_spec : sizeOf Lean.Meta.MonadSimp.Result.rfl = 1
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonNat : Lean.FromJson ℕ
-- Init.Data.Array.Lemmas
Array.all_eq_true : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.all p = true ↔ ∀ (i : ℕ) (x : i < as.size), p as[i] = true
-- Mathlib.RingTheory.LocalRing.Module
/-- Given `M₁ → M₂ → M₃ → 0` and `N₁ → N₂ → N₃ → 0`,
if `M₁ ⊗ N₃ → M₂ ⊗ N₃` and `M₂ ⊗ N₁ → M₂ ⊗ N₂` are both injective,
then `M₃ ⊗ N₁ → M₃ ⊗ N₂` is also injective.
 -/
lTensor_injective_of_exact_of_exact_of_rTensor_injective : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N₁ : Type u_8} {N₂ : Type u_9}
  {N₃ : Type u_10} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  {f₁ : M₁ →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {g₁ : N₁ →ₗ[R] N₂} {g₂ : N₂ →ₗ[R] N₃},
  Function.Exact ⇑f₁ ⇑f₂ →
    Function.Surjective ⇑f₂ →
      Function.Exact ⇑g₁ ⇑g₂ →
        Function.Surjective ⇑g₂ →
          Function.Injective ⇑(LinearMap.rTensor N₃ f₁) →
            Function.Injective ⇑(LinearMap.lTensor M₂ g₁) → Function.Injective ⇑(LinearMap.lTensor M₃ g₁)
-- Mathlib.Logic.Small.Set
small_sep : ∀ {α : Type u1} (s : Set α) (P : α → Prop) [Small.{u, u1} ↑s], Small.{u, u1} ↑{x | x ∈ s ∧ P x}
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_prod_of_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R}
  {s : Finset ι},
  (∀ i ∈ s, m.leadingCoeff (P i) ∈ nonZeroDivisors R) → m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_fun_add : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f → μ.Integrable g → ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]