mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.SpanRank
Ideal.spanFinrank_map_eq_of_ringEquiv : ∀ {R : Type u} [inst : Semiring R] {T : Type v} [inst_1 : Semiring T] (f : R ≃+* T) (I : Ideal R),
  Submodule.spanFinrank (Ideal.map f I) = Submodule.spanFinrank I
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.homotopyTo_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  {p q : ↑(GenLoop N X x)} (H : (↑p).HomotopyRel (↑q) (Cube.boundary N)) (t : ↑unitInterval × ↑unitInterval)
  (tₙ : { j // j ≠ i } → ↑unitInterval), ((GenLoop.homotopyTo i H) t) tₙ = H (t.1, (Cube.insertAt i) (t.2, tₙ))
-- Mathlib.Algebra.Ring.Action.Invariant
IsInvariantSubring.smul_mem : ∀ {M : Type u_1} {R : Type u_2} {inst : Monoid M} {inst_1 : Ring R} {inst_2 : MulSemiringAction M R} {S : Subring R}
  [self : IsInvariantSubring M S] (m : M) {x : R}, x ∈ S → m • x ∈ S
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.eq_2 : ∀ (s a : String) (as : List String), s.intercalate (a :: as) = String.intercalate.go✝ a s as
-- Batteries.Data.List.Scan
List.partialSums_ne_nil : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] {l : List α}, l.partialSums ≠ []
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.presheafIsFinite_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w))
  [CategoryTheory.PresheafIsFinite F] {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F') [CategoryTheory.Epi f],
  CategoryTheory.PresheafIsFinite F'
-- Mathlib.Analysis.Distribution.Sobolev
FourierTransform.fourierInvCLM.congr_simp : ∀ (R : Type u_2) (E : Type u_3) {F : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransformInv E F] [inst_6 : FourierInvAdd E F]
  [inst_7 : FourierInvSMul R E F] [inst_8 : TopologicalSpace E] [inst_9 : TopologicalSpace F]
  [inst_10 : ContinuousFourierInv E F], FourierTransform.fourierInvCLM R E = FourierTransform.fourierInvCLM R E
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_inv_rpow : ∀ {y : ℝ}, y ≠ 0 → ∀ (x : ENNReal), (x ^ y⁻¹) ^ y = x
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.hausdorffEDist_iUnion_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ι : Sort u_2} {s t : ι → Set α},
  Metric.hausdorffEDist (⋃ i, s i) (⋃ i, t i) ≤ ⨆ i, Metric.hausdorffEDist (s i) (t i)
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.instBEqStyleError.beq : Mathlib.Linter.TextBased.StyleError✝ → Mathlib.Linter.TextBased.StyleError✝ → Bool
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cones.RepresentableBy X) {Y : C} (f : Y ⟶ X),
  CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h f = { pt := Y, π := h.homEquiv f }
