mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Separation.Basic
/-- In an R₁ space, the bornologies `relativelyCompact` and `inCompact` are equal.  -/
Bornology.relativelyCompact_eq_inCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R1Space X], Bornology.relativelyCompact X = Bornology.inCompact X
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.retractClosure_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊥.retractClosure = ⊥
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ},
  (Std.DHashMap.emptyWithCapacity c).contains a = false
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for measurable finite measure sets with respect to some class of sets,
then its restriction to any set is also inner regular for measurable finite measure sets, with
respect to the same class of sets.  -/
MeasureTheory.Measure.InnerRegularWRT.restrict : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set α → Prop},
  (μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤) →
    ∀ (A : Set α), (μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s ∧ (μ.restrict A) s ≠ ⊤
-- Mathlib.Algebra.Order.Ring.Star
/-- A commutative star-ordered semiring is an ordered semiring.  -/
StarOrderedRing.toIsOrderedRing : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R],
  IsOrderedRing R
-- Mathlib.Data.List.Perm.Subperm
List.map_subperm_map_iff : ∀ {α : Type u_2} {β : Type u_3} {l₁ l₂ : List α} {f : α → β},
  Function.Injective f → ((List.map f l₁).Subperm (List.map f l₂) ↔ l₁.Subperm l₂)
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_empty_iff : ∀ {α : Type u_1} {s : Set α}, sᶜ = ∅ ↔ s = Set.univ
-- Mathlib.Algebra.Algebra.Defs
smul_algebraMap : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_2}
  [inst_3 : Monoid α] [inst_4 : MulDistribMulAction α A] [SMulCommClass α R A] (a : α) (r : R),
  a • (algebraMap R A) r = (algebraMap R A) r
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.sum_finset_product_right' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ)
  (t : γ → Finset α),
  (∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) → ∀ {f : α → γ → β}, ∑ p ∈ r, f p.1 p.2 = ∑ c ∈ s, ∑ a ∈ t c, f a c
