mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `b₈` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.b₈ : {R : Type u} → [CommRing R] → WeierstrassCurve R → R
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `n`-th homology of the alternating constant complex is `X` for `n = 0`.  -/
ChainComplex.alternatingConstHomologyDataZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X : C) → (n : ℕ) → n = 0 → (HomologicalComplex.sc (ChainComplex.alternatingConst.obj X) n).HomologyData
-- Lean.Parser.Term
Lean.Parser.Term.char : Lean.Parser.Parser
-- Mathlib.Data.Sum.Order
Sum.inr_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], StrictMono Sum.inr
-- Lean.Message
/-- Without context, a `MessageData` object may be missing information
(e.g. hover info) for pretty printing, or may print an error. Hence,
`addMessageContext` should be called on all constructed `MessageData`
(e.g. via `m!`) before taking it out of context (e.g. leaving `MetaM` or
`CoreM`).
 -/
Lean.AddMessageContext.addMessageContext : {m : Type → Type} → [self : Lean.AddMessageContext m] → Lean.MessageData → m Lean.MessageData
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.isSplitEpi_iff_surjective : ∀ {X Y : Type u} (f : X ⟶ Y), CategoryTheory.IsSplitEpi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.String.Basic
String.get! : String → String.Pos.Raw → Char
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.measure_notConvergentSeq_tendsto_zero : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι] [Countable ι],
  (∀ (n : ι), Measurable fun a => edist (f n a) (g a)) →
    MeasurableSet s →
      μ s ≠ ⊤ →
        (∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
          ∀ (n : ℕ),
            Filter.Tendsto (fun j => μ (s ∩ MeasureTheory.Egorov.notConvergentSeq f g n j)) Filter.atTop (nhds 0)
-- Mathlib.Data.Seq.Defs
/-- Map a function over a sequence.  -/
Stream'.Seq.map : {α : Type u} → {β : Type v} → (α → β) → Stream'.Seq α → Stream'.Seq β
-- Mathlib.Topology.Spectral.Hom
SpectralMap.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : TopologicalSpace α} {inst_1 : TopologicalSpace β} {toFun : α → β}
  {spectral' : IsSpectralMap toFun} {toFun_1 : α → β} {spectral'_1 : IsSpectralMap toFun_1},
  { toFun := toFun, spectral' := spectral' } = { toFun := toFun_1, spectral' := spectral'_1 } → toFun = toFun_1
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.LinearEquiv.coe_lift : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (g : M ≃ₗ[R] N),
  ↑(DividedPowerAlgebra.mapEquiv g) = DividedPowerAlgebra.map R ↑g
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_Iio_add_one : ∀ {a : Ordinal.{u}} {f : ↑(Set.Iio a) → Ordinal.{u}}, StrictMono f → Order.IsSuccPrelimit a → ⨆ i, f i + 1 = ⨆ i, f i
-- Init.Data.String.Lemmas.Pattern.Split.Char
_private.Init.Data.String.Lemmas.Pattern.Split.Char.0.String.Slice.Pattern.Model.split.eq_1 : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} (firstRejected curr : s.Pos)
  (hle : firstRejected ≤ curr),
  String.Slice.Pattern.Model.split pat firstRejected curr hle =
    if h : curr = s.endPos then [s.subslice firstRejected curr hle]
    else
      match hd : String.Slice.Pattern.Model.matchAt? pat curr with
      | some pos =>
        have this := ⋯;
        s.subslice firstRejected curr hle :: String.Slice.Pattern.Model.split pat pos pos ⋯
      | none => String.Slice.Pattern.Model.split pat firstRejected (curr.next h) ⋯
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_Icc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Neg.neg '' Set.Icc a b = Set.Icc (-b) (-a)
-- Mathlib.Probability.StrongLaw
/-- **Strong law of large numbers**, almost sure version: if `X n` is a sequence of independent
identically distributed integrable random variables taking values in a Banach space,
then `n⁻¹ • ∑ i ∈ range n, X i` converges almost surely to `𝔼[X 0]`. We give here the strong
version, due to Etemadi, that only requires pairwise independence.  -/
ProbabilityTheory.strong_law_ae : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : MeasurableSpace E] [BorelSpace E] (X : ℕ → Ω → E),
  MeasureTheory.Integrable (X 0) μ →
    Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
        ∀ᵐ (ω : Ω) ∂μ,
          Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))
