mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrder.mk : {α : Type u_1} →
  [inst : Preorder α] →
    (finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α) →
      (∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) →
        (∀ (a b x : α), x ∈ finsetIco a b ↔ a ≤ x ∧ x < b) →
          (∀ (a b x : α), x ∈ finsetIoc a b ↔ a < x ∧ x ≤ b) →
            (∀ (a b x : α), x ∈ finsetIoo a b ↔ a < x ∧ x < b) → LocallyFiniteOrder α
-- Mathlib.Topology.Compactification.StoneCech
preStoneCech_hom_ext : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [T2Space β]
  {g₁ g₂ : PreStoneCech α → β}, Continuous g₁ → Continuous g₂ → g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit → g₁ = g₂
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedSnapshot.toSnapshot : Lean.Language.Lean.HeaderProcessedSnapshot → Lean.Language.Snapshot
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_inv_smul_union : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (c⁻¹ • s ∪ t) = μ (s ∪ c • t)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact)
  [inst_3 : HasDerivedCategory C] {X : C} {n₀ : ℕ} (x : CategoryTheory.Abelian.Ext X S.X₃ n₀) {n₁ : ℕ}
  (h : n₀ + 1 = n₁),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op ((DerivedCategory.singleFunctor C 0).obj X))).homologySequenceδ
          hS.singleTriangle ↑n₀ ↑n₁ ⋯))
      x.hom =
    (x.comp hS.extClass h).hom
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.add_injective_of_disjoint : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ : AddSubgroup G}, Disjoint H₁ H₂ → Function.Injective fun g => ↑g.1 + ↑g.2
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.M.mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  (x y : (j : J) × ↑(F.obj j)),
  (∃ k f g,
      (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd) →
    AddMonCat.FilteredColimits.M.mk F x = AddMonCat.FilteredColimits.M.mk F y
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instReprCtorInfo.repr : Lean.Compiler.LCNF.CtorInfo → ℕ → Std.Format
-- Lean.Language.Basic
/-- A typed snapshot paired with a `SnapshotTreeTransform`.  -/
Lean.Language.TransformedSnap : Type → Type
-- Init.Data.Vector.Lemmas
Vector.toList_pop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.pop.toList = xs.toList.dropLast
-- Mathlib.Algebra.Homology.Embedding.TruncGE
ComplexShape.Embedding.restrictionToTruncGE'NatTrans_app : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncGE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c'),
  (e.restrictionToTruncGE'NatTrans C).app K = K.restrictionToTruncGE' e
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.not_equiv_of_X_ne : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 → ¬P ≈ Q
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_mono : ∀ {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.IsSplitMono CategoryTheory.Limits.biprod.inr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.pointEquiv_symm_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {x y : R} (h : W'.Equation x y),
  W'.pointEquiv.symm (some ⟨(x, y), h⟩) = WeierstrassCurve.Affine.Point.mk h
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mk : {α : Type u_6} → [inst : LE α] → (toProd : α × α) → toProd.1 ≤ toProd.2 → NonemptyInterval α
-- Mathlib.Algebra.Algebra.Equiv
/-- Turn an element of a type `F` satisfying `AlgEquivClass F R A B` into an actual `AlgEquiv`.
This is declared as the default coercion from `F` to `A ≃ₐ[R] B`.  -/
AlgEquivClass.toAlgEquiv : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] → [inst_5 : EquivLike F A B] → [AlgEquivClass F R A B] → F → A ≃ₐ[R] B
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.one_smul : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] (x : TensorProduct R M N), 1 • x = x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.splitter : (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) →
  (op : Std.Tactic.BVDecide.BVUnOp) →
    (Unit → motive Std.Tactic.BVDecide.BVUnOp.not) →
      ((distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance)) →
        ((distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance)) →
          ((distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance)) →
            (Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) →
              (Unit → motive Std.Tactic.BVDecide.BVUnOp.clz) →
                (Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop) → motive op
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- A submodule over `k` which is stable under scalar multiplication by elements of `G` is a
submodule over `SkewMonoidAlgebra k G`  -/
SkewMonoidAlgebra.submoduleOfSmulMem : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] →
      [inst_1 : Monoid G] →
        [inst_2 : MulSemiringAction G k] →
          {V : Type u_4} →
            [inst_3 : AddCommMonoid V] →
              [inst_4 : Module k V] →
                [inst_5 : Module (SkewMonoidAlgebra k G) V] →
                  [IsScalarTower k (SkewMonoidAlgebra k G) V] →
                    (W : Submodule k V) →
                      (∀ (g : G), ∀ v ∈ W, (SkewMonoidAlgebra.of k G) g • v ∈ W) → Submodule (SkewMonoidAlgebra k G) V
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_le_minKeyD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α},
      (t.erase k).isEmpty = false →
        ∀ {fallback : α}, (cmp (t.minKeyD fallback) ((t.erase k).minKeyD fallback)).isLE = true
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⊤.dualAnnihilator = ⊥
-- Init.Data.String.TakeDrop
/-- Checks whether the second string \(`s`\) begins with a prefix \(`p`\).

