mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Length
Submodule.height_lt_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  [IsNoetherian R M] (N : Submodule R M), Order.height N < ⊤
-- Mathlib.Analysis.Normed.Ring.Int
Int.toNat_add_toNat_neg_eq_norm : ∀ (n : ℤ), ↑n.toNat + ↑(-n).toNat = ‖n‖
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
_private.Mathlib.MeasureTheory.Measure.Haar.Quotient.0.termπ : Lean.ParserDescr
-- Mathlib.Order.WellFounded
/-- Given a function `f : α → β` where `β` carries a well-founded `<`, and a non-empty subset `s`
of `α`, this is an element of `s` whose image under `f` is minimal in the sense of
`Function.not_lt_argminOn`.

See also `Set.Finite.exists_minimalFor` and related lemmas for the case when `α` or `s` is finite.

TODO Consider removing this definition in favour of `exists_minimalFor_of_wellFoundedLT`.  -/
Function.argminOn : {α : Type u_1} → {β : Type u_2} → (α → β) → [inst : LT β] → [WellFoundedLT β] → (s : Set α) → s.Nonempty → α
-- Mathlib.Probability.Distributions.Gamma
/-- The Lebesgue integral of the gamma pdf over nonpositive reals equals 0  -/
ProbabilityTheory.lintegral_gammaPDF_of_nonpos : ∀ {x a r : ℝ}, x ≤ 0 → ∫⁻ (y : ℝ) in Set.Iio x, ProbabilityTheory.gammaPDF a r y = 0
-- Mathlib.Data.Set.Image
Set.preimage_rangeSplitting : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → Set.preimage (Set.rangeSplitting f) = Set.image (Set.rangeFactorization f)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ) (X : C),
  (t.natTransTruncGEOfLE a a ⋯).app X = CategoryTheory.CategoryStruct.id ((t.truncGE a).obj X)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.toCircle_zsmul : ∀ {T : ℝ} (x : AddCircle T) (n : ℤ), (n • x).toCircle = x.toCircle ^ n
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.ground_not_isBase : ∀ {α : Type u_1} (M : Matroid α) [h : M✶.RankPos], ¬M.IsBase M.E
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.withZero_apply_symm_apply : ∀ {G : Type u_6} {H : Type u_7} [inst : Group G] [inst_1 : PartialOrder G] [inst_2 : Group H] [inst_3 : PartialOrder H]
  (e : G ≃*o H) (a : WithZero H), (OrderMonoidIso.withZero e).symm a = (WithZero.map' ↑(↑e).symm) a
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_mul_left : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α}, (f * g).NeBot → f.NeBot
-- Lean.Util.LeanOptions
/-- Add the options from `new`, overriding those in `self`.  -/
Lean.LeanOptions.append : Lean.LeanOptions → Lean.LeanOptions → Lean.LeanOptions
-- Init.Internal.Order.Lemmas
Lean.Order.Option.monotone_getDM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] {α : Type u}
  {γ : Type w} [inst_2 : Lean.Order.PartialOrder γ] (o : Option α) (y : γ → m α),
  Lean.Order.monotone y → Lean.Order.monotone fun x => o.getDM (y x)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioi_or_Iio : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  a ≠ 0 →
    ∀ {U V : Set α},
      U ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a} →
        V = (fun x => a * x) ⁻¹' U → V ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- An equivalence of categories lifts to an equivalence of their group objects.  -/
CategoryTheory.Equivalence.mapGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (e : C ≌ D) → [e.functor.Monoidal] → [e.inverse.Monoidal] → CategoryTheory.Grp C ≌ CategoryTheory.Grp D
-- Batteries.Data.Fin.Lemmas
Fin.find?_zero : ∀ {p : Fin 0 → Bool}, Fin.find? p = none
-- Init.System.IO
IO.FS.instInhabitedSystemTime : Inhabited IO.FS.SystemTime
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instFiniteResidueField : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsMaximal], Module.Finite R I.ResidueField
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.const_one : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : One β],
  ContinuousMap.const α 1 = 1
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Restrict a `w'`-small `0`-hypercover to a `w'`-`0`-hypercover.  -/
CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} → {S : C} → (E : J.ZeroHypercover S) → [E.Small] → J.ZeroHypercover S
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.uniformContinuous_eval_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] [ContinuousSMul 𝕜 E] (x : ι → E),
  UniformContinuous fun f => f x
