mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_4 : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.clear p k q) =
    insert (Turing.PartrecToTM2.Λ'.clear p k q) (Turing.PartrecToTM2.trStmts₁ q)
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.equivalenceOfEquiv_functor : ∀ {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I),
  (CategoryTheory.Pi.equivalenceOfEquiv C e).functor =
    CategoryTheory.Functor.pi' fun i =>
      (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm i)).comp (CategoryTheory.Pi.eqToEquivalence C ⋯).functor
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsNonZero → ∀ (k : K), ⇑β = k • ⇑α → k = -1 ∨ k = 0 ∨ k = 1
-- Std.Do.Triple.SpecLemmas
MonadState.modifyGet.eq_1 : ∀ {σ : Type u} (m : Type u → Type v) [self : MonadState σ m], @modifyGet σ m self = self.3
-- Mathlib.MeasureTheory.Integral.CircleIntegral
le_radius_cauchyPowerSeries : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : NNReal),
  ↑R ≤ (cauchyPowerSeries f c ↑R).radius
-- Mathlib.RingTheory.Binomial
Ring.multichoose_succ_succ : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Pow R ℕ] [NatPowAssoc R] [inst_3 : BinomialRing R] (r : R)
  (k : ℕ), Ring.multichoose (r + 1) (k + 1) = Ring.multichoose r (k + 1) + Ring.multichoose (r + 1) k
-- Mathlib.RingTheory.Spectrum.Prime.Topology
_private.Mathlib.RingTheory.Spectrum.Prime.Topology.0.PrimeSpectrum.«termZ(_)» : Lean.ParserDescr
-- Init.Data.Vector.Lemmas
Vector.flatten.eq_1 : ∀ {α : Type u_1} {n m : ℕ} (xs : Vector (Vector α n) m),
  xs.flatten = Vector.mk (Array.map Vector.toArray xs.toArray).flatten ⋯
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.linearIndependent_rows_of_det_ne_zero : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] [IsDomain R]
  {A : Matrix m m R}, A.det ≠ 0 → LinearIndependent R fun i => A i
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_norm_rpow_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} {p : ENNReal},
  MeasureTheory.AEStronglyMeasurable f μ →
    p ≠ 0 → p ≠ ⊤ → (MeasureTheory.Integrable (fun x => ‖f x‖ ^ p.toReal) μ ↔ MeasureTheory.MemLp f p μ)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing.eq_1 : ∀ (x : ONote),
  x.fastGrowing =
    match (motive := (x_1 : Option ONote ⊕ (ℕ → ONote)) → x.FundamentalSequenceProp x_1 → ℕ → ℕ) x.fundamentalSequence,
      ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), h =>
      have this := ⋯;
      fun i => a.fastGrowing^[i] i
    | Sum.inr f, h => fun i =>
      have this := ⋯;
      (f i).fastGrowing i
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.liftHom.match_1.eq_1 : ∀ {B : Type u_1} [inst : Quiver B] (motive : (x x_1 : CategoryTheory.FreeBicategory B) → (x ⟶ x_1) → Sort u_3)
  (x x_1 : B) (f : x ⟶ x_1) (h_1 : (x x_2 : B) → (f : x ⟶ x_2) → motive x x_2 (CategoryTheory.FreeBicategory.Hom.of f))
  (h_2 : (a : B) → motive a a (CategoryTheory.FreeBicategory.Hom.id a))
  (h_3 :
    (x x_2 b : B) →
      (f : CategoryTheory.FreeBicategory.Hom x b) →
        (g : CategoryTheory.FreeBicategory.Hom b x_2) → motive x x_2 (f.comp g)),
  (match x, x_1, CategoryTheory.FreeBicategory.Hom.of f with
    | x, x_2, CategoryTheory.FreeBicategory.Hom.of f => h_1 x x_2 f
    | a, .(a), CategoryTheory.FreeBicategory.Hom.id .(a) => h_2 a
    | x, x_2, f.comp g => h_3 x x_2 b f g) =
    h_1 x x_1 f
