mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.innerRegular : ∀ {α : Type u_1} {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : μ.Regular], μ.InnerRegularWRT IsCompact IsOpen
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite R M], ∃ n S x, ∀ (i : Fin n), IsSimpleModule R ↥(S i)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (f : W.LeftFraction X Y),
  CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk f =
    CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk f
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ordFrac_eq_div : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : Ring.KrullDimLE 1 R] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] [inst_6 : Nontrivial R]
  (a b : ↥(nonZeroDivisors R)),
  (Ring.ordFrac R) (IsLocalization.mk' K (↑a) b) = (Ring.ordMonoidWithZeroHom R) ↑a / (Ring.ordMonoidWithZeroHom R) ↑b
-- Lean.Parser.Attr
Lean.Parser.priorityParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.forgetCreatesLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} →
      [CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor] →
        CategoryTheory.CreatesLimitsOfSize.{v, u, v₁, v₁, max u₁ v₁, u₁} T.forget
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabSorry : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_bsup_le : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u}},
  (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ o.card
-- Mathlib.Algebra.Azumaya.Basic
IsAzumaya.coe_tensorEquivEnd : ∀ (R : Type u_1) [inst : CommSemiring R], ↑(IsAzumaya.tensorEquivEnd R) = AlgHom.mulLeftRight R R
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
_private.Mathlib.MeasureTheory.Integral.IntegralEqImproper.0.MeasureTheory.lintegral_tendsto_of_monotone_of_nat : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {φ : ℕ → Set α},
  MeasureTheory.AECover μ Filter.atTop φ →
    Monotone φ →
      ∀ {f : α → ENNReal},
        AEMeasurable f μ → Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), f x ∂μ))
-- Init.Data.String.Lemmas.FindPos
String.Pos.ofToSlice_prev : ∀ {s : String} {p : s.toSlice.Pos} {h : p ≠ s.toSlice.startPos},
  String.Pos.ofToSlice (p.prev h) = (String.Pos.ofToSlice p).prev ⋯
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
/-- We say that a morphism `f : X ⟶ Y` is geometrically connected if for all `Spec K ⟶ Y` with `K`
a field, `X ×[Y] Spec K` is connected.  -/
AlgebraicGeometry.GeometricallyConnected : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Topology.Constructions
CofiniteTopology.nhds_eq : ∀ {X : Type u} (x : CofiniteTopology X), nhds x = pure x ⊔ Filter.cofinite
-- Mathlib.NumberTheory.LSeries.MellinEqDirichlet
/-- Tailored version for even Jacobi theta functions.  -/
hasSum_mellin_pi_mul_sq : ∀ {ι : Type u_1} [Countable ι] {a : ι → ℂ} {r : ι → ℝ} {F : ℝ → ℂ} {s : ℂ},
  0 < s.re →
    (∀ t ∈ Set.Ioi 0, HasSum (fun i => if r i = 0 then 0 else a i * ↑(Real.exp (-Real.pi * r i ^ 2 * t))) (F t)) →
      (Summable fun i => ‖a i‖ / |r i| ^ s.re) → HasSum (fun i => s.Gammaℝ * a i / ↑|r i| ^ s) (mellin F (s / 2))
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Equivalent.pi : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} {Nᵢ : ι → Type u_9} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : (i : ι) → AddCommMonoid (Nᵢ i)] [inst_3 : AddCommMonoid P]
  [inst_4 : (i : ι) → Module R (Mᵢ i)] [inst_5 : (i : ι) → Module R (Nᵢ i)] [inst_6 : Module R P] [inst_7 : Fintype ι]
  {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P},
  (∀ (i : ι), (Q i).Equivalent (Q' i)) → (QuadraticMap.pi Q).Equivalent (QuadraticMap.pi Q')
-- Lean.Meta.AppBuilder
/-- Returns `eq_false' h`
`h` must have type definitionally equal to `p → False` in the current
reducibility setting.  -/
Lean.Meta.mkEqFalse' : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listDecode.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'}, FirstOrder.Language.Term.listDecode [] = []
-- Lean.Parser.Term.Basic
/-- Implicit binder, like `{x y : A}` or `{x y}`.
In regular applications, whenever all parameters before it have been specified,
then a `_` placeholder is automatically inserted for this parameter.
Implicit parameters should be able to be determined from the other arguments and the return type
by unification.

In `@` explicit mode, implicit binders behave like explicit binders.
 -/
