mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  {f g : α → ENNReal},
  AEMeasurable f μ →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ) → f ≤ᵐ[μ] g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_inv_mul_iff_mul_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, b < a⁻¹ * c ↔ a * b < c
-- Mathlib.Algebra.Order.Module.Defs
smul_le_smul : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [inst_4 : Zero β] [PosSMulMono α β] [SMulPosMono α β],
  a₁ ≤ a₂ → b₁ ≤ b₂ → 0 ≤ a₁ → 0 ≤ b₂ → a₁ • b₁ ≤ a₂ • b₂
-- Init.Data.String.Legacy
/-- Splits a string at each character for which `p` returns `true`.

The characters that satisfy `p` are not included in any of the resulting strings. If multiple
characters in a row satisfy `p`, then the resulting list will contain empty strings.

This is a legacy function. Use `String.split` instead.

Examples:
* `"coffee tea water".split (·.isWhitespace) = ["coffee", "tea", "water"]`
* `"coffee  tea  water".split (·.isWhitespace) = ["coffee", "", "tea", "", "water"]`
* `"fun x =>\n  x + 1\n".split (· == '\n') = ["fun x =>", "  x + 1", ""]`
 -/
String.splitToList : String → (Char → Bool) → List String
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_biSup : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_5} {s : Set ι} {H : ι → Subgroup G},
  (∀ i ∈ s, (H i).Characteristic) → (⨆ i ∈ s, H i).Characteristic
-- Mathlib.Data.FinEnum.Option
/-- This is an arbitrary choice of insertion rank for a default instance.
It keeps the mapping of the existing `α`-inhabitants intact, modulo `Fin.castSucc`.  -/
FinEnum.instFinEnumOptionLast : (α : Type u) → [FinEnum α] → FinEnum (Option α)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
/-- The `j`th entry of `accumulate n m t` is the sum of `t i` over all `i ≥ j`.  -/
Fin.accumulate : (n m : ℕ) → (Fin n → ℕ) →+ Fin m → ℕ
-- Mathlib.Tactic.HigherOrder
/-- `mkComp v e` checks whether `e` is a sequence of nested applications `f (g (h v))`, and if so,
returns the expression `f ∘ g ∘ h`. If `e = v` it returns `id`.  -/
Mathlib.Tactic.mkComp : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- The functoriality of `H.obj G` identifies (through
`Wedge.IsLimit.hom_ext`) with the functoriality on ends induced by
functoriality of `internalHomDiagramFunctor F|>.obj G`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (self : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) {c c' : C} (f : c ⟶ c') (j : C),
  CategoryTheory.CategoryStruct.comp (H.map f) (self.π c' j) =
    CategoryTheory.CategoryStruct.comp (self.π c j)
      ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f)))
-- Mathlib.Algebra.Opposites
MulOpposite.opEquiv_symm_apply : ∀ {α : Type u_1}, ⇑MulOpposite.opEquiv.symm = MulOpposite.unop
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcomp₁_obj_hom_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F))
  (X_1 : C),
  ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).hom.app X_1 =
    CategoryTheory.CategoryStruct.comp (X.left.map (f.app X_1)) (X.hom.app X_1)
-- Mathlib.RepresentationTheory.Character
FDRep.char_one : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Monoid G] (V : FDRep k G),
  V.character 1 = ↑(Module.finrank k ↑V.V)
-- Lean.Meta.Tactic.Grind.Types
/-- `splitSource` to use when internalizing this fact.  -/
Lean.Meta.Grind.NewRawFact.splitSource : Lean.Meta.Grind.NewRawFact → Lean.Meta.Grind.SplitSource
-- Mathlib.Data.Nat.Choose.Multinomial
/-- Positivity extension for `Multiset.multinomial`.
 -/
Multiset.evalMultinomial : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.eq_maximalIdeal_iff_under_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [hI : I.IsPrime] {J : Ideal (Localization.AtPrime I)},
  Ideal.under R J = I ↔ J = IsLocalRing.maximalIdeal (Localization.AtPrime I)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.prod_coe : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {s : Multiset { a // Irreducible a }},
  Associates.FactorSet.prod ↑s = (Multiset.map Subtype.val s).prod
-- Mathlib.Topology.Separation.Basic
Inseparable.eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {x y : X}, Inseparable x y → x = y
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.collectedBasis_mem : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2}
  (v : (i : ι) → Module.Basis (α i) R ↥(A i)) (a : (i : ι) × α i), (h.collectedBasis v) a ∈ A a.fst
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.resize : Lean.PArray ℚ → ℕ → Lean.PArray ℚ
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
Irreducible.maximalIdeal_eq_setOfPred_le_v_coe : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)
  [inst_2 : IsDiscreteValuationRing ↥v.integer] {ϖ : ↥v.integer},
  Irreducible ϖ → ↑(IsLocalRing.maximalIdeal ↥v.integer) = {y | v ↑y ≤ v ↑ϖ}
