mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.mk.injEq : ∀ {Ω : Type w} (obj : Set Ω) (hom : ↑obj → ↑obj → Set Ω) (id : (X : ↑obj) → ↑(hom X X))
  (comp : {X Y Z : ↑obj} → ↑(hom X Y) → ↑(hom Y Z) → ↑(hom X Z))
  (id_comp :
    autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp (id X) f = f) CategoryTheory.SmallCategoryOfSet.id_comp._autoParam)
  (comp_id :
    autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp f (id Y) = f) CategoryTheory.SmallCategoryOfSet.comp_id._autoParam)
  (assoc :
    autoParam
      (∀ {X Y Z T : ↑obj} (f : ↑(hom X Y)) (g : ↑(hom Y Z)) (h : ↑(hom Z T)), comp (comp f g) h = comp f (comp g h))
      CategoryTheory.SmallCategoryOfSet.assoc._autoParam)
  (obj_1 : Set Ω) (hom_1 : ↑obj_1 → ↑obj_1 → Set Ω) (id_1 : (X : ↑obj_1) → ↑(hom_1 X X))
  (comp_1 : {X Y Z : ↑obj_1} → ↑(hom_1 X Y) → ↑(hom_1 Y Z) → ↑(hom_1 X Z))
  (id_comp_1 :
    autoParam (∀ {X Y : ↑obj_1} (f : ↑(hom_1 X Y)), comp_1 (id_1 X) f = f)
      CategoryTheory.SmallCategoryOfSet.id_comp._autoParam)
  (comp_id_1 :
    autoParam (∀ {X Y : ↑obj_1} (f : ↑(hom_1 X Y)), comp_1 f (id_1 Y) = f)
      CategoryTheory.SmallCategoryOfSet.comp_id._autoParam)
  (assoc_1 :
    autoParam
      (∀ {X Y Z T : ↑obj_1} (f : ↑(hom_1 X Y)) (g : ↑(hom_1 Y Z)) (h : ↑(hom_1 Z T)),
        comp_1 (comp_1 f g) h = comp_1 f (comp_1 g h))
      CategoryTheory.SmallCategoryOfSet.assoc._autoParam),
  ({ obj := obj, hom := hom, id := id, comp := comp, id_comp := id_comp, comp_id := comp_id, assoc := assoc } =
      { obj := obj_1, hom := hom_1, id := id_1, comp := comp_1, id_comp := id_comp_1, comp_id := comp_id_1,
        assoc := assoc_1 }) =
    (obj = obj_1 ∧ hom ≍ hom_1 ∧ id ≍ id_1 ∧ comp ≍ comp_1)
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- `IsCompressed u v s` expresses that `s` is UV-compressed.  -/
UV.IsCompressed : {α : Type u_1} →
  [inst : GeneralizedBooleanAlgebra α] →
    [DecidableRel Disjoint] → [DecidableLE α] → [DecidableEq α] → α → α → Finset α → Prop
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.comapEquiv_symm : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (e : R ≃+* S),
  (PrimeSpectrum.comapEquiv e).symm = PrimeSpectrum.comapEquiv e.symm
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart_sub : ∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ],
  (s - t).singularPart μ = s.singularPart μ - t.singularPart μ
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- Two equal relative morphisms are homotopic.  -/
SSet.RelativeMorphism.Homotopy.ofEq : {X Y : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} → {φ : A.toSSet ⟶ B.toSSet} → {f g : SSet.RelativeMorphism A B φ} → f = g → f.Homotopy g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.WeierstrassCurve.Jacobian.toAffine_slope_of_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 →
        W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3) =
          (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) / (P 2 * Q 2 * WeierstrassCurve.Jacobian.addZ P Q)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.ext : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] {f g : A →⋆ₙₐ[R] B}, (∀ (x : A), f x = g x) → f = g
-- Mathlib.Topology.Maps.Strict.Basic
/-- Assume that `g : Y → Z` is an embedding. Then `f : X → Y` is strict
if and only if `g ∘ f` is strict.  -/
Topology.IsEmbedding.isStrictMap_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z},
  Topology.IsEmbedding g → (Topology.IsStrictMap f ↔ Topology.IsStrictMap (g ∘ f))
-- Mathlib.Data.FunLike.Basic
DFunLike.toCoeFun : {F : Sort u_1} → {α : Sort u_2} → {β : α → Sort u_3} → [i : DFunLike F α β] → CoeFun F fun x => (a : α) → β a
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_of_one_lt_sumInv_aux : ∀ {pqr : List ℕ+}, pqr.SortedLE → pqr.length = 3 → 1 < ADEInequality.sumInv ↑pqr → ADEInequality.Admissible ↑pqr
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.GrothendieckTopology.isClosed_χ_app_apply_of_isSheaf_of_isSeparated : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) [CategoryTheory.Mono m],
  CategoryTheory.Presieve.IsSheaf J F →
    CategoryTheory.Presieve.IsSeparated J G →
      ∀ (X : Cᵒᵖ) (x : G.obj X),
        J.IsClosed ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Presheaf.χ m).app X)) x)