Lean.Parser.Term.implicitBinder : optParam Bool false → Lean.Parser.Parser
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.ofLinear_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} (x : M₂),
  (LinearEquiv.ofLinear f g h₁ h₂).symm x = g x
-- Mathlib.Data.Finite.Defs
Bool.instFinite : Finite Bool
-- Mathlib.Analysis.InnerProductSpace.Defs
instCoreOfCore : (𝕜 : Type u_4) →
  (F : Type u_5) →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] → [cd : InnerProductSpace.Core 𝕜 F] → PreInnerProductSpace.Core 𝕜 F
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.WF)
  (h' : k ∈ Std.DHashMap.Raw.filterMap f m), (f k (m.get k ⋯)).isSome = true
-- Init.Data.List.Sublist
List.tail_sublist : ∀ {α : Type u_1} (l : List α), l.tail.Sublist l
-- Lean.Meta.Tactic.Grind.Types
/-- Number of applications per function symbol. This information is only collected if `set_option diagnostics true`  -/
Lean.Meta.Grind.Counters.apps : Lean.Meta.Grind.Counters → Lean.PHashMap Lean.Name ℕ
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.instBinderF : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `IsCentralScalar` across an `Equiv`  -/
Equiv.isCentralScalar : ∀ (M : Type u_1) {α : Type u_4} {β : Type u_5} [inst : SMul M β] [inst_1 : SMul Mᵐᵒᵖ β] (e : α ≃ β)
  [IsCentralScalar M β], IsCentralScalar M α
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_dual' : ∀ {α : Type u_1} {E : Set α} {M : Matroid α}, M.E = E → (M.restrictSubtype E)✶ = M✶.restrictSubtype E
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.toNontrivial : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsStrictOrderedRing R], Nontrivial R
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.prod : ∀ {α : Type u_1} {M : Type u_3} [inst : CommMonoid M] {ι : Type u_4} {f : ι → α → M},
  (∀ (i : ι), Function.HasFiniteMulSupport (f i)) →
    ∀ (s : Finset ι), Function.HasFiniteMulSupport fun a => ∏ i ∈ s, f i a
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso.inv.app X).left =
    CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
/-- Set of representatives for the orbits under `S` and `T`  -/
FixedDetMatrices.reps : (m : ℤ) → Set (FixedDetMatrix (Fin 2) ℤ m)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ext : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  {w w' : HNNExtension.NormalWord d}, w.head = w'.head → w.toList = w'.toList → w = w'
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.comp_f₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.ShortComplex C}
  (h : S₃.L₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₁ h =
    CategoryTheory.CategoryStruct.comp f.f₁ (CategoryTheory.CategoryStruct.comp g.f₁ h)
-- Mathlib.Algebra.Homology.Functor
HomologicalComplex.complexOfFunctorsToFunctorToComplex_obj : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3}
  {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c),
  HomologicalComplex.complexOfFunctorsToFunctorToComplex.obj C = C.asFunctor
-- Mathlib.Analysis.Normed.Module.Basic
/-- A normed vector space over an infinite normed field is a noncompact space.
This cannot be an instance because in order to apply it,
Lean would have to search for `NormedSpace 𝕜 E` with unknown `𝕜`.
We register this as an instance in two cases: `𝕜 = E` and `𝕜 = ℝ`.  -/
NormedSpace.noncompactSpace : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NormedField 𝕜] [Infinite 𝕜] [inst_2 : NormedAddCommGroup E] [Nontrivial E]
  [NormedSpace 𝕜 E], NoncompactSpace E
-- Mathlib.FieldTheory.Finite.Valuation
FiniteField.instIsTrivialOn : ∀ {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [inst : Field Fq] [Finite Fq] [inst_2 : Ring A] [inst_3 : Algebra Fq A]
  [inst_4 : LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ), Valuation.IsTrivialOn Fq v
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.compCLMOfAntilipschitz_apply : ∀ (𝕜 : Type u_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedAddCommGroup D]
  [inst_6 : NormedSpace ℝ D] [inst_7 : NormedSpace 𝕜 F] {K : NNReal} {g : D → E} (hg : Function.HasTemperateGrowth g)
  (h'g : AntilipschitzWith K g) (f : SchwartzMap E F), ⇑((SchwartzMap.compCLMOfAntilipschitz 𝕜 hg h'g) f) = ⇑f ∘ g
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- The relative gluing datum associated to the family of the `colim Dᵢ`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰 →
                      [∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                            CategoryTheory.Limits.PreservesColimitsOfShape J
                              (CategoryTheory.MorphismProperty.Over.pullback P ⊤
                                (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))] →
                        AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.absoluteForm.sizeOf_spec : ∀ (uri : Std.Http.URI), sizeOf (Std.Http.RequestTarget.absoluteForm uri) = 1 + sizeOf uri
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_Icc : ∀ {a b : ℝ}, MeasureTheory.volume.real (Set.Icc a b) = max (b - a) 0
-- Mathlib.Order.Interval.Finset.Basic
Finset.left_notMem_Ioo : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], a ∉ Finset.Ioo a b
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F] (K₁ : CochainComplex C₁ ℤ)
  (K₂ : CochainComplex C₂ ℤ) (n : ℤ),
  (CategoryTheory.Functor.commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).inv.app K₁ =
    (K₁.mapBifunctorShift₁Iso K₂ F n).inv
