mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Given a diagram `D` of limit cones over the `F.obj j`, and a cone over `uncurry.obj F`,
we can construct a cone over the diagram consisting of the cone points from `D`.
 -/
CategoryTheory.Limits.coneOfConeUncurry : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              {D : CategoryTheory.Limits.DiagramOfCones F} →
                ((j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) →
                  CategoryTheory.Limits.Cone (CategoryTheory.Functor.uncurry.obj F) →
                    CategoryTheory.Limits.Cone D.conePoints
-- Init.Core
instInhabitedTask.default : {α : Type u} → [Inhabited α] → Task α
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.prod'CompSnd_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor A C) (X : A), (F.prod'CompSnd G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj X)
-- Lean.Compiler.LCNF.Basic
/-- Return true iff `c.size ≤ n`  -/
Lean.Compiler.LCNF.Code.sizeLe : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → ℕ → Bool
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.gt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.gt = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.gt = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.gt with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_3 ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- If `V` is a `2`-truncated simplicial sets, this is the family of
morphisms in `V.HomotopyCategory` corresponding to the edges of `V`.
(Any morphism in `V.HomotopyCategory` is in the multiplicative closure
of this family of morphisms, see `multiplicativeClosure_morphismPropertyHomMk`.)  -/
SSet.Truncated.HomotopyCategory.morphismPropertyHomMk : (V : SSet.Truncated 2) → CategoryTheory.MorphismProperty V.HomotopyCategory
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instAdditiveTruncGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), (t.truncGE n).Additive
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.nontrivial : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) [Nontrivial R], Nontrivial ↥s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_erase_eq_of_not_compare_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).maxKey? = t.maxKey?
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_sub : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g g₂ : M [⋀^ι]→ₗ[R] N'), ↑(g - g₂) = ↑g - ↑g₂
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ z₁_1 : CochainComplex.HomComplex.Cochain F G n₁),
  z₁ = z₁_1 →
    ∀ (z₂ z₂_1 : CochainComplex.HomComplex.Cochain G K n₂),
      z₂ = z₂_1 → ∀ (h : n₁ + n₂ = n₁₂) (T : CochainComplex.HomComplex.Triplet n₁₂), z₁.comp z₂ h T = z₁_1.comp z₂_1 h T
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- An additive group topology on an additive group `α` is a topology for which addition and
negation are continuous.  -/
AddGroupTopology : (α : Type u) → [AddGroup α] → Type u
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.op_boundaryGE_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {j : ι},
  e.op.BoundaryGE j ↔ e.BoundaryLE j
-- Mathlib.MeasureTheory.Group.Measure
/-- **Alias** of `MeasureTheory.tendsto_measure_smul_sdiff_isCompact_isClosed`.

---

Continuity of the measure of translates of a compact set:
Given a closed compact set `k` in a topological group,
the measure of `g • k \ k` tends to zero as `g` tends to `1`.  -/
MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [μ.InnerRegularCompactLTTop] {k : Set G},
  IsCompact k → IsClosed k → Filter.Tendsto (fun g => μ (g • k \ k)) (nhds 1) (nhds 0)