-- Mathlib.GroupTheory.Coset.Defs
Subgroup.quotientEquivOfEq.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h : s = t),
  Subgroup.quotientEquivOfEq h =
    { toFun := Quotient.map' id ⋯, invFun := Quotient.map' id ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_div_iff_of_pos_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (a / c ≤ b / c ↔ a ≤ b)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.mono_homologyMap_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n q : ℤ),
  q ≤ n →
    CategoryTheory.Mono
      (HomologicalComplex.homologyMap (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π✝ f n) q)
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_ai_cert : Lean.Grind.AC.Expr → Lean.Grind.AC.Expr → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.RingTheory.Ideal.Colon
Submodule.iInf_colon : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Set M}
  {ι : Sort u_3} (f : ι → Submodule R M), (⨅ i, f i).colon S = ⨅ i, (f i).colon S
-- Lean.Data.Json.Parser
Lean.Json.Parser.arrayCore : Array Lean.Json → Std.Internal.Parsec.String.Parser (Array Lean.Json)
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
Fin.nndist_insertNth_insertNth : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_4} [inst : (i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1))
  (x y : α i) (f g : (j : Fin n) → α (i.succAbove j)),
  nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g)
-- Init.Omega.Constraint
Lean.Omega.Constraint.sat.eq_1 : ∀ (c : Lean.Omega.Constraint) (t : ℤ), c.sat t = decide (c.lowerBound.sat t = true ∧ c.upperBound.sat t = true)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.insert_inj_on' : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), Set.InjOn (fun a => insert a s) ↑sᶜ
-- Mathlib.Algebra.BigOperators.Finprod
finprod_of_not_hasFiniteMulSupport : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M}, ¬Function.HasFiniteMulSupport f → ∏ᶠ (i : α), f i = 1
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of a field element can be expressed as a sum over the positive parts
of the logarithms of its various absolute values.  -/
Height.logHeight₁_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.logHeight₁ x =
    (Multiset.map (fun v => (v x).posLog) Height.AdmissibleAbsValues.archAbsVal).sum +
      ∑ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), (↑v x).posLog
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_toContinuousMultilinearMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N), ⇑f.toContinuousMultilinearMap = ⇑f
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊤.starProjection = ContinuousLinearMap.id 𝕜 E
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Let `f` be a local homeomorphism of a nontrivially normed field, let `a` be a point in its
target. if `f` is `n` times continuously differentiable at `f.symm a`, and if the derivative at
`f.symm a` is nonzero, then `f.symm` is `n` times continuously differentiable at the point `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
OpenPartialHomeomorph.contDiffAt_symm_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [CompleteSpace 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜)
  {f₀' a : 𝕜},
  f₀' ≠ 0 →
    a ∈ f.target → HasDerivAt (↑f) f₀' (↑f.symm a) → ContDiffAt 𝕜 n (↑f) (↑f.symm a) → ContDiffAt 𝕜 n (↑f.symm) a
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.range_succ' : ∀ {n nn n' : ℕ}, Mathlib.Meta.NormNum.IsNat n nn → nn = n'.succ → Finset.range n = Finset.cons n' (Finset.range n') ⋯
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The leading coefficient of a product of polynomials is equal to
the product of the leading coefficients, provided that this product is nonzero.

See `Polynomial.leadingCoeff_multiset_prod` (without the `'`) for a version for integral domains,
where this condition is automatically satisfied.
 -/
Polynomial.leadingCoeff_multiset_prod' : ∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
  (Multiset.map Polynomial.leadingCoeff t).prod ≠ 0 →
    t.prod.leadingCoeff = (Multiset.map Polynomial.leadingCoeff t).prod
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.foldr_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} {δ : Type w} [Std.TransCmp cmp]
  {f : α → β → δ → δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.TreeMap.Raw.foldr f init t₁ = Std.TreeMap.Raw.foldr f init t₂
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
/-- **Alias** of `CategoryTheory.Functor.mapVertexGroup_apply`. -/
CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup_apply : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type v} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (c : C) (a : c ⟶ c), (φ.mapVertexGroup c) a = φ.map a
-- Mathlib.Computability.PartrecBasis
/-- Analogous to `Nat.Partrec'` for `ℕ`-valued functions, a predicate for partial recursive
vector-valued functions.  -/
Nat.Partrec'.Vec : {n m : ℕ} → (List.Vector ℕ n → List.Vector ℕ m) → Prop
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.oddKernel_functional_equation : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.oddKernel a x = 1 / x ^ (3 / 2) * HurwitzZeta.sinKernel a (1 / x)
-- Lean.DocString.Parser
/-- Items like 1)  -/
Lean.Doc.Parser.OrderedListType.parenAfter : Lean.Doc.Parser.OrderedListType
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If two sets coincide locally, then derivatives within these sets
are the same.  -/
mfderivWithin_congr_set : ∀ {𝕜 : 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'] {f : M → M'} {x : M} {s t : Set M},
  s =ᶠ[nhds x] t → mfderiv[s] f x = mfderiv[t] f x
