mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.NormalExpr.brecOn.eq : ∀ {motive : Mathlib.Tactic.BicategoryLike.NormalExpr → Sort u} (t : Mathlib.Tactic.BicategoryLike.NormalExpr)
  (F_1 : (t : Mathlib.Tactic.BicategoryLike.NormalExpr) → Mathlib.Tactic.BicategoryLike.NormalExpr.below t → motive t),
  Mathlib.Tactic.BicategoryLike.NormalExpr.brecOn t F_1 =
    F_1 t (Mathlib.Tactic.BicategoryLike.NormalExpr.brecOn.go t F_1).2
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumClique.maximum : ∀ {α : Type u_3} [inst : Finite α] {G : SimpleGraph α} {s : Finset α},
  G.IsMaximumClique s → ∀ (t : Finset α), G.IsClique ↑t → t.card ≤ s.card
-- Mathlib.Data.Seq.Basic
Stream'.Seq.terminates_ofList : ∀ {α : Type u} (l : List α), (↑l).Terminates
-- Std.Http.Data.Headers
/-- Inserts a new key with an array of values.
 -/
Std.Http.Headers.insertMany : Std.Http.Headers → Std.Http.Header.Name → Array Std.Http.Header.Value → Std.Http.Headers
-- Mathlib.Topology.LocallyFinsupp
/-- If `X` is T1 and if `U` is closed, then the support of support of a function with locally finite
support within `U` is also closed.
 -/
Function.locallyFinsuppWithin.closedSupport : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [T1Space X] [inst_2 : Zero Y]
  (D : Function.locallyFinsuppWithin U Y), IsClosed U → IsClosed D.support
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mk_hom_eq_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T), (CategoryTheory.CostructuredArrow.mk f).hom = f
-- Mathlib.Algebra.Group.Basic
sub_eq_add_zero_sub : ∀ {G : Type u_3} [inst : SubNegMonoid G] (a b : G), a - b = a + (0 - b)
-- Lean.MonadEnv
/-- Matches if `e` is a constant that is a non-recursive inductive type with no indices and with one constructor.
Such a type satisfies `Lean.isNonRecStructure`.
See also `Lean.matchConstStructure` for a less restrictive version.
 -/
Lean.matchConstNonRecStructure : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [Lean.MonadEnv m] →
        [Lean.MonadError m] →
          Lean.Expr → (Unit → m α) → (Lean.InductiveVal → List Lean.Level → Lean.ConstructorVal → m α) → m α
-- Mathlib.Order.SupIndep
iSupIndep.comp' : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ι → α} {f : ι' → ι},
  iSupIndep (t ∘ f) → Function.Surjective f → iSupIndep t
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsIrreducible s ↔ (PrimeSpectrum.vanishingIdeal s).IsPrime
-- Mathlib.RingTheory.Multiplicity
emultiplicity_map_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] {F : Type u_3} [inst_2 : EquivLike F α β]
  [MulEquivClass F α β] (f : F) {a b : α}, emultiplicity (f a) (f b) = emultiplicity a b
