mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS_nc.induct_unfolding : ∀ (motive : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → Prop),
  (∀ (n : ℤ), motive (Lean.Grind.CommRing.Expr.num n) (Lean.Grind.CommRing.Poly.num ↑n.natAbs)) →
    (∀ (x : Lean.Grind.CommRing.Var), motive (Lean.Grind.CommRing.Expr.var x) (Lean.Grind.CommRing.Poly.ofVar x)) →
      (∀ (a b : Lean.Grind.CommRing.Expr),
          motive a a.toPolyS_nc → motive b b.toPolyS_nc → motive (a.add b) (a.toPolyS_nc.combine b.toPolyS_nc)) →
        (∀ (a b : Lean.Grind.CommRing.Expr),
            motive a a.toPolyS_nc → motive b b.toPolyS_nc → motive (a.mul b) (a.toPolyS_nc.mul_nc b.toPolyS_nc)) →
          (∀ (k : ℕ) (n : ℤ),
              motive ((Lean.Grind.CommRing.Expr.num n).pow k) (Lean.Grind.CommRing.Poly.num (↑n.natAbs ^ k))) →
            (∀ (k : ℕ) (x : Lean.Grind.CommRing.Var),
                motive ((Lean.Grind.CommRing.Expr.var x).pow k)
                  (Lean.Grind.CommRing.Poly.ofMon
                    (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit))) →
              (∀ (a : Lean.Grind.CommRing.Expr) (k : ℕ),
                  (∀ (n : ℤ), a = Lean.Grind.CommRing.Expr.num n → False) →
                    (∀ (x : Lean.Grind.CommRing.Var), a = Lean.Grind.CommRing.Expr.var x → False) →
                      motive a a.toPolyS_nc → motive (a.pow k) (a.toPolyS_nc.pow_nc k)) →
                (∀ (n : ℕ), motive (Lean.Grind.CommRing.Expr.natCast n) (Lean.Grind.CommRing.Poly.num ↑n)) →
                  (∀ (a b : Lean.Grind.CommRing.Expr), motive (a.sub b) (Lean.Grind.CommRing.Poly.num 0)) →
                    (∀ (a : Lean.Grind.CommRing.Expr), motive a.neg (Lean.Grind.CommRing.Poly.num 0)) →
                      (∀ (k : ℤ), motive (Lean.Grind.CommRing.Expr.intCast k) (Lean.Grind.CommRing.Poly.num 0)) →
                        ∀ (a : Lean.Grind.CommRing.Expr), motive a a.toPolyS_nc
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The completed L-function of a Dirichlet character is differentiable, with the following
exceptions: at `s = 1` if `χ` is the trivial character (to any modulus); and at `s = 0` if the
modulus is 1. This result is best possible.

Note both `χ` and `s` are explicit arguments: we will always be able to infer one or other
of them from the hypotheses, but it's not clear which!
 -/
DirichletCharacter.differentiableAt_completedLFunction : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ),
  s ≠ 0 ∨ N ≠ 1 → s ≠ 1 ∨ χ ≠ 1 → DifferentiableAt ℂ (DirichletCharacter.completedLFunction χ) s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.unitOfList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {hd : α} {tl : List α},
  Std.ExtHashMap.unitOfList (hd :: tl) = (∅.insertIfNew hd ()).insertManyIfNewUnit tl
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.DecompositionResult.comp.injEq : ∀ (f g f_1 g_1 : Lean.Expr),
  (Mathlib.Meta.FunProp.DecompositionResult.comp f g = Mathlib.Meta.FunProp.DecompositionResult.comp f_1 g_1) =
    (f = f_1 ∧ g = g_1)
-- Mathlib.RingTheory.Polynomial.Basic
/-- The equivalence between monic polynomials of degree `n` and polynomials of degree less than
`n`, formed by adding a term `X ^ n`.  -/
Polynomial.monicEquivDegreeLT : {R : Type u} →
  [inst : Semiring R] → [Nontrivial R] → (n : ℕ) → { p // p.Monic ∧ p.natDegree = n } ≃ ↥(Polynomial.degreeLT R n)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformEmbedding.of_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β} {g : β → γ}, UniformContinuous f → UniformContinuous g → IsUniformEmbedding (g ∘ f) → IsUniformEmbedding f
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.IsInternal.toBaseChange_injective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (ℳ : ι → Submodule R M) [inst_3 : DecidableEq ι] [inst_4 : CommSemiring S]
  [inst_5 : Algebra R S], DirectSum.IsInternal ℳ → ∀ (i : ι), Function.Injective ⇑(Submodule.toBaseChange S (ℳ i))
-- Mathlib.Control.Monad.Writer
Writer : Type u_1 → Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Equivalence
/-- The `functor` functor that sends an equivalence of categories to its functor.  -/
CategoryTheory.Equivalence.functorFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C ≌ D) (CategoryTheory.Functor C D)
-- Mathlib.Algebra.Group.Defs
add_ne_add_right : ∀ {G : Type u_1} [inst : Add G] [IsLeftCancelAdd G] (a : G) {b c : G}, a + b ≠ a + c ↔ b ≠ c
-- Mathlib.Analysis.Convex.Side
AffineSubspace.isPreconnected_setOfPred_wSameSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P),
  IsPreconnected {y | s.WSameSide x y}
