mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- The Stieltjes outer measure associated to a Stieltjes function.  -/
StieltjesFunction.outer : {R : Type u_1} →
  [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → StieltjesFunction R → MeasureTheory.OuterMeasure R
-- Mathlib.Topology.Bases
TopologicalSpace.Countable.to_separableSpace : ∀ {α : Type u} [t : TopologicalSpace α] [Countable α], TopologicalSpace.SeparableSpace α
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_div_two : ∀ {a b : ℕ}, (a ^^^ b) / 2 = a / 2 ^^^ b / 2
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.pullback.congr_simp : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (f f_1 : E →ₛₗ[σ₁₂] E₂),
  f = f_1 → Seminorm.pullback f = Seminorm.pullback f_1
-- Init.Data.Array.Lemmas
Array.filterMap_replicate_of_some : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : ℕ} {f : α → Option β},
  f a = some b → Array.filterMap f (Array.replicate n a) = Array.replicate n b
-- Mathlib.RepresentationTheory.Rep.Basic
_private.Mathlib.RepresentationTheory.Rep.Basic.0.Rep.Hom.mk.inj : ∀ {k : Type u} {G : Type v} {inst : Semiring k} {inst_1 : Monoid G} {A B : Rep.{w, u, v} k G}
  {hom' hom'_1 : A.ρ.IntertwiningMap B.ρ}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Init.MethodSpecsSimp
Pow.pow_eq_hPow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β], Pow.pow = HPow.hPow
-- Lean.Elab.InfoTree.Types
Lean.Elab.ChoiceInfo.mk : Lean.Elab.ElabInfo → Lean.Elab.ChoiceInfo
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.conj_mul : ∀ (z w : Complex.UnitDisc), star (z * w) = star z * star w
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Pair.mk : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              {i : ι} →
                (toPair : Monoid.CoprodI.Word.Pair G i) →
                  (∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ toPair.tail.toList → g ∈ d.set i_1) →
                    Monoid.PushoutI.NormalWord.Pair d i
-- Init.Data.Format.Basic
Std.Format.nest.inj : ∀ {indent : ℤ} {f : Std.Format} {indent_1 : ℤ} {f_1 : Std.Format},
  Std.Format.nest indent f = Std.Format.nest indent_1 f_1 → indent = indent_1 ∧ f = f_1
-- Mathlib.Algebra.Lie.Basic
/-- A Lie module is a module over a commutative ring, together with a linear action of a Lie
algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms.  -/
LieModule : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] → [LieAlgebra R L] → [inst_3 : AddCommGroup M] → [Module R M] → [LieRingModule L M] → Prop
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.ClosedOpen.toList_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)...=Std.PRange.succ hi).toList = List.map Std.PRange.succ (lo...=hi).toList
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
/-- `HomOrthogonal.MatrixDecomposition` as an `R`-linear equivalence.  -/
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {s : ι → C} →
        [inst_1 : CategoryTheory.Preadditive C] →
          [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            {R : Type u_2} →
              [inst_3 : Semiring R] →
                [inst_4 : CategoryTheory.Linear R C] →
                  CategoryTheory.HomOrthogonal s →
                    {α β : Type} →
                      [inst_5 : Finite α] →
                        [inst_6 : Finite β] →
                          {f : α → ι} →
                            {g : β → ι} →
                              ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃ₗ[R]
                                (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))
-- Mathlib.GroupTheory.CoprodI
/-- A `Word` is a `List (Σ i, M i)`, such that `1` is not in the list, and no
two adjacent letters are from the same summand  -/
Monoid.CoprodI.Word.toList : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → Monoid.CoprodI.Word M → List ((i : ι) × M i)
-- Init.Data.String.Slice
/-- Constructs a new string obtained by replacing all occurrences of `pattern` with
`replacement` in `s`.

This function is generic over all currently supported patterns. The replacement may be a
`String` or a `String.Slice`.

Examples:

* `"red green blue".toSlice.replace 'e' "" = "rd grn blu"`