-- Mathlib.Analysis.Convex.Intrinsic
closure_sdiff_intrinsicFrontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [inst_5 : MetricSpace P]
  [inst_6 : NormedAddTorsor V P] (s : Set P), closure s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_of_le_of_ne` -/
ssubset_of_subset_of_ne : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a ≠ b → a ⊂ b
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm.inj : ∀ {c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr} {e : Lean.Meta.Grind.Arith.CommRing.RingExpr}
  {p : Lean.Grind.CommRing.Poly} {c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr}
  {e_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr} {p_1 : Lean.Grind.CommRing.Poly},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm c e p =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm c_1 e_1 p_1 →
    c = c_1 ∧ e = e_1 ∧ p = p_1
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
/-- Every regular measure is induced by a positive linear functional on `C_c(X, ℝ≥0)`.
That is, `NNRealRMK.rieszMeasure` is a surjective function onto regular measures.  -/
NNRealRMK.rieszMeasure_integralLinearMap : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X]
  [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X] {μ : MeasureTheory.Measure X} [inst_5 : μ.Regular],
  NNRealRMK.rieszMeasure (CompactlySupportedContinuousMap.integralLinearMap μ) = μ
-- Mathlib.Data.Semiquot
Semiquot.instOrderTopOfInhabited : {α : Type u_1} → [Inhabited α] → OrderTop (Semiquot α)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceSub : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff' : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G}
  {f' : G →L[𝕜] F}, HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f (↑iso.symm ∘SL f') s x
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.coe_IccExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : LinearOrder α]
  [inst_3 : OrderTopology α] {a b : α} (h : a ≤ b) (f : C(↑(Set.Icc a b), β)),
  ⇑(ContinuousMap.IccExtend h f) = Set.IccExtend h ⇑f
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_inv_distrib : ∀ {ι : Type u_1} {G : Type u_5} {s : Finset ι} [inst : DivisionCommMonoid G] (f : ι → G),
  ∏ x ∈ s, (f x)⁻¹ = (∏ x ∈ s, f x)⁻¹
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.nnnorm_changeOrigin_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {x : E} (k : ℕ),
  ↑‖x‖₊ < p.radius → ‖p.changeOrigin x k‖₊ ≤ ∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
-- Mathlib.RingTheory.Extension.Generators
/-- Given `R[X] → S` and `S[Y] → T`, this is the lift of an element in `ker(S[Y] → T)`
to `ker(R[X][Y] → S[Y] → T)` constructed from `P.σ`.
 -/
Algebra.Generators.kerCompPreimage : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {ι' : Type u_3} →
              {T : Type u_7} →
                [inst_3 : CommRing T] →
                  [inst_4 : Algebra R T] →
                    [inst_5 : Algebra S T] →
                      [inst_6 : IsScalarTower R S T] →
                        (Q : Algebra.Generators S T ι') → (P : Algebra.Generators R S ι) → ↥Q.ker → ↥(Q.comp P).ker
-- Mathlib.Data.List.Infix
List.IsPrefix.flatten : ∀ {α : Type u_1} {l₁ l₂ : List (List α)}, l₁ <+: l₂ → l₁.flatten <+: l₂.flatten
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.reverse_charpoly : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.charpoly.reverse = M.charpolyRev
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonResolvableCompletionItem.fromJson : Lean.Json → Except String Lean.Lsp.ResolvableCompletionItem
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_eq_top : ∀ {a : ENNReal}, a⁻¹ = ⊤ ↔ a = 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y) Z ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv Z)
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
        h)
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- A module is finite if and only if the bottom submodule is CoFG.  -/
Module.Finite.iff_cofg_bot : ∀ (R : Type u_1) [inst : Ring R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ⊥.CoFG ↔ Module.Finite R M
-- Mathlib.Data.Num.Bitwise
SNum.zero.sizeOf_spec : ∀ (a : Bool), sizeOf (SNum.zero a) = 1 + sizeOf a
-- Init.Data.SInt.Lemmas
Int64.ofNat_int8ToNatClampNeg : ∀ (x : Int8), 0 ≤ x → Int64.ofNat x.toNatClampNeg = x.toInt64
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C), S.Exact ↔ CategoryTheory.Epi (imageToKernel S.f S.g ⋯)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_iInf_comap_of_surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_3}
  {f : L.Hom M N},
  Function.Surjective ⇑f →
    ∀ (S : ι → L.Substructure N),
      FirstOrder.Language.Substructure.map f (⨅ i, FirstOrder.Language.Substructure.comap f (S i)) = ⨅ i, S i
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Add suggestion `tac` to the list of tactics that solve the goal.  -/
Mathlib.Tactic.ClickSuggestions.addSolvedSuggestion : Lean.TSyntax `tactic → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM Unit
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.labellingStarEquiv_symm_apply_fst : ∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M)
  (x : Quiver.SchreierGraph V ι) (x_1 : Quiver.Star (Quiver.SingleObj.star S)),
  ((Quiver.SchreierGraph.labellingStarEquiv ι x).symm x_1).fst = ι x_1.snd • x
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAt.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3} [inst_1 : TopologicalSpace H]
  {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M}
  {g : M → G}, ContMDiffAt I' I n g x → ∀ (m : ℕ), ContMDiffAt I' I n (fun x => g x ^ m) x
-- Mathlib.Geometry.Polygon.Basic
/-- The `i`-th edge as a set of points using an `affineSegment`.  -/
Polygon.edgeSet : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      {n : ℕ} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → [PartialOrder R] → Polygon P n → Fin n → Set P
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.prevn : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it →
    ∀ n ≤ l.length, String.Legacy.Iterator.ValidFor (List.drop n l) ((List.take n l).reverse ++ r) (it.prevn n)
-- Mathlib.GroupTheory.OrderOfElement
not_isOfFinAddOrder_of_isAddTorsionFree : ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} [IsAddTorsionFree G], a ≠ 0 → ¬IsOfFinAddOrder a
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.smul_eval : ∀ (lc : Lean.Omega.LinearCombo) (i : ℤ) (v : Lean.Omega.Coeffs), (i * lc).eval v = i * lc.eval v
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.instFromJsonOptions : Lean.FromJson Lean.Lsp.CreateFile.Options
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.contDiffOn' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {m n : WithTop ℕ∞},
  m ≤ n → (m = ↑⊤ → n = ⊤) → ContDiffWithinAt 𝕜 n f s x → ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPtInd_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α), MeasureTheory.SimpleFunc.nearestPtInd e 0 = MeasureTheory.SimpleFunc.const α 0
-- Mathlib.Analysis.Normed.Group.Subgroup
Subgroup.normedGroup.eq_1 : ∀ {E : Type u_1} [inst : NormedGroup E] {s : Subgroup E},
  Subgroup.normedGroup =
    { toNorm := Subgroup.seminormedGroup.toNorm, toGroup := s.toGroup, toMetricSpace := Subtype.metricSpace,
      dist_eq := ⋯ }
