mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {inst_1 : LinearOrder J} {inst_2 : SuccOrder J} {inst_3 : OrderBot J}
  {inst_4 : CategoryTheory.Limits.HasIterationOfShape J C} {inst_5 : WellFoundedLT J} {j : J} {x y : Φ.Iteration j},
  x = y ↔ x.F = y.F
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f g : X ⟶ Y}, HomotopicalAlgebra.RightHomotopyRel f g → ∃ P, P.IsGood ∧ Nonempty (P.RightHomotopy f g)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_alterₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [inst_4 : Std.LawfulBEqOrd α] {t : Std.DTreeMap.Internal.Impl α β} {a : α} {f : Option (β a) → Option (β a)}
  (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.alterₘ a f t htb).toListModel.Perm (Std.Internal.List.alterKey a f t.toListModel)
-- Mathlib.Algebra.Order.Group.MinMax
min_sub_sub_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  min (a - b) (a - c) = a - max b c
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.mk_apply : ∀ {G : Type w} [inst : TopologicalSpace G] (toFun : TopologicalSpace.Compacts G → NNReal)
  (mono' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun K₁ ≤ toFun K₂)
  (sup_disjoint' :
    ∀ (K₁ K₂ : TopologicalSpace.Compacts G),
      Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂)
  (sup_le' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂)
  (K : TopologicalSpace.Compacts G),
  { toFun := toFun, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' } K = ↑(toFun K)
-- Mathlib.RingTheory.Finiteness.Quotient
/-- `B ⧸ P` is a finite `A ⧸ p`-module if `B` is a finite `A`-module.  -/
module_finite_of_liesOver : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p] [Module.Finite A B], Module.Finite (A ⧸ p) (B ⧸ P)
-- Mathlib.Data.List.Sort
OrderEmbedding.sortedGE_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) {l : List α},
  (List.map (⇑e) l).SortedGE ↔ l.SortedGE
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.pi_bot : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)], (AddSubgroup.pi Set.univ fun i => ⊥) = ⊥
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_def : ∀ {α : Type u_1} [inst : LE α] {x y : WithZero α}, x ≤ y ↔ ∀ (a : α), x = ↑a → ∃ b, y = ↑b ∧ a ≤ b
-- Mathlib.Data.Part
Part.mem_some : ∀ {α : Type u_1} (a : α), a ∈ Part.some a
-- Mathlib.Data.Finset.Sum
Finset.sumEquiv_apply_snd : ∀ {α : Type u_4} {β : Type u_5} (s : Finset (α ⊕ β)), (Finset.sumEquiv s).2 = s.toRight
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftUnshift_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ)
  (hn : n + a = n') (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p' + n' = q),
  (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow •
      CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p' p ⋯).inv (γ.v p' q ⋯)
-- Std.Tactic.BVDecide.Syntax
/-- Split hypotheses of the form `h : (x && y) = true` into `h1 : x = true` and `h2 : y = true`.
This has synergy potential with embedded constraint substitution. Because embedded constraint
substitution is the only use case for this feature it is automatically disabled whenever embedded
constraint substitution is disabled.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.andFlattening : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The colimit of `F ⋙ forget MonCat` in the category of types.
In the following, we will construct a monoid structure on `M`.
 -/
MonCat.FilteredColimits.M : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J MonCat → Type (max u v)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x)) f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (Y.fromSpecResidueField T.y)) g
-- Mathlib.Algebra.DirectSum.Module
DirectSum.congrLinearEquiv_toLinearMap : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} {N : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (N i)]
  [inst_2 : (i : ι) → Module R (N i)] {P : ι → Type u_4} [inst_3 : (i : ι) → AddCommMonoid (P i)]
  [inst_4 : (i : ι) → Module R (P i)] (u : (i : ι) → N i ≃ₗ[R] P i),
  ↑(DirectSum.congrLinearEquiv u) = DirectSum.lmap fun i => ↑(u i)
