mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Sort
List.insertionSort_cons : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (a : α) (l : List α),
  List.insertionSort r (a :: l) = List.orderedInsert r a (List.insertionSort r l)
-- Mathlib.Topology.Maps.Strict.Group
/-- An additive group homomorphism is strict if and only if its `rangeRestrict` is an
open quotient map.  -/
AddMonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G →+ H} [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H] [IsTopologicalAddGroup G], Topology.IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed : ∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension S K L] (M : Type u_1) [inst_4 : Field M] [inst_5 : Algebra K M] [IsSepClosed M],
  Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Prefunctor.to_ofQuivHom : ∀ {C D : CategoryTheory.Quiv} (F : C ⟶ D),
  CategoryTheory.Prefunctor.toQuivHom (CategoryTheory.Prefunctor.ofQuivHom F) = F
-- Mathlib.Data.PNat.Basic
/-- `PNat.coe` promoted to a `MonoidHom`.  -/
PNat.coeMonoidHom : ℕ+ →* ℕ
-- Mathlib.Data.Finsupp.Basic
Finsupp.support_mapDomain_embedding : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α ↪ β) (x : α →₀ M),
  (Finsupp.mapDomain (⇑f) x).support = Finset.map f x.support
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of the inverse of a field element `x`
is the same as the logarithmic height of `x`.  -/
Height.logHeight₁_inv : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.logHeight₁ x⁻¹ = Height.logHeight₁ x
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_finsetSum' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} (s : Finset ι)
  {f : ι → α → E},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) →
    MeasureTheory.setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, MeasureTheory.setToFun μ T hT (f i)
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.instStarMemClass : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R], StarMemClass (NonUnitalStarSubsemiring R) R
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- The inclusion `U ⊓ V ⟶ U` as a morphism in the category of open sets.  -/
TopologicalSpace.OpenNhds.infLELeft : {X : TopCat} → {x : ↑X} → (U V : TopologicalSpace.OpenNhds x) → U ⊓ V ⟶ U
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.map_eq : ∀ (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} (f : α → β) (a : P.A) (g : P.B a → α), P.map f ⟨a, g⟩ = ⟨a, f ∘ g⟩
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance.eq_1 : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.variance X μ = (ProbabilityTheory.evariance X μ).toReal
-- Mathlib.Analysis.Normed.Group.AddTorsor
dist_vadd_cancel_right : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v₁ v₂ : V) (x : P), dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
-- Std.Http.Protocol.H1.Parser
/-- Parses a status-code (3 decimal digits), the following reason phrase, and the
terminating CRLF; returns a typed `Status`.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseStatusCode : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.Status
-- Mathlib.Topology.VectorBundle.Basic
/-- Natural identification of `VectorPrebundle` as a `FiberPrebundle`.  -/
VectorPrebundle.toFiberPrebundle : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : (x : B) → TopologicalSpace (E x)] → VectorPrebundle R F E → FiberPrebundle F E
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addFundamentalInterior.eq_1 : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α),
  MeasureTheory.addFundamentalInterior G s = s \ ⋃ g, ⋃ (_ : g ≠ 0), g +ᵥ s
-- Mathlib.Data.DFinsupp.BigOperators
RingHom.map_dfinsuppSumAddHom : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : NonAssocSemiring R]
  [inst_2 : NonAssocSemiring S] [inst_3 : (i : ι) → AddZeroClass (β i)] (h : R →+* S) (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i →+ R), h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => h.toAddMonoidHom.comp (g i)) f