-- Mathlib.RingTheory.HopkinsLevitzki
IsSemiprimaryRing.induction : ∀ (R₀ : Type u_1) (R : Type u_2) (M : Type u) [inst : Ring R₀] [inst_1 : Ring R] [inst_2 : Module R₀ R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R₀ M] [inst_5 : Module R M] [IsScalarTower R₀ R M] [IsSemiprimaryRing R]
  {P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop},
  (∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
      [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑(Ring.jacobson R) → P M) →
    (∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
        [inst_11 : IsScalarTower R₀ R M],
        have N := Ring.jacobson R • ⊤;
        P ↥N → P (M ⧸ N) → P M) →
      P M
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.mkStrictMonoAux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
/-- Right multiplication by a unitary as a linear isometric equivalence.  -/
Unitary.mulRight : (R : Type u_1) →
  {A : Type u_2} →
    [inst : NormedRing A] →
      [inst_1 : StarRing A] →
        [CStarRing A] → [inst_3 : Ring R] → [inst_4 : Module R A] → [IsScalarTower R A A] → ↥(unitary A) → A ≃ₗᵢ[R] A
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1π_eq_zero_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : ↥(groupCohomology.cocycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π A)) x = 0 ↔ ⇑x ∈ groupCohomology.coboundaries₁ A
-- Init.Data.Nat.MinMax
Nat.min_le_left : ∀ (a b : ℕ), min a b ≤ a
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instForInSigmaOfMonad : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForIn m (Std.DTreeMap.Raw α β cmp) ((a : α) × β a)
-- Mathlib.Computability.ContextFreeGrammar
/-- Add extra prefix to context-free deriving.  -/
ContextFreeGrammar.Derives.append_left : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)},
  g.Derives v w → ∀ (p : List (Symbol T g.NT)), g.Derives (p ++ v) (p ++ w)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.keys_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c : ℕ}, (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).keys = []
-- Mathlib.Data.Sum.Interval
Sum.Icc_inr_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₂ : α) (b₁ : β), Finset.Icc (Sum.inr b₁) (Sum.inl a₂) = ∅
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- Given an embedding `e : c.Embedding c'` of complexes shapes, this is the
morphism `K.extend e ⟶ L.extend e` induced by a morphism `K ⟶ L` in
`HomologicalComplex C c`.  -/
HomologicalComplex.extendMap : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                {K L : HomologicalComplex C c} → (K ⟶ L) → (e : c.Embedding c') → K.extend e ⟶ L.extend e
-- Mathlib.RingTheory.Regular.RegularSequence
/-- The equivalence between M ⧸ (r₀, r₁, …, rₙ)M and (M ⧸ r₀M) ⧸ (r₁, …, rₙ) (M ⧸ r₀M).  -/
Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner : {R : Type u_1} →
  (M : Type u_3) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (r : R) → (rs : List R) → (M ⧸ Ideal.ofList (r :: rs) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instCreatesLimitsOfShapeIndFunctorOppositeTypeDiscreteInclusionOfHasLimitsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type v} →
      [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C] →
        CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Ind.inclusion C)
-- Init.Internal.Order.Basic
_private.Init.Internal.Order.Basic.0.EST.bind.eq_1 : ∀ {ε σ α β : Type} (x : EST ε σ α) (f : α → EST ε σ β) (s : Void σ),
  x.bind f s =
    match x s with
    | EST.Out.ok a s => f a s
    | EST.Out.error e s => EST.Out.error e s
-- Mathlib.Data.Sigma.Interval
Sigma.Ico_mk_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a b : α i),
  Finset.Ico ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ico a b)