* `"red green blue".toSlice.replace (fun c => c == 'u' || c == 'e') "" = "rd grn bl"`

* `"red green blue".toSlice.replace "e" "" = "rd grn blu"`

* `"red green blue".toSlice.replace "ee" "E" = "red grEn blue"`

* `"red green blue".toSlice.replace "e" "E" = "rEd grEEn bluE"`

* `"aaaaa".toSlice.replace "aa" "b" = "bba"`

* `"abc".toSlice.replace "" "k" = "kakbkck"`
 -/
String.Slice.replace : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        {α : Type u_1} →
          [String.ToSlice α] →
            String.Slice → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → α → String
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.neg_comp : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_7} [inst : Neg G] (f : β → G) (g : α → β), (-f) ∘ g = -f ∘ g
-- Mathlib.Algebra.Group.Conj
ConjClasses.carrier_eq_preimage_mk : ∀ {α : Type u} [inst : Monoid α] {a : ConjClasses α}, a.carrier = ConjClasses.mk ⁻¹' {a}
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
IsNonarchimedean.apply_sum_eq_of_lt : ∀ {R : Type u_1} [inst : LinearOrder R] {α : Type u_2} {β : Type u_3} [inst_1 : AddCommGroup α] {f : α → R},
  IsNonarchimedean f →
    (∀ (a : α), f a = f (-a)) →
      ∀ {s : Finset β} {l : β → α} {k : β}, k ∈ s → (∀ j ∈ s, j ≠ k → f (l j) < f (l k)) → f (∑ i ∈ s, l i) = f (l k)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- A semilinear set is proper if it is a finite union of proper linear sets.  -/
IsProperSemilinearSet : {M : Type u_1} → [AddCommMonoid M] → Set M → Prop
-- Mathlib.Analysis.Normed.Group.Basic
nndist_mulIndicator : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedGroup E] (s t : Set α) (f : α → E) (x : α),
  nndist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(symmDiff s t).mulIndicator f x‖₊
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_testBit_zero_shiftRight_one : ∀ (n : ℕ), Nat.bit (n.testBit 0) (n >>> 1) = n
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.oneCochainOfTwoSplitting_apply : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L) {s₁ s₂ : L →ₗ[R] E.L}
  (hs₁ : Function.LeftInverse ⇑E.proj ⇑s₁) (hs₂ : Function.LeftInverse ⇑E.proj ⇑s₂) (x : L),
  (E.oneCochainOfTwoSplitting hs₁ hs₂) x = E.toKer.symm ⟨s₁ x - s₂ x, ⋯⟩
-- Lean.Elab.Arg
Lean.Elab.Term.Arg.expr : Lean.Expr → Lean.Elab.Term.Arg
-- Mathlib.Order.GameAdd
Sym2.GameAdd.fst_snd : ∀ {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α}, rα a₁ a₂ → Sym2.GameAdd rα s(a₁, b) s(b, a₂)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.strongHomClass : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.StrongHomClass (L.ElementaryEmbedding M N) M N
-- Mathlib.Data.Finset.Sum
Finset.disjSum_inj : ∀ {α : Type u_4} {β : Type u_5} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β}, s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂
-- Mathlib.Order.CompleteLattice.Basic
Prod.iInf_mk : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : InfSet α] [inst_1 : InfSet β] (f : ι → α) (g : ι → β),
  ⨅ i, (f i, g i) = (⨅ i, f i, ⨅ i, g i)