-- Mathlib.Geometry.Manifold.Instances.Sphere
instChartedSpaceEuclideanSpaceRealFinElemHAddNatOfNatSphere : (n : ℕ) → ChartedSpace (EuclideanSpace ℝ (Fin n)) ↑(Metric.sphere 0 1)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensCarrierAbPresheaf : {X : AlgebraicGeometry.Scheme} →
  {M : X.Modules} → {U : X.Opens} → Module ↑(X.presheaf.obj (Opposite.op U)) ↑(M.presheaf.obj (Opposite.op U))
-- Mathlib.GroupTheory.Transfer
AddSubgroup.leftTransversals.diff.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
  (S T : H.LeftTransversal) [inst_2 : H.FiniteIndex],
  AddSubgroup.leftTransversals.diff ϕ S T = ∑ q, ϕ ⟨-↑(⋯.leftQuotientEquiv q) + ↑(⋯.leftQuotientEquiv q), ⋯⟩
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_self_of_eq_zero : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] {x : F}, x = 0 → inner 𝕜 x x = 0
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.all.eq_def : ∀ (x : ℕ) (x_1 : (i : ℕ) → i < x → Bool),
  x.all x_1 =
    match x, x_1 with
    | 0, f => true
    | n.succ, f => (n.all fun i h => f i ⋯) && f n ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.erase_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M), AddMonoidAlgebra.erase m 0 = 0
-- Mathlib.Algebra.BigOperators.Associated
Associates.exists_mem_multiset_le_of_prime : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] {s : Multiset (Associates M₀)} {p : Associates M₀},
  Prime p → p ≤ s.prod → ∃ a ∈ s, p ≤ a
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.vadd_mem_fundamentalDomain : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (y : ↥(Submodule.span ℤ (Set.range ⇑b))) (x : E),
  y +ᵥ x ∈ ZSpan.fundamentalDomain b ↔ y = -ZSpan.floor b x
-- Init.Data.Array.Range
/-- Replace `zipIdx` with a starting index with `zipIdx` starting from 0,
followed by a `map` increasing the indices.  -/
Array.zipIdx_eq_map_add : ∀ {α : Type u_1} {xs : Array α} {i : ℕ},
  xs.zipIdx i =
    Array.map
      (fun x =>
        match x with
        | (a, j) => (a, i + j))
      xs.zipIdx
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ↑(ProjectiveSpectrum.top 𝒜))
  (z : HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.stalkToFiberRingHom 𝒜 x))
      (AlgebraicGeometry.homogeneousLocalizationToStalk 𝒜 x z) =
    z