-- Mathlib.Order.Cofinal
/-- In a linear order with no maximum, cofinal sets are the same as unbounded sets.  -/
not_bddAbove_iff_isCofinal : ∀ {α : Type u_1} [inst : LinearOrder α] [NoMaxOrder α] {s : Set α}, ¬BddAbove s ↔ IsCofinal s
-- Mathlib.Algebra.Homology.HomotopyCategory
instCategoryHomotopyCategory : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        (c : ComplexShape ι) → CategoryTheory.Category.{max u_2 v, max (max u_2 u) v} (HomotopyCategory V c)
-- Mathlib.Topology.MetricSpace.Holder
holderOnWith_univ : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
  {f : X → Y}, HolderOnWith C r f Set.univ ↔ HolderWith C r f
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.pointwiseCocone_ι_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : J) (Y : K),
  ((CategoryTheory.Limits.pointwiseCocone F).ι.app X).app Y = CategoryTheory.Limits.colimit.ι (F.flip.obj Y) X
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instInhabitedComonadHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} → Inhabited (CategoryTheory.ComonadHom G G)
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.coeDelaborator.delabHead : Lean.Meta.CoeFnInfo → ℕ → Bool → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.range : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {f : M →ₗ[S] M}, LinearMap.IsProj m f → f.range = m
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- For any function `f` from a normed vector space to a normed vector space, the set of points
`x` such that `f` is continuously polynomial at `x` is open.  -/
isOpen_cpolynomialAt : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F),
  IsOpen {x | CPolynomialAt 𝕜 f x}
-- Lean.Widget.UserWidget
Lean.Widget.UserWidgetDefinition.mk : String → String → Lean.Widget.UserWidgetDefinition
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSub_nsmul : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (r : R) (s : ↥S)
  (n : ℕ), AddCommute r ↑s → n • (r -ₒ s) = n • r -ₒ n • s
-- Init.Data.Bool
Bool.not_ite_eq_true_eq_true : ∀ {p : Prop} [h : Decidable p] {b c : Bool}, (¬if p then b = true else c = true) ↔ if p then b = false else c = false
-- Mathlib.Data.EReal.Inv
EReal.div_eq_iff : ∀ {a b c : EReal}, b ≠ ⊥ → b ≠ ⊤ → b ≠ 0 → (c / b = a ↔ c = a * b)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Order.IsSuccLimit.ordinalPred_eq : ∀ {o : Ordinal.{u_4}}, Order.IsSuccLimit o → o.pred = o
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- UV-compression is injective on the sets that are not UV-compressed.  -/
UV.compress_injOn : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v : α} [inst_3 : DecidableEq α], Set.InjOn (UV.compress u v) ↑({a ∈ s | UV.compress u v a ∉ s})
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.NormNoninc.zero : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂],
  NormedAddGroupHom.NormNoninc 0
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Nanosecond.Offset n
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.ToCodeBlock.expandNestedActionAux : Lean.Name → Bool → Bool → Lean.Syntax → StateT (List Lean.Syntax) Lean.Elab.Term.Do.ToCodeBlock.M Lean.Syntax
-- Mathlib.Data.Seq.Parallel
Computation.Corec.f.match_1.hcongr_6 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (β β' : Type u_2),
      β = β' →
        ∀ (motive : α ⊕ β → Sort u_3) (motive' : α' ⊕ β' → Sort u_3),
          motive ≍ motive' →
            ∀ (x : α ⊕ β) (x' : α' ⊕ β'),
              x ≍ x' →
                ∀ (h_1 : (a : α) → motive (Sum.inl a)) (h_1' : (a : α') → motive' (Sum.inl a)),
                  h_1 ≍ h_1' →
                    ∀ (h_2 : (val : β) → motive (Sum.inr val)) (h_2' : (val : β') → motive' (Sum.inr val)),
                      h_2 ≍ h_2' →
                        (match x with
                          | Sum.inl a => h_1 a
                          | Sum.inr val => h_2 val) ≍
                          match x' with
                          | Sum.inl a => h_1' a
                          | Sum.inr val => h_2' val
-- Mathlib.Order.Types.Arithmetic
/-- The order type of the rational numbers. 

Conventions for notations in identifiers:

 * The recommended spelling of `η` in identifiers is `eta`. -/
OrderType.eta : OrderType.{0}
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.defEq.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Basic
Lean.Meta.WhnfCache : Type
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.id_toFun : ∀ (α : Type u_2) [inst : Min α] [inst_1 : Top α] (a : α), (InfTopHom.id α) a = a
-- Mathlib.Order.Interval.Finset.Basic
BddAbove.finite : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrderBot α] {s : Set α}, BddAbove s → s.Finite
-- Mathlib.Data.Num.Basic
PosNum.instAdd : Add PosNum
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.CommGrp C} (e : G.X ≅ H.X)
  (one_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
      _auto_105✝)
  (mul_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
          CategoryTheory.MonObj.mul)
      _auto_107✝),
  (CategoryTheory.CommGrp.mkIso e one_f mul_f).inv.hom.hom.hom = e.inv
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasLeftKanLift.mk' : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a},
  CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftLift f g) →
    CategoryTheory.Bicategory.HasLeftKanLift f g
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- A `𝕜`-affine isometric embedding of one normed add-torsor over a normed `𝕜`-space into
another, denoted as `f : P →ᵃⁱ[𝕜] P₂`.  -/
«term_→ᵃⁱ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.comp_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ}
  {P Q R : TopCat.Presheaf C X} (f : P ⟶ Q) (g : Q ⟶ R),
  (CategoryTheory.CategoryStruct.comp f g).app U = CategoryTheory.CategoryStruct.comp (f.app U) (g.app U)
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.faithful_exists : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  (f : X ⟶ Y), (CategoryTheory.MonoOver.exists f).Faithful
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.mk.sizeOf_spec : ∀ (mvar key : Lean.Expr) (mctx : Lean.MetavarContext) (instances : Array Lean.Meta.SynthInstance.Instance)
  (currInstanceIdx : ℕ) (typeHasMVars : Bool),
  sizeOf
      { mvar := mvar, key := key, mctx := mctx, instances := instances, currInstanceIdx := currInstanceIdx,
        typeHasMVars := typeHasMVars } =
    1 + sizeOf mvar + sizeOf key + sizeOf mctx + sizeOf instances + sizeOf currInstanceIdx + sizeOf typeHasMVars