-- Mathlib.Analysis.Convex.Between
affineSegment_comm : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] (x y : P), affineSegment R x y = affineSegment R y x
-- Mathlib.RingTheory.Jacobson.Radical
Module.map_jacobson_of_bijective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Bijective ⇑f → Submodule.map f (Module.jacobson R M) = Module.jacobson R₂ M₂
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The identity map as an equivariant monoid homomorphism.  -/
MulDistribMulActionHom.id : (M : Type u_1) →
  [inst : Monoid M] → {A : Type u_4} → [inst_1 : Monoid A] → [inst_2 : MulDistribMulAction M A] → A →*[M] A
-- Mathlib.Topology.Sets.Opens
Homeomorph.opensCongr_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  f.opensCongr.symm = f.symm.opensCongr
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry.prevSiblings : Lean.Server.FileWorker.NamespaceEntry → Array Lean.Lsp.DocumentSymbol
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)]
  {c : ℕ}, (Std.DHashMap.emptyWithCapacity c).get! a = default
-- Mathlib.MeasureTheory.Measure.Prod
/-- Note: the converse is not true without assuming that `s` is measurable. For a counterexample,
see Walter Rudin *Real and Complex Analysis*, example (c) in section 8.9.  -/
MeasureTheory.Measure.measure_ae_null_of_prod_null : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)},
  (μ.prod ν) s = 0 → (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_vecMul_apply : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (v : V) (vec : V → α),
  Matrix.vecMul vec (SimpleGraph.adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] (U : ↑Y.affineOpens),
  (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.fromNormalization f).base).obj ↑U =
    AlgebraicGeometry.Scheme.Hom.opensRange ((AlgebraicGeometry.Scheme.Hom.normalizationOpenCover f).f U)
-- Mathlib.Data.List.Sort
List.sortedLE_iff_pairwise : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLE ↔ List.Pairwise (fun x1 x2 => x1 ≤ x2) l
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.natCast_mul_inj : ∀ {n : ℕ} {a b : Cardinal.{u_1}}, n ≠ 0 → (↑n * a = ↑n * b ↔ a = b)
-- Init.Core
/-- The **quotient axiom**, which asserts the equality of elements related by the quotient's relation.

The relation `r` does not need to be an equivalence relation to use this axiom. When `r` is not an
equivalence relation, the quotient is with respect to the equivalence relation generated by `r`.

`Quot.sound` is part of the built-in primitive quotient type:
 * `Quot` is the built-in quotient type.
 * `Quot.mk` places elements of the underlying type `α` into the quotient.
 * `Quot.lift` allows the definition of functions from the quotient to some other type.
 * `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
   with `Quot.mk`; it is analogous to the [recursor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=recursors) for a
   structure.

[Quotient types](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=quotients) are described in more detail in the Lean Language
Reference.
 -/
Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sSup_neg : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M] (s : Set M),
  sSup (-s) = -sInf s
-- Mathlib.RingTheory.Spectrum.Prime.Module
/-- `M[1/f] = 0` if and only if `D(f) ∩ Supp M = 0`.  -/
LocalizedModule.subsingleton_iff_disjoint : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : R},
  Subsingleton (LocalizedModule.Away f M) ↔ Disjoint (↑(PrimeSpectrum.basicOpen f)) (Module.support R M)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_not_contains_map_fst : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValue? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) =
      if Std.Internal.List.containsKey k l₂ = true then none else Std.Internal.List.getValue? k l₁
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.top_rpow_of_neg : ∀ {y : ℝ}, y < 0 → ⊤ ^ y = 0
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.data.injEq : ∀ (fData fData_1 : Mathlib.Meta.FunProp.FunctionData),
  (Mathlib.Meta.FunProp.MaybeFunctionData.data fData = Mathlib.Meta.FunProp.MaybeFunctionData.data fData_1) =
    (fData = fData_1)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.dropSuffix_prop_eq_dropSuffix_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.dropSuffix p = s.dropSuffix fun x => decide (p x)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.Pattern.Model.find?_eq_none_iff : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [inst_4 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id]
  [∀ (s : String.Slice), Std.LawfulIteratorLoop (σ s) Id Id] [inst_6 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] {s : String.Slice},
  s.find? pat = none ↔ ∀ (pos : s.Pos), ¬String.Slice.Pattern.Model.MatchesAt pat pos
-- Mathlib.Data.Multiset.UnionInter
Multiset.cons_union_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α), a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t
-- Batteries.CodeAction.Misc
/-- The "Add subgoals" code action puts `· done` subgoals for any goals remaining at the end of a
proof.
```
example : True ∧ True := by
  constructor
  -- <- here
