mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.range_eq : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), Set.range ⇑e = Set.univ
-- Init.Data.Range.Polymorphic.NatLemmas
/-- Induction principle for proving properties of `Nat`-based ranges of the form `a...=b` by
varying the upper bound.

In the `base` case, one proves that for any `a : Nat` and `b : Nat` with
`b ≤ a`, the statement holds for the subsingleton range `a...=b`.

In the `step` case, one proves that for any `a : Nat` and `b : Nat`, if the
statement holds for `a...=b`, it also holds for the larger range `a...=(b + 1)`.

The following is an example reproving `length_toList_rcc`.

```
example (a b : Nat) : (a...=b).toList.length = b + 1 - a := by
  induction a, b using Nat.induct_rcc_right
  case base a b hge =>
    by_cases h : b < a
    · simp only [Nat.toList_rcc_eq_nil, List.length_nil, *]
      omega
    · have : b = a := by omega
      simp only [Nat.toList_rcc_eq_singleton, List.length_singleton,
        Nat.add_sub_cancel_left, *]
  case step a b hle ih =>
    rw [Nat.toList_rcc_succ_right_eq_append (by omega), List.length_append,
      List.length_singleton, ih] <;> omega
``` -/
Nat.induct_rcc_right : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (a b : ℕ), b ≤ a → motive a b) → (∀ (a b : ℕ), a ≤ b → motive a b → motive a (b + 1)) → ∀ (a b : ℕ), motive a b
-- Mathlib.Algebra.Group.Pi.Basic
Pi.leftCancelSemigroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → LeftCancelSemigroup (f i)],
  Pi.leftCancelSemigroup = { toSemigroup := Pi.semigroup, toIsLeftCancelMul := ⋯ }
-- Mathlib.Analysis.Convex.Between
/-- A point lies in the closed interior of a 1-dimensional face of a simplex if and only if it lies
weakly between its vertices.  -/
Affine.Simplex.mem_closedInterior_face_iff_wbtw : ∀ {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] {n : ℕ} (s : Affine.Simplex R P n) {p : P}
  {i j : Fin (n + 1)} (h : i ≠ j), p ∈ (s.face ⋯).closedInterior ↔ Wbtw R (s.points i) p (s.points j)
-- Batteries.Data.List.Lemmas
List.count_getElem_take_succ : ∀ {α : Type u_1} [inst : BEq α] [EquivBEq α] {xs : List α} {i : ℕ} {hi : i < xs.length},
  List.count xs[i] (List.take (i + 1) xs) = List.count xs[i] (List.take i xs) + 1
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_le_coeIdeal' : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [IsLocalization S P], S ≤ nonZeroDivisors R → ∀ {I J : Ideal R}, ↑I ≤ ↑J ↔ I ≤ J
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.repr_ceil_apply : ∀ {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 : E) (i : ι), (b.repr ↑(ZSpan.ceil b m)) i = ↑⌈(b.repr m) i⌉
-- Init.Omega.LinearCombo
Lean.Omega.instReprLinearCombo.repr : Lean.Omega.LinearCombo → ℕ → Std.Format
-- Mathlib.Algebra.Order.Field.Power
Even.zpow_pos : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  Even n → a ≠ 0 → 0 < a ^ n
-- Mathlib.Data.Set.Opposite
Set.singleton_unop : ∀ {α : Type u_1} (x : αᵒᵖ), {x}.unop = {Opposite.unop x}
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.refl_apply : ∀ (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : Mul M] (m : M), (ContinuousMulEquiv.refl M) m = m
-- Mathlib.Data.PFun
/-- The monad `bind` function, pointwise `Part.bind`  -/
PFun.bind : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α →. β) → (β → α →. γ) → α →. γ
-- Mathlib.Data.List.Defs
/-- List of all permutations of `l`.

```
     permutations [1, 2, 3] =
       [[1, 2, 3], [2, 1, 3], [3, 2, 1],
        [2, 3, 1], [3, 1, 2], [1, 3, 2]]
```
 -/
