mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.String.Basic
/-- Internal implementation of `toAsciiByteArray`.
`loop p out = out ++ toAsciiByteArray ({ s with startPos := p } : Substring)`
 -/
String.toAsciiByteArray.loop : String → String.Pos.Raw → ByteArray → ByteArray
-- Batteries.CodeAction.Misc
/-- The "Add subgoals" code action puts `· done` subgoals for any goals remaining at the end of a
proof.
```
example : True ∧ True := by
  constructor
  -- <- here
```
is transformed to
```
example : True ∧ True := by
  constructor
  · done
  · done
```
 -/
Batteries.CodeAction.addSubgoalsAction : Batteries.CodeAction.TacticCodeAction
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flip_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.flip.X₂ = sq.X₃
-- Lean.Elab.Calc
/-- A relation term like `a ≤ b`  -/
Lean.Elab.Term.CalcStepView.term : Lean.Elab.Term.CalcStepView → Lean.Term
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.xa.injEq : ∀ {n : ℕ} (a a_1 : ZMod (2 * n)), (QuaternionGroup.xa a = QuaternionGroup.xa a_1) = (a = a_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ordCompare_maxKey_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap α (fun x => β) compare} {k : α}
  {f : β → β} {he : (Std.DTreeMap.Const.modify t k f).isEmpty = false},
  compare ((Std.DTreeMap.Const.modify t k f).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Analysis.Complex.Basic
Complex.hasSum_ofReal : ∀ {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} {x : ℝ}, HasSum (fun x => ↑(f x)) (↑x) L ↔ HasSum f x L
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.mem_zeroLocus_iff : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) (x : ↥X),
  x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_g₁ : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d),
  ((SSet.relativeCellComplexOfMono i).attachCells d x).g₁ = SSet.relativeCellComplexOfMono.t i d
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.comp_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E},
  AnalyticWithinAt 𝕜 f s x → ∀ (y : E), AnalyticWithinAt 𝕜 (fun z => f (z - y)) (s + {y}) (x + y)
-- Mathlib.RingTheory.MvPolynomial.EulerIdentity
MvPolynomial.IsWeightedHomogeneous.pderiv : ∀ {R : Type u_1} {σ : Type u_2} {M : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R}
  [inst_1 : AddCancelCommMonoid M] {w : σ → M} {n n' : M} {i : σ},
  MvPolynomial.IsWeightedHomogeneous w φ n →
    n' + w i = n → MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.pderiv i) φ) n'
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An alternative definition of the norm on the quotient group: the norm of `((x : M) : M ⧸ S)` is
equal to the distance from `x` to `S`.  -/
QuotientAddGroup.norm_mk : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M), ‖↑x‖ = Metric.infDist x ↑S
-- Mathlib.Algebra.Group.Shrink
Shrink.instIsLeftCancelAdd : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Add α] [IsLeftCancelAdd α], IsLeftCancelAdd (Shrink.{v, u_2} α)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.eq_zero_iff_coeFn_eq_zero : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : ↥(lp E p)},
  f = 0 ↔ ↑f = 0
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), Set.uIoc a b = Set.Ioc (min a b) (max a b)
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.EStateM.instMonadAttach.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 :
    (a_1 : α) → (s'_1 : σ) → EStateM.Result.ok a s' = EStateM.Result.ok a_1 s'_1 → motive (EStateM.Result.ok a_1 s'_1))
  (h_2 :
    (e : ε) → (s'_1 : σ) → EStateM.Result.ok a s' = EStateM.Result.error e s'_1 → motive (EStateM.Result.error e s'_1)),
  (match h : EStateM.Result.ok a s' with
    | EStateM.Result.ok a_1 s'_1 => h_1 a_1 s'_1 h
    | EStateM.Result.error e s'_1 => h_2 e s'_1 h) =
    h_1 a s' ⋯
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.mem_sieves_iff_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X}
  (J : CategoryTheory.GrothendieckTopology C), S ∈ J.sieves X ↔ S ∈ J X
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.instIsHomologicalHomologyFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ), (DerivedCategory.homologyFunctor C n).IsHomological
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.map_isometryOfOrthonormal : ∀ {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {F' : Type u_6}
  [inst_2 : NormedAddCommGroup F'] [inst_3 : InnerProductSpace ℝ F'] (v : OrthonormalBasis (Fin 2) ℝ F)
  (f : F ≃ₗᵢ[ℝ] F'), Complex.isometryOfOrthonormal (v.map f) = (Complex.isometryOfOrthonormal v).trans f
-- Mathlib.Algebra.Polynomial.Div
Polynomial.degree_divByMonic_lt : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), p ≠ 0 → 0 < q.degree → (p /ₘ q).degree < p.degree
-- Mathlib.Data.Tree.Get
/-- **Alias** of `BinaryTree.getOrElse`.  -/
Tree.getOrElse : {α : Type u_1} → PosNum → Tree α → α → α
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = false ↔ ∃ a, m.contains a = true
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_neg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → E}, μ.withDensityᵥ (-f) = -μ.withDensityᵥ f
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.DescendsAlong.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C},
  (∀ {A X Y Z : C} {fst : A ⟶ X} {snd : A ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z},
      CategoryTheory.IsPullback fst snd f g → Q f → P fst → P g) →
    P.DescendsAlong Q
