mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.le_cancel_var : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] (ctx : Lean.Grind.CommRing.Context α) (c : ℤ)
  (x : Lean.Grind.CommRing.Var) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.cancel_var_cert c x p₁ p₂ = true →
    ↑c * Lean.Grind.CommRing.Var.denote ctx x = 1 →
      Lean.Grind.CommRing.Poly.denote ctx p₁ ≤ 0 → Lean.Grind.CommRing.Poly.denote ctx p₂ ≤ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter m₂ ⋯).getKey? k = none
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.RightFraction₂ X Y) [W.HasLeftCalculusOfFractions],
  ∃ ψ,
    CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f ∧
      CategoryTheory.CategoryStruct.comp φ.f' ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f'
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₂_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF], W.b₂ = 4 * W.a₂
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.ExprInfo.mk.inj : ∀ {expr : Lean.Expr} {bvars : List Lean.FVarId} {lctx : Lean.LocalContext} {localInsts : Lean.LocalInstances}
  {cfg : Lean.Meta.Config} {expr_1 : Lean.Expr} {bvars_1 : List Lean.FVarId} {lctx_1 : Lean.LocalContext}
  {localInsts_1 : Lean.LocalInstances} {cfg_1 : Lean.Meta.Config},
  { expr := expr, bvars := bvars, lctx := lctx, localInsts := localInsts, cfg := cfg } =
      { expr := expr_1, bvars := bvars_1, lctx := lctx_1, localInsts := localInsts_1, cfg := cfg_1 } →
    expr = expr_1 ∧ bvars = bvars_1 ∧ lctx = lctx_1 ∧ localInsts = localInsts_1 ∧ cfg = cfg_1
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- For every functor `G` on the Grothendieck construction `Grothendieck F`, if `G` has a colimit
and every fiber of `G` has a colimit, then taking this colimit is isomorphic to first taking the
fiberwise colimit and then the colimit of the resulting functor.  -/
CategoryTheory.Limits.colimitFiberwiseColimitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) →
            [inst_2 :
                ∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.Limits.HasColimit
                    ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] →
              [inst_3 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] →
                CategoryTheory.Limits.colimit (CategoryTheory.Limits.fiberwiseColimit G) ≅
                  CategoryTheory.Limits.colimit G
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map₂_bot_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithOne β), WithOne.map₂ f 1 b = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {i : ℕ},
  i < r.toList.length → (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least).isSome = true
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_idem : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] (A : Matrix m n α) (j : n) (x y : m → α),
  (A.updateCol j x).updateCol j y = A.updateCol j y
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k a : α} {fallback v : β},
      Std.DHashMap.Internal.Raw₀.Const.getD (m.insert k v) a fallback =
        if (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback
-- Mathlib.Data.Fin.Tuple.Basic
/-- `Fin.snoc` is the same as appending a one-tuple  -/
Fin.snoc_eq_append : ∀ {n : ℕ} {α : Sort u_2} (xs : Fin n → α) (x : α), Fin.snoc xs x = Fin.append xs (Fin.cons x Fin.elim0)
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.ofFn.match_1.eq_2 : ∀ {α : Type u_2} (motive : (x : ℕ) → (Fin x → α) → Sort u_1) (n : ℕ) (f : Fin (n + 1) → α)
  (h_1 : (x : Fin 0 → α) → motive 0 x) (h_2 : (n : ℕ) → (f : Fin (n + 1) → α) → motive n.succ f),
  (match n.succ, f with
    | 0, x => h_1 x
    | n.succ, f => h_2 n f) =
    h_2 n f
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.totalSpaceMk_isInducing' : ∀ {B : Type u_2} {F : Type u_3} {inst : TopologicalSpace B} {inst_1 : TopologicalSpace F} {E : B → Type u_5}
  {inst_2 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_3 : (b : B) → TopologicalSpace (E b)}
  [self : FiberBundle F E] (b : B), Topology.IsInducing (Bundle.TotalSpace.mk b)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_isBase_iff : ∀ {α : Type u_1} {X : Set α} {M : Matroid α} {B : Set ↑X},
  (M.restrictSubtype X).IsBase B ↔ M.IsBasis' (Subtype.val '' B) X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.map_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z S T : C} (f₁ : S ⟶ W) (f₂ : S ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPushout f₁ f₂] (g₁ : T ⟶ Y) (g₂ : T ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
  (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁)
  (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂) [CategoryTheory.IsIso i₁]
  [CategoryTheory.IsIso i₂] [CategoryTheory.IsIso i₃],
  CategoryTheory.IsIso (CategoryTheory.Limits.pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
-- Mathlib.Order.RelIso.Basic
/-- `Sum.inr` as a relation embedding into `Sum.Lex r s`.  -/
RelEmbedding.sumLexInr : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → s ↪r Sum.Lex r s
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedComp_π : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃)
      (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃) j) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j)
        (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₂ F₃) j))
      (CategoryTheory.eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j))
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.le_centralizer_iff_isAddCommutative : ∀ {G : Type u_1} [inst : AddGroup G] {K : AddSubgroup G}, K ≤ AddSubgroup.centralizer ↑K ↔ IsAddCommutative ↥K
-- Init.Data.UInt.Lemmas
UInt64.sub_eq_add_mul : ∀ (a b : UInt64), a - b = a + 18446744073709551615 * b
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- The natural coercion from a continuous algebra isomorphism to a continuous
algebra morphism.  -/
ContinuousAlgEquiv.toContinuousAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (A ≃A[R] B) → A →A[R] B
-- Mathlib.Data.Option.Basic
Option.getD_default_eq_iget : ∀ {α : Type u_1} [inst : Inhabited α] (o : Option α), o.getD default = o.iget
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.cycleOf_eq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (c : ↥g.cycleFactorsFinset), g.cycleOf (a c) = ↑c
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- The subgroup `SL(2, ℤ) ∩ g⁻¹ Γ g`, for `Γ` a subgroup of `SL(2, ℤ)` and `g ∈ GL(2, ℝ)`.  -/
CongruenceSubgroup.conjGL : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ) → GL (Fin 2) ℝ → Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The residue of `Λ(s)` at `s = 1` is equal to `1`.  -/
completedRiemannZeta_residue_one : Filter.Tendsto (fun s => (s - 1) * completedRiemannZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1)
-- Mathlib.Logic.Equiv.Prod
Equiv.sumProdDistrib_symm_apply_left : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × γ),
  (Equiv.sumProdDistrib α β γ).symm (Sum.inl a) = (Sum.inl a.1, a.2)