-- Init.ShareCommon
MonadShareCommon : (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- A homeomorphism induces a partial homeomorphism on the whole space  -/
Homeomorph.toPartialHomeomorph : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → PartialHomeomorph X Y
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- The submodule generated by a single element is finite-dimensional.  -/
FiniteDimensional.span_singleton : ∀ (K : Type u) {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (x : V),
  FiniteDimensional K ↥(K ∙ x)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSliceData.mk.injEq : ∀ {α : Type u} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Roi α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Roi α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Data.List.Permutation
/-- An expository lemma to show how all of `ts`, `r`, and `f` can be eliminated from
`permutationsAux2`.

`(permutationsAux2 t [] [] ys id).2`, which appears on the RHS, is a list whose elements are
produced by inserting `t` into every non-terminal position of `ys` in order. As an example:
```lean
#eval permutationsAux2 1 [] [] [2, 3, 4] id
-- [[1, 2, 3, 4], [2, 1, 3, 4], [2, 3, 1, 4]]
```
 -/
List.permutationsAux2_snd_eq : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β),
  (List.permutationsAux2 t ts r ys f).2 = List.map (fun x => f (x ++ ts)) (List.permutationsAux2 t [] [] ys id).2 ++ r
-- Mathlib.RingTheory.WittVector.Frobenius
_private.Mathlib.RingTheory.WittVector.Frobenius.0.WittVector.termV : Lean.ParserDescr
-- Init.Data.SInt.Lemmas
Int32.toISize_ne_minValue : ∀ (a : Int32), a ≠ Int32.minValue → a.toISize ≠ ISize.minValue
-- Mathlib.Data.Num.Basic
/-- Converts a `ZNum` to `Option PosNum`, where it is `some` if the `ZNum` was positive and `none`
otherwise.  -/
PosNum.ofZNum' : ZNum → Option PosNum
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in a slice `s` that is
strictly before `pos`. If there is no such match `none` is returned.

This function is generic over all currently supported patterns except
`String`/`String.Slice`.

Examples:

* `(("abc".toSlice.endPos.prev (by decide)).revFind? Char.isAlpha).map (·.get!) == some 'b'`

* `"abc".toSlice.startPos.revFind? Char.isAlpha == none` -/
String.Slice.Pos.revFind? : {ρ : 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] →
        {s : String.Slice} → s.Pos → (pattern : ρ) → [String.Slice.Pattern.ToBackwardSearcher pattern σ] → Option s.Pos
-- Mathlib.Data.Nat.Cast.Defs
AddMonoidWithOne.mk : {R : Type u_2} →
  [toNatCast : NatCast R] →
    [toAddMonoid : AddMonoid R] →
      [toOne : One R] →
        autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam →
          autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam → AddMonoidWithOne R
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.mk.sizeOf_spec : ∀ (username : String) (uid gid : Option UInt64) (shell homedir : Option String),
  sizeOf { username := username, uid := uid, gid := gid, shell := shell, homedir := homedir } =
    1 + sizeOf username + sizeOf uid + sizeOf gid + sizeOf shell + sizeOf homedir
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- The nonnegative real power function `x^y`, defined for `x : ℝ≥0` and `y : ℝ` as the
restriction of the real power function. For `x > 0`, it is equal to `exp (y log x)`. For `x = 0`,
one sets `0 ^ 0 = 1` and `0 ^ y = 0` for `y ≠ 0`.  -/
NNReal.rpow : NNReal → ℝ → NNReal
-- Mathlib.Algebra.GroupWithZero.Pi
MulHom.single_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MulZeroClass (α i)] [inst_1 : DecidableEq ι] (i : ι) (x : α i)
  (j : ι), (MulHom.single i) x j = Pi.single i x j
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.erase.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 → t.erase a = t_1.erase a_1
-- Init.Data.ByteArray.Lemmas
List.getElem_eq_getElem_toByteArray : ∀ {l : List UInt8} {i : ℕ} {h : i < l.length}, l[i] = l.toByteArray[i]
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Class formula**. This is a special case of
`AddAction.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = Quotient.out`.  -/
AddAction.selfEquivSigmaOrbitsQuotientStabilizer : (G : Type u) →
  (X : Type v) →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] → X ≃ (ω : Quotient (AddAction.orbitRel G X)) × G ⧸ AddAction.stabilizer G ω.out
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.one_le_rpow_of_pos_of_le_one_of_neg : ∀ {x : ENNReal} {z : ℝ}, 0 < x → x ≤ 1 → z < 0 → 1 ≤ x ^ z
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_natSub : ∀ {a b a' b' c : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' →
    Mathlib.Meta.NormNum.IsNat b b' → a'.sub b' = c → Mathlib.Meta.NormNum.IsNat (a - b) c
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given an injective `CommMonoid` homomorphism `g : M →* P`, and a submonoid `S ⊆ M`,
the induced monoid homomorphism from the localization of `M` at `S` to the
localization of `P` at `g S`, is injective.
 -/
Submonoid.LocalizationMap.map_injective_of_injective : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {Q : Type u_4} [inst_3 : CommMonoid Q],
  Function.Injective ⇑g → ∀ (k : (Submonoid.map g S).LocalizationMap Q), Function.Injective ⇑(f.map ⋯ k)
-- Init.Data.Int.DivMod.Lemmas
Int.natCast_tdiv_eq_ediv : ∀ {a : ℕ} {b : ℤ}, (↑a).tdiv b = ↑a / b
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft' : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.inv f) z)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y z)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.mk.injEq : ∀ {α : Type u_2} [inst : MeasurableSpace α] (posPart negPart : MeasureTheory.Measure α)
  [posPart_finite : MeasureTheory.IsFiniteMeasure posPart] [negPart_finite : MeasureTheory.IsFiniteMeasure negPart]
  (mutuallySingular : posPart.MutuallySingular negPart) (posPart_1 negPart_1 : MeasureTheory.Measure α)
  (posPart_finite_1 : MeasureTheory.IsFiniteMeasure posPart_1)
  (negPart_finite_1 : MeasureTheory.IsFiniteMeasure negPart_1)
  (mutuallySingular_1 : posPart_1.MutuallySingular negPart_1),
  ({ posPart := posPart, negPart := negPart, posPart_finite := posPart_finite, negPart_finite := negPart_finite,
        mutuallySingular := mutuallySingular } =
      { posPart := posPart_1, negPart := negPart_1, posPart_finite := posPart_finite_1,
        negPart_finite := negPart_finite_1, mutuallySingular := mutuallySingular_1 }) =
    (posPart = posPart_1 ∧ negPart = negPart_1)
-- Mathlib.Combinatorics.HalesJewett
/-- Consider a line `l : Line α ι` as a function `α → ι → α`.  -/
Combinatorics.Line.toFun : {α : Type u_2} → {ι : Type u_3} → Combinatorics.Line α ι → α → ι → α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited α]
  {f : α → β → Option γ} {k : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filterMap f m).getKey! k =
    ((m.getKey? k).pfilter fun x h' => (f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)).isSome).get!
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory C] →
              [inst_4 : CategoryTheory.MonoidalCategory D] →
                (L : CategoryTheory.Functor C D) →
                  (W : CategoryTheory.MorphismProperty C) →
                    [L.Monoidal] →
                      (F : CategoryTheory.Functor D E) →
                        (G : CategoryTheory.Functor C E) →
                          [CategoryTheory.Localization.Lifting L W G F] →
                            CategoryTheory.Localization.Lifting₂ L L W W
                              (CategoryTheory.MonoidalCategory.curriedTensorPost G)
                              (CategoryTheory.MonoidalCategory.curriedTensorPost F)
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instIsClosedUnderColimitsOfShapeFunctorOppositeTypeIsIndObjectOfIsFiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsFiltered J],
  CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape CategoryTheory.Limits.IsIndObject J
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Constructor for `SSet.Edge` which takes as an input a term in the definitionally
equal type `SSet.Truncated.Edge` for the `2`-truncation of the simplicial set.
(This definition is made to contain abuse of defeq in other definitions.)  -/
SSet.Edge.ofTruncated : {X : SSet} → {x₀ x₁ : X.obj (Opposite.op { len := 0 })} → SSet.Truncated.Edge x₀ x₁ → SSet.Edge x₀ x₁
-- Init.Data.UInt.Bitwise
UInt64.toUInt8_shiftLeft : ∀ (a b : UInt64), b < 8 → (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8
-- Mathlib.RingTheory.Ideal.Nonunits
map_mem_nonunits_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : Monoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (f : F) [IsLocalHom f] (a : α), f a ∈ nonunits β ↔ a ∈ nonunits α
-- Init.Data.SInt.Lemmas
BitVec.ofInt_int32ToInt : ∀ (x : Int32), BitVec.ofInt 32 x.toInt = x.toBitVec
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.Λ'.normal.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {a a_1 : Λ}, Turing.TM0to1.Λ'.normal a = Turing.TM0to1.Λ'.normal a_1 → a = a_1
-- Mathlib.GroupTheory.OrderOfElement
exists_zsmul_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] [Finite G] (x : G), ∃ i, ∃ (_ : i ≠ 0), i • x = 0
-- Init.Data.UInt.Lemmas
Fin.mk_uInt64ToNat : ∀ (n : UInt64), ⟨n.toNat, ⋯⟩ = n.toFin
-- Mathlib.Data.Finset.Insert
Finset.default_singleton : ∀ {α : Type u_1} (i : α), ↑default = i
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.section_comp_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsReflexivePair f g] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.commonSection f g) (CategoryTheory.CategoryStruct.comp g h) = h
-- Lean.Data.Lsp.Utf16
Lean.String.utf16Length : String → ℕ
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.mk'_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) [inst_3 : CategoryTheory.BimonObj X],
  (CategoryTheory.Bimon.mk' X).X = CategoryTheory.Bimon.mk'X X
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence : ∀ {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence},
  T ⊨ᵇ φ → ∀ (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M], M ⊨ φ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfZeroLE_real_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i j : Set α}
  (hi : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i) (hi₁ : MeasurableSet i),
  MeasurableSet j → (s.toMeasureOfZeroLE i hi₁ hi).real j = s (i ∩ j)