-- Mathlib.Data.Set.Lattice
Set.union_iInter₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : Set α) (t : (i : ι) → κ i → Set α),
  s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_sub : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : AddLeftMono α] (s t : NonemptyInterval α), (s - t).toProd.2 = s.toProd.2 - t.toProd.1
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.instIsComm𝔾ₘ : ∀ {R : Type u_1} [inst : CommRing R], FormalGroup.𝔾ₘ.IsComm
-- Mathlib.Order.SetNotation
Set.iSup_eq_iUnion : ∀ {α : Type u} {ι : Sort v} (s : ι → Set α), iSup s = Set.iUnion s
-- Mathlib.Data.Matrix.Composition
Matrix.comp_single_single : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} [inst : DecidableEq I]
  [inst_1 : DecidableEq J] [inst_2 : DecidableEq K] [inst_3 : DecidableEq L] [inst_4 : Zero R] (i : I) (j : J) (k : K)
  (l : L) (r : R), (Matrix.comp I J K L R) (Matrix.single i j (Matrix.single k l r)) = Matrix.single (i, k) (j, l) r
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- The counit for the equivalence `CommMon (C ⥤ D) ≌ C ⥤ CommMon D`.
 -/
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [inst_3 : CategoryTheory.BraidedCategory D] →
            CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.comp
                CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor ≅
              CategoryTheory.Functor.id (CategoryTheory.Functor C (CategoryTheory.CommMon D))
-- Mathlib.Algebra.Opposites
PreOpposite.op'.sizeOf_spec : ∀ {α : Type u_3} [inst : SizeOf α] (unop' : α), sizeOf { unop' := unop' } = 1 + sizeOf unop'
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Continuations as in `ToPartrec.Cont` but with the data removed. This is done because we want
the set of all continuations in the program to be finite (so that it can ultimately be encoded into
the finite state machine of a Turing machine), but a continuation can handle a potentially infinite
number of data values during execution.  -/
Turing.PartrecToTM2.Cont' : Type
-- Mathlib.GroupTheory.GroupAction.OfQuotient
MulDistribMulAction.instQuotientSubgroupSubtypeMemSubgroup : {G : Type u_1} →
  [inst : Group G] →
    {H : Subgroup G} →
      [inst_1 : H.Normal] →
        {α : Type u_3} →
          [inst_2 : Group α] →
            [inst_3 : MulDistribMulAction G α] → MulDistribMulAction (G ⧸ H) ↥(FixedPoints.subgroup (↥H) α)
-- Mathlib.Order.Atoms
OrderIso.isSimpleOrder : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β), IsSimpleOrder α
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesIsoSc'_inv_iCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (K.iCycles j) = (K.sc' i j k).iCycles
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_isoIsPushout_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : CategoryTheory.IsPushout f g inl inr)
  (h' : CategoryTheory.IsPushout f g inl' inr') {Z_1 : C} (h_1 : P' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom h_1) =
    CategoryTheory.CategoryStruct.comp inl' h_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insertIfNew_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF),
  t.isEmpty = false →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare ((Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKeyD fallback) (t.minKeyD fallback)).isLE =
        true