-- Mathlib.Algebra.DirectSum.Ring
/-- Families of `AddMonoidHom`s preserving `DirectSum.One.one` and `DirectSum.Mul.mul`
are isomorphic to `RingHom`s on `⨁ i, A i`. This is a stronger version of `DFinsupp.liftAddHom`.
 -/
DirectSum.liftRingHom : {ι : Type u_1} →
  [inst : DecidableEq ι] →
    {A : ι → Type u_2} →
      {R : Type u_3} →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : DirectSum.GSemiring A] →
              [inst_4 : Semiring R] →
                { f //
                    f GradedMonoid.GOne.one = 1 ∧
                      ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj } ≃
                  ((DirectSum ι fun i => A i) →+* R)
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.exists_iff : ∀ {α : Type w} {P : Std.Iterators.Types.ArrayIterator α → Prop},
  (∃ s, P s) ↔ ∃ array pos, P { array := array, pos := pos }
-- Mathlib.Logic.Small.Defs
/-- Constructor for `Small α` from an explicit witness type and equivalence.
 -/
Small.mk' : ∀ {α : Type v} {S : Type w} (e : α ≃ S), Small.{w, v} α
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
exists_lt_add_iff_lt_left : ∀ {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {b c : α} [inst_1 : Add α] [CanonicallyOrderedAdd α]
  [AddLeftReflectLT α] [IsLeftCancelAdd α], (∃ a < b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_preimage : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β)
  (μ : MeasureTheory.Measure β),
  Function.Injective f →
    Measurable f →
      (∀ (t : Set α), MeasurableSet t → MeasureTheory.NullMeasurableSet (f '' t) μ) →
        ∀ {s : Set β}, MeasurableSet s → (MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = μ (s ∩ Set.range f)
-- Std.Data.ByteSlice
/-- The starting index is no later than the ending index.

The ending index is exclusive. If the starting and ending indices are equal, then the byte slice is
empty.
 -/
ByteSlice.start_le_stop : ∀ (xs : ByteSlice), xs.start ≤ xs.stop
-- Mathlib.Algebra.Star.Basic
RingHom.involutiveStar : {R : Type u} →
  [inst : CommSemiring R] → [StarRing R] → {S : Type u_1} → [inst_2 : NonAssocSemiring S] → InvolutiveStar (S →+* R)
-- Mathlib.RingTheory.Idempotents
isIdempotentElem_one_sub_one_sub_pow_pow : ∀ {R : Type u_1} [inst : Ring R] (x : R) (n : ℕ), (x - x ^ 2) ^ n = 0 → IsIdempotentElem (1 - (1 - x ^ n) ^ n)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_inter_distrib_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
-- Mathlib.CategoryTheory.Triangulated.Yoneda
CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (B : C),
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).op.map
      (CategoryTheory.preadditiveYoneda.obj B)).Exact
-- Batteries.Data.Array.Match
Array.PrefixTable.mk.injEq : ∀ {α : Type u_1} (toArray : Array (α × ℕ)) (valid : ∀ {i : ℕ} (h : i < toArray.size), toArray[i].2 ≤ i)
  (toArray_1 : Array (α × ℕ)) (valid_1 : ∀ {i : ℕ} (h : i < toArray_1.size), toArray_1[i].2 ≤ i),
  ({ toArray := toArray, valid := valid } = { toArray := toArray_1, valid := valid_1 }) = (toArray = toArray_1)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ≅ y) (z : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.hom z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.inv z) h) =
    h
-- Init.Data.SInt.Lemmas
Int64.toInt16_ofBitVec : ∀ (b : BitVec 64), (Int64.ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  [inst_5 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)))
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) Y Z)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) Y Z))
      (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addEntries.inj : ∀ {entries entries_1 : Array Lean.Meta.SimpEntry},
  Lean.Elab.Tactic.ElabSimpArgResult.addEntries entries = Lean.Elab.Tactic.ElabSimpArgResult.addEntries entries_1 →
    entries = entries_1
-- Mathlib.Data.List.Cycle
Cycle.map_coe : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α), Cycle.map f ↑l = ↑(List.map f l)
-- Init.Data.Option.Basic
/-- The minimum of two optional values, with `none` treated as the least element. This function is
usually accessed through the `Min (Option α)` instance, rather than directly.