List.permutations : {α : Type u_1} → List α → List (List α)
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Polynomial.eq_quadratic_of_degree_le_two : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R},
  p.degree ≤ 2 →
    p = Polynomial.C (p.coeff 2) * Polynomial.X ^ 2 + Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.extendScalars_inf : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E'),
  IntermediateField.extendScalars h ⊓ IntermediateField.extendScalars h' = IntermediateField.extendScalars ⋯
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.mk_Ioi_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedGT α] (i : α),
  ((Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2) → Cardinal.mk ↑(Set.Ioi i) < Cardinal.mk α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertMany_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp],
  Std.ExtDTreeMap.Const.insertMany t [] = t
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_C : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (r : R),
  (PowerSeries.expand p hp) (PowerSeries.C r) = PowerSeries.C r
-- Mathlib.Algebra.Star.Unitary
commute_unitary_iff_star_left_conjugate : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {x u : R}, u ∈ unitary R → (Commute u x ↔ star u * x * u = x)
-- Mathlib.Order.SymmDiff
bot_bihimp : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), bihimp ⊥ a = aᶜ
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.coe_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : α), ↑(a * b) = ↑a * ↑b
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_coeff : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.norm_eq_coeff_cert lhs rhs p k = true →
    (Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs) =
      (Int.Internal.Linear.Poly.denote' ctx p = 0)
-- Mathlib.Data.PNat.Xgcd
/-- `x` satisfies `a / d = w + x` at the final step.  -/
PNat.XgcdType.x : PNat.XgcdType → ℕ
-- Mathlib.Analysis.Normed.Algebra.Exponential
Ring.inverse_exp : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (x : 𝔸),
  Ring.inverse (NormedSpace.exp x) = NormedSpace.exp (-x)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousSMul.measurableSMul₂ : ∀ {M : Type u_7} {α : Type u_8} [inst : TopologicalSpace M] [inst_1 : MeasurableSpace M] [OpensMeasurableSpace M]
  [inst_3 : TopologicalSpace α] [SecondCountableTopologyEither M α] [inst_5 : MeasurableSpace α] [BorelSpace α]
  [inst_7 : SMul M α] [ContinuousSMul M α], MeasurableSMul₂ M α
-- Init.Control.Lawful.MonadAttach.Instances
instWeaklyLawfulMonadAttachExceptTOfLawfulMonad : ∀ {m : Type (max u_1 u_2) → Type u_3} {ε : Type (max u_1 u_2)} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [WeaklyLawfulMonadAttach m], WeaklyLawfulMonadAttach (ExceptT ε m)
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.smul_mem_smul_iff : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (g : G) {x : X} {pt : DiscreteTiling.PlacedTile ps}, g • x ∈ g • pt ↔ x ∈ pt
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- Every linear isometry on a real finite-dimensional Hilbert space is measure-preserving.  -/
LinearIsometryEquiv.measurePreserving : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : MeasurableSpace F] [inst_7 : BorelSpace F] [inst_8 : FiniteDimensional ℝ E] [inst_9 : FiniteDimensional ℝ F]
  (f : E ≃ₗᵢ[ℝ] F), MeasureTheory.MeasurePreserving (⇑f) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.ext : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂} {inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂}
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {x y : P.Hom Q},
  x.weightMap = y.weightMap → x.coweightMap = y.coweightMap → x.indexEquiv = y.indexEquiv → x = y
-- Init.Data.Nat.Div.Basic
_private.Init.Data.Nat.Div.Basic.0.Nat.mod.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (n m : ℕ) (h_1 : (x : ℕ) → motive 0 x)
  (h_2 : (n n_1 : ℕ) → n = n_1.succ → (m : ℕ) → motive n_1.succ m),
  (match n.succ, m with
    | 0, x => h_1 x
    | n@h:n_1.succ, m => h_2 n n_1 h m) =
    h_2 n.succ n ⋯ m
