mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- A divisibility constraint and its justification/proof.  -/
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr : Type
-- Mathlib.RingTheory.Localization.AtPrime.Extension
/-- For `R ⊆ S` an extension of Dedekind domains and `p` a prime ideal of `R`, the bijection
between the primes of `S` over `p` and the primes over the maximal ideal of `Rₚ` in `Sₚ` where
`Rₚ` and `Sₚ` are resp. the localizations of `R` and `S` at the complement of `p`.
 -/
IsDedekindDomain.primesOverEquivPrimesOver : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            [inst_3 : p.IsPrime] →
              (Rₚ : Type u_3) →
                [inst_4 : CommRing Rₚ] →
                  [inst_5 : Algebra R Rₚ] →
                    [IsLocalization.AtPrime Rₚ p] →
                      [inst_7 : IsLocalRing Rₚ] →
                        (Sₚ : Type u_4) →
                          [inst_8 : CommRing Sₚ] →
                            [inst_9 : Algebra S Sₚ] →
                              [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] →
                                [inst_11 : Algebra Rₚ Sₚ] →
                                  [IsDomain R] →
                                    [IsDedekindDomain S] →
                                      [Module.IsTorsionFree R S] →
                                        [inst_15 : Algebra R Sₚ] →
                                          [IsScalarTower R S Sₚ] →
                                            [IsScalarTower R Rₚ Sₚ] →
                                              p ≠ ⊥ →
                                                ↑(p.primesOver S) ≃o ↑((IsLocalRing.maximalIdeal Rₚ).primesOver Sₚ)
-- Batteries.Data.String.Matcher
/-- Returns all the substrings of `s` that match `pattern`.
 -/
String.findAllSubstr : String → Substring.Raw → Array Substring.Raw
-- Mathlib.Order.Category.BddOrd
_private.Mathlib.Order.Category.BddOrd.0.BddOrd.Hom.mk.inj : ∀ {X Y : BddOrd} {hom' hom'_1 : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Pi.opensMeasurableSpace : ∀ {ι : Type u_6} {X : ι → Type u_7} [Countable ι] [t' : (i : ι) → TopologicalSpace (X i)]
  [inst : (i : ι) → MeasurableSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)]
  [∀ (i : ι), OpensMeasurableSpace (X i)], OpensMeasurableSpace ((i : ι) → X i)
-- Init.Data.SInt.Basic
/-- Obtain the `BitVec` that contains the 2's complement representation of the `Int16`.
 -/
Int16.toBitVec : Int16 → BitVec 16
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_add_ediv_mul : ∀ (a b : ℤ), a % b + a / b * b = a
-- Mathlib.RingTheory.RingHom.FinitePresentation
/-- Being finitely-presented respects isomorphisms.  -/
RingHom.finitePresentation_respectsIso : RingHom.RespectsIso @RingHom.FinitePresentation
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Continuous f → Continuous g → Topology.IsQuotientMap (g ∘ f) → Topology.IsQuotientMap g
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply : ∀ {M : Type u_5} [inst : AddMonoid M] {α : Type u_12} {β : Type u_13} (fg : (α →₀ M) × (β →₀ M)),
  Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg = fg.1.sumElim fg.2
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.evaluation.congr_simp : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens) (x : ↥X) (hx : x ∈ U), X.evaluation U x hx = X.evaluation U x hx
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toPseudofunctor_mapComp : ∀ {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)
  {a b c : CategoryTheory.LocallyDiscrete C} (x : a ⟶ b) (x_1 : b ⟶ c),
  F.toPseudofunctor.mapComp x x_1 =
    match x with
    | { as := f } =>
      match x_1 with
      | { as := g } => CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.Category.AlgCat.Basic