Prior to `nightly-2025-02-27`, `none` was treated as the greatest element, so
`min none (some x) = min (some x) none = some x`.

Examples:
 * `Option.min (some 2) (some 5) = some 2`
 * `Option.min (some 5) (some 2) = some 2`
 * `Option.min (some 2) none = none`
 * `Option.min none (some 5) = none`
 * `Option.min none none = none`
 -/
Option.min : {α : Type u_1} → [Min α] → Option α → Option α → Option α
-- Mathlib.ModelTheory.Substructures
/-- The image of a substructure along a homomorphism is a substructure.  -/
FirstOrder.Language.Substructure.map : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Hom M N → L.Substructure M → L.Substructure N
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.Context.mk.sizeOf_spec : ∀ (red : Lean.Meta.TransparencyMode) (evalAtom : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result),
  sizeOf { red := red, evalAtom := evalAtom } = 1 + sizeOf red
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mapAlgHom.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f f_1 : S →ₐ[R] T) (e_f : f = f_1) (p : Polynomial S)
  (q : Polynomial T) (h : q ∣ Polynomial.map (↑f) p), AdjoinRoot.mapAlgHom f p q h = AdjoinRoot.mapAlgHom f_1 p q ⋯
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces,
which is smooth, symmetric, and with support equal to the unit ball.  -/
ExistsContDiffBumpBase.u : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → [FiniteDimensional ℝ E] → E → ℝ
-- Lean.Util.Recognizers
Lean.Expr.app1? : Lean.Expr → Lean.Name → Option Lean.Expr
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If we single out one member of an affine-independent family of points and affinely transport
all others along the line joining them to this member, the resulting new family of points is affine-
independent.

This is the affine version of `LinearIndependent.units_smul`.  -/
AffineIndependent.units_lineMap : ∀ {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] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p → ∀ (j : ι) (w : ι → kˣ), AffineIndependent k fun i => (AffineMap.lineMap (p j) (p i)) ↑(w i)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_of_ne_zero : ∀ {o : Ordinal.{u}}, o ≠ 0 → Ordinal.veblen o = Ordinal.derivFamily fun x => Ordinal.veblen ↑x
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symmEquiv_apply_symm_apply : ∀ (P : Type u_9) (Q : Type u_10) [inst : Mul P] [inst_1 : Mul Q] (h : P ≃* Q) (a : P),
  ((MulEquiv.symmEquiv P Q) h).symm a = h a
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.instIsTopologicalGroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (N : Subgroup G)
  [inst_3 : N.Normal], IsTopologicalGroup (G ⧸ N)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Two affine subspaces are parallel if one is related to the other by adding the same vector
to all points.  -/
AffineSubspace.Parallel : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → AffineSubspace k P → AffineSubspace k P → Prop
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap'_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData)
  (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) {Z : C} (h : h₃.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₂ h₃) h)
-- Mathlib.Order.Grade
grade_covBy_grade_iff : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : LinearOrder α] [inst_2 : GradeOrder 𝕆 α] {a b : α},
  grade 𝕆 a ⋖ grade 𝕆 b ↔ a ⋖ b
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- The reverse of the characteristic polynomial of a matrix.

It has some advantages over the characteristic polynomial, including the fact that it can be
extended to infinite dimensions (for appropriate operators). In such settings it is known as the
"characteristic power series".  -/
Matrix.charpolyRev : {R : Type u} → [inst : CommRing R] → {n : Type v} → [DecidableEq n] → [Fintype n] → Matrix n n R → Polynomial R
-- Mathlib.CategoryTheory.Localization.HasLocalization
CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : W.HasLocalization], W.Q'.IsLocalization W
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.map_vadd : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (p : P) (v : V),
  f (v +ᵥ p) = f.linearIsometry v +ᵥ f p
-- Init.Data.Array.Lemmas
Array.prod_singleton : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.LawfulRightIdentity (fun x1 x2 => x1 * x2) 1] {x : α},
  #[x].prod = x
-- Batteries.Classes.Order
/-- `cmp x y ≠ .gt` holds iff `x ≤ y` is true.  -/
Std.LawfulBCmp.isLE_iff_le : ∀ {α : Type u_1} {inst : LE α} {inst_1 : LT α} {inst_2 : BEq α} {cmp : α → α → Ordering} [self : Std.LawfulBCmp cmp]
  {x y : α}, (cmp x y).isLE = true ↔ x ≤ y