-- Mathlib.GroupTheory.Archimedean
/-- If a nontrivial subgroup of a linear ordered commutative group is disjoint
with the interval `Set.Ioo 1 a` for some `1 < a`, then the set of elements greater than 1 of this
group admits the least element.  -/
Subgroup.exists_isLeast_one_lt : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G},
  H ≠ ⊥ → ∀ {a : G}, 1 < a → Disjoint (↑H) (Set.Ioo 1 a) → ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.pi : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_6}
  {X : ι → Type u_7} [inst_3 : (i : ι) → Convexity.ConvexSpace R (X i)] {s : Set ι} {x : (i : ι) → X i}
  {t : (i : ι) → Set (X i)}, (∀ i ∈ s, Convexity.IsStarConvexSet R (x i) (t i)) → Convexity.IsStarConvexSet R x (s.pi t)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snocEquiv_symm_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) (f : (i : Fin (n + 1)) → α i),
  (Fin.snocEquiv α).symm f = (f (Fin.last n), Fin.init f)
-- Mathlib.Order.Interval.Basic
/-- `{a}` as an interval.  -/
Interval.pure : {α : Type u_1} → [inst : Preorder α] → α → Interval α
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousWithinAt_ciInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ᶠ (y : α) in nhdsWithin x s, BddBelow (Set.range fun i => f i y)) →
    (∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x) → UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.ge_ule : ∀ {w : ℕ} (x y : BitVec w), x ≥ y ↔ (!x.ult y) = true
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_some_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {a : α},
  a ∈ t → t.get? a = some (t.get! a)
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Look up an expression in the atoms, recording it if it has not previously appeared.

Return its index, and, if it is new, a collection of interesting facts about the atom.
* for each new atom `a` of the form `((x : Nat) : Int)`, the fact that `0 ≤ a`
* for each new atom `a` of the form `x / k`, for `k` a positive numeral, the facts that
  `k * a ≤ x < k * a + k`
* for each new atom of the form `((a - b : Nat) : Int)`, the fact:
  `b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0`
 -/
Lean.Elab.Tactic.Omega.lookup : Lean.Expr → Lean.Elab.Tactic.Omega.OmegaM (ℕ × Option (List Lean.Expr))
-- Mathlib.Data.Part
/-- `Part` extensionality  -/
Part.ext' : ∀ {α : Type u_1} {o p : Part α}, (o.Dom ↔ p.Dom) → (∀ (h₁ : o.Dom) (h₂ : p.Dom), o.get h₁ = p.get h₂) → o = p
-- Mathlib.Algebra.Homology.LocalCohomology
/-- The diagram of powers of `J` is initial in the diagram of all ideals with
radical containing `J`. This uses Noetherianness.  -/
localCohomology.ideal_powers_initial : ∀ {R : Type u} [inst : CommRing R] {J : Ideal R} [hR : IsNoetherian R R],
  (localCohomology.idealPowersToSelfLERadical J).Initial
-- Mathlib.Topology.Maps.Strict.Group
/-- A group homomorphism is strict if and only if its `rangeRestrict` is an open quotient map.  -/
MonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {f : G →* H} [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H] [IsTopologicalGroup G], Topology.IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- This proves that Inf and restrict commute for outer measures, so long as the set of
outer measures is nonempty.  -/
MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict : ∀ {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) {s : Set α},
  m.Nonempty → (MeasureTheory.OuterMeasure.restrict s) (sInf m) = sInf (⇑(MeasureTheory.OuterMeasure.restrict s) '' m)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.ext_iff : ∀ {X Y : AddMagmaCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.fromStructuredArrow_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.StructuredArrow PUnit.{w + 1} F),
  (CategoryTheory.CategoryOfElements.fromStructuredArrow F).obj X =
    ⟨X.right, (CategoryTheory.ConcreteCategory.hom X.hom) PUnit.unit⟩
-- Mathlib.Algebra.Group.AddChar
/-- The additive characters on a commutative additive group form a commutative group.