This function is generic over all currently supported patterns.

`String.startsWith` is a version that takes the potential prefix after the string.

Examples:

* `"red".isPrefixOf "red green blue" = true`

* `"green".isPrefixOf "red green blue" = false`

* `"".isPrefixOf "red green blue" = true`
 -/
String.isPrefixOf : String → String → Bool
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Multiset.vadd_sum : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : AddAction M N]
  [VAddAssocClass M N N] [VAddCommClass M N N] (s : Multiset N) (b : M),
  s.card • b +ᵥ s.sum = (Multiset.map (fun x => b +ᵥ x) s).sum
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀],
  IsCompact ↑(Valued.integer K) → Nonempty (LocallyFiniteOrder (↥(MonoidHom.mrange Valued.v))ˣ)
-- Mathlib.Data.Quot
/-- Any constant function lifts to a function out of the truncation  -/
Trunc.lift : {α : Sort u_1} → {β : Sort u_2} → (f : α → β) → (∀ (a b : α), f a = f b) → Trunc α → β
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_of_lcm_right_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c : α}, lcm a b ∣ c → a ∣ c
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.instLawfulBEq : LawfulBEq Std.Http.Header.Name
-- Mathlib.Data.Finset.Image
Finset.map_nontrivial : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, (Finset.map f s).Nontrivial ↔ s.Nontrivial
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.instUpwardEnumerable_eq : ISize.instUpwardEnumerable = HasModel.instUpwardEnumerable✝
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal : ∀ (A : Type u_2) [inst : Field A] [inst_1 : CharZero A] (N : ℕ),
  {K | {w | w.IsReal}.Nonempty ∧ |NumberField.discr ↥↑K| ≤ ↑N}.Finite
