mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- If `P` is monotone w.r.t. restricting `domChart` and closed under congruence,
and `f` and `g` are eventually equal near `x`,
then `f` has property `P` at `x` if and only if `g` has property `P` at `x`.  -/
Manifold.LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  Manifold.IsLocalSourceTargetProperty P →
    f =ᶠ[nhds x] g → (Manifold.LiftSourceTargetPropertyAt I J n f x P ↔ Manifold.LiftSourceTargetPropertyAt I J n g x P)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_C_mul_X_pow_le : ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).natDegree ≤ n
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.induction : ∀ {R : Type u_1} [inst : Semiring R] {motive : SkewPolynomial R → Prop} (p : SkewPolynomial R),
  motive 0 →
    (∀ (n : ℕ) (r : R) (q : SkewPolynomial R),
        n ∉ q.support → r ≠ 0 → motive q → motive ((SkewPolynomial.monomial n) r + q)) →
      motive p
-- Lean.Expr
/-- Replace free (or meta) variables `xs` with loose bound variables,
with `xs` ordered from outermost to innermost de Bruijn index.

For example, `e := f x y` with `xs := #[x, y]` goes to `f #1 #0`,
whereas `e := f x y` with `xs := #[y, x]` goes to `f #0 #1`.

Careful, this function does not instantiate assigned meta variables.  -/
Lean.Expr.abstract : Lean.Expr → Array Lean.Expr → Lean.Expr
-- Init.Data.SInt.Lemmas
Int16.toInt32_ne_neg_one : ∀ (a : Int16), a ≠ -1 → a.toInt32 ≠ -1
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_ofFunctionField : ∀ {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.LocallyOfFiniteType sY] (f : AlgebraicGeometry.Spec X.functionField ⟶ Y)
  (h :
    CategoryTheory.CategoryStruct.comp f sY =
      CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) sX),
  (AlgebraicGeometry.Scheme.RationalMap.ofFunctionField sX sY f h).fromFunctionField = f
-- Lean.Elab.DeclModifiers
Lean.Elab.ComputeKind.meta : Lean.Elab.ComputeKind
-- Mathlib.Algebra.Group.TransferInstance
Equiv.one_def : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : One β], 1 = e.symm 1
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.isUnit_of_associated : ∀ {R : Type u} [inst : CommSemiring R] {x y : R}, IsCoprime x y → Associated x y → IsUnit x ∧ IsUnit y
-- Mathlib.Control.Monad.Writer
WriterT.runThe : {M : Type u → Type v} → {α : Type u} → (ω : Type u) → WriterT ω M α → M (α × ω)
-- Init.Data.String.Iterator
/-- The current UTF-8 byte position in the string `s`.

This position is not guaranteed to be valid for the string. If the position is not valid, then the
current character is `(default : Char)`, similar to `String.get` on an invalid position.
 -/
String.Legacy.Iterator.pos : String.Legacy.Iterator → String.Pos.Raw
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α} {hc : t.minD fallback ∈ t}, t.get (t.minD fallback) hc = t.minD fallback
-- Init.Data.Array.Subarray
/-- The starting index is no later than the ending index.

The ending index is exclusive. If the starting and ending indices are equal, then the subarray is
empty.
 -/
Std.Slice.Internal.SubarrayData.start_le_stop : ∀ {α : Type u} (self : Std.Slice.Internal.SubarrayData α), self.start ≤ self.stop
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx.originalMaxHeartbeats : Lean.Elab.Tactic.Try.Ctx → ℕ
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.mk : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [toFlat : Module.Flat R M], (∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤) → Module.FaithfullyFlat R M
-- Mathlib.Topology.Order.Lattice
Continuous.finset_sup' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} (hne : s.Nonempty),
  (∀ i ∈ s, Continuous (f i)) → Continuous (s.sup' hne f)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- The split epi `X.chainComplex R ⟶ X.normalizedChainComplex R`.  -/
SSet.toNormalizedChainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] → (X : SSet) → (R : C) → X.chainComplex R ⟶ X.normalizedChainComplex R
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_sdiff_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Icc b a \ {a} = Set.Ico b a
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_neg : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) (x : ↥s), ↑(-x) = -↑x
-- Mathlib.Topology.Order.LeftRight
nhdsWithinLE_sup_nhdsWithinGE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {s : Set α} (a : α),
  nhdsWithin a (s ∩ Set.Iic a) ⊔ nhdsWithin a (s ∩ Set.Ici a) = nhdsWithin a s