-- Mathlib.SetTheory.ZFC.VonNeumann
Ordinal.toZFSet_subset_vonNeumann : ∀ (o : Ordinal.{u_1}), o.toZFSet ⊆ ZFSet.vonNeumann o
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.pow_apply : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Monoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R] (n : ℕ) (f : BoundedContinuousFunction α R) (x : α),
  (f ^ n) x = f x ^ n
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.fun_add : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f g : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableAdd₂ M],
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun i => f i + g i) μ
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier`.

---

A skeleton intersected with a closed cell of a higher dimension is the skeleton intersected with
the boundary of the cell.  -/
Topology.CWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {m : ℕ} {j : Topology.RelCWComplex.cell C m},
  n ≤ ↑m →
    ↑(Topology.RelCWComplex.skeletonLT C n) ∩ Topology.RelCWComplex.closedCell m j =
      ↑(Topology.RelCWComplex.skeletonLT C n) ∩ Topology.RelCWComplex.cellFrontier m j
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- See Note [custom simps projection]  -/
AffineEquiv.Simps.symm_apply : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → (P₁ ≃ᵃ[k] P₂) → P₂ → P₁
-- Init.Grind.Ring.CommSolver
cond.eq_1 : ∀ {α : Sort u} (x y : α), (bif true then x else y) = x
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_of_apply : ∀ {α : Type u} {β : Type v} {f : α → β} (a : α),
  (FreeAbelianGroup.map f) (FreeAbelianGroup.of a) = FreeAbelianGroup.of (f a)
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.deriv_inv_log : (deriv fun x => (Real.log x)⁻¹) = fun x => -x⁻¹ / Real.log x ^ 2
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.algebraMap_eval_U : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Algebra R R'] (x : R) (n : ℤ),
  (algebraMap R R') (Polynomial.eval x (Polynomial.Chebyshev.U R n)) =
    Polynomial.eval ((algebraMap R R') x) (Polynomial.Chebyshev.U R' n)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A}, NonUnitalSubsemiringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_trans_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D}
  {G G' G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') (x : D) {Z : C}
  (h : G''.obj x ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((adj1.rightAdjointUniq adj2).hom.app x)
      (CategoryTheory.CategoryStruct.comp ((adj2.rightAdjointUniq adj3).hom.app x) h) =
    CategoryTheory.CategoryStruct.comp ((adj1.rightAdjointUniq adj3).hom.app x) h
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- If `M = R^ι`, `ofTensorProduct` is bijective.  -/
AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (ι : Type u_4) [Finite ι],
  Function.Bijective ⇑(AdicCompletion.ofTensorProduct I (ι → R))
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
MulAction.isPreprimitive_fixingSubgroup_insert_iff : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {a : α}
  {t : Set ↥(SubMulAction.ofStabilizer G a)},
  MulAction.IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
      ↥(SubMulAction.ofFixingSubgroup G (insert a (Subtype.val '' t))) ↔
    MulAction.IsPreprimitive ↥(fixingSubgroup (↥(MulAction.stabilizer G a)) t)
      ↥(SubMulAction.ofFixingSubgroup (↥(MulAction.stabilizer G a)) t)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- The type (II) simplex obtained as a face of a type (I) simplex.  -/
SSet.prodStdSimplex.pairingCore.IsIndex.δ : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} →
        {d : ℕ} →
          {hd : x.dim = d + 1} →
            {l : Fin (d + 1)} →
              SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ →
                ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_mem_nhds_of_mem : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x c : α} {ε : ℝ}, x ∈ Metric.ball c ε → Metric.closedBall c ε ∈ nhds x
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.AddConvolutionExistsAt.eq_1 : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') (x : M),
  DiscreteConvolution.AddConvolutionExistsAt L f g x = Summable fun ab => (L (f (↑ab).1)) (g (↑ab).2)
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.mk : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Submodule R M} →
            {ι : Type u_4} →
              {n : ℕ} →
                (bM : Module.Basis ι R M) →
                  (bN : Module.Basis (Fin n) R ↥N) →
                    (f : Fin n ↪ ι) →
                      (a : Fin n → R) → (∀ (i : Fin n), ↑(bN i) = a i • bM (f i)) → Module.Basis.SmithNormalForm N ι n
-- Mathlib.Topology.LocalAtTarget
Set.restrictPreimage.eq_1 : ∀ {α : Type u} {β : Type v} (t : Set β) (f : α → β), t.restrictPreimage f = Set.MapsTo.restrict f (f ⁻¹' t) t ⋯
-- Mathlib.RingTheory.Localization.Cardinality
IsFractionRing.cardinalMk : ∀ (R : Type u) [inst : CommRing R] (L : Type u) [inst_1 : CommRing L] [inst_2 : Algebra R L] [IsFractionRing R L],
  Cardinal.mk L = Cardinal.mk R
-- Init.Data.Fin.Lemmas
Fin.ext_iff : ∀ {n : ℕ} {a b : Fin n}, a = b ↔ ↑a = ↑b
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.compLeftId_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f : v ⟶ v}
  (h : CategoryTheory.Arrow.LeftHomotopy f (CategoryTheory.CategoryStruct.id v)) (g : u ⟶ v),
  (h.compLeftId g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right g) h.hom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.inter! m₂) = true},
  (m₁.inter! m₂).getKey k h_contains = m₁.getKey k ⋯
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- The product of two strongly locally contractible spaces is strongly locally contractible.  -/
instStronglyLocallyContractibleSpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [StronglyLocallyContractibleSpace X] [StronglyLocallyContractibleSpace Y], StronglyLocallyContractibleSpace (X × Y)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.algebraMap_apply : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {r : R}, (algebraMap R (MvPowerSeries σ A)) r = MvPowerSeries.C ((algebraMap R A) r)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite products, then `F.unop : C ⥤ D` reflects finite
coproducts.  -/
CategoryTheory.Limits.reflectsFiniteCoproducts_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteProducts F],
  CategoryTheory.Limits.ReflectsFiniteCoproducts F.unop
-- Init.Data.String.Slice
/-- Creates a new slice that contains the last `n` characters \(Unicode code points\) of `s`.

If `n` is greater than the amount of characters in `s`, returns `s`.

Examples:

* `"red green blue".toSlice.takeEnd 4 == "blue".toSlice`

* `"red green blue".toSlice.takeEnd 1 == "e".toSlice`

* `"red green blue".toSlice.takeEnd 0 == "".toSlice`

* `"red green blue".toSlice.takeEnd 100 == "red green blue".toSlice`
 -/
String.Slice.takeEnd : String.Slice → ℕ → String.Slice
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH0_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  (groupCohomology.shortComplexH0 A).f = ModuleCat.ofHom A.ρ.invariants.subtype
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.edist_eq : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x y : α),
  edist (f x) (f y) = ↑(Dilation.ratio f) * edist x y
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.biprodIsoProd_inv_comp_snd : ∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R),
  CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.snd =
    ModuleCat.ofHom (LinearMap.snd R ↑M ↑N)
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.ext_iff : ∀ {α : Type u} {a b : Additive α}, a = b ↔ Additive.toMul a = Additive.toMul b
-- Mathlib.Topology.Maps.Strict.Basic
/-- Quotient maps are precisely surjective strict maps.  -/
Topology.isQuotientMap_iff_isStrictMap_surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsQuotientMap f ↔ Topology.IsStrictMap f ∧ Function.Surjective f
-- Init.Data.Int.Order
Int.max_eq_right_iff : ∀ {a b : ℤ}, max a b = b ↔ a ≤ b
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheckSite.moduleDoc.inj : ∀ {n n_1 : ℕ}, Lean.Doc.DeferredCheckSite.moduleDoc n = Lean.Doc.DeferredCheckSite.moduleDoc n_1 → n = n_1
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk_eq_zero : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M) {a : M} {ha : a ∈ S}, ⟨a, ha⟩ = 0 ↔ a = 0
-- Mathlib.Order.Bounds.Basic
IsGreatest.mono : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α} {a b : α}, IsGreatest s a → IsGreatest t b → s ⊆ t → a ≤ b
-- Lean.Elab.DeclUtil
Lean.Elab.expandDeclSig : Lean.Syntax → Lean.Syntax × Lean.Syntax
-- Init.Grind.Ordered.Ring
/-- In a strict ordered semiring, we have `0 < 1`.  -/
Lean.Grind.OrderedRing.zero_lt_one : ∀ {R : Type u} {inst : Lean.Grind.Semiring R} {inst_1 : LE R} {inst_2 : LT R} {inst_3 : Std.IsPreorder R}
  [self : Lean.Grind.OrderedRing R], 0 < 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.forget_reflects_iso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T},
  (CategoryTheory.Under.forget X).ReflectsIsomorphisms
-- Mathlib.Order.Preorder.Finite
Set.Infinite.exists_lt_map_eq_of_mapsTo : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] {s : Set α} {t : Set β} {f : α → β},
  s.Infinite → Set.MapsTo f s t → t.Finite → ∃ x ∈ s, ∃ y ∈ s, x < y ∧ f x = f y
-- Init.Data.BitVec.Lemmas
BitVec.append_extractLsb'_of_lt : ∀ {x_len w : ℕ} {hcast : w + (x_len - 1) * w = x_len * w} {x : BitVec (x_len * w)},
  BitVec.cast hcast (BitVec.extractLsb' ((x_len - 1) * w) w x ++ BitVec.extractLsb' 0 ((x_len - 1) * w) x) = x
-- Aesop.Util.Unfold
Aesop.unfoldManyAt : (Lean.Name → Option (Option Lean.Name)) →
  Lean.MVarId → Lean.FVarId → Lean.MetaM (Option (Lean.MVarId × Array Lean.Name))
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- **Alias** of `StarMul.star_mul`. -/
Matrix.star_mul : ∀ {R : Type u} {inst : Mul R} [self : StarMul R] (r s : R), star (r * s) = star s * star r
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true → t.minKey? = none
-- Std.Http.Data.Status
Std.Http.Status.ok.sizeOf_spec : sizeOf Std.Http.Status.ok = 1
-- Mathlib.Data.Set.Function
Set.SurjOn.bijOn_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
  Set.SurjOn f s t → Set.BijOn f (Function.invFunOn f s '' t) t
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpKind.noConfusionType : Sort v✝ → Lean.Elab.Tactic.SimpKind → Lean.Elab.Tactic.SimpKind → Sort v✝
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_preimage_mem_nhds_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set E} {x : M},
  x ∈ f.source → s ∈ nhdsWithin (↑(f.extend I) x) (Set.range ↑I) → ↑(f.extend I) ⁻¹' s ∈ nhds x
-- Mathlib.Data.PNat.Basic
PNat.val_ofNat : ∀ (n : ℕ) [inst : NeZero n], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n],
  Polynomial.IsSplittingField k (FiniteField.Extension k p n) (Polynomial.X ^ Nat.card k ^ n - Polynomial.X)
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.parser.injEq : ∀ (catName declName : Lean.Name) (leading : Bool) (p : Lean.Parser.Parser) (prio : ℕ) (catName_1 declName_1 : Lean.Name)
  (leading_1 : Bool) (p_1 : Lean.Parser.Parser) (prio_1 : ℕ),
  (Lean.Parser.ParserExtension.Entry.parser catName declName leading p prio =
      Lean.Parser.ParserExtension.Entry.parser catName_1 declName_1 leading_1 p_1 prio_1) =
    (catName = catName_1 ∧ declName = declName_1 ∧ leading = leading_1 ∧ p = p_1 ∧ prio = prio_1)
-- Mathlib.Topology.Homotopy.Equiv
/-- If `X` is homotopy equivalent to `Y`, and `Y` is homotopy equivalent to `Z`, then `X` is homotopy
equivalent to `Z`.
 -/
ContinuousMap.HomotopyEquiv.trans : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            ContinuousMap.HomotopyEquiv X Y → ContinuousMap.HomotopyEquiv Y Z → ContinuousMap.HomotopyEquiv X Z
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey?_alter!_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).minKey? = some k ↔
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true
-- Std.Data.TreeMap.Raw.Basic
/-- Returns a list of all values present in the tree map in ascending  order.  -/
Std.TreeMap.Raw.values : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → List β
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative.  -/
Matrix.posSemidef_diagonal_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] {d : n → R}, (Matrix.diagonal d).PosSemidef ↔ ∀ (i : n), 0 ≤ d i
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtOrthonormalBasis_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) {f : ι → E} {i : ι},
  InnerProductSpace.gramSchmidtNormed 𝕜 f i ≠ 0 →
    (InnerProductSpace.gramSchmidtOrthonormalBasis h f) i = InnerProductSpace.gramSchmidtNormed 𝕜 f i
-- Mathlib.MeasureTheory.Integral.Pi
/-- A version of **Fubini's theorem** in `n` variables, for a natural number `n`.  -/
MeasureTheory.integral_fin_nat_prod_eq_prod : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : ℕ} {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)}
  {μ : (i : Fin n) → MeasureTheory.Measure (E i)} [∀ (i : Fin n), MeasureTheory.SigmaFinite (μ i)]
  (f : (i : Fin n) → E i → 𝕜),
  ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂MeasureTheory.Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).mor₂ = CategoryTheory.Limits.biprod.snd
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.iInf_rat_gt_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
  ProbabilityTheory.IsMeasurableRatCDF f → ∀ (a : α) (q : ℚ), ⨅ r, f a ↑r = f a q
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rii α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Rii α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.CategoryTheory.Skeletal
/-- Provides a (noncomputable) isomorphism `X ≅ Y` given that `toSkeleton X = toSkeleton Y`.  -/
CategoryTheory.Skeleton.isoOfEq : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → CategoryTheory.toSkeleton X = CategoryTheory.toSkeleton Y → (X ≅ Y)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult.matcher : Lean.Meta.Match.MatcherResult → Lean.Expr
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.injOn_iff_bijOn_of_mapsTo : ∀ {α : Type u} {s : Set α} {f : α → α}, s.Finite → Set.MapsTo f s s → (Set.InjOn f s ↔ Set.BijOn f s s)
-- Init.Data.BitVec.Bootstrap
BitVec.testBit_toNat : ∀ {w i : ℕ} (x : BitVec w), x.toNat.testBit i = x.getLsbD i
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isHamiltonianCycle_rotate`. -/
SimpleGraph.Walk.IsHamiltonianCycle.rotate : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a v : α} {p : G.Walk a a} (hv : v ∈ p.support),
  p.IsHamiltonianCycle → (p.rotate v hv).IsHamiltonianCycle
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- Any category with products and equalizers has all limits.  -/
CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C]
  [CategoryTheory.Limits.HasEqualizers C], CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