-- Mathlib.Data.Set.Finite.Lattice
/-- If sets `s i` are finite for all `i` from a finite set `t` and are empty for `i ∉ t`, then the
union `⋃ i, s i` is a finite set.  -/
Set.Finite.iUnion : ∀ {α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set ι},
  t.Finite → (∀ i ∈ t, (s i).Finite) → (∀ i ∉ t, s i = ∅) → (⋃ i, s i).Finite
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_throw_lift_ExceptT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {ε : Type u} {m : Type u → Type v} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : MonadExceptOf ε m] {ε' α : Type u} {post : α → Pred}
  {epost : EPost.Cons✝ (ε' → Pred) EPred} (err : ε),
  Std.Internal.Do.wp (MonadExceptOf.throw err) post epost =
    Std.Internal.Do.wp (MonadExceptOf.throw err) (Std.Internal.Do.EPost.Cons.pushExcept post epost) epost.tail
-- Aesop.Search.Expansion
Aesop.RuleResult.proved.sizeOf_spec : ∀ (newRapps : Array Aesop.RappRef), sizeOf (Aesop.RuleResult.proved newRapps) = 1 + sizeOf newRapps
-- Init.Data.Vector.Nat
Vector.prod_eq_foldl_nat : ∀ {n : ℕ} {xs : Vector ℕ n}, xs.prod = Vector.foldl (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instCompactSpaceAutFunctorFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  CompactSpace (CategoryTheory.Aut F)
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valuation.norm_pos_iff_valuation_pos : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀)
  [hv : v.RankOne] {x : L}, 0 < v.norm x ↔ 0 < v x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_fun_pow_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n m : ℕ},
  iteratedDeriv n (fun x => x ^ m) 0 = ↑(if n = m then m.factorial else 0)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The length of reduced words provides a norm on an additive free group.  -/
FreeAddGroup.norm : {α : Type u_1} → [DecidableEq α] → FreeAddGroup α → ℕ
-- Init.Data.Vector.Find
Vector.findFinIdx?_empty : ∀ {α : Type u_1} {p : α → Bool}, Vector.findFinIdx? p #v[] = none
-- Lean.Parser.Term
Lean.Parser.Term.sufficesDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjoint_isClosed : ∀ {𝕜 : 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] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E], Dense ↑T.domain → T.adjoint.IsClosed
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying type.  -/
CommRingCat.carrier : CommRingCat → Type u
-- Mathlib.Algebra.Module.LinearMap.Defs
RingHom.coe_toSemilinearMap : ∀ {R : Type u_1} {S : Type u_5} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S), ⇑f.toSemilinearMap = ⇑f
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomFunctor_obj_obj : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (C : Type u)
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X : Cᵒᵖ) (Y : C),
  ((CategoryTheory.eHomFunctor V C).obj X).obj Y = Opposite.unop X ⟶[V] Y
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
equivTangentBundleProd_symm_apply_snd : ∀ {𝕜 : 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) (M : Type u_4)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  (M' : Type u_7) [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
  (p : TangentBundle I M × TangentBundle I' M'), ((equivTangentBundleProd I M I' M').symm p).snd = (p.1.snd, p.2.snd)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_graph_iff' : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) {x : E × F}, x ∈ f.graph ↔ ∃ y, (↑y, ↑f y) = x
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_absolutelyContinuous' : ∀ (μ : ℝ) {v : NNReal}, v ≠ 0 → MeasureTheory.volume.AbsolutelyContinuous (ProbabilityTheory.gaussianReal μ v)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The cocone associated to the pushout of `f` and `g`  -/
CategoryTheory.Limits.pushout.cocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) → (g : X ⟶ Z) → [CategoryTheory.Limits.HasPushout f g] → CategoryTheory.Limits.PushoutCocone f g
-- Mathlib.Algebra.DirectSum.Module
/-- `uncurry` as a linear map.  -/
DirectSum.sigmaLuncurry : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type v} →
      {α : ι → Type u_1} →
        {δ : (i : ι) → α i → Type w} →
          [DecidableEq ι] →
            [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
              [inst_3 : (i : ι) → (j : α i) → Module R (δ i j)] →
                (DirectSum ι fun i => DirectSum (α i) fun j => δ i j) →ₗ[R]
                  DirectSum ((x : ι) × α x) fun i => δ i.fst i.snd
-- Mathlib.Data.Set.NAry
Set.image2_union_inter_subset : ∀ {α : Type u_1} {β : Type u_3} {f : α → α → β} {s t : Set α},
  (∀ (a b : α), f a b = f b a) → Set.image2 f (s ∪ t) (s ∩ t) ⊆ Set.image2 f s t
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_fiberwise_of_maps_to' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ}
  [inst_1 : DecidableEq κ] {g : ι → κ},
  (∀ i ∈ s, g i ∈ t) → ∀ (f : κ → M), ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (g i)
-- Mathlib.Algebra.FreeMonoid.Basic
/-- if two types are isomorphic, the additive free monoids over those types are
isomorphic  -/
FreeAddMonoid.freeAddMonoidCongr : {α : Type u_6} → {β : Type u_7} → α ≃ β → FreeAddMonoid α ≃+ FreeAddMonoid β
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
HomotopyCategory.homologyFunctor_shiftMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} {n : ℤ}
  (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (a a' : ℤ) (h : n + a = a'),
  (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
      (CategoryTheory.ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ))) a a' h =
    CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app K)
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
        ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app L))
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f : α → E} {l : Filter α} [l.IsMeasurablyGenerated],
  StronglyMeasurableAtFilter f l μ →
    μ.FiniteAtFilter l → ∀ {b : E}, Filter.Tendsto f l (nhds b) → MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X₁ : C}
  [inst_2 : CategoryTheory.MonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one f)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Swapping the first two points preserves affine independence.  -/