_private.Mathlib.Algebra.Category.AlgCat.Basic.0.AlgCat.mk.inj : ∀ {R : Type u} {inst : CommRing R} {carrier : Type v} {isRing : Ring carrier} {isAlgebra : Algebra R carrier}
  {carrier_1 : Type v} {isRing_1 : Ring carrier_1} {isAlgebra_1 : Algebra R carrier_1},
  { carrier := carrier, isRing := isRing, isAlgebra := isAlgebra } =
      { carrier := carrier_1, isRing := isRing_1, isAlgebra := isAlgebra_1 } →
    carrier = carrier_1 ∧ isRing ≍ isRing_1 ∧ isAlgebra ≍ isAlgebra_1
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_symm_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  {X : Cᵒᵖ} (x : F.obj X) (f : F ⟶ G) {Z : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm x) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.uliftYonedaEquiv.symm
        ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (Opposite.unop X)))) x))
      h
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.eventually_atBot_not_isRoot : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜),
  P ≠ 0 → ∀ᶠ (x : 𝕜) in Filter.atBot, ¬P.IsRoot x
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.codRestrict_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {S : Type u_5} [inst_2 : SetLike S N]
  [inst_3 : SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), f x ∈ s) (n : M), (f.codRestrict s h) n = ⟨f n, ⋯⟩
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt16.toBitVec_ite : ∀ {c : Prop} {t e : UInt16} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.ToTerm.toTerm.go : Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.Analysis.Calculus.FDeriv.Extend
/-- If a function `f` is differentiable in a convex open set and continuous on its closure, and its
derivative converges to a limit `f'` at a point on the boundary, then `f` is differentiable there
with derivative `f'`.  -/
hasFDerivWithinAt_closure_of_tendsto_fderiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {f' : E →L[ℝ] F},
  DifferentiableOn ℝ f s →
    Convex ℝ s →
      IsOpen s →
        (∀ y ∈ closure s, ContinuousWithinAt f s y) →
          Filter.Tendsto (fun y => fderiv ℝ f y) (nhdsWithin x s) (nhds f') → HasFDerivWithinAt f f' (closure s) x
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.sInf_isPrime_of_isChain : ∀ {α : Type u} [inst : Semiring α] {s : Set (Ideal α)},
  s.Nonempty → IsChain (fun x1 x2 => x1 ≤ x2) s → (∀ p ∈ s, p.IsPrime) → (sInf s).IsPrime
-- Mathlib.Topology.Connected.Basic
ContinuousOn.image_connectedComponentIn_subset : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α} {a : α},
  ContinuousOn f s → a ∈ s → f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.chromaticNumber_sum : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W},
  (G ⊕g H).chromaticNumber = max G.chromaticNumber H.chromaticNumber
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_subset_Ioo_right : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₂ ≤ a₁ → Set.Ioo b a₂ ⊆ Set.Ioo b a₁
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Products.evalCons : ∀ {I : Type u_1} [inst : LinearOrder I] {C : Set (I → Bool)} {l : List I} {a : I}
  (hla : List.IsChain (fun x1 x2 => x1 > x2) (a :: l)),
  Profinite.NobelingProof.Products.eval C ⟨a :: l, hla⟩ =
    Profinite.NobelingProof.e C a * Profinite.NobelingProof.Products.eval C ⟨l, ⋯⟩