-- Mathlib.NumberTheory.ModularForms.Discriminant
ModularForm.discriminant_isZeroAtImInfty : UpperHalfPlane.IsZeroAtImInfty ModularForm.discriminant
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
OpensMeasurableSpace.mk : ∀ {α : Type u_6} [inst : TopologicalSpace α] [h : MeasurableSpace α], borel α ≤ h → OpensMeasurableSpace α
-- Std.Data.DHashMap.Basic
/-- Creates a hash map from a list of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.DHashMap.Const.unitOfList : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → List α → Std.DHashMap α fun x => Unit
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decomposeAddEquiv_apply : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] (a : M),
  (DirectSum.decomposeAddEquiv ℳ) a = (DirectSum.decompose ℳ) a
-- Init.Prelude
/-- A token produced by the parser from original input that includes both leading and trailing
whitespace as well as position information.

The `leading` whitespace is inferred after parsing by `Syntax.updateLeading`. This is because the
“preceding token” is not well-defined during parsing, especially in the presence of backtracking.
 -/
Lean.SourceInfo.original : Substring.Raw → String.Pos.Raw → Substring.Raw → String.Pos.Raw → Lean.SourceInfo
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal.eq_1 : ∀ (r : ℝ), ENNReal.ofReal r = ↑r.toNNReal
-- Mathlib.Data.ENat.Basic
ENat.WithBot.natCast_add_cancel : ∀ {a b : WithBot ℕ∞} {c : ℕ}, ↑c + a = ↑c + b ↔ a = b
-- Mathlib.Tactic.GCongr.CoreAttrs
Mathlib.Tactic.GCongr.imp_mono : ∀ {a b c d : Prop}, (c → a) → (c → b → d) → (a → b) → c → d
-- Mathlib.Analysis.Normed.Lp.lpHolder
Memℓp.holder_gen_bound : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal)
  [hpqr : p.HolderTriple q r] {e : (i : ι) → E i} {f : (i : ι) → F i},
  0 < p.toReal →
    0 < q.toReal →
      ∀ (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K C D : ℝ},
        (∀ (i : ι), ‖B i‖ ≤ K) →
          0 ≤ K →
            0 ≤ C →
              (∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C) →
                (∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D) →
                  ∀ (s : Finset ι),
                    ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ r.toReal ≤
                      K ^ r.toReal * C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.instIsClosedUnderCokernelsOfIsClosedUnderQuotients : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderQuotients], P.IsClosedUnderCokernels
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCochain_v_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n)
  (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + -1 = p₃) {Z : C} (h_1 : L.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v p₂ p₃ h₂₃) h_1) =
    CategoryTheory.CategoryStruct.comp (β.v p₁ p₃ ⋯) h_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.freeAddGroupCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ),
  (FreeAddGroup.freeAddGroupCongr e).trans (FreeAddGroup.freeAddGroupCongr f) =
    FreeAddGroup.freeAddGroupCongr (e.trans f)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core.injEq : ∀ (e e_1 : Lean.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core e = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core e_1) = (e = e_1)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- If `H` is not `n`-colorable and `G` is `n`-colorable, then `G` is `H.Free`.  -/
SimpleGraph.free_of_colorable : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ} {W : Type u_4} {H : SimpleGraph W}, ¬H.Colorable n → G.Colorable n → H.Free G
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.throwNoScope : Lean.Elab.Command.CommandElabM Unit
-- Lean.Parser.Command
Lean.Parser.Command.structureTk.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.filter_eq_empty_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool}, Std.ExtTreeMap.filter f t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = false
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.comp.get_mk : ∀ {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α : TypeVec.{u} m} (x : ↑P fun i => ↑(Q i) α),
  MvPFunctor.comp.get (MvPFunctor.comp.mk x) = x
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.id_reflectsLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.coprod.eq_1 : ∀ {A : Type u_2} {B : Type u_3} {E : Type u_6} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [inst_4 : AddCommMonoid E] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousAdd E]
  (f : A →ₜ+ E) (g : B →ₜ+ E), f.coprod g = (ContinuousAddMonoidHom.add E).comp (f.prodMap g)