-- Init.Data.List.Nat.Modify
List.length_modify : ∀ {α : Type u_1} (f : α → α) (l : List α) (i : ℕ), (l.modify i f).length = l.length
-- Batteries.Lean.EStateM
EStateM.run_tryFinally' : ∀ {ε σ α β : Type u_1} (x : EStateM ε σ α) (h : Option α → EStateM ε σ β) (s : σ),
  (tryFinally' x h).run s =
    match x.run s with
    | EStateM.Result.ok a s =>
      match (h (some a)).run s with
      | EStateM.Result.ok b s => EStateM.Result.ok (a, b) s
      | EStateM.Result.error e s => EStateM.Result.error e s
    | EStateM.Result.error e₁ s =>
      match (h none).run s with
      | EStateM.Result.ok a s => EStateM.Result.error e₁ s
      | EStateM.Result.error e₂ s => EStateM.Result.error e₂ s
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.le_ofSliceFrom_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos},
  q ≤ String.Slice.Pos.ofSliceFrom p ↔ ∀ (h : p₀ ≤ q), p₀.sliceFrom q h ≤ p
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticStructFieldCompletion : Lean.FileMap → String.Pos.Raw → Lean.Syntax → Bool
-- Mathlib.Order.Max
IsBot.not_isMax : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α} [Nontrivial α], IsBot a → ¬IsMax a
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFieldInfo.inj : ∀ {i i_1 : Lean.Elab.FieldInfo}, Lean.Elab.Info.ofFieldInfo i = Lean.Elab.Info.ofFieldInfo i_1 → i = i_1
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_abs_eq_two_mul_integral_negPart_add_integral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → ∫ (x : α), |f x| ∂μ = 2 * ∫ (x : α), (f x)⁻ ∂μ + ∫ (x : α), f x ∂μ
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.toLinearMap_convOne : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R C] [inst_4 : Algebra R A], WithConv.toConv (WithConv.ofConv 1).toLinearMap = 1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.diff m₂).getKey? k = none
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_add_ratCast : ∀ (q : ℚ) {x : ℝ}, Irrational (x + ↑q) → Irrational x
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddLeftCancelSemigroupOfAddOpposite : {M : Type u_1} → [AddLeftCancelSemigroup Mᵃᵒᵖ] → AddLeftCancelSemigroup Mᵈᵃᵃ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.equiv_iff_toArray_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.toArray = t₂.toArray)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.comp.eq_1 : ∀ {E : Type u_3} {F : Type u_4} [inst : AddGroup E] [inst_1 : AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E),
  p.comp f = { toFun := fun x => p (f x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }
-- Mathlib.Topology.Constructible
IsRetrocompact_iff_isSpectralMap_subtypeVal : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, IsRetrocompact s ↔ IsSpectralMap Subtype.val
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangent.infDist_eq_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P},
  s.IsTangent as → Metric.infDist s.center ↑as = s.radius
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.exists_valuation_div_valuation_eq : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] (γ : ValuativeRel.ValueGroupWithZero R),
  ∃ a b, (ValuativeRel.valuation R) a / (ValuativeRel.valuation R) ↑b = γ
-- Init.Data.SInt.Bitwise
Int64.xor_comm : ∀ (a b : Int64), a ^^^ b = b ^^^ a
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.bicone_ι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (b : J), (CategoryTheory.Limits.biproduct.bicone f).ι b = CategoryTheory.Limits.biproduct.ι f b
-- Plausible.DeriveArbitrary
/-- Creates a `Header` for the `Arbitrary` typeclass  -/
_private.Plausible.DeriveArbitrary.0.Plausible.mkArbitraryHeader : Lean.InductiveVal → Lean.Elab.TermElabM Lean.Elab.Deriving.Header
-- Mathlib.Data.Multiset.Bind
Multiset.count_sum : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α},
  Multiset.count a (Multiset.map f m).sum = (Multiset.map (fun b => Multiset.count a (f b)) m).sum
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves addition  -/
AddHom.map_add' : ∀ {M : Type u_10} {N : Type u_11} [inst : Add M] [inst_1 : Add N] (self : M →ₙ+ N) (x y : M),
  self.toFun (x + y) = self.toFun x + self.toFun y
-- Init.Data.Array.Find
Array.findSomeRev?_push_of_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} {xs : Array α},
  (f a).isSome = true → Array.findSomeRev? f (xs.push a) = f a