-- Mathlib.Order.Filter.Map
Filter.mem_seq_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter (α → β)} {g : Filter α} {s : Set β},
  s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s
-- Lean.Meta.SameCtorUtils
_private.Lean.Meta.SameCtorUtils.0.Lean.Meta.withSharedCtorIndices.go : {α : Type} →
  Lean.Expr →
    (Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) →
      Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → List Bool → List Lean.Expr → Array Lean.Expr → Lean.MetaM α
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Expr.updateForallS! : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_two_pi_sub : ∀ (x : ℝ), Real.sin (2 * Real.pi - x) = -Real.sin x
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.congr_d : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {d d' : M.Derivation φ}, d = d' → ∀ {X : Dᵒᵖ} (b : ↑(R.obj X)), d.d b = d'.d b
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- radius of the sphere; not required to be positive  -/
EuclideanGeometry.Sphere.radius : {P : Type u_2} → [inst : MetricSpace P] → EuclideanGeometry.Sphere P → ℝ
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.pow : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : Module.End K M}
  [FiniteDimensional K M], f.IsSemisimple → ∀ (n : ℕ), (f ^ n).IsSemisimple
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The orthocenter lies in the affine span.  -/
Affine.Triangle.orthocenter_mem_affineSpan : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P), t.orthocenter ∈ affineSpan ℝ (Set.range t.points)
-- Init.Data.SInt.Bitwise
ISize.xor_self : ∀ {a : ISize}, a ^^^ a = 0
-- Mathlib.RingTheory.Flat.Equalizer
Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {A : Type u_4}
  [inst_7 : CommRing A] [inst_8 : Algebra R A] [inst_9 : Module.Flat R T] (h₁ : Function.Surjective ⇑(algebraMap S T))
  (x : A) (y : S) (z : ↥(RingHom.ker (algebraMap S T))),
  ↑((Algebra.kerTensorProductMapIdToAlgHomEquiv R S T A h₁).symm (x ⊗ₜ[R] y ⊗ₜ[S] z)) = x ⊗ₜ[R] (y * ↑z)
-- Init.Data.List.BasicAux
/-- Returns the first element in the list. If the list is empty, panics and returns `default`.

Safer alternatives include:
* `List.head`, which requires a proof that the list is non-empty,
* `List.head?`, which returns an `Option`, and
* `List.headD`, which returns an explicitly-provided fallback value on empty lists.
 -/
List.head! : {α : Type u_1} → [Inhabited α] → List α → α
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → Array α → Sort u_2) (x : α) (xs : List α) (n : ℕ) (acc : Array α)
  (h_1 : (x : ℕ) → (x_1 : Array α) → motive [] x x_1)
  (h_2 : (head : α) → (xs : List α) → (acc : Array α) → motive (head :: xs) 0 acc)
  (h_3 : (x : α) → (xs : List α) → (n : ℕ) → (acc : Array α) → motive (x :: xs) n.succ acc),
  (match x :: xs, n.succ, acc with
    | [], x, x_1 => h_1 x x_1
    | head :: xs, 0, acc => h_2 head xs acc
    | x :: xs, n.succ, acc => h_3 x xs n acc) =
    h_3 x xs n acc
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.orthogonalDecomposition.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  K.orthogonalDecomposition =
    { toLinearEquiv := (K.prodEquivOfIsCompl Kᗮ ⋯).symm.trans (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm, norm_map' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- An embedding gives rise to a copy.  -/
SimpleGraph.Embedding.toCopy : {α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → A ↪g B → A.Copy B
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaCurry_apply : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) (i : ι) (j : α i),
  (f.sigmaCurry i) j = f ⟨i, j⟩
-- Mathlib.Data.List.Palindrome
List.Palindrome.map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} (f : α → β), l.Palindrome → (List.map f l).Palindrome
-- Mathlib.Data.Nat.Squarefree
/-- Returns the smallest prime factor `p` of `n` such that `p^2 ∣ n`, or `none` if there is no
such `p` (that is, `n` is squarefree). See also `Nat.squarefree_iff_minSqFac`.  -/
Nat.minSqFac : ℕ → Option ℕ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instSDiff : {α : Type u_1} → [inst : MeasurableSpace α] → SDiff (Subtype MeasurableSet)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet_mixedEmbedding : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.RingOfIntegers K}
  (hx : (NumberField.mixedEmbedding K) ↑x ∈ NumberField.mixedEmbedding.fundamentalCone.integerSet K),
  ↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet ⟨(NumberField.mixedEmbedding K) ↑x, hx⟩) = x
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).map f = ((Opposite.unop F).map f.op).op
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.str.injEq : ∀ (val val_1 : String), (Lean.Compiler.LCNF.LitValue.str val = Lean.Compiler.LCNF.LitValue.str val_1) = (val = val_1)
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.map_injective_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {I : Type u_3} {e : I → R},
  Function.Injective ⇑f → (OrthogonalIdempotents (⇑f ∘ e) ↔ OrthogonalIdempotents e)
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.right_mem : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLink e x y → y ∈ G.vertexSet
-- Init.System.IOError
/-- A protocol error occurred.