-- Mathlib.Order.IsNormal
Order.IsNormal.strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Order.IsNormal f → StrictMono f
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lmul''_eq_lid_comp_mapOfCompatibleSMul : ∀ (R : Type uR) {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.TensorProduct.lmul'' R =
    (↑(Algebra.TensorProduct.lid S S)).comp (Algebra.TensorProduct.mapOfCompatibleSMul S R S S S)
-- Mathlib.Tactic.Sat.FromLRAT
/-- Build the type and value of the reified theorem. This rewrites all the SAT definitions
into standard operators on `Prop`, for example if the formula is `[[1, 2], [-1, 2], [-2]]` then
this produces a proof of `⊢ ∀ a b : Prop, (a ∧ b) ∨ (¬a ∧ b) ∨ ¬b`. We use the input `nvars` to
decide how many quantifiers to use.

Most of the proof is under `2 * nvars + 1` quantifiers
`a1 .. an : Prop, v : Valuation, h1 : v 0 ↔ a1, ... hn : v (n-1) ↔ an ⊢ ...`, and we do the index
arithmetic by hand.

  1. First, we call `reifyFormula ctx'` which returns `a` and `pr : reify v ctx' a`
  2. Then we build `fun (v : Valuation) (h1 : v 0 ↔ a1) ... (hn : v (n-1) ↔ an) ↦ pr`
  3. We have to lower expression `a` from step 1 out of the quantifiers by lowering all variable
     indices by `nvars+1`. This is okay because `v` and `h1..hn` do not appear in `a`.
  4. We construct the expression `ps`, which is `a1 .. an : Prop ⊢ [a1, ..., an] : List Prop`
  5. `refute ctx (hf : ctx.proof []) (fun v h1 .. hn ↦ pr) : a` forces some definitional unfolding
     since `fun h1 .. hn ↦ pr` should have type `implies v (reify v ctx a) [a1, ..., an] a`,
     which involves unfolding `implies` n times as well as `ctx ↦ ctx'`.
  6. Finally, we `intro a1 ... an` so that we have a proof of `∀ a1 ... an, a`.
 -/
Mathlib.Tactic.Sat.buildReify : Lean.Expr → Lean.Expr → Lean.Expr → ℕ → Lean.Expr × Lean.Expr
-- Mathlib.Topology.EMetricSpace.Defs
edist_toMul : ∀ {X : Type u_1} [inst : EDist X] (a b : Additive X), edist (Additive.toMul a) (Additive.toMul b) = edist a b
-- Init.Data.List.Zip
List.tail_zip : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, (l₁.zip l₂).tail = l₁.tail.zip l₂.tail
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The pullback cone reconstructed using `PullbackCone.mk` from a pullback cone that is a
limit, is also a limit.  -/
CategoryTheory.Limits.PullbackCone.mkSelfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {t : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsLimit t →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk t.fst t.snd ⋯)
-- Mathlib.Topology.Category.FinTopCat
FintypeCatDiscrete.instDiscreteTopologyObjFinite : ∀ (X : FintypeCat), DiscreteTopology X.obj
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_iSizeToInt : ∀ (x : ISize) {h₁ : Int32.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int32.maxValue.toInt},
  Int32.ofIntLE x.toInt h₁ h₂ = x.toInt32
-- Mathlib.Data.Int.ModEq
/-- `a ≡ b [ZMOD n]` when `a % n = b % n`.  -/
Int.ModEq : ℤ → ℤ → ℤ → Prop
-- Mathlib.CategoryTheory.Equivalence
/-- The triangle law for the forwards direction of an equivalence: the unit and counit compose
to the identity when whiskered along the forwards direction.

We state this as a family of equalities among morphisms instead of an equality of natural
transformations to avoid abusing defeq or inserting natural transformations like `F ⟶ F𝟭`.  -/
CategoryTheory.Equivalence.functor_unitIso_comp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (self : C ≌ D) (X : C),
  CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X))
      (self.counitIso.hom.app (self.functor.obj X)) =
    CategoryTheory.CategoryStruct.id (self.functor.obj X)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.sphere_zero_right : ∀ (n k : ℕ), Behrend.sphere (n + 1) 0 k = ∅