-- Mathlib.AlgebraicGeometry.ResidueField
/-- The residue field of `X` at a point `x` is the residue field of the stalk of `X`
at `x`.  -/
AlgebraicGeometry.Scheme.residueField : (X : AlgebraicGeometry.Scheme) → ↥X → CommRingCat
-- Mathlib.Order.SymmDiff
symmDiff_le : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b ⊔ c → b ≤ a ⊔ c → symmDiff a b ≤ c
-- Mathlib.Topology.UnitInterval
unitInterval.toNNReal_one : unitInterval.toNNReal 1 = 1
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  ModuleCat.Hom.hom S.moduleCatLeftHomologyData.f' = S.moduleCatToCycles
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- Continuous linear equivalences between the domains and the codomains
generate a continuous linear equivalence between the spaces of continuous alternating maps.  -/
ContinuousLinearEquiv.continuousAlternatingMapCongr : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {E' : Type u_3} →
      {F : Type u_4} →
        {G : Type u_5} →
          {ι : Type u_6} →
            [inst : NormedField 𝕜] →
              [inst_1 : AddCommGroup E] →
                [inst_2 : Module 𝕜 E] →
                  [inst_3 : TopologicalSpace E] →
                    [inst_4 : AddCommGroup E'] →
                      [inst_5 : Module 𝕜 E'] →
                        [inst_6 : TopologicalSpace E'] →
                          [inst_7 : AddCommGroup F] →
                            [inst_8 : Module 𝕜 F] →
                              [inst_9 : TopologicalSpace F] →
                                [inst_10 : IsTopologicalAddGroup F] →
                                  [inst_11 : ContinuousConstSMul 𝕜 F] →
                                    [inst_12 : AddCommGroup G] →
                                      [inst_13 : Module 𝕜 G] →
                                        [inst_14 : TopologicalSpace G] →
                                          [inst_15 : IsTopologicalAddGroup G] →
                                            [inst_16 : ContinuousConstSMul 𝕜 G] →
                                              (E ≃L[𝕜] E') → (F ≃L[𝕜] G) → E [⋀^ι]→L[𝕜] F ≃L[𝕜] E' [⋀^ι]→L[𝕜] G
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_sup_comap_of_surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Surjective ⇑f →
    ∀ (S T : L.Substructure N),
      FirstOrder.Language.Substructure.map f
          (FirstOrder.Language.Substructure.comap f S ⊔ FirstOrder.Language.Substructure.comap f T) =
        S ⊔ T
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- If `f` is a smooth partition of unity on a set `s : Set M` and `g : ι → M → F` is a family of
functions such that `g i` is $C^n$ smooth at every point of the topological support of `f i`, then
the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the whole manifold.  -/
SmoothPartitionOfUnity.contMDiff_finsum_smul : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
  (f : SmoothPartitionOfUnity ι I M s) {n : ℕ∞} {g : ι → M → F},
  (∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), ContMDiffAt I (modelWithCornersSelf ℝ F) (↑n) (g i) x) →
    ContMDiff I (modelWithCornersSelf ℝ F) ↑n fun x => ∑ᶠ (i : ι), (f i) x • g i x
-- Mathlib.Algebra.Order.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : LinearOrderedCommGroupWithZero B] {f : A →*₀ B}
  (a : f.ValueGroup₀ˣ), 0 < MonoidWithZeroHom.ValueGroup₀.embedding ↑a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α},
  k ∈ t → t.get? k = some k
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
/-- If `f` is a morphism of monoid objects internal to `Cᴹᵒᵖ`,
so is `f.unmop`.  -/
MonObj.unmop_isMonHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : Cᴹᵒᵖ}
  [inst_2 : CategoryTheory.MonObj M] {N : Cᴹᵒᵖ} [inst_3 : CategoryTheory.MonObj N] (f : M ⟶ N)
  [CategoryTheory.IsMonHom f], CategoryTheory.IsMonHom f.unmop
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `s` is a measurable set, a weakly regular measure `μ` is finite on `s`, and `ε` is a positive
number, then there exist a closed set `K ⊆ s` such that `μ s < μ K + ε`.  -/
MeasurableSet.exists_isClosed_lt_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.WeaklyRegular] {s : Set α},
  MeasurableSet s → μ s ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ s, IsClosed K ∧ μ s < μ K + ε