-- Mathlib.Order.Completion
DedekindCut.ofAttribute_eq_principal : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Concept.ofAttribute (fun x1 x2 => x1 ≤ x2) a = DedekindCut.principal a
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.zero_mem : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L), 0 ∈ L'
-- Mathlib.Data.Finite.Defs
/-- A type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 -/
Finite : Sort u_3 → Prop
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- The constant Cauchy sequence  -/
_private.Mathlib.Algebra.Order.CauSeq.Basic.0.CauSeq.termConst : Lean.ParserDescr
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- Extract the `sheaf C (X : Top)` from a `SheafedSpace C`.  -/
AlgebraicGeometry.SheafedSpace.sheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : AlgebraicGeometry.SheafedSpace C) → TopCat.Sheaf C ↑X.toPresheafedSpace
-- Mathlib.Algebra.Module.Basic
/-- If `E` is a vector space over two division semirings `R` and `S`, then scalar multiplications
agree on inverses of natural numbers in `R` and `S`.  -/
inv_natCast_smul_eq : ∀ {E : Type u_5} (R : Type u_6) (S : Type u_7) [inst : AddCommMonoid E] [inst_1 : DivisionSemiring R]
  [inst_2 : DivisionSemiring S] [inst_3 : Module R E] [inst_4 : Module S E] (n : ℕ) (x : E), (↑n)⁻¹ • x = (↑n)⁻¹ • x
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumDiffSubset_symm_apply_of_notMem : ∀ {α : Type u_3} {s t : Set α} (h : s ⊆ t) [inst : DecidablePred fun x => x ∈ s] {x : ↑t} (hx : ↑x ∉ s),
  (Equiv.Set.sumDiffSubset h).symm x = Sum.inr ⟨↑x, ⋯⟩
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  k ∈ t.insertMany l → (List.map Prod.fst l).contains k = false → k ∈ t
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F : C ⥤ D` is initial, we denote by `lift F d` an arbitrary choice of object in `C` such that
there exists a morphism `F.obj (lift F d) ⟶ d`.
 -/
CategoryTheory.Functor.Initial.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C D) → [F.Initial] → D → C
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_ssubset_Icc_right : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₂ ≤ b₂ → a₂ ≤ a₁ → b₁ < b₂ → Finset.Icc a₁ b₁ ⊂ Finset.Icc a₂ b₂
-- Init.Data.List.Nat.Basic
List.length_filter_pos_iff : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, 0 < (List.filter p l).length ↔ ∃ x ∈ l, p x = true
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [inst : Zero R], (↑x).imK = 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.anyM_filterM : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : MonadLiftT m n] [inst_3 : Monad m] [LawfulMonad m] [inst_5 : Monad n] [inst_6 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] {it : Std.IterM m β} {f p : β → n (ULift.{w, 0} Bool)},
  Std.IterM.anyM p (Std.IterM.filterM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        if __do_lift.down = true then p x else pure { down := false })
      (Std.IterM.mapM pure it)
-- Mathlib.RingTheory.FinitePresentation
/-- `R[X]` is finitely presented as `R`-algebra.  -/
Algebra.FinitePresentation.polynomial : ∀ (R : Type w₁) (A : Type w₂) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A], Algebra.FinitePresentation R (Polynomial A)
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.compCreatesColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [ℰ : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
                  [CategoryTheory.CreatesColimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] →
                    CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.leftUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (P : C),
  (CategoryTheory.Limits.coprod.leftUnitor P).hom =
    CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.initial.to P) (CategoryTheory.CategoryStruct.id P)
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.below.zero : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {motive : (a : R) → IsSumSq a → Prop},
  IsSumSq.below ⋯
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_subset_Ico_union_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.hasSum_iff_tendsto_nat : ∀ {f : ℕ → ENNReal} (r : ENNReal),
  HasSum f r ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds r)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.emptyWithCapacity_eq_empty : ∀ {α : Type u_1} (n : ℕ), Std.Sat.CNF.emptyWithCapacity n = Std.Sat.CNF.empty
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.eq_iff`. -/
Topology.CWComplex.Subcomplex.eq_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E F : Topology.RelCWComplex.Subcomplex C), E = F ↔ ↑E = ↑F
-- Mathlib.Analysis.SpecialFunctions.Sqrt
ContDiffOn.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞} {s : Set E},
  ContDiffOn ℝ n f s → (∀ x ∈ s, f x ≠ 0) → ContDiffOn ℝ n (fun y => √(f y)) s
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.sub' : ∀ {n a b c d : ℕ}, (c ≤ a ↔ d ≤ b) → a ≡ b [MOD n] → c ≡ d [MOD n] → a - c ≡ b - d [MOD n]
-- Mathlib.CategoryTheory.Action.Continuous
CategoryTheory.Functor.mapContAction_map : ∀ {V : Type u_5} {W : Type u_6} [inst : CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7}
  {CV : V → Type u_8} [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_2 : CategoryTheory.ConcreteCategory V FV] [inst_3 : CategoryTheory.HasForget₂ V TopCat]
  [inst_4 : CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10}
  [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [inst_6 : CategoryTheory.ConcreteCategory W FW]
  [inst_7 : CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [inst_8 : Monoid G] [inst_9 : TopologicalSpace G]
  (F : CategoryTheory.Functor V W) (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
  {X Y : ContAction V G} (f : X ⟶ Y),
  (CategoryTheory.Functor.mapContAction G F H).map f = CategoryTheory.ObjectProperty.homMk ((F.mapAction G).map f.hom)
-- Init.Data.BitVec.Bitblast
BitVec.bit_not_testBit : ∀ {w : ℕ} (x : BitVec w) (i : Fin w), (BitVec.iunfoldr (fun i c => (c, !x[↑i])) ()).2[↑i] = !x.getLsbD ↑i
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
AlgebraicIndependent.subalgebraAlgebraicClosure : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x →
    ∀ [inst_3 : IsDomain R] [NoZeroDivisors A], AlgebraicIndependent (↥(Subalgebra.algebraicClosure R A)) x
-- Mathlib.Data.List.Perm.Basic
/-- **Alias** of the reverse direction of `List.perm_insertIdx_iff_of_le`. -/
List.Perm.insertIdx_of_le : ∀ {α : Type u_1} {l₁ l₂ : List α} {m n : ℕ},
  m ≤ l₁.length → n ≤ l₂.length → ∀ (a : α), l₁.Perm l₂ → (l₁.insertIdx m a).Perm (l₂.insertIdx n a)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` is bounded.  -/
FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, ↑r < p.radius → ∃ C > 0, ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C
-- Mathlib.Algebra.Module.Presentation.Basic
/-- The linear map `(relations.R →₀ A) →ₗ[A] (relations.G →₀ A)` corresponding to the relations
given by `relations : Relations A`.  -/
Module.Relations.map : {A : Type u} → [inst : Ring A] → (relations : Module.Relations A) → (relations.R →₀ A) →ₗ[A] relations.G →₀ A
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.proved : Option (Array Aesop.Script.LazyStep) → Aesop.NormRuleResult
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instInhabitedCustomEliminators.default : Lean.Meta.CustomEliminators
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.addEquiv'.eq_1 : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : IsAddKleinFour G₁] (e : G₁ ≃ G₂)
  (he : e 0 = 0) (h : AddMonoid.exponent G₂ = 2), IsAddKleinFour.addEquiv' e he h = { toEquiv := e, map_add' := ⋯ }
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integral.eq_1 : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : Fintype ι] (I : BoxIntegral.Box ι)
  (l : BoxIntegral.IntegrationParams) (f : (ι → ℝ) → E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤),
  BoxIntegral.integral I l f vol = if h : BoxIntegral.Integrable I l f vol then Exists.choose h else 0
-- Init.Data.String.Basic
String.Pos.Raw.utf8GetAux? : List Char → String.Pos.Raw → String.Pos.Raw → Option Char
-- Mathlib.CategoryTheory.Localization.OfQuotient
CategoryTheory.Quotient.isLocalization_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) (W : CategoryTheory.MorphismProperty C),
  W.IsInvertedBy (CategoryTheory.Quotient.functor r) →
    (∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π) → (CategoryTheory.Quotient.functor r).IsLocalization W
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonpos_of_mul_nonpos_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R], a * b ≤ 0 → 0 < b → a ≤ 0
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.aeval_minpoly_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsAlgebraic K L]
  (x : L) (c : ConjRootClass K L), (Polynomial.aeval x) c.minpoly = 0 ↔ ConjRootClass.mk K x = c
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestAttemptAll.go : Array (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) →
  ℕ →
    Option Lean.Elab.Tactic.SavedState →
      Array (Lean.TSyntax `tactic) → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Lean.Meta.ForEachExpr
/-- Return true iff `x` is a metavariable with an anonymous user facing name.  -/
_private.Lean.Meta.ForEachExpr.0.Lean.Meta.shouldInferBinderName : {m : Type → Type u_1} → [Monad m] → [MonadLiftT Lean.MetaM m] → Lean.Expr → m Bool
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.inter_mem : ∀ {α : Type u_1} {C : Set (Set α)}, MeasureTheory.IsSetSemiring C → ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.restrict_biUnion : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J), J ∈ π → (π.biUnion πi).restrict J = πi J
-- Mathlib.Data.List.Cycle
Cycle.instMembership : {α : Type u_1} → Membership α (Cycle α)
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
/-- The measure defined through a sigma-subadditive
content on a semiring coincides with the content on the semiring.  -/
MeasureTheory.AddContent.measure_eq : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} [mα : MeasurableSpace α] (m : MeasureTheory.AddContent ENNReal C)
  (hC : MeasureTheory.IsSetSemiring C) (hC_gen : mα = MeasurableSpace.generateFrom C)
  (m_sigma_subadd : m.IsSigmaSubadditive), s ∈ C → (m.measure hC ⋯ m_sigma_subadd) s = m s
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whisker.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.Cone.whisker E c = { pt := c.pt, π := E.whiskerLeft c.π }