-- Mathlib.RingTheory.Localization.InvSubmonoid
/-- There is a canonical map from `M` to `invSubmonoid` sending `x` to `1 / x`.  -/
IsLocalization.toInvSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [IsLocalization M S] → ↥M →* ↥(IsLocalization.invSubmonoid M S)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.eq_of_length_zero : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), p.length = 0 → a = b
-- Mathlib.Algebra.Group.AddChar
AddChar.mk : {A : Type u_1} →
  [inst : AddMonoid A] →
    {M : Type u_2} →
      [inst_1 : Monoid M] →
        (toFun : A → M) → toFun 0 = 1 → (∀ (a b : A), toFun (a + b) = toFun a * toFun b) → AddChar A M
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_succ_succ : ∀ {m n : ℕ}, ((m + 1)...n + 1).toArray = Array.map (fun x => x + 1) (m...n).toArray
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.instIsIsoτ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) [CategoryTheory.IsIso f], CategoryTheory.IsIso f.τ₁
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- The elements in the match result.

The `Nat` in the tree map represents the `score` of the results.
The elements are arrays of arrays, where each sub-array corresponds to one discr tree pattern.
 -/
Lean.Meta.RefinedDiscrTree.MatchResult.elts : {α : Type} → Lean.Meta.RefinedDiscrTree.MatchResult α → Std.TreeMap ℕ (Array (Array α)) compare
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_zero : ↑0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.append_reverseAux : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk u x),
  (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.sub.match_3.eq_1 : ∀ (motive : ONote → ONote → Sort u_1) (x : ONote) (h_1 : (x : ONote) → motive ONote.zero x)
  (h_2 : (o : ONote) → motive o ONote.zero)
  (h_3 :
    (o₁ e₁ : ONote) →
      (n₁ : ℕ+) →
        (a₁ : ONote) →
          o₁ = e₁.oadd n₁ a₁ → (e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)),
  (match ONote.zero, x with
    | ONote.zero, x => h_1 x
    | o, ONote.zero => h_2 o
    | o₁@h:(e₁.oadd n₁ a₁), e₂.oadd n₂ a₂ => h_3 o₁ e₁ n₁ a₁ h e₂ n₂ a₂) =
    h_1 x
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentChangeRegistrationOptions.mk.sizeOf_spec : ∀ (documentSelector? : Option Lean.Lsp.DocumentSelector) (syncKind : Lean.Lsp.TextDocumentSyncKind),
  sizeOf { documentSelector? := documentSelector?, syncKind := syncKind } =
    1 + sizeOf documentSelector? + sizeOf syncKind
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {b c d : α}, min c d < b → Set.Iic b ∪ Set.Ioc c d = Set.Iic (max b d)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_add_union_subset : ∀ {α : Type u_2} [inst : AddCommSemigroup α] {s t : Set α}, s ∩ t + (s ∪ t) ⊆ s + t
-- Mathlib.Order.Heyting.Basic
sdiff_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), (a \ b) \ c = a \ (b ⊔ c)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.DTreeMap.map f t},
  Std.DTreeMap.Const.get (Std.DTreeMap.map f t) k h' = f k (Std.DTreeMap.Const.get t k ⋯)
-- Mathlib.Data.Quot
Quotient.map_surjective : ∀ {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {f : α → β} (h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b),
  Function.Surjective f → Function.Surjective (Quotient.map f h)
-- Mathlib.Algebra.Lie.TransferInstance
Equiv.lieEquiv_apply : ∀ {R : Type u_1} {L' : Type u_2} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (e : L' ≃ L) (a : L'), (Equiv.lieEquiv R e) a = e a
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_algebraMap : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GSemiring 𝒜] [inst_9 : DirectSum.GSemiring ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (r : R),
  (TensorProduct.gradedComm R 𝒜 ℬ)
      ((algebraMap R (TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i))) r) =
    (algebraMap R (TensorProduct R (DirectSum ι fun i => ℬ i) (DirectSum ι fun i => 𝒜 i))) r
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.mk_normalize : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α),
  Associates.mk (normalize x) = Associates.mk x
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- `rel` as a ring congruence.  -/
LinearAlgebra.FreeProduct.ringCon : {I : Type u} →
  [DecidableEq I] →
    (R : Type v) →
      [inst : CommSemiring R] →
        (A : I → Type w) →
          [inst_1 : (i : I) → Semiring (A i)] →
            [inst_2 : (i : I) → Algebra R (A i)] → RingCon (LinearAlgebra.FreeProduct.FreeTensorAlgebra R A)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_le_restrict_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
  MeasurableSet i → (v.restrict i ≤ w.restrict i ↔ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ w j)