-- Mathlib.Algebra.GCDMonoid.Basic
instCommutativeGcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α], Std.Commutative gcd
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_neg : ∀ {R : Type u_1} [inst : Ring R] (p : SkewPolynomial R) (n : ℕ), (-p).coeff n = -p.coeff n
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.toContinuousMap_apply_eq_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  (α : ODE.FunSpace t₀ x₀ r L) (t : ↑(Set.Icc tmin tmax)), (ODE.FunSpace.toContinuousMap α) t = α.toFun t
-- Lean.Language.Basic
Lean.Language.ProcessingContext.mk.inj : ∀ {toInputContext toInputContext_1 : Lean.Parser.InputContext},
  { toInputContext := toInputContext } = { toInputContext := toInputContext_1 } → toInputContext = toInputContext_1
-- Aesop.Tree.Data
Aesop.Rapp.instHashable : Hashable Aesop.Rapp
-- Mathlib.Algebra.Group.Defs
CancelCommMonoid.toCommMonoid : {M : Type u} → [self : CancelCommMonoid M] → CommMonoid M
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_rangeRestrict : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), f.rangeRestrict.ker = f.ker
-- Init.Data.Array.Lemmas
Array.map_filterMap_of_inv : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {g : β → α},
  (∀ (x : α), Option.map g (f x) = some x) → ∀ {xs : Array α}, Array.map g (Array.filterMap f xs) = xs
-- Mathlib.Algebra.Group.PUnit
PUnit.mul_eq : ∀ (x y : PUnit.{u_1 + 1}), x * y = PUnit.unit
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.vadd_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ[σ] F)
  (g : E →ₛₗ.[σ] F) (x : ↥(f +ᵥ g).domain), ↑(f +ᵥ g) x = f ↑x + ↑g x