AffineIndependent.comm_left : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, AffineIndependent k ![p₁, p₂, p₃] → AffineIndependent k ![p₂, p₁, p₃]
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_copy : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α) (s : Set α) (hs : s = ↑L), ↑(L.copy s hs) = s
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract_eq_fract : ∀ {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 ι] (m n : E),
  ZSpan.fract b m = ZSpan.fract b n ↔ -m + n ∈ Submodule.span ℤ (Set.range ⇑b)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.coe_ofSpan : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : ⊤ ≤ Submodule.span K s), ⇑(Module.Basis.ofSpan hs) = Subtype.val
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_iff_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
  Filter.Tendsto f l₁ l₂ ↔ l₁ ≤ Filter.comap f l₂
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.add_const : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {γ : Type u_7} {f : E → γ} [inst_4 : AddCommMonoid γ] [inst_5 : PartialOrder γ]
  [IsOrderedCancelAddMonoid γ] [inst_7 : Module 𝕜 γ],
  StrictConcaveOn 𝕜 s f → ∀ (b : γ), StrictConcaveOn 𝕜 s (f + fun x => b)
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat.eq_1 : ∀ (q : ℚ), q.toNNRat = ⟨max q 0, ⋯⟩
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_mul_right : ∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M),
  edist (a * c) (b * c) = edist a b
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For a nonzero `k = r/s ∈ K`, the fractional ideal `(k)` is equal to the product
`∏_v v^(val_v(r) - val_v(s))`.  -/
FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {n : R},
  n ≠ 0 →
    ∀ (d : ↥(nonZeroDivisors R)),
      ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R),
          ↑v.asIdeal ^
            (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) -
              ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
        FractionalIdeal.spanSingleton (nonZeroDivisors R) (IsLocalization.mk' K n d)
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_toUInt8 : ∀ (n : UInt32), n.toUInt8.toUInt16 = n.toUInt16 % 256
-- Mathlib.GroupTheory.OrderOfElement
nsmul_eq_zero_iff_modEq : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, n • x = 0 ↔ n ≡ 0 [MOD addOrderOf x]
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_of_omega0_sq_le : ∀ {o : Ordinal.{u_1}}, Ordinal.omega0 ^ 2 ≤ o → Cardinal.preBeth o = Cardinal.beth o
-- Mathlib.Algebra.Group.Equiv.Defs
/-- A bijective `AddSemigroup` homomorphism is an isomorphism  -/
AddEquiv.ofBijective : {M : Type u_9} →
  {N : Type u_10} →
    {F : Type u_11} →
      [inst : Add M] →
        [inst_1 : Add N] → [inst_2 : FunLike F M N] → [AddHomClass F M N] → (f : F) → Function.Bijective ⇑f → M ≃+ N
-- Init.Data.Array.Zip
Array.zipWithAll_replicate : ∀ {α : Type u_1} {β : Type u_2} {α_1 : Type u_3} {f : Option α → Option β → α_1} {a : α} {b : β} {n : ℕ},
  Array.zipWithAll f (Array.replicate n a) (Array.replicate n b) = Array.replicate n (f (some a) (some b))
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_ball : ∀ (a r : ℝ), MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal (2 * r)
-- Mathlib.Topology.MetricSpace.Defs
dist_toDual : ∀ {X : Type u_1} [inst : Dist X] (a b : X), dist (OrderDual.toDual a) (OrderDual.toDual b) = dist a b
-- Mathlib.CategoryTheory.ComposableArrows.Four
/-- The morphism `mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃₄` when `f₃ ≫ f₃ = f₃₄`.  -/
CategoryTheory.ComposableArrows.fourδ₄Toδ₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {i₀ i₁ i₂ i₃ i₄ : C} →
      (f₁ : i₀ ⟶ i₁) →
        (f₂ : i₁ ⟶ i₂) →
          (f₃ : i₂ ⟶ i₃) →
            (f₄ : i₃ ⟶ i₄) →
              (f₃₄ : i₂ ⟶ i₄) →
                autoParam (CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄)
                    CategoryTheory.ComposableArrows.fourδ₄Toδ₃._auto_1 →
                  (CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃₄)
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.sdiff_compl_neighborFinset_inter_eq : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V] {v w : V},
  G.Adj v w →
    ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) = (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.Result.map.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → motive (EStateM.Result.ok a s')) →
        ((e : ε) → (s' : σ) → motive (EStateM.Result.error e s')) → motive x
-- Mathlib.Analysis.Distribution.Distribution
Distribution.lineDerivCLM_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] {n k : ℕ∞}
  [inst_5 : IsTopologicalAddGroup F] [inst_6 : ContinuousSMul ℝ F] {v₁ v₂ : E},
  Distribution.lineDerivCLM (v₁ + v₂) = Distribution.lineDerivCLM v₁ + Distribution.lineDerivCLM v₂
-- Mathlib.Control.Basic
fish_assoc : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α : Type u_1} {β γ φ : Type u} (f : α → m β) (g : β → m γ)
  (h : γ → m φ), (f >=> g) >=> h = f >=> g >=> h
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- The Dirichlet density is at most `1`.  -/
NumberField.Set.HasDirichletDensity.le_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ},
  NumberField.Set.HasDirichletDensity S δ → δ ≤ 1
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] (h : B →A[R] C)
  (f : A →A[R] B), ↑(h.comp f) = (↑h).comp ↑f