This corresponds to the POSIX errors `EPROTO`, `EPROTONOSUPPORT`, and `EPROTOTYPE`.
 -/
IO.Error.protocolError : UInt32 → String → IO.Error
-- Mathlib.Algebra.Lie.Basis.Basic
/-- A basis for a semisimple Lie algebra distinguishes a natural Cartan subalgebra and a base
for the associated root system.  -/
LieAlgebra.Basis : (ι : Type u_1) →
  {R : Type u_2} →
    {L : Type u_3} →
      [Finite ι] →
        [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieSubalgebra R L → Type (max u_1 u_3)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.isSemilinearSet_setOfFloorNeg : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsSemilinearSet (IsProperLinearSet.setOfFloorNeg✝ hs)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C}
  [inst_1 : SizeOf C] (f : X.I → Y.I) (φ : (i : X.I) → X.obj i ⟶ Y.obj (f i)), sizeOf { f := f, φ := φ } = 1
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.pathComposition_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Paths C} (f : X ⟶ Y),
  (CategoryTheory.pathComposition C).map f = CategoryTheory.composePath f
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.sum_f : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} (s : SingularManifold X k I) (t : SingularManifold X k I),
  (s.sum t).f = Sum.elim s.f t.f
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_surjective : ∀ {M : Type u_1} [inst : Monoid M], Function.Surjective Submonoid.units
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodAssoc_symm_apply_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] (x : M),
  (MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inl x) = Monoid.Coprod.inl (Monoid.Coprod.inl x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α} {hc : t.contains km = true}, t.maxKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- This is a cofork which is helpful for establishing monadicity: the morphism from the Beck
coequalizer to this cofork is the unit for the adjunction on the comparison functor.
 -/