-- Mathlib.Order.Bounds.Basic
bddAbove_preimage_toDual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set αᵒᵈ}, BddAbove (⇑OrderDual.toDual ⁻¹' s) ↔ BddBelow s
-- Mathlib.Data.ENNReal.Inv
ENNReal.le_of_forall_nnreal_lt : ∀ {x y : ENNReal}, (∀ (r : NNReal), ↑r < x → ↑r ≤ y) → x ≤ y
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.unsortedEigenvectorBasis : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {T : E →ₗ[𝕜] E} →
            [FiniteDimensional 𝕜 E] → {n : ℕ} → T.IsSymmetric → Module.finrank 𝕜 E = n → OrthonormalBasis (Fin n) 𝕜 E
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_ofNat : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Algebra ℝ A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] (n : ℕ)
  [inst_11 : n.AtLeastTwo], CFC.abs (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_uIoo_val : ∀ {n : ℕ} (i j : Fin n), Fin.val ⁻¹' Set.uIoo ↑i ↑j = Set.uIoo i j
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.coe_toLieSubalgebra : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  ↑(LieIdeal.toLieSubalgebra R L I) = ↑I
-- Init.Data.UInt.Bitwise
instAssociativeUInt64HXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instNegHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → Neg (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneBack_obj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (t : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)),
  (CategoryTheory.WithTerminal.coneBack✝.obj t).pt = CategoryTheory.Over.mk (t.π.app CategoryTheory.WithTerminal.star)
-- Lean.Meta.Tactic.Grind.Types
/-- Context for `GrindM` monad.  -/
Lean.Meta.Grind.Context : Type
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.getKey?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α},
  m.getKey? a = Std.DHashMap.Internal.Raw₀.getKey? ⟨m, ⋯⟩ a
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.utf8GetAux.match_1.splitter : (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) →
  (x : List Char) →
    (x_1 x_2 : String.Pos.Raw) →
      ((x x_3 : String.Pos.Raw) → motive [] x x_3) →
        ((c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p) → motive x x_1 x_2
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The positive cone of an ordered module is always pointed.  -/
ConvexCone.pointed_positive : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : PartialOrder M] [inst_4 : IsOrderedAddMonoid M] [inst_5 : Module R M] [inst_6 : PosSMulMono R M],
  (ConvexCone.positive R M).Pointed
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRel.eq_def : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (g n))) (fr : (n : ℕ) → L.Relations n → L'.Relations n)
  (h : (n : ℕ) → L'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) (x : ℕ) (x_1 : L.BoundedFormula α x),
  FirstOrder.Language.BoundedFormula.mapTermRel ft fr h x_1 =
    match x, x_1 with
    | _n, FirstOrder.Language.BoundedFormula.falsum => FirstOrder.Language.BoundedFormula.falsum
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ =>
      FirstOrder.Language.BoundedFormula.equal (ft _n t₁) (ft _n t₂)
    | _n, FirstOrder.Language.BoundedFormula.rel R ts =>
      FirstOrder.Language.BoundedFormula.rel (fr l R) fun i => ft _n (ts i)
    | _n, φ₁.imp φ₂ =>
      (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h φ₁).imp
        (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h φ₂)
    | n, φ.all => (h n (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h φ)).all
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.biprodIsoProd_inv_comp_snd_apply : ∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R) (x : ↑M × ↑N),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.snd)
      ((CategoryTheory.ConcreteCategory.hom (M.biprodIsoProd N).inv) x) =
    x.2
-- Mathlib.Tactic.Translate.Core
/-- The `insert_cast`/`insert_cast_fun` attributes create an abstraction boundary for the tagged
constant when translating it. For example, `Set.Icc`, `Monotone`, `DecidableLT`, `WCovBy` are all
morally self-dual, but their definition is not self-dual. So, in order to allow these constants
to be self-dual, we need to not unfold their definition in the proof term that we translate.  -/
Mathlib.Tactic.Translate.TranslateData.unfoldBoundaries? : Mathlib.Tactic.Translate.TranslateData → Option Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedQuery : Inhabited Std.Http.URI.Query
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for shift left on `BitVec`.  -/
BitVec.reduceHShiftLeft : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.MetricSpace.Lipschitz
LocallyLipschitz.const_min : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → ℝ},
  LocallyLipschitz f → ∀ (a : ℝ), LocallyLipschitz fun x => min a (f x)
-- Lean.Elab.Util
Lean.Elab.liftMacroM : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [Lean.Elab.MonadMacroAdapter m] →
        [Lean.MonadEnv m] →
          [Lean.MonadRecDepth m] →
            [Lean.MonadError m] →
              [Lean.MonadResolveName m] →
                [Lean.MonadTrace m] →
                  [Lean.MonadOptions m] → [Lean.AddMessageContext m] → [MonadLiftT IO m] → Lean.MacroM α → m α
-- Init.Data.Array.MinMax
Array.le_min?_iff : ∀ {α : Type u_1} {a : α} [inst : Min α] [inst_1 : LE α] [Std.LawfulOrderInf α] {xs : Array α},
  xs.min? = some a → ∀ {x : α}, x ≤ a ↔ ∀ b ∈ xs, x ≤ b
-- Lean.Util.PPExt
Lean.pp.rawOnError : Lean.Option Bool
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.hasCoeToLax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → Coe (CategoryTheory.Pseudofunctor B C) (CategoryTheory.LaxFunctor B C)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientInfEquivProdNormalQuotient.eq_1 : ∀ {G : Type u} [inst : Group G] (H N : Subgroup G) [hN : N.Normal],
  QuotientGroup.quotientInfEquivProdNormalQuotient H N = QuotientGroup.quotientInfEquivProdNormalizerQuotient H N ⋯
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_intCast_mul_add' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoMod hp (↑m * p + a) b = ↑m * p + toIcoMod hp a b
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.ae_eq_of_smul_dirac : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {P : MeasureTheory.Measure Ω} {c : ENNReal} [MeasurableSingletonClass 𝓧] {x : 𝓧},
  ProbabilityTheory.HasLaw X (c • MeasureTheory.Measure.dirac x) P → X =ᵐ[P] fun x_1 => x