-- Mathlib.Data.List.Permutation
List.permutationsAux_cons : ∀ {α : Type u_1} (t : α) (ts is : List α),
  (t :: ts).permutationsAux is =
    List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) (ts.permutationsAux (t :: is)) is.permutations
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_inf_le : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α},
  Coheyting.boundary (a ⊓ b) ≤ Coheyting.boundary a ⊔ Coheyting.boundary b
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  IsUniformEmbedding ⇑(ContinuousLinearMap.pi (ContDiffMapSupportedIn.structureMapCLM 𝕜 n))
-- Mathlib.Order.Hom.Bounded
TopHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Top α] [inst_1 : Top β] [inst_2 : Top γ] (f : TopHom β γ)
  (g : TopHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.MeasureTheory.Measure.Support
/-- In a hereditarily Lindelöf space, the support of a measure is conull.  -/
MeasureTheory.Measure.support_mem_ae : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X], μ.support ∈ MeasureTheory.ae μ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults.mk : {α : Type} →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree α →
    Array Lean.Meta.RefinedDiscrTree.ImportFailure✝ → Lean.Meta.RefinedDiscrTree.InitResults✝ α
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = false ↔ ∃ a, a ∈ m
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_coe_pi : (↑Real.pi).sign = 0
-- Mathlib.Data.Set.Piecewise
Set.univ_pi_piecewise : ∀ {ι : Type u_8} {α : ι → Type u_9} (s : Set ι) (t t' : (i : ι) → Set (α i)) [inst : (x : ι) → Decidable (x ∈ s)],
  Set.univ.pi (s.piecewise t t') = s.pi t ∩ sᶜ.pi t'
-- Mathlib.RingTheory.ClassGroup.Basic
/-- A fractional ideal is principal if a power coprime to the class number is principal.  -/
FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [inst_4 : IsDomain R] [IsDedekindDomain R] [inst_6 : Fintype (ClassGroup R)] {n : ℕ},
  n.Coprime (Fintype.card (ClassGroup R)) →
    ∀ (I : FractionalIdeal (nonZeroDivisors R) K), (↑(I ^ n)).IsPrincipal → (↑I).IsPrincipal
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.expect : {α β : Type} → Std.Http.Server.Connection.PollSources✝ α β → Option ℕ
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `Equiv.addRight` as an `OrderIso`. See also `OrderEmbedding.addRight`.  -/
OrderIso.addRight : {α : Type u} → [inst : AddGroup α] → [inst_1 : LE α] → [AddRightMono α] → α → α ≃o α
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- `v ≤[i] w` is notation for `v.restrict i ≤ w.restrict i`.  -/
MeasureTheory.«term_≤[_]_» : Lean.TrailingParserDescr
-- Init.Data.String.Subslice
String.Slice.endExclusive_subslice : ∀ {s : String.Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd},
  (s.subslice newStart newEnd h).endExclusive = newEnd
-- Mathlib.Order.RelSeries
RelSeries.cons.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newHead : α) (rel : (newHead, p.head) ∈ r),
  p.cons newHead rel = (RelSeries.singleton r newHead).append p rel
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological_G : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M],
  (Module.Presentation.tautological A M).G = M
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- The end of a graph, defined as the sections of the functor `component_compl_functor` .  -/
SimpleGraph.end : {V : Type u} → (G : SimpleGraph V) → Set ((j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j)
-- Std.Sync.Broadcast
Std.Broadcast.Error.alreadyClosed.sizeOf_spec : sizeOf Std.Broadcast.Error.alreadyClosed = 1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.appHom_valid_glue : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K] {X : D} {Y : C}
  (f : Opposite.op X ⟶ Opposite.op (G.obj Y)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCoverDense.Types.appHom α X) (ℱ'.obj.map f) =
    CategoryTheory.CategoryStruct.comp (ℱ.map f) (α.app (Opposite.op Y))
-- Lean.Declaration
Lean.instBEqConstructorVal : BEq Lean.ConstructorVal
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurePreserving_iterate : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  (g : α →ₘ[μ] γ) {f : α → α} (hf : MeasureTheory.MeasurePreserving f μ μ) (n : ℕ),
  (fun x => x.compMeasurePreserving f hf)^[n] g = g.compMeasurePreserving f^[n] ⋯
-- Std.Time.Format.Basic
/-- Constructs a `FormatType` function to format a date into a string using a `GenericFormat`.
 -/
Std.Time.GenericFormat.formatBuilder : {aw : Std.Time.Awareness} → (format : Std.Time.GenericFormat aw) → Std.Time.FormatType String format.string
-- Mathlib.Order.SuccPred.Basic
WithBot.instPredOrder : {α : Type u_1} →
  [inst : PartialOrder α] → [inst_1 : PredOrder α] → [(a : α) → Decidable (Order.pred a = a)] → PredOrder (WithBot α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKey?.isSome = true
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mk : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] → (toAddSubgroup : AddSubgroup G) → IsOpen toAddSubgroup.carrier → OpenAddSubgroup G
-- Mathlib.Analysis.Asymptotics.Defs
/-- If `u = O(v)` along `l`, then `(u / v) * v = u` eventually at `l`.  -/
Asymptotics.IsBigO.eventually_mul_div_cancel : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
  u =O[l] v → u / v * v =ᶠ[l] u
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.OplaxTrans X Y)
  (θ : CategoryTheory.Oplax.OplaxTrans Y Z) {a b : B} (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.comp η θ).naturality f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) (θ.app b))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f))
            (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).inv)))