-- Std.Sync.Broadcast
/-- Subscribes a new `Receiver` in the `Bounded` channel.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.subscribe : {α : Type} → Std.Bounded✝ α → IO (Std.Bounded.Receiver✝ α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- `log x` is bounded above by a multiple of every power of `x` with positive exponent.  -/
Real.log_le_rpow_div : ∀ {x ε : ℝ}, 0 ≤ x → 0 < ε → Real.log x ≤ x ^ ε / ε
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey?.bind t.getKey? = t.minKey?
-- Mathlib.CategoryTheory.EpiMono
/-- The retraction of a split monomorphism has an obvious section.  -/
CategoryTheory.SplitMono.splitEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : Y ⟶ X} → (se : CategoryTheory.SplitMono f) → CategoryTheory.SplitEpi se.retraction
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_zero : ∀ (n : ℤ), n <<< 0 = n
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_zero : Nat.sqrt 0 = 0
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
as `multiplicity p.asIdeal I`.  -/
IsDedekindDomain.HeightOneSpectrum.factorization_eq_multiplicity : ∀ {R : Type u_3} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ ⊥ → ∀ (p : IsDedekindDomain.HeightOneSpectrum R), (factorization I) p.asIdeal = multiplicity p.asIdeal I
-- Init.Data.Float.Float32
/-- Computes the arc sine (inverse sine) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`asinf`.
 -/
Float32.asin : Float32 → Float32
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainTopCoeff_zero_right : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) [inst_8 : Nontrivial L],
  α.IsNonZero → LieModule.chainTopCoeff (⇑α) 0 = 1
-- Mathlib.Data.Set.Image
Set.preimage_ofPred_eq : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : β → α}, f ⁻¹' {a | p a} = {a | p (f a)}
-- Init.Data.List.Attach
List.pmap_eq_self : ∀ {α : Type u_1} {l : List α} {p : α → Prop} {hp : ∀ a ∈ l, p a} {f : (a : α) → p a → α},
  List.pmap f l hp = l ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a
-- Lean.Elab.Binders
/-- Auxiliary functions for converting `id_1 ... id_n` application into `#[id_1, ..., id_m]`
It is used at `expandFunBinders`.  -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.getFunBinderIds? : Lean.Syntax → OptionT Lean.MacroM (Array Lean.Syntax)
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.add_neg_cancel : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → a + b + -a = b
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.Even.gammaFactor_def : ∀ {N : ℕ} {χ : DirichletCharacter ℂ N}, χ.Even → ∀ (s : ℂ), χ.gammaFactor s = s.Gammaℝ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Hover.mk : Lean.Lsp.MarkupContent → Option Lean.Lsp.Range → Lean.Lsp.Hover
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.addSimproc : Lean.Meta.Simprocs → Lean.CoreM Lean.Meta.Simprocs
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₂'_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₂'.g = S.L₃.f
-- Lean.Elab.Tactic.Grind.Param
/-- Returns `true` if we should keep the theorem when `only` is used.
We keep
1- Local theorems. We use anchors to restrict their instantiation.
2- `match`-equations. They are always active.
 -/
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.Grind.shouldKeep : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.GrindM Bool
-- Init.PropLemmas
Decidable.or_iff_not_imp_right : ∀ {b a : Prop} [Decidable b], a ∨ b ↔ ¬b → a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.triangle : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''},
  CategoryTheory.CategoryStruct.comp (ψ.associator (CategoryTheory.Limits.CatCospanTransform.id F' G') φ).hom
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom) =
    CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ
-- Mathlib.FieldTheory.Tower
/-- **Alias** of `Module.Finite.left`.

---

In a tower of field extensions `A / K / F`, if `A / F` is finite, so is `K / F`.

(In fact, it suffices that `A` is a nontrivial ring.)

Note this cannot be an instance as Lean cannot infer `A`.
 -/