-- Mathlib.Data.EReal.Basic
EReal.image_coe_Iio : ∀ (x : ℝ), Real.toEReal '' Set.Iio x = Set.Ioo ⊥ ↑x
-- Init.Data.List.Basic
List.replace_cons : ∀ {α : Type u} {as : List α} {b c : α} [inst : BEq α] {a : α},
  (a :: as).replace b c =
    match b == a with
    | true => c :: as
    | false => a :: as.replace b c
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instQuasiSeparatedMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.QuasiSeparated (f ∣_ V)
-- Mathlib.Algebra.LinearRecurrence
/-- A solution of a `LinearRecurrence` which satisfies certain initial conditions.
We will prove this is the only such solution.  -/
LinearRecurrence.mkSol : {R : Type u_1} → [inst : CommSemiring R] → (E : LinearRecurrence R) → (Fin E.order → R) → ℕ → R
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.productMap_right : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : CommSemiring S] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R S]
  (f : A →ₐ[R] S) (g : B →ₐ[R] S), (Algebra.TensorProduct.productMap f g).comp Algebra.TensorProduct.includeRight = g
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_union : ∀ {α : Type u_2} [inst : Mul α] {s t₁ t₂ : Set α}, s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.symm : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v.MutuallySingular w → w.MutuallySingular v
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.rootSpace_le_of_apply_coroot_ne_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L)
  {α : LieModule.Weight K (↥H) L},
  LieAlgebra.rootSpace H ⇑α ≤ LieSubmodule.restr I H →
    ∀ {γ : ↥H → K}, γ (LieAlgebra.IsKilling.coroot α) ≠ 0 → LieAlgebra.rootSpace H γ ≤ LieSubmodule.restr I H
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivAt_iff_isLittleO_nhds_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x ↔ (fun h => f (x + h) - f x - f' h) =o[nhds 0] fun h => h
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essImage.liftFunctor_obj : ∀ {J : Type u_1} {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [inst_3 : F.Full] [inst_4 : F.Faithful]
  (hG : ∀ (j : J), F.essImage (G.obj j)) (j : J),
  (CategoryTheory.Functor.essImage.liftFunctor G F hG).obj j =
    F.toEssImage.objPreimage { obj := G.obj j, property := ⋯ }
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.totalLengthFilter.eq_1 : ∀ {X : Type u_1} [inst : PseudoMetricSpace X],
  AbsolutelyContinuousOnInterval.totalLengthFilter =
    Filter.comap (fun E => ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) (nhds 0)
-- Mathlib.Tactic.Qify
Mathlib.Tactic.Qify.intCast_le : ∀ (a b : ℤ), a ≤ b ↔ ↑a ≤ ↑b
-- Init.Prelude
/-- `letFun v (fun x => b)` is a function version of `have x := v; b`.
This is equal to `(fun x => b) v`, so the value of `x` is not accessible to `b`.
This is in contrast to `let x := v; b`, where the value of `x` is accessible to `b`.

This used to be the way `have`/`let_fun` syntax was encoded,
and there used to be special support for `letFun` in WHNF and `simp`.
 -/
letFun : {α : Sort u} → {β : α → Sort v} → (v : α) → ((x : α) → β x) → β v
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.characteristic_kleinFour : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → (alternatingGroup.kleinFour α).Characteristic
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_left_K : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).left.K =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.addRight.eq_1 : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), Equiv.addRight a = (toAddUnits a).addRight
-- Mathlib.Topology.Algebra.Group.Basic
/-- A version of `Homeomorph.mulRight a⁻¹ b` that is defeq to `b / a`.  -/
Homeomorph.divRight : {G : Type w} → [inst : Group G] → [inst_1 : TopologicalSpace G] → [IsTopologicalGroup G] → G → G ≃ₜ G
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
inv_riemannZeta_sub_sub_isLittleO : (fun s => (riemannZeta s)⁻¹ - (s - 1)) =o[nhdsWithin 1 {1}ᶜ] fun x => x - 1
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instSMul : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  {S : Type u_5} →
                    [inst_6 : Monoid S] →
                      [inst_7 : DistribMulAction S M] →
                        [SMulCommClass R S M] → [SMulCommClass S A M] → SMul S (Derivation R A M)
-- Mathlib.Algebra.Order.Monovary
monovary_inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {f : ι → α} {g : ι → β},
  StrongLT 0 f → StrongLT 0 g → (Monovary f⁻¹ g⁻¹ ↔ Monovary f g)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.mem_maximalAtlas_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I n M ↔ e ∈ StructureGroupoid.maximalAtlas M (contDiffGroupoid n I)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.instHasInjectiveResolutions : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C], CategoryTheory.HasInjectiveResolutions C
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
/-- The map from `X` to `WithLp p X` as a measurable equivalence.  -/
MeasurableEquiv.toLp : (p : ENNReal) → (X : Type u_1) → [inst : MeasurableSpace X] → X ≃ᵐ WithLp p X
-- Mathlib.Data.Set.Function
Set.eqOn_refl : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.EqOn f f s
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The `n`th homotopy group at `x` defined as the quotient of `Ω^n x` by the
`GenLoop.Homotopic` relation.  -/
HomotopyGroup : Type u_3 → (X : Type u_4) → [TopologicalSpace X] → X → Type (max u_3 u_4)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Predicate typeclass for expressing that `a * b = 0` implies `a = 0` or `b = 0`
for all `a` and `b` of type `M₀`. It is weaker than `IsCancelMulZero` in general,
but equivalent to it if `M₀` is a (not necessarily unital or associative) ring.  -/
NoZeroDivisors : (M₀ : Type u_2) → [Mul M₀] → [Zero M₀] → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' fallback : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getKeyD k' fallback =
    if compare k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else fallback else t.getKeyD k' fallback
