mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPairHomMk_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (p : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ⟶ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
  (q : F.obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) q =
        CategoryTheory.CategoryStruct.comp p (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
      CategoryTheory.Limits.parallelPairHomMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) q =
        CategoryTheory.CategoryStruct.comp p (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
      CategoryTheory.Limits.parallelPairHomMk._auto_3)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.parallelPairHomMk p q hl hr).app X = CategoryTheory.Limits.WalkingParallelPair.casesOn X p q
-- Init.Data.List.MinMaxOn
List.le_apply_minOn_take : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} {i : ℕ} (h : List.take i xs ≠ []), f (List.minOn f xs ⋯) ≤ f (List.minOn f (List.take i xs) h)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.not_mem_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α}, k ∉ ∅
-- Init.Prelude
/-- A monad that supports syntax quotations. Syntax quotations (in term
position) are monadic values that when executed retrieve the current "macro
scope" from the monad and apply it to every identifier they introduce
(independent of whether this identifier turns out to be a reference to an
existing declaration, or an actually fresh binding during further
elaboration). We also apply the position of the result of `getRef` to each
introduced symbol, which results in better error positions than not applying
any position.  -/
Lean.MonadQuotation : (Type → Type) → Type 1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.left_unitor : {B : Type u} →
  [inst : Quiver B] →
    {a b : CategoryTheory.FreeBicategory B} →
      (f : a ⟶ b) →
        CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) f
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.ext_iff : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f g : ContDiffMapSupportedIn E F n K},
  f = g ↔ ∀ (a : E), f a = g a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.Data.List.Cycle
Cycle.chain_of_pairwise : ∀ {α : Type u_1} {r : α → α → Prop} {s : Cycle α}, (∀ a ∈ s, ∀ b ∈ s, r a b) → Cycle.Chain r s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- For a nonempty set, the affine span is `⊤` iff its vector span is `⊤`.  -/
AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s : Set P}, s.Nonempty → (affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤)
-- Batteries.Util.ExtendedBinder
/-- An extended binder has the form `x`, `x : ty`, or `x pred`
where `pred` is a `binderPred` like `< 2`.
 -/