-- Lean.LocalContext
Lean.LocalDecl.setType : Lean.LocalDecl → Lean.Expr → Lean.LocalDecl
-- Init.Data.Vector.Monadic
Vector.mapM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n n' : ℕ} [inst : Monad m] [LawfulMonad m] {f : α → m β}
  {xs : Vector α n} {ys : Vector α n'},
  Vector.mapM f (xs ++ ys) = do
    let __do_lift ← Vector.mapM f xs
    let __do_lift_1 ← Vector.mapM f ys
    pure (__do_lift ++ __do_lift_1)
-- Mathlib.Algebra.Group.UniqueProds.Basic
Multiplicative.instUniqueProdsOfUniqueSums : ∀ {M : Type u_1} [inst : Add M] [UniqueSums M], UniqueProds (Multiplicative M)
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.adhesive_of_preserves_and_reflects_isomorphism : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Adhesive D] [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.HasPushouts C]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F] [F.ReflectsIsomorphisms],
  CategoryTheory.Adhesive C
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.mem_sdiff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} {s t : L.DefinableSet A α}
  {x : α → M}, x ∈ s \ t ↔ x ∈ s ∧ x ∉ t
-- Mathlib.Order.Interval.Finset.Basic
/-- `Finset.cons` version of `Finset.Ioi_insert`.  -/
Finset.Ici_eq_cons_Ioi : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
  Finset.Ici a = Finset.cons a (Finset.Ioi a) ⋯
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.instCoeResultExpr : Coe Lean.Meta.LetToHave.Result✝ Lean.Expr
-- Init.Data.OfScientific
instOfScientificFloat32 : OfScientific Float32
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableWithinAt_smul_const_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {a : 𝕜}
  {s : (x : B) → E x} {u : Set B} {x₀ : B}, MDiffAt[u] (T% s) x₀ → (MDiffAt[u] fun x => ⟨x, (a • s) x⟩) x₀
-- Lean.MetavarContext
Lean.MetavarContext.getLevelDecl : Lean.MetavarContext → Lean.LMVarId → Lean.LevelMetavarDecl
-- Mathlib.Data.Int.Cast.Lemmas
Commute.intCast_mul_right : ∀ {α : Type u_3} [inst : Ring α] {a b : α}, Commute a b → ∀ (m : ℤ), Commute a (↑m * b)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabDescr.mk : (Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep1) →
  Lean.Elab.Command.InductiveElabDescr
-- Mathlib.Topology.MetricSpace.IsometricSMul
Additive.isIsIsometricVAdd' : ∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul M M],
  IsIsometricVAdd (Additive M) (Additive M)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y
            Z).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
        Z)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- `u` is a **quasi-inverse** to `v` if `u ∘ₗ v ≈ id` and `v ∘ₗ u ≈ id` modulo