FiniteDimensional.left : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Ring F] [inst_1 : Ring K] [inst_2 : Module F K]
  [inst_3 : AddCommGroup A] [inst_4 : Module K A] [Module.IsTorsionFree K A] [inst_6 : Module F A] [IsNoetherian F A]
  [IsScalarTower F K A] [IsDomain K] [Nontrivial A], Module.Finite F K
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsLocallyFiniteMeasure.finiteAtNhds : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {inst : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : MeasureTheory.IsLocallyFiniteMeasure μ] (x : α), μ.FiniteAtFilter (nhds x)
-- Mathlib.Analysis.Asymptotics.Defs
/-- The Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is
a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by a constant multiple of `‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided
by this definition.  -/
Asymptotics.«term_=O[_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Int.Cast.Basic
Int.cast_zero : ∀ {R : Type u} [inst : AddGroupWithOne R], ↑0 = 0
-- Mathlib.CategoryTheory.Localization.Bifunctor
/-- Classes of morphisms `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂` are said
to be inverted by `F : C₁ ⥤ C₂ ⥤ E` if `W₁.prod W₂` is inverted by
the functor `uncurry.obj F : C₁ × C₂ ⥤ E`.  -/
CategoryTheory.MorphismProperty.IsInvertedBy₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {E : Type u_5} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} E] →
            CategoryTheory.MorphismProperty C₁ →
              CategoryTheory.MorphismProperty C₂ → CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E) → Prop
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i j : D.J),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.f i j)
-- Mathlib.Dynamics.FixedPoints.Basic
Function.IsFixedPt.equiv_symm_iff : ∀ {α : Type u_1} {x : α} {e : Equiv.Perm α}, Function.IsFixedPt (⇑(Equiv.symm e)) x ↔ Function.IsFixedPt (⇑e) x
-- Mathlib.LinearAlgebra.LeftExact
LinearMap.exact_lcomp_of_exact_of_surjective : ∀ {R : Type u_1} [inst : CommRing R] {M1 : Type u_2} {M2 : Type u_3} {M3 : Type u_4} (N : Type u_5)
  [inst_1 : AddCommGroup M1] [inst_2 : AddCommGroup M2] [inst_3 : AddCommGroup M3] [inst_4 : AddCommGroup N]
  [inst_5 : Module R M1] [inst_6 : Module R M2] [inst_7 : Module R M3] [inst_8 : Module R N] {f : M1 →ₗ[R] M2}
  {g : M2 →ₗ[R] M3},
  Function.Exact ⇑f ⇑g → Function.Surjective ⇑g → Function.Exact ⇑(LinearMap.lcomp R N g) ⇑(LinearMap.lcomp R N f)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommComon C} {f g : A ⟶ B},
  f = g ↔ f.hom.hom = g.hom.hom
-- Init.Data.String.Basic
String.Slice.Pos.sliceFrom_inj : ∀ {s : String.Slice} {p₀ pos pos' : s.Pos} {h : p₀ ≤ pos} {h' : p₀ ≤ pos'},
  p₀.sliceFrom pos h = p₀.sliceFrom pos' h' ↔ pos = pos'
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_bot : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}, f =Θ[⊥] g
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.mkEMatchTheoremWithKind?.collect : Lean.Expr →
  Lean.Meta.Grind.SymbolPriorities →
    Bool → Bool → Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Option (List Lean.Expr × List Lean.HeadIndex))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_some_getD_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β},
  m.contains a = true → Std.ExtDHashMap.Const.get? m a = some (Std.ExtDHashMap.Const.getD m a fallback)
-- Mathlib.Order.Interval.Finset.Nat
Finset.range_image_pred_top_sub : ∀ (n : ℕ), Finset.image (fun j => n - 1 - j) (Finset.range n) = Finset.range n
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.map_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β} {g : β → γ},
  UniformContinuous f →
    UniformContinuous g → SeparationQuotient.map g ∘ SeparationQuotient.map f = SeparationQuotient.map (g ∘ f)
-- Mathlib.Algebra.Free
FreeAddSemigroup.traverse_add : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) [LawfulApplicative m]
  (x y : FreeAddSemigroup α), traverse F (x + y) = (fun x1 x2 => x1 + x2) <$> traverse F x <*> traverse F y
-- Lean.Parser.Do
Lean.Parser.Term.doUnless.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.ExtendFrom
/-- If a function `f` to a T₃ space `Y` has a limit within a
dense set `A` for any `x`, then `extendFrom A f` is continuous.  -/
continuous_extendFrom : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [RegularSpace Y] {f : X → Y}
  {A : Set X}, Dense A → (∀ (x : X), ∃ y, Filter.Tendsto f (nhdsWithin x A) (nhds y)) → Continuous (extendFrom A f)
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.filteredClosure.below : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] →
      {α : Type w} →
        {f : α → C} →
          {motive : (a : C) → CategoryTheory.IsFiltered.filteredClosure f a → Prop} →
            {a : C} → CategoryTheory.IsFiltered.filteredClosure f a → Prop
-- Mathlib.NumberTheory.Chebyshev
Nat.primeFactors_lcmUpto : ∀ (n : ℕ), n.lcmUpto.primeFactors = n.primesLE
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqAlt : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Alt pu → Lean.Compiler.LCNF.Alt pu → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.ext_iff : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  {x y : f.Homotopy g}, x = y ↔ x.h = y.h
-- Mathlib.Analysis.Calculus.LocalExtr.Rolle
/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has derivative `f'`
on `(a, b)` and has the same limit `l` at `𝓝[>] a` and `𝓝[<] b`, then `f' c = 0`
for some `c ∈ (a, b)`.  -/
exists_hasDerivAt_eq_zero' : ∀ {f f' : ℝ → ℝ} {a b l : ℝ},
  a < b →
    Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
      Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l) →
        (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) → ∃ c ∈ Set.Ioo a b, f' c = 0