-- Mathlib.Algebra.Quaternion
Quaternion.im_sub : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a - b).im = a.im - b.im
-- Init.Data.Dyadic.Basic
Dyadic.le_refl : ∀ (x : Dyadic), x ≤ x
-- Mathlib.Data.Stream.Init
Stream'.map_tail : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream' α), Stream'.map f s.tail = (Stream'.map f s).tail
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.addMonoidObj.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) (j : J),
  AddMonCat.addMonoidObj F j = (F.obj j).str
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_range_comp : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {ι : Sort u_5} (f : ι → α) (g : α → M),
  (Set.range f).mulIndicator g ∘ f = g ∘ f
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.mkGateCached.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.decls.size ≤ (Std.Sat.AIG.mkGateCached.go aig input).aig.decls.size
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- Given a family of opens `U` and an open `Y` equal to the union of opens in `U`, we may
take the presieve on `Y` associated to `U` and the sieve generated by it, and form the
full subcategory (subposet) of opens contained in `Y` (`over Y`) consisting of arrows
in the sieve. This full subcategory is equivalent to `OpensLeCover U`, the (poset)
category of opens contained in some `U i`.  -/
TopCat.Presheaf.generateEquivalenceOpensLe_inverse' : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      {Y : TopologicalSpace.Opens ↑X} →
        Y = iSup U →
          CategoryTheory.Functor (TopCat.Presheaf.SheafCondition.OpensLeCover U)
            (CategoryTheory.ObjectProperty.FullSubcategory fun f =>
              (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom)
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_inducedMap : ∀ (α : Type u_2) (β : Type u_3) (γ : Type u_4) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Field β] [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [inst_6 : Field γ]
  [inst_7 : ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] [Archimedean α] (a : α),
  ConditionallyCompleteLinearOrderedField.inducedMap β γ (ConditionallyCompleteLinearOrderedField.inducedMap α β a) =
    ConditionallyCompleteLinearOrderedField.inducedMap α γ a
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.instIsOrderedAddMonoid : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsOrderedAddMonoid (Submodule R M)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- a colimit cokernel cofork of `f`  -/
CategoryTheory.Abelian.AbelianStruct.cokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Abelian.AbelianStruct f → CategoryTheory.Limits.CokernelCofork f
-- Mathlib.Data.Matrix.Basic
Matrix.coe_ofLinearEquiv_symm : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_7) {α : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α], ⇑(Matrix.ofLinearEquiv R).symm = ⇑Matrix.of.symm
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  Std.DTreeMap.Raw.foldrM f init t = Array.foldrM (fun a b => f a.fst a.snd b) init t.toArray
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.inv_eq_of_mul : ∀ {G : Type u_1} [inst : Group G] {a b : G}, a * b = 1 → a⁻¹ = b
-- Init.Core
/-- Similar to `Lean.reduceBool` for closed `Nat` terms.

Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`.
The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection).
 -/
Lean.reduceNat : ℕ → ℕ
-- Mathlib.Order.Bounds.Image
BddAbove.image2_bddBelow : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.ofCocone_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  [inst_2 : CategoryTheory.IsFiltered I] {F : CategoryTheory.Functor I C}
  (c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)) (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).I = I
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.toArchimedeanStrata : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] → HahnEmbedding.Seed K M R → HahnEmbedding.ArchimedeanStrata K M
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalGroup.mulInvClosureNhd.mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : Group G],
  T ∈ nhds 1 → T⁻¹ = T → IsOpen T → W * T ⊆ W → IsTopologicalGroup.mulInvClosureNhd T W
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.reverse.eq_1 : ∀ {α : Type u_1}, FreeAddMonoid.reverse = List.reverse
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [IsDomain R] {f v : Fin n → R},
  Function.Injective f → (∀ (i : Fin n), ∑ j, v j * f j ^ ↑i = 0) → v = 0
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.algebraMap_elemReduct_eq : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (a : L),
  (algebraMap K L) (IsPurelyInseparable.elemReduct K a) = a ^ ringExpChar K ^ IsPurelyInseparable.elemExponent K a
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor_preserves_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  (x : ↑X), ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C x)).PreservesMonomorphisms
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (Z : C),
  (CategoryTheory.InjectiveResolution.ofCocomplex Z).d 0 1 = CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z)
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instOneSubtypeMemAddSubgroup : {R : Type u_1} → [inst : Ring R] → [inst_1 : StarRing R] → One ↥(selfAdjoint R)
-- Mathlib.Order.UpperLower.Closure
instDecidablePredMemUpperClosure.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : DecidablePred fun x => ∃ a ∈ s, a ≤ x],
  instDecidablePredMemUpperClosure = inst_1
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₁₂.τ₁ = f
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.instBEqRealizeConstKey.beq : Lean.Environment.RealizeConstKey✝ → Lean.Environment.RealizeConstKey✝ → Bool
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.fibration_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CochainComplex.Plus C} (f : X ⟶ Y),
  HomotopicalAlgebra.Fibration f ↔ CochainComplex.degreewiseEpiWithInjectiveKernel f.hom
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- A complete lattice is a conditionally complete lattice, as there are no restrictions
on the properties of sInf and sSup in a complete lattice.  -/
CompleteLattice.toConditionallyCompleteLattice : {α : Type u_1} → [CompleteLattice α] → ConditionallyCompleteLattice α
-- Lean.Expr
Lean.MVarId.mk.sizeOf_spec : ∀ (name : Lean.Name), sizeOf { name := name } = 1 + sizeOf name
-- Mathlib.Topology.LocallyConstant.Basic
/-- The equivalence between `LocallyConstant X Y` and `LocallyConstant X Z` given an
equivalence `Y ≃ Z`
 -/
LocallyConstant.congrRight : {X : Type u_1} →
  {Y : Type u_2} → {Z : Type u_3} → [inst : TopologicalSpace X] → Y ≃ Z → LocallyConstant X Y ≃ LocallyConstant X Z
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffWithinAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [ContMDiffMul I n G] {f g : M → G} {s : Set M} {x : M},
  ContMDiffWithinAt I' I n f s x → ContMDiffWithinAt I' I n g s x → ContMDiffWithinAt I' I n (f * g) s x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_const_mul_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (r : R) (a : A),
  autoParam (p a) cfcₙ_const_mul_id._auto_1 → cfcₙ (fun x => r * x) a = r • a
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.toMonoidal_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D),
  Function.Injective (@CategoryTheory.Functor.Braided.toMonoidal C inst inst_1 inst_2 D inst_3 inst_4 inst_5 F)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_Ioo : ∀ {a b : ℝ}, 0 < a → a ≤ b → Real.log '' Set.Ioo a b = Set.Ioo (Real.log a) (Real.log b)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- If `G` preserves pullbacks and `C` has them, then the pullback cone constructed of the mapped
morphisms of the pullback cone is a limit.  -/
CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            (f : X ⟶ Z) →
              (g : Y ⟶ Z) →
                [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] →
                  [inst_3 : CategoryTheory.Limits.HasPullback f g] →
                    have this := ⋯;
                    CategoryTheory.Limits.IsLimit
                      (CategoryTheory.Limits.PullbackCone.mk (G.map (CategoryTheory.Limits.pullback.fst f g))
                        (G.map (CategoryTheory.Limits.pullback.snd f g)) this)
-- Mathlib.Probability.Independence.Process.Basic
/-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
for all $s_1, ..., s_p \in S$ and $t_1, ..., t_q \in T$ the two families
$(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent.

This version only requires a.e.-measurability.  -/
ProbabilityTheory.IndepFun.process_indepFun_process₀ : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : Type u_4} {𝓧 : S → Type u_5}
  {𝓨 : T → Type u_6} [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : (j : T) → MeasurableSpace (𝓨 j)]
  {X : (i : S) → Ω → 𝓧 i} {Y : (j : T) → Ω → 𝓨 j},
  (∀ (i : S), AEMeasurable (X i) P) →
    (∀ (j : T), AEMeasurable (Y j) P) →
      (∀ (I : Finset S) (J : Finset T), ProbabilityTheory.IndepFun (fun ω i => X (↑i) ω) (fun ω j => Y (↑j) ω) P) →
        ∀ [MeasureTheory.IsZeroOrProbabilityMeasure P],
          ProbabilityTheory.IndepFun (fun ω i => X i ω) (fun ω j => Y j ω) P
-- Aesop.Saturate
_private.Aesop.Saturate.0.Aesop.Stateful.Queue : Type
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.toMatrix_sylvesterMap' : ∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n),
  (LinearMap.toMatrix (((Polynomial.degreeLT.basis R m).prod (Polynomial.degreeLT.basis R n)).reindex finSumFinEquiv)
        (Polynomial.degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) =
    f.sylvester g m n
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.isThreeCycle_swap_mul_swap_same : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {a b c : α},
  a ≠ b → a ≠ c → b ≠ c → (Equiv.swap a b * Equiv.swap a c).IsThreeCycle
-- Lean.Parser.Command
/-- `#eval e` evaluates the expression `e` by compiling it and running the compiled code. It then
prints the resulting value.

* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
  to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
  Users can define `MonadEval` instances to extend the list of supported monads.

The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.

Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.

Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
  usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
  when there is no other way to print the result.

See also: `#reduce e` for evaluation by term reduction.
 -/
Lean.Parser.Command.eval : Lean.Parser.Parser