-- Init.Data.BitVec.Lemmas
BitVec.ofBool_xor_ofBool : ∀ {b b' : Bool}, BitVec.ofBool b ^^^ BitVec.ofBool b' = BitVec.ofBool (b ^^ b')
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.stateful : Lean.TSyntax `Lean.binderIdent → Lean.Parser.Tactic.MCasesPat
-- Mathlib.Data.Set.Basic
Set.inf_eq_inter : ∀ {α : Type u}, (fun x1 x2 => x1 ⊓ x2) = fun x1 x2 => x1 ∩ x2
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f).inv f =
    Y.ofRestrict ⋯
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_transpose : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M], LinearMap.trace R (Module.Dual R M) ∘ₗ Module.Dual.transpose = LinearMap.trace R M
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_symm : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A),
  (CategoryTheory.shiftFunctorComm C i j).symm = CategoryTheory.shiftFunctorComm C j i
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- A non-quantitative version of Markov inequality for integrable functions: the measure of points
where `‖f x‖ > ε` is finite for all positive `ε`.  -/
MeasureTheory.Integrable.measure_norm_gt_lt_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.Integrable f μ → ∀ {ε : ℝ}, 0 < ε → μ {x | ε < ‖f x‖} < ⊤
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))),
  (TopologicalSpace.Opens.map U.toSpecΓ.base).obj (PrimeSpectrum.basicOpen r) =
    (TopologicalSpace.Opens.map U.ι.base).obj (X.basicOpen r)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) {n : ℕ} (x : ↑(F.H' n S.X₄)),
  CategoryTheory.Abelian.Ext.biprodAddEquiv.symm
      ((CategoryTheory.ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
        ((CategoryTheory.ConcreteCategory.hom (S.toBiprod F n)) x)) =
    (CategoryTheory.Abelian.Ext.mk₀ S.shortComplex.g).comp x ⋯
-- Init.Data.Int.Order
Int.natAbs_sign_of_ne_zero : ∀ {z : ℤ}, z ≠ 0 → z.sign.natAbs = 1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- A stack action is a command that interacts with the top of a stack. Our default position
is at the bottom of all the stacks, so we have to hold on to this action while going to the end
to modify the stack.  -/
Turing.TM2to1.StAct : (K : Type u_1) → (K → Type u_2) → Type u_4 → K → Type (max u_2 u_4)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsRightQuasiInverse.congr : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃},
  u.IsRightQuasiInverse v → u' ≈ u → v' ≈ v → u'.IsRightQuasiInverse v'
-- Mathlib.Data.Set.Finite.Basic
Finset.exists_notMem : ∀ {α : Type u} [Infinite α] (s : Finset α), ∃ a, a ∉ s
-- Mathlib.Topology.Connected.PathConnected
Joined.somePath.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (h : Joined x y), h.somePath = h.somePath
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
le_or_lt_of_add_le_add : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddLeftMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α},
  a₁ + b₁ ≤ a₂ + b₂ → a₁ ≤ a₂ ∨ b₁ < b₂
-- Init.Data.UInt.Bitwise
USize.toUInt8_not : ∀ (a : USize), (~~~a).toUInt8 = ~~~a.toUInt8
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- Given `x, y : E ⊗ F`, `x = y` iff `⟪a ⊗ₜ b, x⟫ = ⟪a ⊗ₜ b, y⟫` for all `a, b`.  -/
TensorProduct.ext_iff_inner_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  {x y : TensorProduct 𝕜 E F}, x = y ↔ ∀ (a : E) (b : F), inner 𝕜 (a ⊗ₜ[𝕜] b) x = inner 𝕜 (a ⊗ₜ[𝕜] b) y
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_surjective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Surjective ⇑f → Function.Surjective (AddSubsemigroup.map f)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toContinuousAffineMap_injective : ∀ {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 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂],
  Function.Injective ContinuousAffineEquiv.toContinuousAffineMap
-- Mathlib.ModelTheory.Algebra.Field.CharP
/-- For a given natural number `n`, `eqZero n` is the sentence in the language of rings
saying that `n` is zero.  -/
FirstOrder.Field.eqZero : ℕ → FirstOrder.Language.ring.Sentence
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_nonpos_iff_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, a + -b ≤ 0 ↔ a ≤ b
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_const_iff : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {l : Filter α} [l.NeBot] {d : E''} {c : F''}, ((fun _x => d) =o[l] fun _x => c) ↔ d = 0
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_eq_of_parseFirstByte_eq_twoMore : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
    b.toBitVec = 14#4 ++ BitVec.setWidth 4 b.toBitVec
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFn_sub : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (f g : ↥(lp E p)),
  ↑(f - g) = ↑f - ↑g
-- Mathlib.Logic.Basic
bex_def : ∀ {α : Sort u_1} {p q : α → Prop}, (∃ x, ∃ (_ : p x), q x) ↔ ∃ x, p x ∧ q x
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- The point mass distribution concentrated at `x`.  -/
Convexity.StdSimplex.single : {R : Type u} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] → {M : Type u_9} → [IsStrictOrderedRing R] → M → Convexity.StdSimplex R M
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_zero'_apply : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂)
  (p : MvPolynomial σ R), MvPolynomial.eval₂ f (fun x => 0) p = f (MvPolynomial.constantCoeff p)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R) (x : R),
  (DoubleQuot.quotQuotEquivQuotSup I J).symm ((Ideal.Quotient.mk (I ⊔ J)) x) = (DoubleQuot.quotQuotMk I J) x
-- Init.WF
PSigma.lexNdepWf : ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop},
  WellFounded r → WellFounded s → WellFounded (PSigma.lexNdep r s)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.branch : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} → {σ : Type u_4} → (σ → Bool) → Turing.TM2.Stmt Γ Λ σ → Turing.TM2.Stmt Γ Λ σ → Turing.TM2.Stmt Γ Λ σ
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
Submodule.subtypeₗᵢ_toLinearMap : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {R' : Type u_11} [inst_1 : Ring R'] [inst_2 : Module R' E]
  (p : Submodule R' E), p.subtypeₗᵢ.toLinearMap = p.subtype