-- Mathlib.Data.Rel
SetRel.mem_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S : SetRel β γ} {a : α} {c : γ},
  (a, c) ∈ R.comp S ↔ ∃ b, (a, b) ∈ R ∧ (b, c) ∈ S
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- Open immersions are étale.  -/
AlgebraicGeometry.Etale.instOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.Etale f
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isZero_truncGE_obj_of_isLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ (X : C) [t.IsLE X n₀], CategoryTheory.Limits.IsZero ((t.truncGE n₁).obj X)
-- Batteries.Data.List.Basic
List.takeD_succ : ∀ {α : Type u_1} {n : ℕ} (l : List α) (a : α), List.takeD (n + 1) l a = l.head?.getD a :: List.takeD n l.tail a
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended_le_one_of_le_one : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N),
  ∀ I ≤ 1, FractionalIdeal.extended L hf I ≤ 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n),
  ∀ curr ≤ n - 1,
    ∀ (acc : aig.RefVec w) (lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool),
      (∀ (idx : ℕ) (hidx : idx < w),
          ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.sshiftRightRec rhs curr).getLsbD idx) →
        (∀ (idx : ℕ) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx) →
          ∀ (idx : ℕ) (hidx : idx < w),
            ⟦assign,
                { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go aig distance curr acc).aig,
                  ref :=
                    (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go aig distance curr acc).vec.get idx
                      hidx }⟧ =
              (lhs.sshiftRightRec rhs (n - 1)).getLsbD idx
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isEmbedding_coe_of_bot : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  Topology.IsEmbedding DFunLike.coe
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- To show two wide pullback cones are isomorphic, it suffices to give a compatible isomorphism
of their cone points.  -/
CategoryTheory.Limits.WidePullbackCone.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_2} →
      {X : C} →
        {Y : ι → C} →
          {f : (i : ι) → Y i ⟶ X} →
            {s t : CategoryTheory.Limits.WidePullbackCone f} →
              (e : s.pt ≅ t.pt) →
                autoParam (CategoryTheory.CategoryStruct.comp e.hom t.base = s.base)
                    CategoryTheory.Limits.WidePullbackCone.ext._auto_1 →
                  autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp e.hom (t.π i) = s.π i)
                      CategoryTheory.Limits.WidePullbackCone.ext._auto_3 →
                    (s ≅ t)
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (p.projection q hpq) x = ↑((p.projectionOnto q hpq) x)
-- Lean.Elab.Coinductive
Lean.Elab.Command.instInhabitedCoinductiveElabData.default : Lean.Elab.Command.CoinductiveElabData
-- Lean.Elab.Command
Lean.Elab.Command.liftIO : {α : Type} → IO α → Lean.Elab.Command.CommandElabM α
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `posPart`. `a⁺` is always nonnegative, and positive if `a` is.  -/
Mathlib.Meta.Positivity.evalPosPart : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonneg_iff_left_nonneg_of_pos : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R],
  0 < b → (0 ≤ a * b ↔ 0 ≤ a)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The Cartesian product of two multilinear maps, as a multilinear map.  -/
MultilinearMap.prod : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        {M₃ : Type v₃} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : (i : ι) → Module R (M₁ i)] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module R M₃] →
                        MultilinearMap R M₁ M₂ → MultilinearMap R M₁ M₃ → MultilinearMap R M₁ (M₂ × M₃)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.instConcreteCategoryMulHomCarrier : CategoryTheory.ConcreteCategory MagmaCat fun x1 x2 => ↑x1 →ₙ* ↑x2