```
is transformed to
```
example : True ∧ True := by
  constructor
  · done
  · done
```
 -/
Batteries.CodeAction.addSubgoalsActionCore : Lean.Lsp.CodeActionParams →
  ℕ → Lean.Syntax.Stack → List Lean.MVarId → Lean.Server.RequestM (Array Lean.Server.LazyCodeAction)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.toFinset_zero : ∀ {α : Type u_2} [inst : Zero α], Set.toFinset 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multicospanShapeEnd_snd : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (f : CategoryTheory.Arrow J),
  (CategoryTheory.Limits.multicospanShapeEnd J).snd f = f.right
-- Mathlib.Order.Bounds.Basic
IsGreatest.upperBounds_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → upperBounds s = Set.Ici a
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.spectrum.«term↑ₐ_2» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `MulEquiv α β` is the type of an equiv `α ≃ β` which preserves multiplication.  -/
MulEquiv : (M : Type u_9) → (N : Type u_10) → [Mul M] → [Mul N] → Type (max u_10 u_9)
-- Mathlib.Tactic.Simps.Basic
/-- name for this projection used in the generated `simp` lemmas  -/
Simps.ParsedProjectionData.newName : Simps.ParsedProjectionData → Lean.Name
-- Init.Prelude
ReaderT.instApplicativeOfMonad : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → Applicative (ReaderT ρ m)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.proj_pi : ∀ {R : Type u_1} [inst : Semiring R] {M₂ : Type u_3} [inst_1 : TopologicalSpace M₂] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M₂] {ι : Type u_4} {φ : ι → Type u_5} [inst_4 : (i : ι) → TopologicalSpace (φ i)]
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →L[R] φ i) (i : ι),
  ContinuousLinearMap.proj i ∘SL ContinuousLinearMap.pi f = f i
-- Mathlib.Data.List.Duplicate
List.duplicate_iff_two_le_count : ∀ {α : Type u_1} {l : List α} {x : α} [inst : DecidableEq α], List.Duplicate x l ↔ 2 ≤ List.count x l
-- Mathlib.RingTheory.PicardGroup
ClassGroup.equivPic_symm_apply : ∀ (R : Type u_5) [inst : CommRing R] [inst_1 : IsDomain R] (a : CommRing.Pic R),
  (ClassGroup.equivPic R).symm a =
    (ClassGroup.mulEquivUnitsSubmoduleQuotRange R).symm
      ((QuotientGroup.congr (Submodule.unitsToPic R (FractionRing R)).ker (Units.map ↑(Submodule.spanSingleton R)).range
          (MulEquiv.refl (Submodule R (FractionRing R))ˣ) ⋯)
        ((QuotientGroup.quotientKerEquivRange (Submodule.unitsToPic R (FractionRing R))).symm
          ((MulEquiv.subgroupCongr ⋯).symm ((MulEquiv.subgroupCongr ⋯).symm (Subgroup.topEquiv.symm a)))))
-- Lean.Elab.Arg
Lean.Elab.Term.Arg.stx : Lean.Syntax → Lean.Elab.Term.Arg
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.hasFiniteIntegral : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε}, MeasureTheory.Integrable f μ → MeasureTheory.HasFiniteIntegral f μ
-- Init.Data.List.Sublist
List.IsSuffix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.reverse <+: l₂.reverse
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅},
  t.contains (t.min he) = true