-- Mathlib.RingTheory.Regular.RegularSequence
/-- An alternate induction principle from `IsWeaklyRegular.recIterModByRegular`
where we mod out by successive elements in both the module and the base ring.
This is useful for propagating certain properties of the initial `M`, e.g.
faithfulness or freeness, throughout the induction.  -/
RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing : {motive :
    (R : Type u) →
      [inst : CommRing R] →
        (M : Type v) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → (rs : List R) → RingTheory.Sequence.IsWeaklyRegular M rs → Sort u_7} →
  ((R : Type u) →
      [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → motive R M [] ⋯) →
    ({R : Type u} →
        [inst : CommRing R] →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    (h1 : IsSMulRegular M r) →
                      (h2 :
                          RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M)
                            (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) →
                        motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
                            (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) h2 →
                          motive R M (r :: rs) ⋯) →
      {R : Type u} →
        [inst : CommRing R] →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → (h : RingTheory.Sequence.IsWeaklyRegular M rs) → motive R M rs h
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_sum_measure_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [inst : TopologicalSpace β] {f : α → β}
  [TopologicalSpace.PseudoMetrizableSpace β] {_m : MeasurableSpace α} {μ : ι → MeasureTheory.Measure α},
  MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.sum μ) ↔
    ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ i)
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- The composition of two cover-preserving functors is cover-preserving.  -/
CategoryTheory.CoverPreserving.comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) {L : CategoryTheory.GrothendieckTopology A}
  {F : CategoryTheory.Functor C D},
  CategoryTheory.CoverPreserving J K F →
    ∀ {G : CategoryTheory.Functor D A},
      CategoryTheory.CoverPreserving K L G → CategoryTheory.CoverPreserving J L (F.comp G)
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for the full range `*...*`.
This is an internal function.
Use `Rio.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Rii.Internal.iter : {α : Type u} → [Std.PRange.UpwardEnumerable α] → [Std.PRange.Least? α] → Std.Rii α → Std.Iter α
-- Mathlib.Order.WellFoundedSet
/-- A version of **Dickson's lemma** on finite product of well-quasi-ordered sets.
See `Pi.wellQuasiOrderedLE` when the type `α i` is `WellQuasiOrderedLE`.  -/
Set.IsPWO.pi : ∀ {ι : Type u_1} {α : ι → Type u_6} [Finite ι] [inst : (i : ι) → Preorder (α i)] {s : (i : ι) → Set (α i)},
  (∀ (i : ι), (s i).IsPWO) → (Set.univ.pi s).IsPWO
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.leadingCoeff f ∈ nonZeroDivisors R → f ∈ nonZeroDivisors (MvPolynomial σ R)
-- Std.Http.Server.Connection
/-- The client connection.
 -/
Std.Http.Server.Connection.socket : {α : Type} → Std.Http.Server.Connection α → α
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.contradiction : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Algebra.Algebra.Equiv
/-- Algebra equivalences are reflexive.  -/
AlgEquiv.refl : {R : Type uR} →
  {A₁ : Type uA₁} → [inst : CommSemiring R] → [inst_1 : Semiring A₁] → [inst_2 : Algebra R A₁] → A₁ ≃ₐ[R] A₁
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesRxiSize.size_eq : ∀ {α : Type u_1} {β : Type u_2} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.PRange.UpwardEnumerable β}
  {inst_2 : Std.Rxi.HasSize α} {inst_3 : Std.Rxi.HasSize β} {f : Std.PRange.UpwardEnumerable.Map α β}
  [self : f.PreservesRxiSize] {b : α}, Std.Rxi.HasSize.size b = Std.Rxi.HasSize.size (f.toFun b)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_ofNat_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocDiv hp a (OfNat.ofNat m * p + b) = OfNat.ofNat m + toIocDiv hp a b
-- Plausible.Random
Plausible.BoundedRandom.mk : {m : Type u → Type u_1} →
  {α : Type u} →
    [inst : LE α] →
      ({g : Type} → (lo hi : α) → lo ≤ hi → [RandomGen g] → Plausible.RandGT g m { a // lo ≤ a ∧ a ≤ hi }) →
        Plausible.BoundedRandom m α
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.lambda.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t t_1 : CategoryTheory.Limits.IsLimit c),
  t = t_1 →
    ∀ [inst_2 : CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor],
      CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t = CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t_1
-- Init.Data.SInt.Lemmas
Int16.toInt_inj : ∀ {x y : Int16}, x.toInt = y.toInt ↔ x = y
-- Mathlib.Analysis.Normed.Module.FiniteDimension
isOpen_setOfPred_linearIndependent : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι], IsOpen {f | LinearIndependent 𝕜 f}
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatch_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat (pos.cast hst) ↔ String.Slice.Pattern.Model.IsLongestMatch pat pos
-- Mathlib.Data.ULift
PLift.up_surjective : ∀ {α : Sort u}, Function.Surjective PLift.up
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharThreeNF_spec_of_b₂_ne_zero : ∀ {F : Type u_2} [inst : Field F] [inst_1 : CharP F 3] (W : WeierstrassCurve F),
  W.b₂ ≠ 0 → (W.toCharThreeNF • W).IsCharThreeJNeZeroNF
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f],
  AlgebraicGeometry.Scheme.Hom.opensRange f = ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₆.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.b₆ = W.a₃ ^ 2 + 4 * W.a₆
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsStableUnderComposition.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (CategoryTheory.CategoryStruct.comp f g)) →
    P.IsStableUnderComposition
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.ofHom_apply : ∀ {R S : Type u} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (r : R),
  (CategoryTheory.ConcreteCategory.hom (RingCat.ofHom f)) r = f r