-- Mathlib.Algebra.Homology.Localization
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {ι : Type u_3} {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.CategoryWithHomology C] [inst_5 : CategoryTheory.CategoryWithHomology D]
  [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] [inst_7 : F.Additive] [inst_8 : F.PreservesHomology]
  [inst_9 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_10 : c.QFactorsThroughHomotopy C]
  [inst_11 : c.QFactorsThroughHomotopy D]
  [inst_12 : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)]
  (K : HomologicalComplex C c) {Z : HomologicalComplexUpToQuasiIso D c}
  (h :
    HomologicalComplexUpToQuasiIso.Qh.obj ((F.mapHomotopyCategory c).obj ((HomotopyCategory.quotient C c).obj K)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K)) h =
    CategoryTheory.CategoryStruct.comp
      ((F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K))
      (CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K)
        (CategoryTheory.CategoryStruct.comp
          ((HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K))
          (CategoryTheory.CategoryStruct.comp
            (HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)) h)))
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.coe_of : ∀ (V : Type u) [inst : SeminormedAddCommGroup V], { carrier := V, str := inst }.carrier = V
-- Mathlib.Algebra.Group.Basic
sub_add_sub_cancel : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a - b + (b - c) = a - c
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.ofLinearEquiv.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsAdicComplete I M], AdicCompletion.ofLinearEquiv I M = LinearEquiv.ofBijective (AdicCompletion.of I M) ⋯
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimension : ∀ {n : ℕ} {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] [Finite ι] (P : Algebra.SubmersivePresentation R S ι σ),
  P.dimension = n → Algebra.IsStandardSmoothOfRelativeDimension n R S
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMap.toNNReal_algebraMap : ∀ {X : Type u_1} [inst : TopologicalSpace X] (r : NNReal),
  ((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = (algebraMap NNReal C(X, NNReal)) r
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The application of this functor to an object  -/
CategoryTheory.EnrichedFunctor.obj : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} → [inst_3 : CategoryTheory.EnrichedCategory V D] → CategoryTheory.EnrichedFunctor V C D → C → D
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {n : ℕ} (f : 𝕜 → 𝕜') (c : 𝕜'),
  iteratedDeriv n (fun x => f x / c) x = iteratedDeriv n f x / c
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
/-- map operation defined on a vector of functors  -/
MvQPF.Comp.map' : {n m : ℕ} →
  {G : Fin2 n → TypeVec.{u} m → Type u} →
    {α β : TypeVec.{u} m} → α.Arrow β → [(i : Fin2 n) → MvFunctor (G i)] → TypeVec.Arrow (fun i => G i α) fun i => G i β
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.measure_eq_top_of_setLIntegral_ne_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α},
  AEMeasurable f (μ.restrict s) → ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤ → μ {x | x ∈ s ∧ f x = ⊤} = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).contains k = true
-- Init.System.IO
/-- Handles any exception that might be thrown by an `EIO ε` action, transforming it into an
exception-free `BaseIO` action.
 -/