-- Init.Data.Int.Order
Int.sub_lt_iff : ∀ {a b c : ℤ}, a - b < c ↔ a < c + b
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.instReprLabel : Repr Lean.Meta.NormCast.Label
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- The natural equivalence `(E × E₂) × E₃ ≃ E × (E₂ × E₃)` is a linear isometry.  -/
LinearIsometryEquiv.prodAssoc : (R : Type u_1) →
  (E : Type u_5) →
    (E₂ : Type u_6) →
      (E₃ : Type u_7) →
        [inst : Semiring R] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : SeminormedAddCommGroup E₂] →
              [inst_3 : SeminormedAddCommGroup E₃] →
                [inst_4 : Module R E] →
                  [inst_5 : Module R E₂] → [inst_6 : Module R E₃] → (E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_left_le_mk_sub_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a ≤ ArchimedeanClass.mk (a - b) ↔ ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k a : α},
  Std.DHashMap.Const.get! (m.erase k) a = if (k == a) = true then default else Std.DHashMap.Const.get! m a
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_induction_on : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} {C : R → Prop} {r : R},
  r ∈ M * N → (∀ m ∈ M, ∀ n ∈ N, C (m * n)) → (∀ (x y : R), C x → C y → C (x + y)) → C r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {a : α} {b : β a}, (Std.DTreeMap.Internal.Impl.insert! a b t).getKey! a = a
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.needMoreData.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (size : Option ℕ),
  sizeOf (Std.Http.Protocol.H1.Event.needMoreData size) = 1 + sizeOf size
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mapDomain_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} {f : G → G'} {a : G} {b : k},
  (SkewMonoidAlgebra.mapDomain f) (SkewMonoidAlgebra.single a b) = SkewMonoidAlgebra.single (f a) b
-- Init.Data.UInt.Lemmas
UInt8.toNat_one : UInt8.toNat 1 = 1
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_eq_getD_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {a : α}, m.get! a = m.getD a default
-- Mathlib.Algebra.Lie.Ideal
LieHom.mem_idealRange_iff : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'),
  f.IsIdealMorphism → ∀ {y : L'}, y ∈ f.idealRange ↔ ∃ x, f x = y
-- Init.Data.UInt.Lemmas
UInt64.size_sub_one_mod_uSizeSize : 18446744073709551615 % USize.size = USize.size - 1
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ioi_strictMono : ∀ (α : Type u_1) [inst : Preorder α], StrictMono UpperSet.Ioi
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.getKeyD a fallback = t_1.getKeyD a_1 fallback_1
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.primesOver.isMaximal : ∀ {A : Type u_1} [inst : CommRing A] {p : Ideal A} [p.IsMaximal] {B : Type u_2} [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [Algebra.IsIntegral A B] (Q : ↑(p.primesOver B)), (↑Q).IsMaximal
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.expandNonAtomicDiscrs?.loop : Lean.Syntax → List Lean.Syntax → Array Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.univ : ∀ {α : Type u_2} [inst : LE α], CountableSupClosed Set.univ
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddBelow.range_inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {α : Type u_4} {f : α → G},
  BddBelow (Set.range f) → BddAbove (Set.range fun x => (f x)⁻¹)
-- Mathlib.Order.Minimal
minimal_iff : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : PartialOrder α], Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → y ≤ x → x = y
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- A **Fredholm decomposition** of a topological vector space `E` is the data of two subspaces
`X₀` and `X₁` which are topological complements, and where `X₀` is finite dimensional.

Note that we purposefully use the index `₀` for the "inessential" (i.e. finite dimensional)
part of the decomposition.  -/
FredholmDecomposition : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] → [inst_1 : AddCommGroup E] → [Module 𝕜 E] → [TopologicalSpace E] → Type u_2