-- Init.Data.UInt.Lemmas
UInt64.toNat_zero : UInt64.toNat 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Complex.sinh` is complex analytic.  -/
Complex.analyticWithinAt_sinh : ∀ {x : ℂ} {s : Set ℂ}, AnalyticWithinAt ℂ Complex.sinh s x
-- Init.Data.Fin.Lemmas
Fin.add_zero : ∀ {n : ℕ} [inst : NeZero n] (k : Fin n), k + 0 = k
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.toCycles_descCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ}
  (x : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ A)
  (hx : CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0),
  CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (X.descCycles f g fg h x hx) = x
-- Mathlib.Algebra.Homology.Localization
HomologicalComplex.homologyFunctor_inverts_quasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.CategoryWithHomology C] (i : ι),
  (HomologicalComplex.quasiIso C c).IsInvertedBy (HomologicalComplex.homologyFunctor C c i)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.emultiplicity_le_of_multiplicity_le : ∀ {α : Type u_1} [inst : Monoid α] {a b : α},
  FiniteMultiplicity a b → ∀ {n : ℕ}, multiplicity a b ≤ n → emultiplicity a b ≤ ↑n
-- Mathlib.Order.SetNotation
/-- Union of a set of sets.  -/
Set.sUnion : {α : Type u} → Set (Set α) → Set α
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Ioo : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a < b → frontier (Set.Ioo a b) = {a, b}
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.codisjoint_one_iff : ∀ (R : Type u) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (I : Ideal A),
  Codisjoint 1 (Submodule.restrictScalars (↥S) I) ↔
    Codisjoint (Subalgebra.toSubmodule S) (Submodule.restrictScalars R I)
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_3.eq_1 : ∀ {α : Type u_1} (motive : List (Computation α) × Stream'.WSeq (Computation α) → Sort u_2) (l : List (Computation α))
  (S : Stream'.WSeq (Computation α))
  (h_1 : (l : List (Computation α)) → (S : Stream'.WSeq (Computation α)) → motive (l, S)),
  (match (l, S) with
    | (l, S) => h_1 l S) =
    h_1 l S
-- Mathlib.Topology.Order.Compact
cocompact_le_atBot : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTop α] [CompactIccSpace α],
  Filter.cocompact α ≤ Filter.atBot
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.contra : ∀ {a b k : ℤ}, 0 < k → -k < b → b < 0 → a * k + b = 0 → False
-- Mathlib.Data.List.Cycle
Cycle.Subsingleton.nodup : ∀ {α : Type u_1} {s : Cycle α}, s.Subsingleton → s.Nodup
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.hom₂_ofHom₂ : ∀ {R : Type u_1} [inst : CommSemiring R] {M N P : SemimoduleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P),
  SemimoduleCat.Hom.hom₂ (SemimoduleCat.ofHom₂ f) = f
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitIsoSwapCompColim_inv_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]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K),
  (CategoryTheory.Limits.colimitIsoSwapCompColim G).inv.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (G.flipIsoCurrySwapUncurry.inv.app X))
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation G X).inv
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inlCokernelCofork_π : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.biprod.inlCokernelCofork X Y) = CategoryTheory.Limits.biprod.snd
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.length_quotient_pow_maximalIdeal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (n : ℕ),
  Module.length R (R ⧸ IsLocalRing.maximalIdeal R ^ n) = ↑n
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd'_hom_app_f' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ),
  ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n =
    (HomologicalComplex.XIsoOfEq K ⋯).hom
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.eq_toPath_comp_of_length_eq_succ : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) {n : ℕ},
  p.length = n + 1 → ∃ c f q, ∃ (_ : q.length = n), p = f.toPath.comp q
-- Init.Data.List.Attach
List.getLast_attachWith : ∀ {α : Type u_1} {P : α → Prop} {xs : List α} {H : ∀ a ∈ xs, P a} (h : xs.attachWith P H ≠ []),
  (xs.attachWith P H).getLast h = ⟨xs.getLast ⋯, ⋯⟩
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeWhile_eq_sliceTo_skipPrefixWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  s.takeWhile pat = s.sliceTo (s.skipPrefixWhile pat)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_one : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α], Equiv.Perm.sign 1 = 1
-- Mathlib.Topology.NhdsKer
specializes_iff_nhdsKer_subset : ∀ {X : Type u_2} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ nhdsKer {x} ⊆ nhdsKer {y}
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.of_quotient_center_nilpotent`.

---

If the quotient by `center G` is nilpotent, then so is G.  -/
of_quotient_center_nilpotent : ∀ {G : Type u_1} [inst : Group G], Group.IsNilpotent (G ⧸ Subgroup.center G) → Group.IsNilpotent G
-- Mathlib.Topology.Subpath
Path.range_subpath_of_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval),
  t₀ ≤ t₁ → Set.range ⇑(γ.subpath t₀ t₁) = ⇑γ '' Set.Icc t₀ t₁
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.prod_one_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {f : ι → R} (s : Finset ι),
  ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.mapExactFunctor_mk₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Abelian.Ext.mapExactFunctor F (CategoryTheory.Abelian.Ext.mk₀ f) =
    CategoryTheory.Abelian.Ext.mk₀ (F.map f)
-- Mathlib.GroupTheory.Divisible
/-- **Alias** of `RootableBy.surjective_pow`. -/
pow_left_surj_of_rootableBy : ∀ (A : Type u_1) (α : Type u_2) [inst : Monoid A] [inst_1 : Pow A α] [inst_2 : Zero α] [RootableBy A α] {n : α},
  n ≠ 0 → Function.Surjective fun a => a ^ n
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.weakEquivalences_over_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence f ↔ HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Over.Hom.left f)
-- Lean.Elab.InfoTree.Main
Lean.Elab.MacroExpansionInfo.format : Lean.Elab.ContextInfo → Lean.Elab.MacroExpansionInfo → IO Std.Format