EIO.catchExceptions : {ε α : Type} → EIO ε α → (ε → BaseIO α) → BaseIO α
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The forgetful functor from commutative group objects to the ambient category.  -/
CategoryTheory.CommGrp.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Functor (CategoryTheory.CommGrp C) C
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.zero_notMem_range_root : ∀ {ι : 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) [NeZero 2],
  0 ∉ Set.range ⇑P.root
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F)
  {s : Set E}, DifferentiableOn 𝕜 (⇑f) s
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andIntro.inj : ∀ {ak : Mathlib.Tactic.ITauto.AndKind} {p₁ p₂ : Mathlib.Tactic.ITauto.Proof} {ak_1 : Mathlib.Tactic.ITauto.AndKind}
  {p₁_1 p₂_1 : Mathlib.Tactic.ITauto.Proof},
  Mathlib.Tactic.ITauto.Proof.andIntro ak p₁ p₂ = Mathlib.Tactic.ITauto.Proof.andIntro ak_1 p₁_1 p₂_1 →
    ak = ak_1 ∧ p₁ = p₁_1 ∧ p₂ = p₂_1
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isFractional_span_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {s : Set P}, IsFractional S (Submodule.span R s) ↔ ∃ a ∈ S, ∀ b ∈ s, IsLocalization.IsInteger R (a • b)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoCofanPt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C}
  (i : 𝒜),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f i)
      (CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt 𝒜 f).hom =
    (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearMap.coe_toContinuousLinearMap : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F' : Type x}
  [inst_5 : AddCommGroup F'] [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [inst_8 : IsTopologicalAddGroup F']
  [inst_9 : ContinuousSMul 𝕜 F'] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : FiniteDimensional 𝕜 E]
  (f : E →ₗ[𝕜] F'), ↑(LinearMap.toContinuousLinearMap f) = f
-- Lean.Parser.Basic
Lean.Parser.longestMatchFnAux : Option Lean.Syntax → ℕ → ℕ → String.Pos.Raw → ℕ → List (Lean.Parser.Parser × ℕ) → Lean.Parser.ParserFn
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_ne_top : ∀ {a b : ENNReal}, a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.isTerminalΩ₀`.

---

The main non-trivial result: `h.Ω₀` is actually a terminal object.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.isTerminalΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) →
          CategoryTheory.Limits.IsTerminal (CategoryTheory.Subobject.underlying.obj h.Ω₀)
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_zero : ∀ (a : ℤ), a % 0 = a
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem:
For a sequence of Borel probability measures, if the liminf of the measures of any open set is at
least the measure of the open set under a candidate limit measure, then for any set whose
boundary carries no probability mass under the candidate limit measure, then its measures under the
sequence converge to its measure under the candidate limit measure.
 -/
MeasureTheory.tendsto_measure_of_null_frontier : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2}
  {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L) →
    ∀ {E : Set Ω}, μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))
-- Mathlib.Algebra.BigOperators.RingEquiv
RingEquiv.map_sum : ∀ {α : Type u_1} {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] (g : R ≃+* S) (f : α → R) (s : Finset α), g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eval_derivative : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R] [inst_2 : DecidableEq R],
  f.Splits →
    ∀ (x : R),
      Polynomial.eval x (Polynomial.derivative f) =
        f.leadingCoeff *
          (Multiset.map (fun a => (Multiset.map (fun x_1 => x - x_1) (f.roots.erase a)).prod) f.roots).sum
-- Aesop.Tree.Data
Aesop.Goal.lastExpandedInIteration : Aesop.Goal → Aesop.Iteration
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.disjoint_of_disjoint_support : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {H K : Subgroup (Equiv.Perm α)},
  (∀ a ∈ H, ∀ b ∈ K, Disjoint a.support b.support) → Disjoint H K
-- Mathlib.CategoryTheory.Category.Quiv
/-- Composition in the category of quivers equals prefunctor composition.  -/
CategoryTheory.Quiv.comp_eq_comp : ∀ {X Y Z : CategoryTheory.Quiv} (F : X ⟶ Y) (G : Y ⟶ Z), CategoryTheory.CategoryStruct.comp F G = F ⋙q G
-- Mathlib.Data.ZMod.Basic
ZMod.ringHom_map_cast : ∀ {n : ℕ} {R : Type u_1} [inst : NonAssocRing R] (f : R →+* ZMod n) (k : ZMod n), f k.cast = k
-- Mathlib.Algebra.AffineMonoid.Embedding
/-- The dimension of an affine monoid `M`, namely the minimum `n` for which `M` embeds into `ℤⁿ`.  -/
AffineAddMonoid.dim : (M : Type u_1) → [AddCancelCommMonoid M] → ℕ
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.comap : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : β → α),
  l.HasBasis p s → (Filter.comap f l).HasBasis p fun i => f ⁻¹' s i
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.hasColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat)
  [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, v + 1} AddCommGrpCat],
  CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, max u₁ v, max (max (max (v + 1) u) u₁) v₁} (PresheafOfModules R)
-- Mathlib.Algebra.Group.UniqueProds.Basic
instUniqueSumsFinsupp : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddZeroClass G] [UniqueSums G], UniqueSums (ι →₀ G)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true ↔ k ∈ t
-- Lean.Environment
/-- Mapping from constant name to module (index) where constant has been declared.
Recall that a Lean file has a header where previously compiled modules can be imported.
Each imported module has a unique `ModuleIdx`.
Many extensions use the `ModuleIdx` to efficiently retrieve information stored in imported modules.

Remark: this mapping also contains auxiliary constants, created by the code generator, that are **not** in
the field `constants`. These auxiliary constants are invisible to the Lean kernel and elaborator.
Only the code generator uses them.
 -/
Lean.Environment.const2ModIdx : Lean.Environment → Std.HashMap Lean.Name Lean.ModuleIdx
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_eq_self_iff_mem : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ↑⌊a⌋ = a ↔ a ∈ Set.range Int.cast
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.disjoint_interior_closedInterior_faceOpposite : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} [inst_5 : NeZero n] (s : Affine.Simplex k P n)
  (i : Fin (n + 1)), Disjoint s.interior (s.faceOpposite i).closedInterior