-- Init.Data.UInt.Bitwise
UInt32.ofFin_shiftRight : ∀ (a b : Fin UInt32.size), ↑b < 32 → UInt32.ofFin (a >>> b) = UInt32.ofFin a >>> UInt32.ofFin b
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanDidOpenTextDocumentParams.mk.sizeOf_spec : ∀ (toDidOpenTextDocumentParams : Lean.Lsp.DidOpenTextDocumentParams)
  (dependencyBuildMode? : Option Lean.Lsp.DependencyBuildMode),
  sizeOf { toDidOpenTextDocumentParams := toDidOpenTextDocumentParams, dependencyBuildMode? := dependencyBuildMode? } =
    1 + sizeOf toDidOpenTextDocumentParams + sizeOf dependencyBuildMode?
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.locallyIntegrableOn : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X},
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.LocallyIntegrableOn f s μ
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path includes the data of `n` 1-simplices in `X`.  -/
SSet.Truncated.Path₁.arrow : {X : SSet.Truncated 1} →
  {n : ℕ} → X.Path₁ n → Fin n → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Path₁._proof_2 })
-- Init.Data.SInt.Lemmas
ISize.ofNat_int8ToNatClampNeg : ∀ (x : Int8), 0 ≤ x → ISize.ofNat x.toNatClampNeg = x.toISize
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_natCast : ∀ {w : ℕ} (n : ℕ), { toFin := ↑n } = ↑n
-- Std.Time.Date.Unit.Weekday
/-- Converts a `Weekday` to a `Nat`.
 -/
Std.Time.Weekday.toNat : Std.Time.Weekday → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A version of `Cocone.ext` for `Cofan`s.  -/
CategoryTheory.Limits.Cofan.ext : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        {c₁ c₂ : CategoryTheory.Limits.Cofan f} →
          (e : c₁.pt ≅ c₂.pt) →
            autoParam (∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b)
                CategoryTheory.Limits.Cofan.ext._auto_1 →
              (c₁ ≅ c₂)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod.congr_simp : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p p_1 : α} (e_p : p = p_1) (hp : 0 < p) (a a_1 : α),
  a = a_1 → ∀ (b b_1 : α), b = b_1 → toIocMod hp a b = toIocMod ⋯ a_1 b_1
-- Init.Data.Int.DivMod.Lemmas
Int.neg_mul_tmod_left : ∀ (a b : ℤ), (-(a * b)).tmod b = 0
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.uniqueAlgEquiv.eq_1 : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] [inst_4 : Subsingleton M],
  AddMonoidAlgebra.uniqueAlgEquiv R M =
    { toEquiv := (AddMonoidAlgebra.uniqueRingEquiv M).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.monic : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.IsMonicOfDegree n → p.Monic
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.whiskerRight_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  {M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : M₁ ⟶ M₂)
  (M₃ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f M₃).app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.app X) (M₃.obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_hom_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} {Z : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} Z] (U : CategoryTheory.Functor X Y) (V : CategoryTheory.Functor Y Z)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Z) (x : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).hom.app X_1).snd.app x =
    CategoryTheory.CategoryStruct.id (X_1.snd.obj (V.obj (U.obj x)))
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.realSize.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Sort u_2) (rank : ℕ) (val : α)
  (c : Batteries.BinomialHeap.Imp.HeapNode α) (s : Batteries.BinomialHeap.Imp.Heap α)
  (h_1 : Unit → motive Batteries.BinomialHeap.Imp.Heap.nil)
  (h_2 :
    (rank : ℕ) →
      (val : α) →
        (c : Batteries.BinomialHeap.Imp.HeapNode α) →
          (s : Batteries.BinomialHeap.Imp.Heap α) → motive (Batteries.BinomialHeap.Imp.Heap.cons rank val c s)),
  (match Batteries.BinomialHeap.Imp.Heap.cons rank val c s with
    | Batteries.BinomialHeap.Imp.Heap.nil => h_1 ()
    | Batteries.BinomialHeap.Imp.Heap.cons rank val c s => h_2 rank val c s) =
    h_2 rank val c s
-- Mathlib.Topology.Order.Lattice
ContinuousAt.finset_sup' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {x : X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousAt (f i) x) → ContinuousAt (s.sup' hne f) x
-- Init.Data.Order.PackageFactories
/-- Use this factory to conveniently define a linear preorder on a type `α` and all the associated
operations and instances given an `Ord α` instance.

Creates a `LinearPreorderPackage α` instance. Such an instance entails `LE α`, `LT α`, `BEq α` and
`Ord α` instances as well as an `IsLinearPreorder α` instance and `LawfulOrder*` instances proving
the compatibility of the operations with the linear preorder.

In the presence of `Ord α` and `TransOrd α` instances, no arguments are required and the factory can
be used as in this example:

```lean
public instance : LinearPreorderPackage X := .ofOrd X
```

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly
provide some arguments:

```lean
public instance : LinearPreorderPackage X := .ofOrd X {
  ord := sorry
  transOrd := sorry }
```

It is also possible to do all of this by hand, without resorting to `LinearPreorderPackage`. This
can be useful if, say, one wants to avoid specifying an `LT α` instance, which is not possible with
`LinearPreorderPackage`.

**How the arguments are filled**

Lean tries to fill all of the fields of the `args : Packages.LinearPreorderOfOrdArgs α` parameter
automatically. If it fails, it is necessary to provide some of the fields manually.

* For the data-carrying typeclasses `LE`, `LT`, `BEq` and `Ord`, existing instances are always
  preferred. If no existing instances can be synthesized, it is attempted to derive an instance from
  the `Ord` instance.
* Some proof obligations can be filled automatically if the data-carrying typeclasses have been
  derived from the `Ord` instance. For example: If the `beq` field is omitted and no `BEq α` instance
  can be synthesized, it is derived from the `Ord α` instance. In this case, `beq_iff`
  can be omitted because Lean can infer that `BEq α` and `Ord α` are compatible.
* Other proof obligations, for example `transOrd`, can be omitted if a matching instance can be
  synthesized.
 -/
Std.LinearPreorderPackage.ofOrd : (α : Type u) →
  autoParam (Std.Packages.LinearPreorderOfOrdArgs α) Std.LinearPreorderPackage.ofOrd._auto_1 →
    Std.LinearPreorderPackage α
-- Mathlib.Order.Iterate
Function.iterate_le_id_of_le_id : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α}, f ≤ id → ∀ (n : ℕ), f^[n] ≤ id
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.ext_iff : ∀ {α : Type u_2} {M : Type u_3} [inst : Monoid M] {rels : FreeMonoid α → FreeMonoid α → Prop}
  {φ ψ : PresentedMonoid rels →* M}, φ = ψ ↔ ∀ (x : α), φ (PresentedMonoid.of rels x) = ψ (PresentedMonoid.of rels x)
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.mk : {α : Type u_1} →
  [toCompleteLattice : CompleteLattice α] →
    [toHImp : HImp α] →
      (∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) → [toCompl : Compl α] → (∀ (a : α), a ⇨ ⊥ = aᶜ) → Order.Frame α
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.nextCoeff_map_of_leadingCoeff_ne_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {p : Polynomial R} (f : R →+* S),
  f p.leadingCoeff ≠ 0 → (Polynomial.map f p).nextCoeff = f p.nextCoeff
-- Lean.Parser.Term
/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`.  -/
Lean.Parser.Term.explicitUniv : Lean.Parser.TrailingParser
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_eq_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {a b : R}, EuclideanDomain.gcd a b = a ↔ a ∣ b
-- Init.Data.UInt.Lemmas
UInt32.neg_mul : ∀ (a b : UInt32), -a * b = -(a * b)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.bilin : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} →
            {A : Type u_3} →
              [inst_3 : Ring A] → [inst_4 : Algebra R A] → CliffordAlgebra.EvenHom Q A → M →ₗ[R] M →ₗ[R] A
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_mem_pointwise_smul : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G] (m : G) (a : α)
  (S : Subgroup G), m ∈ S → a • m ∈ a • S
-- Mathlib.LinearAlgebra.RootSystem.Reduced
/-- See also `RootPairing.pairingIn_one_four_iff`.  -/
RootPairing.pairing_one_four_iff : ∀ {ι : 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] (P : RootPairing ι R M N) (i j : ι) [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [Module.IsTorsionFree R N],
  P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i
-- Mathlib.CategoryTheory.Core
/-- The isomorphism of objects of `C` underlying a morphism in `Core C`.  -/
CategoryTheory.CoreHom.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : CategoryTheory.Core C} → CategoryTheory.CoreHom X Y → (X.of ≅ Y.of)
-- Init.Data.Array.BinSearch
/-- Inserts an element into a sorted array such that the resulting array is sorted. If the element is
already present in the array, it is not inserted.

The ordering predicate `lt` should be a total order on elements, and the array `as` should be sorted
with respect to `lt`.

`Array.binInsertM` is a more general operator that provides greater control over the handling of
duplicate elements in addition to running in a monad.

Examples:
* `#[0, 1, 3, 5].binInsert (· < ·) 2 = #[0, 1, 2, 3, 5]`
* `#[0, 1, 3, 5].binInsert (· < ·) 1 = #[0, 1, 3, 5]`
* `#[].binInsert (· < ·) 1 = #[1]`
 -/