-- Mathlib.Order.Lattice
SemilatticeInf.mk : {α : Type u} →
  [toPartialOrder : PartialOrder α] →
    (inf : α → α → α) →
      (∀ (a b : α), inf a b ≤ a) →
        (∀ (a b : α), inf a b ≤ b) → (∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c) → SemilatticeInf α
-- Mathlib.Data.List.Chain
/-- If there is an `r`-chain starting from `a` and ending at `b`, then `a` and `b` are related by the
reflexive transitive closure of `r`.
 -/
List.relationReflTransGen_of_exists_isChain_cons : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α} (l : List α),
  List.IsChain r (a :: l) → (a :: l).getLast ⋯ = b → Relation.ReflTransGen r a b
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.instToString : ToString Mathlib.Tactic.Translate.ArgReorder
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr : Type
-- Mathlib.Algebra.Group.Prod
AddEquiv.uniqueProd_symm_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : Unique N] (a : M),
  AddEquiv.uniqueProd.symm a = (default, a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
bot_lt_affineSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, ⊥ < affineSpan k s ↔ s.Nonempty
-- Init.Data.Int.DivMod.Lemmas
Int.neg_emod_self : ∀ (a : ℤ), -a % a = 0
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (k : K) {Z : C}
  (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).inv h) =
    CategoryTheory.CategoryStruct.comp (G.map (e.counitInv.app k))
      (CategoryTheory.CategoryStruct.comp (w.hom.app (e.inverse.obj k))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (e.inverse.obj k)) h))
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.eigenvalues_def : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  hT.eigenvalues hn =
    LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn ∘
      ⇑(Tuple.sort (LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn)) ∘ ⇑Fin.revPerm
-- Mathlib.Order.Disjoint
IsCompl.ofDual : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a b : αᵒᵈ},
  IsCompl a b → IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b)
-- Lean.Linter.UnusedVariables
/-- The main data structure used to collect information from the info tree regarding unused
variables.  -/
Lean.Linter.UnusedVariables.References : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β}, Std.DHashMap.Const.getD (m.erase k) k fallback = fallback