CategoryTheory.Monad.MonadicityInternal.unitCofork : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            {adj : F ⊣ G} →
              (A : adj.toMonad.Algebra) →
                [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] →
                  CategoryTheory.Limits.Cofork (G.map (F.map A.a)) (G.map (adj.counit.app (F.obj A.A)))
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- the sign of the vertical differential in the total complex  -/
TotalComplexShape.ε₂ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) → (c₁₂ : ComplexShape I₁₂) → [self : TotalComplexShape c₁ c₂ c₁₂] → I₁ × I₂ → ℤˣ
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_eq_top_of_not_reachable : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, ¬G.Reachable u v → G.edist u v = ⊤
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.mk.injEq : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (toPartialEquiv : PartialEquiv X X)
  (isDecompOn' : ∃ S, Equidecomp.IsDecompOn (↑toPartialEquiv) toPartialEquiv.source S)
  (toPartialEquiv_1 : PartialEquiv X X)
  (isDecompOn'_1 : ∃ S, Equidecomp.IsDecompOn (↑toPartialEquiv_1) toPartialEquiv_1.source S),
  ({ toPartialEquiv := toPartialEquiv, isDecompOn' := isDecompOn' } =
      { toPartialEquiv := toPartialEquiv_1, isDecompOn' := isDecompOn'_1 }) =
    (toPartialEquiv = toPartialEquiv_1)
-- Mathlib.Data.Finset.Sort
Finset.sorted_zero_eq_min' : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {h : 0 < (s.sort fun a b => a ≤ b).length},
  (s.sort fun a b => a ≤ b)[0] = s.min' ⋯
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ElimStatus.failure.injEq : ∀ (ts ts_1 : List Lean.Expr),
  (Mathlib.Tactic.Choose.ElimStatus.failure ts = Mathlib.Tactic.Choose.ElimStatus.failure ts_1) = (ts = ts_1)
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- Given an embedding `e : c.Embedding c'` of complex shapes, this is
the functor `HomologicalComplex C c ⥤ HomologicalComplex C c'` which
extend complexes along `e`: the extended complexes are zero
in the degrees that are not in the image of `e.f`.  -/
ComplexShape.Embedding.extendFunctor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        c.Embedding c' →
          (C : Type u_3) →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [CategoryTheory.Limits.HasZeroObject C] →
                [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  CategoryTheory.Functor (HomologicalComplex C c) (HomologicalComplex C c')
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- The underlying topological space is T2.  -/
CompHausLike.is_hausdorff : ∀ {P : TopCat → Prop} (self : CompHausLike P), T2Space ↑self.toTop
-- Mathlib.Order.Filter.Pointwise
Filter.le_add_iff : ∀ {α : Type u_2} [inst : Add α] {f g h : Filter α}, h ≤ f + g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s + t ∈ h
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts properly on `X`, then the quotient space is Hausdorff (T2).  -/
t2Space_quotient_addAction_of_properVAdd : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperVAdd G X], T2Space (Quotient (AddAction.orbitRel G X))
-- Mathlib.MeasureTheory.Measure.Regular
/-- Any sigma finite measure on a `σ`-compact pseudometrizable space is inner regular.  -/
MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite : ∀ {X : Type u_3} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [SigmaCompactSpace X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite μ],
  μ.InnerRegular
-- Std.Http.Protocol.H1.Parser
Std.Http.Protocol.H1.TakeResult.complete : ByteSlice → Std.Http.Protocol.H1.TakeResult
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.lintegral_enorm_neg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, ∫⁻ (a : α), ‖(-f) a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ
-- Init.Sym.Lemmas
Lean.Sym.BitVec.lt_eq_true : ∀ {n : ℕ} (a b : BitVec n), decide (a < b) = true → (a < b) = True
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.contains.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k' : α) →
                (v : β k') →
                  (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)) →
            motive t
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.mapHomologicalComplexObjIso_inv_map_π₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  {D : Type u_3} [inst_5 : CategoryTheory.Category.{v_2, u_3} D] [inst_6 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_7 : H.Additive]
  [inst_8 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj K).X i)
        (((H.mapHomologicalComplex c).obj K).X i)]
  [inst_9 : ((H.mapHomologicalComplex c).obj K).HasPathObject]
  [inst_10 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)
        (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)]
  [inst_11 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift
        (CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op))
        (-CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op)))]
  [inst_12 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.op.mapHomologicalComplex c.symm).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K.op)
          (-CategoryTheory.CategoryStruct.id K.op)))]
  [inst_13 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.op.X i) (K.op.X i)] (hc : ∀ (i : α), ∃ j, c.Rel i j)
  {Z : HomologicalComplex D c} (h : (H.mapHomologicalComplex c).obj K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.mapHomologicalComplexObjIso K H hc).inv
      (CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex c).map (HomologicalComplex.pathObject.π₁ K)) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.π₁ ((H.mapHomologicalComplex c).obj K)) h
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.top_prod_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N], ⊤.prod ⊤ = ⊤
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instIsAffineHomDescScheme : ∀ {U V X : AlgebraicGeometry.Scheme} (f : U ⟶ X) (g : V ⟶ X) [AlgebraicGeometry.IsAffineHom f]
  [AlgebraicGeometry.IsAffineHom g], AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.coprod.desc f g)
-- Lean.DocString.Types
Lean.Doc.Inline.linebreak.inj : ∀ {i : Type u} {string string_1 : String},
  Lean.Doc.Inline.linebreak string = Lean.Doc.Inline.linebreak string_1 → string = string_1
-- Mathlib.RingTheory.Ideal.Maps
/-- The map on ideals induced by a surjective map preserves inclusion.  -/
Ideal.orderEmbeddingOfSurjective : {R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : FunLike F R S] → (f : F) → [RingHomClass F R S] → Function.Surjective ⇑f → Ideal S ↪o Ideal R
-- Mathlib.Data.Set.Basic
/-- **Alias** of the reverse direction of `Set.compl_ssubset_univ`. -/
Set.Nonempty.compl_ssubset_univ : ∀ {α : Type u} {s : Set α}, s.Nonempty → sᶜ ⊂ Set.univ