Note that the inverse is defined using negation on the domain; we do not assume `M` has an
inversion operation for the definition (but see `AddChar.map_neg_eq_inv` below).  -/
AddChar.instCommGroup : {A : Type u_1} → {M : Type u_2} → [inst : AddCommGroup A] → [inst_1 : CommMonoid M] → CommGroup (AddChar A M)
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.derivation_C : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (Polynomial R) A] (D : Derivation R (Polynomial R) A) (a : R), D (Polynomial.C a) = 0
-- Std.Data.DTreeMap.Internal.Operations
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Internal.Impl.ofList : {α : Type u} → {β : α → Type v} → [Ord α] → List ((a : α) × β a) → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Condensed.Light.Functors
instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Faithful
-- Mathlib.Analysis.Analytic.Constructions
/-- The geometric series `1 + x + x ^ 2 + ...` as a `FormalMultilinearSeries`.  -/
formalMultilinearSeries_geometric : (𝕜 : Type u_2) →
  [inst : NontriviallyNormedField 𝕜] →
    (A : Type u_7) → [inst_1 : NormedRing A] → [inst_2 : NormedAlgebra 𝕜 A] → FormalMultilinearSeries 𝕜 A A
-- Mathlib.Algebra.Order.GroupWithZero.Basic
MulPosMono.toMulPosStrictMono : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsRightCancelMulZero α] [MulPosMono α],
  MulPosStrictMono α
-- Mathlib.RingTheory.DividedPowers.Basic
/-- Variant of `DividedPowers.equiv_apply`  -/
DividedPowers.equiv_apply' : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} [inst_1 : CommSemiring B] {J : Ideal B}
  {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) {n : ℕ} {a : A},
  ((DividedPowers.equiv h) hI).dpow n (e a) = e (hI.dpow n a)
-- Init.Data.Nat.Lemmas
Nat.sub_lt_add_one : ∀ (a b : ℕ), a - b < a + 1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.comp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.LaxTrans X Y)
  (θ : CategoryTheory.Oplax.LaxTrans Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_const' : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α}, (∀ᵐ (x : α) (y : α) ∂μ, f x = f y) → AEMeasurable f μ
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_finite : ∀ {α : Type u_1} {M : Matroid α} {R : Set α}, R.Finite → (M.restrict R).Finite
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact : ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [AlgebraicGeometry.QuasiCompactCover 𝒰]
  {U : S.Opens},
  IsCompact ↑U → ∃ n f V, (∀ (i : Fin n), AlgebraicGeometry.IsAffineOpen (V i)) ∧ ⋃ i, ⇑(𝒰.f (f i)) '' ↑(V i) = ↑U
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.instMulActionQuotient.eq_1 : ∀ {S : Type u_2} (M : Type u_3) [inst : Monoid S] [inst_1 : MulAction S M] (c : SMulCon S M),
  SMulCon.instMulActionQuotient M c = { toSMul := SMulCon.instSMulQuotient M c, mul_smul := ⋯, one_smul := ⋯ }
-- Lean.Structure
Lean.instReprStructureFieldInfo : Repr Lean.StructureFieldInfo
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiringClass.mul_mem : ∀ {S : Type u_1} {R : outParam (Type u)} {inst : NonUnitalNonAssocSemiring R} {inst_1 : SetLike S R}
  [self : NonUnitalSubsemiringClass S R] {s : S} {a b : R}, a ∈ s → b ∈ s → a * b ∈ s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- The discriminant of a quadratic form `Q : QuadraticForm R (n → R)` generalizes the discriminant
of a quadratic polynomial.  -/
QuadraticForm.discr' : {R : Type u_3} →
  {n : Type w} → [Fintype n] → [DecidableEq n] → [inst : CommRing R] → [Invertible 2] → QuadraticForm R (n → R) → R
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.structureSheafInType.mul_apply : ∀ {R A : Type u} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)}
  (s t : (AlgebraicGeometry.structureSheafInType R A).obj.obj (Opposite.op U)) (x : ↥U), ↑(s * t) x = ↑s x * ↑t x