-- Mathlib.Data.List.OffDiag
List.offDiag.eq_1 : ∀ {α : Type u_1} (l : List α),
  l.offDiag =
    List.flatMap
      (fun x =>
        match x with
        | (x, n) => List.map (Prod.mk x) (l.eraseIdx n))
      l.zipIdx
-- Init.Data.SInt.Lemmas
UInt32.toUInt32_toInt32 : ∀ (x : UInt32), x.toInt32.toUInt32 = x
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instCompletelyNormalSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [CompletelyNormalSpace M], CompletelyNormalSpace Mᵈᵃᵃ
-- Lean.Elab.MutualInductive
/-- For nested inductive types, the kernel adds a variable number of auxiliary recursors.
Let the elaborator know about them as well. (Other auxiliaries have already been
registered by `addDecl` via `Declaration.getNames`.)
NOTE: If we want to make inductive elaboration parallel, this should switch to using
reserved names.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.addAuxRecs : List Lean.InductiveType → Lean.Elab.TermElabM Unit
-- Mathlib.MeasureTheory.Integral.Layercake
/-- The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:

For a nonnegative function `f` on a measure space, the Lebesgue integral of `f` can
be written (roughly speaking) as: `∫⁻ f ∂μ = ∫⁻ t in 0..∞, μ {ω | f(ω) ≥ t}`.

See `MeasureTheory.lintegral_eq_lintegral_meas_lt` for a version with sets of the form
`{ω | f(ω) > t}` instead.  -/
MeasureTheory.lintegral_eq_lintegral_meas_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} (μ : MeasureTheory.Measure α),
  0 ≤ᵐ[μ] f → AEMeasurable f μ → ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a}
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.of.sizeOf_spec : ∀ {R : Type u_1} {X : Type u_2} [inst : SizeOf R] [inst_1 : SizeOf X] (a : X),
  sizeOf (FreeAlgebra.Pre.of a) = 1 + sizeOf a
-- Init.System.FilePath
/-- Splits a path into a list of individual file names at the platform-specific path separator.
 -/
System.FilePath.components : System.FilePath → List String
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpointWeights_singleton_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  {i j : Fin (n + 1)}, i ≠ j → 0 < s.touchpointWeights {i} i j
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toListRev_ensureTermination : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterators.Finite α m] {it : Std.IterM m β}, it.ensureTermination.toListRev = List.reverse <$> it.toList
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isUltrametricDist_of_forall_nnnorm_mul_le_max_nnnorm : ∀ {S' : Type u_2} [inst : SeminormedGroup S'], (∀ (x y : S'), ‖x * y‖₊ ≤ max ‖x‖₊ ‖y‖₊) → IsUltrametricDist S'
-- Mathlib.RingTheory.HopfAlgebra.Quotient
Ideal.IsHopfIdeal.antipode_mem : ∀ {R : Type u_1} {A : Type u_2} {inst : CommRing R} {inst_1 : Ring A} {inst_2 : HopfAlgebraStruct R A} {I : Ideal A}
  [self : Ideal.IsHopfIdeal R I] ⦃x : A⦄, x ∈ I → (HopfAlgebraStruct.antipode R) x ∈ I
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- `direction_of_nonempty` gives the same submodule as `direction`.  -/
AffineSubspace.directionOfNonempty_eq_direction : ∀ {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 : AffineSubspace k P} (h : (↑s).Nonempty),
  AffineSubspace.directionOfNonempty h = s.direction
-- Init.Data.Bool
Bool.eq_false_or_eq_true : ∀ (b : Bool), b = true ∨ b = false
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceMulOpposite : {α : Type ua} → [UniformSpace α] → UniformSpace αᵐᵒᵖ
-- Mathlib.LinearAlgebra.Dimension.Finite
Module.finite_of_rank_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M], Module.rank R M = 0 → Module.Finite R M
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey? k = none
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.pow_two : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : α), a ^ 2 = a * a
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SupSet γ]
  (f : sSupHom β γ) (g : sSupHom α β), f.comp g = { toFun := ⇑f ∘ ⇑g, map_sSup' := ⋯ }
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_sSup_of_directedOn : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {S : Set (NonUnitalSubsemiring R)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Init.Data.List.Zip
List.map_snd_zip : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, l₂.length ≤ l₁.length → List.map Prod.snd (l₁.zip l₂) = l₂
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMat_.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v₁, u_1} D] [inst_3 : CategoryTheory.Preadditive D]
  (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1) [inst_4 : F.Additive], F.mapMat_ = F_1.mapMat_
-- Mathlib.Order.KrullDimension
Order.krullDim_pos_iff : ∀ {α : Type u_1} [inst : Preorder α], 0 < Order.krullDim α ↔ ∃ x y, x < y