-- Std.Time.Date.Unit.Year
/-- Creates an `Offset` from an integer.
 -/
Std.Time.Year.Offset.ofInt : ℤ → Std.Time.Year.Offset
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α)))
  [i : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] {t : Set α},
  MeasureTheory.IsFundamentalDomain G t ν →
    ∀ {U : Set (Quotient (MulAction.orbitRel G α))},
      MeasurableSet U → μ U = ν (Quotient.mk (MulAction.orbitRel G α) ⁻¹' U ∩ t)
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.isCompact : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β},
  HasCompactSupport f → IsCompact (tsupport f)
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.subset_mapRange_neLocus : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] {M : α → Type u_3} [inst_1 : (a : α) → Zero (N a)]
  [inst_2 : (a : α) → Zero (M a)] [inst_3 : (a : α) → DecidableEq (N a)] [inst_4 : (a : α) → DecidableEq (M a)]
  (f g : Π₀ (a : α), N a) {F : (a : α) → N a → M a} (F0 : ∀ (a : α), F a 0 = 0),
  (DFinsupp.mapRange F F0 f).neLocus (DFinsupp.mapRange F F0 g) ⊆ f.neLocus g
-- Init.Data.FloatArray.Basic
/-- Reference implementation for `foldlM`  -/
FloatArray.foldlM : {β : Type v} →
  {m : Type v → Type w} →
    [Monad m] → (β → Float → m β) → β → (as : FloatArray) → optParam ℕ 0 → optParam ℕ as.size → m β
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.List.toArrayAux.eq_1 : ∀ {α : Type u_1} (x : Array α), [].toArrayAux x = x
-- Mathlib.Algebra.Group.Basic
/-- Composing two multiplications on the left by `y` then `x`
is equal to a multiplication on the left by `x * y`.
 -/
comp_mul_left : ∀ {α : Type u_1} [inst : Semigroup α] (x y : α), ((fun x_1 => x * x_1) ∘ fun x => y * x) = fun x_1 => x * y * x_1
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GCommRing.toGCommSemiring : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddCommMonoid ι] →
      [inst_1 : (i : ι) → AddCommGroup (A i)] → [self : DirectSum.GCommRing A] → DirectSum.GCommSemiring A