-- Mathlib.Probability.Distributions.Pareto
/-- The Pareto pdf is strongly measurable.  -/
ProbabilityTheory.stronglyMeasurable_paretoPDFReal : ∀ (t r : ℝ), MeasureTheory.StronglyMeasurable (ProbabilityTheory.paretoPDFReal t r)
-- Mathlib.Analysis.CStarAlgebra.Classes
instNonUnitalCommCStarAlgebraForall : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [Fintype ι] → [(i : ι) → NonUnitalCommCStarAlgebra (A i)] → NonUnitalCommCStarAlgebra ((i : ι) → A i)
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_allOnes : ∀ {v i : ℕ}, (BitVec.allOnes v).getLsbD i = decide (i < v)
-- Init.Notation
/-- `p,*,?` is shorthand for `sepBy(p, ",", allowTrailingSep)`.
It parses 0 or more occurrences of `p` separated by `,`, possibly including
a trailing `,`, that is: `empty | p | p, | p,p | p,p, | p,p,p | ...`.

It produces a `nullNode` containing a `SepArray` with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
 -/
«stx_,*,?» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.terminal_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Factorisation.terminal.π = CategoryTheory.CategoryStruct.id Y
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.snd_comp_prod : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [inst : VAdd M α] [inst_1 : VAdd N γ]
  [inst_2 : VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ), (AddActionHom.snd N γ δ).comp (f.prod g) = g
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongrAddEquiv.eq_1 : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14}
  {M₁' : Type u_15} {M₂' : Type u_16} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₁']
  [inst_3 : Semiring R₂'] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁']
  [inst_7 : AddCommMonoid M₂'] [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁']
  [inst_11 : Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [inst_12 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_13 : RingHomInvPair σ₂₁ σ₁₂] [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂)
  (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'),
  e₁.arrowCongrAddEquiv e₂ =
    { toFun := fun f => (↑e₂ ∘ₛₗ f) ∘ₛₗ ↑e₁.symm, invFun := fun f => (↑e₂.symm ∘ₛₗ f) ∘ₛₗ ↑e₁, left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoZero'_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (a : A) (ha : a = 0) (X : C),
  (CategoryTheory.Functor.CommShift.isoZero' F A a ha).hom.app X =
    CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero' C a ha).hom.app X))
      ((CategoryTheory.shiftFunctorZero' D a ha).inv.app (F.obj X))
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instMulOneClass : {α : Type u_1} → [MulOneClass α] → MulOneClass (Lex α)
-- Std.Data.HashMap.Lemmas
Std.HashMap.ofList_singleton : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {k : α} {v : β}, Std.HashMap.ofList [(k, v)] = ∅.insert k v
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.of_forall_get?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (∀ (k : α), t₁.get? k = t₂.get? k) → t₁.Equiv t₂
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- As the associator and left and right unitors are defined as eqToIso of category axioms, the
bicategory structure on `CatEnrichedOrdinary C` is strict.  -/
CategoryTheory.CatEnrichedOrdinary.instStrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C],
  CategoryTheory.Bicategory.Strict (CategoryTheory.CatEnrichedOrdinary C)
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Ici ↑a = Set.Ici a
-- Mathlib.Data.ENNReal.Real
ENNReal.natCast_lt_ofReal : ∀ {n : ℕ} {r : ℝ}, ↑n < ENNReal.ofReal r ↔ ↑n < r
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The composite of `(coprod.inl ▷ X) : Y ⊗ X ⟶ (Y ⨿ Z) ⊗ X` and
`(∂R X Y Z).inv :  (Y ⨿ Z) ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)` is equal to the left coprojection
`coprod.inl : Y ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)`.  -/
CategoryTheory.whiskerRight_coprod_inl_rightDistrib_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C]
  {X Y Z Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X)
      (CategoryTheory.CategoryStruct.comp (∂R X Y Z).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
-- Init.Grind.Attr
/-- Reset all `grind` attributes. This command is intended for testing purposes only and should not be used in applications.
 -/
Lean.Parser.resetGrindAttrs : Lean.ParserDescr
-- Batteries.Lean.Expr
/-- Turns an expression that is a natural number literal into a natural number.  -/
Lean.Expr.natLit! : Lean.Expr → ℕ