Array.binInsert : {α : Type u} → (α → α → Bool) → Array α → α → Array α
-- Init.Data.Nat.Lemmas
Nat.mul_div_le_mul_div_assoc : ∀ (a b c : ℕ), a * (b / c) ≤ a * b / c
-- Mathlib.Algebra.Lie.Weights.RootSystem
/-- The root system of a finite-dimensional Lie algebra with non-degenerate Killing form over a
field of characteristic zero, relative to a splitting Cartan subalgebra.  -/
LieAlgebra.IsKilling.rootSystem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [CharZero K] →
        [inst_2 : LieRing L] →
          [inst_3 : LieAlgebra K L] →
            [LieAlgebra.IsKilling K L] →
              [inst_5 : FiniteDimensional K L] →
                (H : LieSubalgebra K L) →
                  [inst_6 : H.IsCartanSubalgebra] →
                    [LieModule.IsTriangularizable K (↥H) L] → RootPairing (↥LieSubalgebra.root) K (Module.Dual K ↥H) ↥H
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.le_topologicalClosure : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (s : Subalgebra R A), s ≤ s.topologicalClosure
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
AddGrpCat.toGrp_obj_coe : ∀ (X : AddGrpCat), ↑(AddGrpCat.toGrp.obj X) = Multiplicative ↑X
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instFaithfulSMul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, FaithfulSMul R W'.CoordinateRing
-- Std.Time.Format.Modifier
Std.Time.ExtendedDayPeriod.midnight.sizeOf_spec : sizeOf Std.Time.ExtendedDayPeriod.midnight = 1
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instRingObjForgetAlgHomCarrier : (R : Type u) → [inst : CommRing R] → {S : AlgCat R} → Ring ((CategoryTheory.forget (AlgCat R)).obj S)
-- Init.Data.Rat.Lemmas
Rat.zpow_add_one : ∀ {q : ℚ}, q ≠ 0 → ∀ (m : ℤ), q ^ (m + 1) = q ^ m * q
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_getKey_getElem?_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtTreeMap α β cmp},
  t₁ = t₂ ↔ (∀ (k : α) (hk : k ∈ t₁) (hk' : k ∈ t₂), t₁.getKey k hk = t₂.getKey k hk') ∧ ∀ (k : α), t₁[k]? = t₂[k]?
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'.go.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (acc : α),
  Lean.Grind.CommRing.Poly.denote'.go ctx p acc =
    match p with
    | Lean.Grind.CommRing.Poly.num 0 => acc
    | Lean.Grind.CommRing.Poly.num k => acc + ↑k
    | Lean.Grind.CommRing.Poly.add k m p =>
      Lean.Grind.CommRing.Poly.denote'.go ctx p (acc + Lean.Grind.CommRing.denoteTerm ctx k m)
-- Mathlib.Analysis.Analytic.Binomial
Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero : ∀ (a : ℕ) {r : ℝ},
  r ≠ 0 →
    HasFPowerSeriesOnBall (fun x => 1 / (r - x) ^ (a + 1))
      (FormalMultilinearSeries.ofScalars ℝ fun n => (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖r‖ₑ
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_add : ∀ {α : Type u} [inst : Add α] (x : WithBot α), ⊥ + x = ⊥
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isNone_min?_eq_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.min?.isNone = t.isEmpty
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_le_ceil : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a b : R}, a ≤ b → ⌈a⌉ ≤ ⌈b⌉
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_eleven : Nat.Prime 11
-- Mathlib.Data.Finset.Image
/-- A special case of `subset_image_iff`,
which corresponds to `Set.subset_range_iff_exists_image_eq` for `Set`.
 -/
Finset.subset_univ_image_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {t : Finset β} {f : α → β},
  t ⊆ Finset.image f Finset.univ ↔ ∃ s', Finset.image f s' = t
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.swap_mem_mulAntidiagonal : ∀ {A : Type u_1} [inst : CommMonoid A] [inst_1 : Finset.HasMulAntidiagonal A] {n : A} {xy : A × A},
  xy.swap ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n ↔ xy ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n
-- Mathlib.Order.Hom.Lattice
/-- The constant function as a `SupHom`.  -/
SupHom.const : (α : Type u_2) → {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → β → SupHom α β