Batteries.ExtendedBinder.extBinder : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasis.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x x_1 : NumberField.mixedEmbedding.realSpace K),
  x = x_1 →
    NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasis K x =
      NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasis K x_1
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.homologyπ_restrictionHomologyIso_inv_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) (hi : c.prev j = i)
  (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j] {Z : C}
  (h : (K.restriction e).homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyπ j')
      (CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv h) =
    CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv
      (CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyπ j) h)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffWithinAt.div` -/
ContDiffWithinAt.fun_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {f g : E → 𝕜} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → g x ≠ 0 → ContDiffWithinAt 𝕜 n (fun i => f i / g i) s x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.deriv_sin : deriv Real.sin = Real.cos
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.instReprValue : Repr Fin.Value✝
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
/-- The function `⟨x, y⟩ ↦ ⟪x, y⟫` bundled as a sesquilinear map.  -/
CStarModule.innerₛₗ : {A : Type u_1} →
  {E : Type u_2} →
    [inst : NonUnitalRing A] →
      [inst_1 : StarRing A] →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module ℂ A] →
            [inst_4 : Module ℂ E] →
              [inst_5 : PartialOrder A] →
                [inst_6 : SMul A E] →
                  [inst_7 : Norm A] → [inst_8 : Norm E] → [CStarModule A E] → [StarModule ℂ A] → E →ₗ⋆[ℂ] E →ₗ[ℂ] A
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- Independent Gaussian random variables are jointly Gaussian.  -/
ProbabilityTheory.IndepFun.hasGaussianLaw : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [CompleteSpace E] [BorelSpace E]
  [SecondCountableTopology E] [inst_5 : NormedAddCommGroup F] [inst_6 : MeasurableSpace F] [CompleteSpace F]
  [BorelSpace F] [SecondCountableTopology F] [inst_10 : NormedSpace ℝ E] [inst_11 : NormedSpace ℝ F] {X : Ω → E}
  {Y : Ω → F},
  ProbabilityTheory.HasGaussianLaw X P →
    ProbabilityTheory.HasGaussianLaw Y P →
      ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongrEquiv_symm_apply : ∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2}
  (σ : ι₁ ≃ ι₂) (m : MultilinearMap R (fun x => M₂) M₃),
  (MultilinearMap.domDomCongrEquiv σ).symm m = MultilinearMap.domDomCongr σ.symm m
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.preimage_toSnowflaking_ball : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.toSnowflaking ⁻¹' Metric.ball x r = Metric.ball (Metric.Snowflaking.ofSnowflaking x) (r ^ α⁻¹)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.le_addIndex_mul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) {V : Set G},
  (interior V).Nonempty →
    MeasureTheory.Measure.haar.addIndex (↑K) V ≤
      MeasureTheory.Measure.haar.addIndex ↑K ↑K₀ * MeasureTheory.Measure.haar.addIndex (↑K₀) V
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tan_int_mul_pi_div_two : ∀ (n : ℤ), Real.tan (↑n * Real.pi / 2) = 0
-- Mathlib.Topology.UniformSpace.Compact
/-- Let `U : ι → Set α` be an open cover of a compact set `K`.
Then there exists an entourage `V`
such that for each `x ∈ K` its `V`-neighborhood is included in some `U i`.

Moreover, one can choose an entourage from a given basis.  -/
Filter.HasBasis.lebesgue_number_lemma : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {ι' : Sort u_2} {ι : Sort u_3} {p : ι' → Prop}
  {V : ι' → Set (α × α)} {U : ι → Set α},
  (uniformity α).HasBasis p V →
    IsCompact K → (∀ (j : ι), IsOpen (U j)) → K ⊆ ⋃ j, U j → ∃ i, p i ∧ ∀ x ∈ K, ∃ j, UniformSpace.ball x (V i) ⊆ U j
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.isAddUnit_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddMonoid α] {A : Matrix m n α},
  IsAddUnit A ↔ ∀ (i : m) (j : n), IsAddUnit (A i j)
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.IsImmersion (CategoryTheory.Limits.pullback.snd f g)
-- Lean.Meta.Eqns
Lean.Meta.GetEqnsFn : Type
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below.nil : ∀
  {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Trimmed → Prop}
  {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} {f : ℝ → ℝ},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below ⋯
-- Mathlib.Order.SymmDiff
symmDiff_le_iff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, symmDiff a b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurableSet_partitionFiltration_memPartitionSet : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) (a : α),
  MeasurableSet (memPartitionSet t n a)
-- Mathlib.Order.InitialSeg
/-- Composition of an initial segment embedding and a principal segment embedding as a principal
segment embedding  -/
InitialSeg.transPrincipal : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {r : α → α → Prop} →
        {s : β → β → Prop} →
          {t : γ → γ → Prop} → [IsWellOrder β s] → [IsTrans γ t] → InitialSeg r s → PrincipalSeg s t → PrincipalSeg r t
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- Translation in the domain does not change the derivative.  -/
derivWithin_comp_const_add : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (a : 𝕜) (s : Set 𝕜) (x : 𝕜),
  derivWithin (fun x => f (a + x)) s x = derivWithin f (a +ᵥ s) (a + x)
-- Mathlib.Algebra.Group.Semiconj.Basic
SemiconjBy.eq_one_iff : ∀ {G : Type u_1} [inst : Group G] (a : G) {x y : G}, SemiconjBy a x y → (x = 1 ↔ y = 1)
-- Mathlib.Analysis.Distribution.TemperateGrowth
MeasureTheory.Measure.HasTemperateGrowth.exists_integrable : ∀ {E : Type u_5} {inst : NormedAddCommGroup E} {inst_1 : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [self : μ.HasTemperateGrowth], ∃ n, MeasureTheory.Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) μ
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.ext_iff : ∀ {x y : SemiSimplexCategory}, x = y ↔ x.len = y.len
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.instInhabited : Inhabited SemiRingCat
-- Mathlib.Combinatorics.Hindman
Ultrafilter.addSemigroup.eq_1 : ∀ {M : Type u_1} [inst : AddSemigroup M], Ultrafilter.addSemigroup = { toAdd := Ultrafilter.add, add_assoc := ⋯ }
-- Lean.Data.KVMap
Lean.instInhabitedDataValue : Inhabited Lean.DataValue
-- Mathlib.Algebra.Module.Submodule.Defs
/-- Copy of a submodule with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
Submodule.copy : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (p : Submodule R M) → (s : Set M) → s = ↑p → Submodule R M
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.map_zpow' : ∀ {M : Type u_4} {N : Type u_5} [inst : DivInvMonoid M] [inst_1 : DivInvMonoid N] (f : M →* N),
  (∀ (x : M), f x⁻¹ = (f x)⁻¹) → ∀ (a : M) (n : ℤ), f (a ^ n) = f a ^ n
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNIndepSet.mk : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, G.IsIndepSet ↑s → s.card = n → G.IsNIndepSet n s
-- Mathlib.SetTheory.Ordinal.Notation
/-- Construct a `NONote` from an ordinal notation (and infer normality)  -/
NONote.mk : (o : ONote) → [h : o.NF] → NONote
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.restrict_self : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.restrict I = π
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.forget_map : ∀ (R : Type u) [inst : CommRing R] {A B : AlgCat R} (f : A ⟶ B),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (AlgCat R)).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget MonCat)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_apply : ∀ {R : Type u} {σ : Type u_1} {a : R} [inst : CommSemiring R], MvPolynomial.C a = (MvPolynomial.monomial 0) a
-- Init.Data.List.Nat.TakeDrop
List.rotateRight_replicate : ∀ {α : Type u_1} {m n : ℕ} {a : α}, (List.replicate m a).rotateRight n = List.replicate m a
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.toMulHom : {M : Type u_10} → {N : Type u_11} → [inst : MulOne M] → [inst_1 : MulOne N] → (M →* N) → M →ₙ* N
-- Mathlib.Order.Sublocale
Sublocale.ext : ∀ {X : Type u_1} [inst : Order.Frame X] {S T : Sublocale X}, (∀ (x : X), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.toNonneg_coe : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : SemilatticeSup α] {a : { x // 0 ≤ x }}, Nonneg.toNonneg ↑a = a
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.mergeSort.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (a b : α) (xs : List α) (le : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match a :: b :: xs, le with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_3 a b xs le
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The square `transformObjPrecomposeObjSquare` respects identities.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_id : ∀ {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] {X : Type u₇}
  {Y : Type u₈} [inst_3 : CategoryTheory.Category.{v₇, u₇} X] [inst_4 : CategoryTheory.Category.{v₈, u₈} Y]
  (U : CategoryTheory.Functor X Y) (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CatCommSq.iso
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj
            (CategoryTheory.Limits.CatCospanTransform.id F G))
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj
            (CategoryTheory.Limits.CatCospanTransform.id F G))).hom
      (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId Y F G).hom
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).leftUnitor.hom
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).rightUnitor.inv)
-- Mathlib.Algebra.Group.Defs
/-- Any `CommMagma G` that satisfies `IsLeftCancelMul G` also satisfies `IsCancelMul G`.  -/
CommMagma.IsLeftCancelMul.toIsCancelMul : ∀ (G : Type u) [inst : CommMagma G] [IsLeftCancelMul G], IsCancelMul G
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.reverse.match_1.splitter : (motive : (x : ℕ) → BitVec x → Sort u_1) →
  (x : ℕ) →
    (x_1 : BitVec x) → ((x : BitVec 0) → motive 0 x) → ((w : ℕ) → (x : BitVec (w + 1)) → motive w.succ x) → motive x x_1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instPreadditive : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → CategoryTheory.Preadditive (PresheafOfModules R)
-- Mathlib.Data.Real.Basic
Real.instAddGroup : AddGroup ℝ
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorSet_def : ∀ (G : Type u_1) [inst : AddGroup G], addCommutatorSet G = {g | ∃ g₁ g₂, ⁅g₁, g₂⁆ = g}
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg_le_neg : ∀ {G : Type u_2} [inst : AddGroup G] (S T : AddSubmonoid G), -S ≤ -T ↔ S ≤ T
-- Mathlib.Algebra.Homology.Augment
CochainComplex.augment_X_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0),
  (C.augment f w).X 0 = X
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.ι_mapBifunctorDesc_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] {A : D} {j : J}
  (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A)) (i₁ : I₁) (i₂ : I₂)
  (h : c₁.π c₂ c (i₁, i₂) = j) {Z : D} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorDesc f) h_1) =
    CategoryTheory.CategoryStruct.comp (f i₁ i₂ h) h_1
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.intercalate.go : String → String.Slice → List String.Slice → String
-- Mathlib.Data.Stream.Init
Stream'.get_append_length : ∀ {α : Type u} (x : List α) (a : Stream' α), (x ++ₛ a).get x.length = a.get 0
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instLawfulHasSizeNat_1 : Std.Rxo.LawfulHasSize ℕ
-- Mathlib.Order.SupIndep
Finset.supIndep_singleton : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] (i : ι) (f : ι → α), {i}.SupIndep f
-- Mathlib.LinearAlgebra.BilinearMap
/-- Restrict the scalars and range of a linear map.  -/
LinearMap.restrictScalarsRange : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {P : Type u_4} →
        {M' : Type u_5} →
          {P' : Type u_6} →
            [inst : Semiring R] →
              [inst_1 : Semiring S] →
                [inst_2 : SMul S R] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : Module R M] →
                      [inst_5 : AddCommMonoid P] →
                        [inst_6 : Module R P] →
                          [inst_7 : Module S M] →
                            [inst_8 : Module S P] →
                              [IsScalarTower S R M] →
                                [IsScalarTower S R P] →
                                  [inst_11 : AddCommMonoid M'] →
                                    [inst_12 : Module S M'] →
                                      [inst_13 : AddCommMonoid P'] →
                                        [inst_14 : Module S P'] →
                                          (i : M' →ₗ[S] M) →
                                            (k : P' →ₗ[S] P) →
                                              Function.Injective ⇑k →
                                                (f : M →ₗ[R] P) → (∀ (m : M'), f (i m) ∈ k.range) → M' →ₗ[S] P'
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.denseRange_intCast : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)], DenseRange Int.cast
-- Init.Conv
Lean.Parser.Tactic.Conv.enterPattern : Lean.ParserDescr
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Every set has a measurable superset. Declare this as local instance as needed.  -/
nonempty_measurable_superset : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : Set α), Nonempty { t // s ⊆ t ∧ MeasurableSet t }
-- Mathlib.Computability.TuringMachine.Config
/-- The semantics of a continuation.  -/
Turing.ToPartrec.Cont.eval : Turing.ToPartrec.Cont → List ℕ →. List ℕ
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.mem_smul_pointwise_iff_exists : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddGroup A] [inst_2 : DistribMulAction M A] (m : A) (a : M)
  (S : AddSubgroup A), m ∈ a • S ↔ ∃ s ∈ S, a • s = m
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- After conversion to normal form at `x`, the function has normal form.  -/
meromorphicNFAt_toMeromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, MeromorphicNFAt (toMeromorphicNFAt f x) x
-- Mathlib.Order.WithBot
WithBot.coe_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] (a b : α), ↑(a ⊔ b) = ↑a ⊔ ↑b
-- Init.Data.Array.MinMax
Array.min?_eq_none_iff : ∀ {α : Type u_1} {xs : Array α} [inst : Min α], xs.min? = none ↔ xs = #[]
-- Mathlib.Order.OrderDual
OrderDual.toDual_le : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ} {b : α}, OrderDual.toDual b ≤ a ↔ OrderDual.ofDual a ≤ b
-- Init.Data.SInt.Lemmas
ISize.toInt_ofIntClamp : ∀ {x : ℤ}, ISize.minValue.toInt ≤ x → x ≤ ISize.maxValue.toInt → (ISize.ofIntClamp x).toInt = x
-- Mathlib.Tactic.GRewrite.Elab
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.elabGRewriteConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Tactic.GRewrite.Config
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_lt_top_iff : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α}, s.einfsep < ⊤ ↔ s.Nontrivial
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
StrongDual.toLinearEquiv_extendRCLikeₗᵢ : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F],
  StrongDual.extendRCLikeₗᵢ.toLinearEquiv = StrongDual.extendRCLikeₗ
-- Lean.Elab.Do.Basic
/-- Throw an error if the given name is not a declared `mut` variable.  -/
Lean.Elab.Do.throwUnlessMutVarDeclared : Lean.Ident → Lean.Elab.Do.DoElabM Unit