-- Mathlib.Tactic.ITauto
/-- Debugging printer for propositions.  -/
Mathlib.Tactic.ITauto.IProp.format : Mathlib.Tactic.ITauto.IProp → Std.Format
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.of_eq_wrap_co_0 : ∀ (i : Lean.Grind.IntInterval) (hi : ℤ), i = Lean.Grind.IntInterval.co 0 hi → ∀ {a b : ℤ}, a = i.wrap b → a = b % hi
-- Mathlib.Data.Prod.TProd
List.TProd.elim.congr_simp : ∀ {ι : Type u} {α : ι → Type v} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] {l : List ι} (x x_1 : List.TProd α l),
  x = x_1 → ∀ {i : ι} (x_2 : i ∈ l), x.elim x_2 = x_1.elim x_2
-- Mathlib.Data.Set.Card
Set.one_lt_ncard_of_nonempty_of_even : ∀ {α : Type u_1} {s : Set α},
  s.Finite → autoParam s.Nonempty Set.one_lt_ncard_of_nonempty_of_even._auto_1 → Even s.ncard → 1 < s.ncard
-- Mathlib.Order.Category.Preord
preordToCat_obj : ∀ (X : Preord), preordToCat.obj X = CategoryTheory.Cat.of ↑X
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.hasLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (pres : CategoryTheory.Limits.LimitPresentation J X), CategoryTheory.Limits.HasLimit pres.diag