-- Init.Core
instDecidableForall : {p q : Prop} → [Decidable p] → [Decidable q] → Decidable (p → q)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The singleton operation as an `AddMonoidHom`.  -/
Set.singletonAddMonoidHom : {α : Type u_2} → [inst : AddZeroClass α] → α →+ Set α
-- Init.Data.String.Pattern.Char
String.Slice.Pattern.Char.instToBackwardSearcherCharDefaultBackwardSearcherForallBoolBeq : {c : Char} →
  String.Slice.Pattern.ToBackwardSearcher c
    (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher fun x => x == c)
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_drop : ∀ {α : Type u_1} {n : ℕ} {xs : Subarray α}, Std.Slice.toList (xs.drop n) = List.drop n (Std.Slice.toList xs)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
PosMulMono.toPosMulStrictMono : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsLeftCancelMulZero α] [PosMulMono α],
  PosMulStrictMono α
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGE.induct_unfolding : ∀ (s : String.Slice) (motive : (offset : String.Pos.Raw) → offset ≤ s.rawEndPos → s.Pos → Prop),
  (∀ (offset : String.Pos.Raw) (h : offset ≤ s.rawEndPos) (h_1 : String.Pos.Raw.IsValidForSlice s offset),
      motive offset h (s.pos offset h_1)) →
    (∀ (offset : String.Pos.Raw) (h : offset ≤ s.rawEndPos),
        ¬String.Pos.Raw.IsValidForSlice s offset →
          ∀ (this : offset < s.rawEndPos),
            motive offset.inc ⋯ (s.posGE offset.inc ⋯) → motive offset h (s.posGE offset.inc ⋯)) →
      ∀ (offset : String.Pos.Raw) (h : offset ≤ s.rawEndPos), motive offset h (s.posGE offset h)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx_eq_entryAtIdx_fst : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced) {i : ℕ} {h : i < t.size},
  t.keyAtIdx htb i h = (t.entryAtIdx htb i h).fst
-- Mathlib.Data.Finsupp.Option
Finsupp.update.eq_1 : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b : M),
  f.update a b =
    { support := if b = 0 then f.support.erase a else insert a f.support, toFun := Function.update (⇑f) a b,
      mem_support_toFun := ⋯ }
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
VectorPrebundle.contMDiffOn_contMDiffCoordChange : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle 𝕜 F E) [ha : VectorPrebundle.IsContMDiff IB a n]
  {e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj} (he : e ∈ a.pretrivializationAtlas)
  (he' : e' ∈ a.pretrivializationAtlas),
  ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (VectorPrebundle.contMDiffCoordChange n IB a he he')
    (e.baseSet ∩ e'.baseSet)
-- Mathlib.Logic.Equiv.Multiset
Denumerable.raise.eq_def : ∀ (x : List ℕ) (x_1 : ℕ),
  Denumerable.raise x x_1 =
    match x, x_1 with
    | [], x => []
    | m :: l, n => (m + n) :: Denumerable.raise l (m + n)
-- Mathlib.Order.Disjoint
codisjoint_assoc : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint (a ⊔ b) c ↔ Codisjoint a (b ⊔ c)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_AllZero : ∀ {li : Tactic.ComputeAsymptotics.UnitMonomial}, li.FirstNonzeroIsPos → ¬li.AllZero
-- Lean.Syntax
Lean.Syntax.instInhabitedRange : Inhabited Lean.Syntax.Range
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instMulAction : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → MulAction R (M →ₚₗ[R] N)
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueue : Type
-- Mathlib.Algebra.Order.Hom.Ring
/-- Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.  -/
OrderRingIso.toOrderRingHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] → [inst_2 : NonAssocSemiring β] → [inst_3 : Preorder β] → α ≃+*o β → α →+*o β
-- Mathlib.Algebra.GCDMonoid.Nat
lcm_eq_nat_lcm : ∀ (m n : ℕ), lcm m n = m.lcm n
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.map_ne_zero_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → (Polynomial.map f p ≠ 0 ↔ p ≠ 0)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Decomp.0.SimpleGraph.Walk.length.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {u : V} →
      (motive : (v : V) → G.Walk u v → Sort u_2) →
        (v : V) →
          (x : G.Walk u v) →
            (Unit → motive u SimpleGraph.Walk.nil) →
              ((v v_1 : V) → (h : G.Adj u v_1) → (q : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h q)) → motive v x
-- Init.Data.ByteArray.Basic
/-- Moves the iterator's position to the end of the array.

Given `i : ByteArray.Iterator`, note that `i.toEnd.atEnd` is always `true`.
 -/
ByteArray.Iterator.toEnd : ByteArray.Iterator → ByteArray.Iterator
-- Mathlib.Algebra.Quaternion
Quaternion.sq_eq_normSq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R},
  a ^ 2 = ↑(Quaternion.normSq a) ↔ a = ↑a.re
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁), CategoryTheory.Epi ((F.shift n₀).map T.mor₂) ↔ F.homologySequenceδ T n₀ n₁ h = 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.comap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (S : CategoryTheory.Subgroupoid D),
  CategoryTheory.Subgroupoid.comap φ S =
    { arrows := fun c d => {f | φ.map f ∈ S.arrows (φ.obj c) (φ.obj d)}, inv := ⋯, mul := ⋯ }
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring module bracket satisfies a Leibniz / Jacobi identity.  -/
LieRingModule.leibniz_lie : ∀ {L : Type v} {M : Type w} {inst : LieRing L} {inst_1 : AddCommGroup M} [self : LieRingModule L M] (x y : L) (m : M),
  ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The chosen equalizer of a parallel pair is a regular monomorphism.  -/