linear maps with noetherian ranges. Recall that if the scalar ring is noetherian
(e.g a field), then "noetherian range" can be replaced by "finitely generated range".  -/
LinearMap.IsQuasiInverse : {K : Type u_1} →
  {V₂ : Type u_4} →
    {V₃ : Type u_6} →
      [inst : CommRing K] →
        [inst_1 : AddCommGroup V₂] →
          [inst_2 : Module K V₂] →
            [inst_3 : AddCommGroup V₃] → [inst_4 : Module K V₃] → (V₃ →ₗ[K] V₂) → (V₂ →ₗ[K] V₃) → Prop
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.instInhabitedDefaultForwardSearcher : {a : Type} →
  {a_1 : a} → {a_2 : String.Slice} → Inhabited (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher a_1 a_2)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.userPostSimprocs : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Simproc
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.one_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (x : A), 1 x = x
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- **Alias** of the forward direction of `lipschitzOnWith_iff_restrict`. -/
LipschitzOnWith.to_restrict : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, LipschitzOnWith K f s → LipschitzWith K (s.domRestrict f)
-- Mathlib.Order.CompleteBooleanAlgebra
le_sdiff_iff : ∀ {α : Type u} [inst : Order.Coframe α] {a b c : α}, a ≤ b \ c ↔ ∀ (d : α), b ≤ c ⊔ d → a ≤ d
-- Lean.Data.NameMap.Basic
Lean.NameSet.instUnion : Union Lean.NameSet
-- Lean.Meta.Sym.InstantiateS
/-- Monad for `instantiateRevBetaS'` with caching keyed by `(expression pointer, binder offset)`.  -/
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.M : Type → Type
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_eq_rpow_right_iff : ∀ {x : NNReal} {y z : ℝ}, x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- This alias for `Functor.CommShift₂.comm` allows to use the dot notation.  -/
CategoryTheory.Functor.commShift₂_comm : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} {inst_2 : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6}
  {inst_3 : AddCommMonoid M} {inst_4 : CategoryTheory.HasShift C₁ M} {inst_5 : CategoryTheory.HasShift C₂ M}
  {inst_6 : CategoryTheory.HasShift D M} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  (h : CategoryTheory.CommShift₂Setup D M) [self : G.CommShift₂ h] (X₁ : C₁) (X₂ : C₂) (m n : M),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso (G.obj ((CategoryTheory.shiftFunctor C₁ m).obj X₁)) n).hom.app X₂)
      ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Functor.commShiftIso (G.flip.obj X₂) m).hom.app X₁)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso (G.flip.obj ((CategoryTheory.shiftFunctor C₂ n).obj X₂)) m).hom.app X₁)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D m).map ((CategoryTheory.Functor.commShiftIso (G.obj X₁) n).hom.app X₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm ((G.obj X₁).obj X₂) m n).inv
          ((↑(h.ε m n)).app
            ((CategoryTheory.shiftFunctor D n).obj ((CategoryTheory.shiftFunctor D m).obj ((G.obj X₁).obj X₂))))))
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorLeftHomEquiv_symm_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X X' Y Y' Z : C} [inst_2 : CategoryTheory.ExactPairing Y Y'] (f : X ⟶ X')
  (g : X' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z),
  (CategoryTheory.tensorLeftHomEquiv X Y Y' Z).symm (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y' f)
      ((CategoryTheory.tensorLeftHomEquiv X' Y Y' Z).symm g)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.quotient : {G : Type u} →
  (X : Type v) →
    [inst : AddGroup G] →
      [inst_1 : AddMonoid X] →
        [inst_2 : AddAction X G] → (H : AddSubgroup G) → [AddAction.QuotientAction X H] → AddAction X (G ⧸ H)
-- Mathlib.Probability.BrownianMotion.Basic
/-- A stochastic process is called **pre-Brownian** if its finite-dimensional laws are those
of the Brownian motion, see `projectiveFamily`.

Note: we name the constructor `mk'` so as to define later `IsPreBrownianReal.mk`, which to
pre-Brownian motion will associate a continuous modification,
in a way similar to `AEMeasurable.mk`.  -/
ProbabilityTheory.IsPreBrownianReal : {Ω : Type u_1} →
  {mΩ : MeasurableSpace Ω} →
    (NNReal → Ω → ℝ) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsPreBrownianReal._auto_1 → Prop
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharType.lower : Lean.FuzzyMatching.CharType
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- Left action for the tensor product of two bimodules.  -/
Bimod.TensorBimod.actLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        {R S T : CategoryTheory.Mon C} →
          (P : Bimod R S) →
            (Q : Bimod S T) →
              [∀ (X : C),
                    CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                      (CategoryTheory.MonoidalCategory.tensorLeft X)] →
                CategoryTheory.MonoidalCategoryStruct.tensorObj R.X (Bimod.TensorBimod.X P Q) ⟶ Bimod.TensorBimod.X P Q
-- Mathlib.Order.Hom.CompleteLattice
/-- Copy of a `sSupHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
sSupHom.copy : {α : Type u_2} →
  {β : Type u_3} → [inst : SupSet α] → [inst_1 : SupSet β] → (f : sSupHom α β) → (f' : α → β) → f' = ⇑f → sSupHom α β
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.ext : {α β σ : Type} →
  Lean.ScopedEnvExtension α β σ →
    Lean.PersistentEnvExtension (Lean.ScopedEnvExtension.Entry α) (Lean.ScopedEnvExtension.Entry β)
      (Lean.ScopedEnvExtension.StateStack α β σ)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM : Type → Type
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.upper_le_upper : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), J ∈ π → J.upper ≤ I.upper
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput : Type
-- Init.Data.List.FinRange
List.finRange_succ_last : ∀ {n : ℕ}, List.finRange (n + 1) = List.map Fin.castSucc (List.finRange n) ++ [Fin.last n]
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictMono_dual_iff`. -/
StrictMono.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → StrictMono (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.below.endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive :
    (a : s.Pos) →
      (a_1 : List (String.Slice.Pattern.SearchStep s)) → String.Slice.Pattern.Model.IsValidSearchFrom pat a a_1 → Prop},
  String.Slice.Pattern.Model.IsValidSearchFrom.below ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_preΨ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ),
  (W.baseChange B).preΨ n = Polynomial.map (↑f) ((W.baseChange A).preΨ n)