-- Init.Data.Vector.Zip
Vector.zip_map : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {n : ℕ} {f : α → γ} {g : β → δ} {as : Vector α n}
  {bs : Vector β n}, (Vector.map f as).zip (Vector.map g bs) = Vector.map (Prod.map f g) (as.zip bs)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.rangeChange.sizeOf_spec : ∀ (range : Lean.Lsp.Range) (text : String),
  sizeOf (Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range text) = 1 + sizeOf range + sizeOf text
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toArray_eq_match : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α],
  r.toArray =
    match Std.PRange.succ? r.lower with
    | none => #[]
    | some next => if next ≤ r.upper then #[next] ++ (next<...=r.upper).toArray else #[]
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instNormalSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [NormalSpace M], NormalSpace Mᵈᵃᵃ
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (X : CategoryTheory.Sheaf J A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongr.unitIso J K e A).hom.app X).hom.app X_1 =
    X.obj.map (e.unitIso.inv.app (Opposite.unop X_1)).op
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDivMulChar'.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r₁ r₂ : R) (s₁ s₂ : ↥S),
  OreLocalization.oreDivMulChar' r₁ r₂ s₁ s₂ = ⟨OreLocalization.oreNum r₁ s₂, ⟨OreLocalization.oreDenom r₁ s₂, ⋯⟩⟩
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.isCyclic_units_four : IsCyclic (ZMod 4)ˣ
-- Mathlib.Data.Fintype.EquivFin
Quotient.finite : ∀ {α : Sort u_4} [Finite α] (s : Setoid α), Finite (Quotient s)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Mathlib.LinearAlgebra.Trace
LinearMap.toMatrixAlgEquiv'.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LinearMap.toMatrixAlgEquiv' = AlgEquiv.ofLinearEquiv LinearMap.toMatrix' ⋯ ⋯
-- Std.Do.WP.Basic
Std.Do.PredTrans.apply.eq_1 : ∀ {ps : Std.Do.PostShape} {α : Type u} (t : Std.Do.PredTrans ps α) (Q : Std.Do.PostCond α ps), t.apply Q = t.trans Q
-- Mathlib.Topology.Defs.Induced
WithTopology.equiv_apply : ∀ (X : Type u_1) (t : TopologicalSpace X) (self : WithTopology X t), (WithTopology.equiv X t) self = self.ofTopology
-- Mathlib.CategoryTheory.Action.Limits
/-- `Action.forget V G : Action V G ⥤ V` preserves the limit of some `K : J ⥤ Action V G` if
`K ⋙ Action.forget V G` has a limit.  -/
Action.instPreservesLimitForgetOfHasLimitComp : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J] (K : CategoryTheory.Functor J (Action V G))
  [CategoryTheory.Limits.HasLimit (K.comp (Action.forget V G))],
  CategoryTheory.Limits.PreservesLimit K (Action.forget V G)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk_mul_mk : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M) (x y : M) (hx : x ∈ S) (hy : y ∈ S),
  ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Multiset α} {a : α},
  a ∈ s → s.gcd ∣ a
-- Mathlib.LinearAlgebra.DFinsupp
LinearEquiv.map_dfinsuppSumAddHom : ∀ {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁]
  [inst_7 : RingHomInvPair τ₂₁ τ₁₂] {γ : ι → Type u_12} [inst_8 : DecidableEq ι] [inst_9 : (i : ι) → AddZeroClass (γ i)]
  (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i →+ M),
  f ((DFinsupp.sumAddHom g) t) = (DFinsupp.sumAddHom fun i => f.toAddEquiv.toAddMonoidHom.comp (g i)) t
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformly.multipliable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {x : β} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], MultipliableLocallyUniformly f → Multipliable fun x_1 => f x_1 x
-- Mathlib.Algebra.BigOperators.Group.Finset.Interval
Finset.sum_Icc_eq_sum_Ico_add : ∀ {α : Type u_1} [inst : AddCommMonoid α] (f : ℤ → α) {l u : ℤ},
  l ≤ u → ∑ m ∈ Finset.Icc l u, f m = ∑ m ∈ Finset.Ico l u, f m + f u
-- Std.Time.Format.Basic
Std.Time.FormatType.eq_def : ∀ (result : Type) (x : Std.Time.FormatString),
  Std.Time.FormatType result x =
    match x with
    | Std.Time.FormatPart.modifier entry :: xs => Std.Time.TypeFormat entry → Std.Time.FormatType result xs
    | Std.Time.FormatPart.string val :: xs => Std.Time.FormatType result xs
    | [] => result
-- Mathlib.Combinatorics.SimpleGraph.Operations
/-- **Alias** of `SimpleGraph.edgeSet_edge_of_ne`. -/
SimpleGraph.edge_edgeSet_of_ne : ∀ {V : Type u_1} {s t : V}, s ≠ t → (SimpleGraph.edge s t).edgeSet = {s(s, t)}
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.IsKInjective.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {L : CochainComplex C ℤ},
  (∀ {K : CochainComplex C ℤ} (f : K ⟶ L), HomologicalComplex.Acyclic K → Nonempty (Homotopy f 0)) → L.IsKInjective