CategoryTheory.RegularMono.equalizer : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (g h : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)] →
          CategoryTheory.RegularMono (CategoryTheory.Limits.equalizer.ι g h)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
CategoryTheory.Limits.instIsIsoInitialComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasInitial C]
  [inst_3 : CategoryTheory.Limits.HasInitial D]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.initialComparison G)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier : ∀ (R : Type u) [inst : CommRing R] (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ),
  ↑((AlgebraicGeometry.structurePresheafInCommRingCat R).obj U) = (AlgebraicGeometry.structureSheafInType R R).obj.obj U
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
/-- `F : C ⥤ D ⥤ E` preserves finite limits if it does for each `d : D`.  -/
CategoryTheory.preservesFiniteLimits_of_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)),
  (∀ (d : D), CategoryTheory.Limits.PreservesFiniteLimits (F.comp ((CategoryTheory.evaluation D E).obj d))) →
    CategoryTheory.Limits.PreservesFiniteLimits F
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_sub_cancel_right : ∀ {x : ℤ} {n : ℕ} {y : ℤ} (i : ℤ), (x - i).bmod n = (y - i).bmod n ↔ x.bmod n = y.bmod n
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Given a subobject `x`, the `ImageFactorisation` of `x.arrow ≫ f` through `(exists f).obj x`.  -/
CategoryTheory.Subobject.imageFactorisation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasImages C] →
        (f : X ⟶ Y) →
          (x : CategoryTheory.Subobject X) →
            CategoryTheory.Limits.ImageFactorisation (CategoryTheory.CategoryStruct.comp x.arrow f)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.isPretransitive_of_isMultiplyPretransitive : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  MulAction.IsMultiplyPretransitive G α n → MulAction.IsPretransitive G ↑(Set.powersetCard α n)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
Antitone.locallyIntegrable : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ], Antitone f → MeasureTheory.LocallyIntegrable f μ
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.mahlerTerm_apply : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] (a : E) (n : ℕ) (x : ℤ_[p]), (PadicInt.mahlerTerm a n) x = (mahler n) x • a
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.IsSeparated.encard_le_packingNumber : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A C : Set X} {ε : NNReal},
  C ⊆ A → Metric.IsSeparated (↑ε) C → C.encard ≤ Metric.packingNumber ε A
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- `cons (exp, coef) tl` is `Sorted` when `coef` and `tl` are `Sorted` and the leading
exponent of `tl` is less than `exp`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} {f : ℝ → ℝ},
  coef.Sorted →
    tl.leadingExp < ↑exp →
      tl.Sorted →
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
            (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f).Sorted
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_eq_zero : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : EMetricSpace Y] {r : NNReal} {f : X → Y},
  eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
-- Init.Data.UInt.Lemmas
BitVec.ofFin_uInt32ToFin : ∀ (n : UInt32), { toFin := n.toFin } = n.toBitVec