-- Mathlib.Computability.TuringMachine.Computable
/-- A proof of tm outputting l' when given l in at most m steps.  -/
Turing.TM2OutputsInTime : (tm : Turing.FinTM2) → List (tm.Γ tm.k₀) → Option (List (tm.Γ tm.k₁)) → ℕ → Type
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNorm_mul : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalNormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R]
  [Nontrivial R], ‖ContinuousLinearMap.mul 𝕜 R‖ = 1
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- A certificate that proves `subject = result.norm` via `result.proof`  -/
Mathlib.Tactic.Determinant.Cert : {u : Lean.Level} → {α : Q(Type u)} → Q(CommRing «$α») → Type
-- Mathlib.Topology.Metrizable.Basic
/-- Construct on a pseudometrizable space a countably generated uniformity
compatible with the topology. Use `pseudoMetrizableSpaceUniformity_countably_generated` for a proof
that this uniformity is countably generated.  -/
TopologicalSpace.pseudoMetrizableSpaceUniformity : (X : Type u_5) → [inst : TopologicalSpace X] → [h : TopologicalSpace.PseudoMetrizableSpace X] → UniformSpace X
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainAddEquiv.eq_1 : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N] (e : M ≃ N),
  MonoidAlgebra.mapDomainAddEquiv R e =
    { toFun := fun x => MonoidAlgebra.mapDomain (⇑e) x, invFun := fun x => MonoidAlgebra.mapDomain (⇑e.symm) x,
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.coe_algHomEquivPrimeSpectrum : ∀ {k : Type u_1} {R : Type u_2} [inst : Field k] [inst_1 : CommRing R] [inst_2 : Algebra k R]
  [inst_3 : Algebra.IsFiniteSplit k R] (f : R →ₐ[k] k),
  ((Algebra.IsFiniteSplit.algHomEquivPrimeSpectrum k R) f).asIdeal = RingHom.ker f
-- Aesop.Forward.State
Aesop.ClusterState.instInhabited : Inhabited Aesop.ClusterState
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.CompactSpace.isFiniteMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α] [CompactSpace α]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ], MeasureTheory.IsFiniteMeasure μ
-- Batteries.Classes.RatCast
instCoeTailRatOfRatCast : {K : Type u_1} → [RatCast K] → CoeTail ℚ K
-- Mathlib.RingTheory.Extension.Generators
/-- The forwards direction of the canonical isomorphism `T ⊗[R] R[Xᵢ] ≃ₐ[T] T[Xᵢ]` as
a map of extensions.  -/
Algebra.Generators.baseChangeFromBaseChange : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            (P : Algebra.Generators R S ι) →
              (T : Type u_2) →
                [inst_3 : CommRing T] →
                  [inst_4 : Algebra R T] → P.toExtension.baseChange.Hom (Algebra.Generators.baseChange T P).toExtension
-- Mathlib.MeasureTheory.Measure.Regular
/-- A measure `μ` is regular if
- it is finite on all compact sets;
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using compact sets:
  `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open.  -/
MeasureTheory.Measure.Regular : {α : Type u_1} → [inst : MeasurableSpace α] → [TopologicalSpace α] → MeasureTheory.Measure α → Prop