-- Init.Data.SInt.Lemmas
Int32.toInt64_ofInt : ∀ {n : ℤ}, Int32.minValue.toInt ≤ n → n ≤ Int32.maxValue.toInt → (Int32.ofInt n).toInt64 = Int64.ofInt n
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedGroup.toGroup : {E : Type u_8} → [self : SeminormedGroup E] → Group E
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id._auto_3),
  CategoryTheory.CategoryStruct.comp (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv
      (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) =
    CategoryTheory.CategoryStruct.id
      (X'.E (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃) (CategoryTheory.homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂)
-- Init.Data.SInt.Lemmas
ISize.eq_sub_iff_add_eq : ∀ {a b c : ISize}, a = c - b ↔ a + b = c
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps.mk : Array (String × ProofWidgets.Html) → String → String → String → ℕ → ProofWidgets.Penrose.DiagramProps
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- To construct an isomorphism between tridents,
it suffices to give an isomorphism between the cone points
and check that it commutes with the `ι` morphisms.
 -/
CategoryTheory.Limits.Trident.ext : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {s t : CategoryTheory.Limits.Trident f} →
              (i : s.pt ≅ t.pt) →
                autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι)
                    CategoryTheory.Limits.Trident.ext._auto_1 →
                  (s ≅ t)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestTryTac : Lean.Elab.Tactic.Try.TryTactic
-- Init.Data.String.FindPos
_private.Init.Data.String.FindPos.0.String.Slice.posGE.eq_def : ∀ (s : String.Slice) (offset : String.Pos.Raw) (h : offset ≤ s.rawEndPos),
  s.posGE offset h =
    if h' : String.Pos.Raw.IsValidForSlice s offset then s.pos offset h'
    else
      have this := ⋯;
      s.posGE offset.inc ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- the pentagon relation expressing the compatibility of the left
and right homology data  -/
CategoryTheory.ShortComplex.HomologyData.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.HomologyData) {Z : C} (h : self.right.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.left.π
      (CategoryTheory.CategoryStruct.comp self.iso.hom (CategoryTheory.CategoryStruct.comp self.right.ι h)) =
    CategoryTheory.CategoryStruct.comp self.left.i (CategoryTheory.CategoryStruct.comp self.right.p h)
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquivClass.instStarHomClass : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Add A] [inst_1 : Mul A] [inst_2 : Star A] [inst_3 : Add B]
  [inst_4 : Mul B] [inst_5 : Star B] [inst_6 : EquivLike F A B] [hF : StarRingEquivClass F A B], StarHomClass F A B
-- Std.Async.Process
/-- Sets the title of the current process.
 -/
Std.IO.Process.setProcessTitle : String → IO Unit
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_double : Primrec fun n => 2 * n
-- Mathlib.Order.SupIndep
Finset.SupIndep.disjoint_sup_sup : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α] {s : Finset ι} {f : ι → α}
  {u v : Finset ι}, s.SupIndep f → u ⊆ s → v ⊆ s → Disjoint u v → Disjoint (u.sup f) (v.sup f)
-- Mathlib.Order.Partition.Basic
Partition.eq_of_mem_of_mem : ∀ {α : Type u_1} {x : α} {u s t : Set α} {P : Partition u}, t ∈ P → s ∈ P → x ∈ t → x ∈ s → t = s
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coim_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (f : CategoryTheory.Arrow C), CategoryTheory.Abelian.coim.obj f = CategoryTheory.Abelian.coimage f.hom
-- Mathlib.Algebra.Order.IsBotOne
not_lt_zero : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], ¬a < 0
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.codRestrict_apply_coe : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p)
  (v : (i : ι) → M₁ i), ↑((f.codRestrict p h) v) = f v
-- Mathlib.Data.Finset.Basic
List.filter_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : List α) (p : α → Prop) [inst_1 : DecidablePred p],
  Finset.filter p s.toFinset = (List.filter (fun b => decide (p b)) s).toFinset