mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.DFinsupp
/-- If a family of submodules is independent, then a choice of nonzero vector from each submodule
forms a linearly independent family.

See also `iSupIndep.linearIndependent'`.  -/
iSupIndep.linearIndependent : ∀ {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] [IsDomain R]
  [Module.IsTorsionFree R N] {ι : Type u_7} (p : ι → Submodule R N),
  iSupIndep p → ∀ {v : ι → N}, (∀ (i : ι), v i ∈ p i) → (∀ (i : ι), v i ≠ 0) → LinearIndependent R v
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioo_toDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  Finset.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioo b a)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (le ge : ℤ → CategoryTheory.ObjectProperty C)
  (le_isClosedUnderIsomorphisms :
    autoParam (∀ (n : ℤ), (le n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam)
  (ge_isClosedUnderIsomorphisms :
    autoParam (∀ (n : ℤ), (ge n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam)
  (le_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le n X → le n' ((CategoryTheory.shiftFunctor C a).obj X))
  (ge_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), ge n X → ge n' ((CategoryTheory.shiftFunctor C a).obj X))
  (zero' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), le 0 X → ge 1 Y → f = 0) (le_zero_le : le 0 ≤ le 1) (ge_one_le : ge 1 ≤ ge 0)
  (exists_triangle_zero_one :
    ∀ (A : C),
      ∃ X Y,
        ∃ (_ : le 0 X) (_ : ge 1 Y),
          ∃ f g h,
            CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (le_1 ge_1 : ℤ → CategoryTheory.ObjectProperty C)
  (le_isClosedUnderIsomorphisms_1 :
    autoParam (∀ (n : ℤ), (le_1 n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam)
  (ge_isClosedUnderIsomorphisms_1 :
    autoParam (∀ (n : ℤ), (ge_1 n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam)
  (le_shift_1 : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le_1 n X → le_1 n' ((CategoryTheory.shiftFunctor C a).obj X))
  (ge_shift_1 : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), ge_1 n X → ge_1 n' ((CategoryTheory.shiftFunctor C a).obj X))
  (zero'_1 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), le_1 0 X → ge_1 1 Y → f = 0) (le_zero_le_1 : le_1 0 ≤ le_1 1)
  (ge_one_le_1 : ge_1 1 ≤ ge_1 0)
  (exists_triangle_zero_one_1 :
    ∀ (A : C),
      ∃ X Y,
        ∃ (_ : le_1 0 X) (_ : ge_1 1 Y),
          ∃ f g h,
            CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  ({ le := le, ge := ge, le_isClosedUnderIsomorphisms := le_isClosedUnderIsomorphisms,
        ge_isClosedUnderIsomorphisms := ge_isClosedUnderIsomorphisms, le_shift := le_shift, ge_shift := ge_shift,
        zero' := zero', le_zero_le := le_zero_le, ge_one_le := ge_one_le,
        exists_triangle_zero_one := exists_triangle_zero_one } =
      { le := le_1, ge := ge_1, le_isClosedUnderIsomorphisms := le_isClosedUnderIsomorphisms_1,
        ge_isClosedUnderIsomorphisms := ge_isClosedUnderIsomorphisms_1, le_shift := le_shift_1, ge_shift := ge_shift_1,
        zero' := zero'_1, le_zero_le := le_zero_le_1, ge_one_le := ge_one_le_1,
        exists_triangle_zero_one := exists_triangle_zero_one_1 }) =
    (le = le_1 ∧ ge = ge_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_left_inj_of_comparable : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddRightStrictMono α] {a b c : α},
  b ≤ c ∨ c ≤ b → (c + a = b + a ↔ c = b)
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ioc_pred_right_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  a < b → insert b (Set.Ioc a (Order.pred b)) = Set.Ioc a b
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.dist_le_opNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  (x y : E), dist (f x) (f y) ≤ ‖f‖ * dist x y
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.bijective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Function.Bijective f
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonFileChangeType : Lean.ToJson Lean.Lsp.FileChangeType
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.degreeOf_prod_eq : ∀ {R : Type u_1} {σ : Type u_2} {n : σ} [inst : CommSemiring R] [NoZeroDivisors R] {ι : Type u_3} (s : Finset ι)
  (f : ι → MvPolynomial σ R),
  (∀ i ∈ s, f i ≠ 0) → MvPolynomial.degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, MvPolynomial.degreeOf n (f i)
-- Mathlib.Order.SupClosed
/-- Every set in a join-semilattice generates a set closed under join.  -/
supClosure : {α : Type u_3} → [SemilatticeSup α] → ClosureOperator (Set α)
-- Mathlib.Data.Finset.Card
Finset.strongInductionOn_eq : ∀ {α : Type u_1} {p : Finset α → Sort u_4} (s : Finset α) (H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s),
  s.strongInductionOn H = H s fun t x => t.strongInductionOn H
-- Mathlib.Algebra.Field.Basic
div_neg_self : ∀ {K : Type u_1} [inst : DivisionRing K] {a : K}, a ≠ 0 → a / -a = -1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- The type of elements of a presheaf of modules. A term of this type is a pair
`⟨X, a⟩` with `X : Cᵒᵖ` and `a : M.obj X`.  -/
PresheafOfModules.Elements : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → PresheafOfModules R → Type (max u₁ v)
-- Init.Control.Basic
/-- Produces an empty collection or recoverable failure.  The `<|>` operator collects values or recovers
from failures. See `Alternative` for more details.
 -/
Alternative.failure : {f : Type u → Type v} → [self : Alternative f] → {α : Type u} → f α
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_ne_zero : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis → ∀ᶠ (x : ℝ) in Filter.atTop, m.toFun basis x ≠ 0
-- Mathlib.Algebra.Order.Monoid.TypeTags
Additive.canonicallyOrderedAdd : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Preorder α] [CanonicallyOrderedMul α], CanonicallyOrderedAdd (Additive α)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- We can set up a coercion from arrows with codomain `X` to `over X`. This most likely should not
be a global instance, but it is sometimes useful.  -/
CategoryTheory.Over.coeFromHom : {T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → {X Y : T} → CoeOut (Y ⟶ X) (CategoryTheory.Over X)
-- Batteries.Data.Array.Scan
Array.toList_scanr : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α},
  (Array.scanr f init as).toList = List.scanr f init as.toList
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finiteDimensional_sup : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L) [FiniteDimensional K ↥E1] [FiniteDimensional K ↥E2], FiniteDimensional K ↥(E1 ⊔ E2)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.insertMany_eq_insertListₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  (l : List (α × β)),
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l) = Std.DHashMap.Internal.Raw₀.Const.insertListₘ m l
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.coe_injective : ∀ {α : Type u}, Function.Injective WithOne.coe
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.orbit_eq_out_smul : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} (x : α ⧸ s),
  MulAction.orbitRel.Quotient.orbit x = Quotient.out x • ↑s
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- The basic open sets form an affine open cover of `Spec R`.  -/
AlgebraicGeometry.Scheme.affineBasisCoverOfAffine : (R : CommRingCat) → (AlgebraicGeometry.Spec R).OpenCover
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_inter!_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k (m₁.inter! m₂) = true ↔
          Std.DTreeMap.Internal.Impl.contains k m₁ = true ∧ Std.DTreeMap.Internal.Impl.contains k m₂ = true
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.diff : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → M.IsRkFinite (X \ Y)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOpEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.coneOpEquiv =
    {
      functor :=
        { obj := fun c => (Opposite.unop c).op, map := fun {X Y} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ },
      inverse :=
        { obj := fun c => Opposite.op c.unop, map := fun {X Y} f => Opposite.op { hom := f.hom.unop, w := ⋯ },
          map_id := ⋯, map_comp := ⋯ },
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ),
      counitIso :=
        CategoryTheory.Iso.refl
          ({ obj := fun c => Opposite.op c.unop, map := fun {X Y} f => Opposite.op { hom := f.hom.unop, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }.comp
            { obj := fun c => (Opposite.unop c).op, map := fun {X Y} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯,
              map_comp := ⋯ }),
      functor_unitIso_comp := ⋯ }
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.below.trans : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} {x y z : M}
  (a : ConGen.Rel r x y) (a_1 : ConGen.Rel r y z),
  ConGen.Rel.below a → motive x y a → ConGen.Rel.below a_1 → motive y z a_1 → ConGen.Rel.below ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.rightComm_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (m : M) (n : N) (p : P),
  (TensorProduct.rightComm R M N P) (m ⊗ₜ[R] n ⊗ₜ[R] p) = m ⊗ₜ[R] p ⊗ₜ[R] n
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_eq_empty_iff : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Icc a b = ∅ ↔ ¬a ≤ b
-- Mathlib.Algebra.Order.Field.Basic
one_div_le_one_div_of_le : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → a ≤ b → 1 / b ≤ 1 / a
-- Batteries.Data.MLList.Basic
/-- Implementation of `MLList.chunk`.  -/
_private.Batteries.Data.MLList.Basic.0.MLList.chunk.go : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → ℕ → ℕ → Array α → MLList m α → MLList m (Array α)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.toBilin'Aux_toMatrixAux`. -/
toBilin'Aux_toMatrixAux : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B₂ : LinearMap.BilinForm R₁ (n → R₁)), ((LinearMap.BilinForm.toMatrixAux fun j => Pi.single j 1) B₂).toBilin'Aux = B₂
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_singleton : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E} {a : α}
  (hf : BoundedVariationOn f Set.univ), hf.vectorMeasure {a} = Function.rightLim f a - Function.leftLim f a
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_add_eq_left_of_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜},
  analyticOrderAt f z₀ < analyticOrderAt g z₀ → analyticOrderAt (f + g) z₀ = analyticOrderAt f z₀
-- Mathlib.Topology.Algebra.Group.Basic
continuous_div_left' : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Div G] [ContinuousDiv G] (a : G), Continuous fun x => a / x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.epi_of_epi_image : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] [CategoryTheory.Epi (CategoryTheory.Limits.image.ι f)]
  [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)], CategoryTheory.Epi f
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.forall_iff_forall_finsupp : ∀ {R : Type u} [inst : Semiring R] (P : Polynomial R → Prop),
  (∀ (p : Polynomial R), P p) ↔ ∀ (q : AddMonoidAlgebra R ℕ), P { toFinsupp := q }
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.smul_right : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} (a : R) (x y : M), (B x) (a • y) = a * (B x) y
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- The volume of `(ConvexBodyLt K f)` where `convexBodyLT K f` is the set of points `x`
such that `‖x w‖ < f w` for all infinite places `w`.  -/
NumberField.mixedEmbedding.convexBodyLT_volume : ∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal) [inst_1 : NumberField K],
  MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) =
    ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑(∏ w, f w ^ w.mult)
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_comp_C : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S), (MvPolynomial.bind₂ f).comp MvPolynomial.C = f
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
Quiver.Hom.unop_inj_iff : ∀ {C : Type u₁} [inst : Quiver C] {X Y : Cᵒᵖ} {a₁ a₂ : X ⟶ Y}, a₁ = a₂ ↔ a₁.unop = a₂.unop
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
MeasureTheory.Lp.boundedContinuousFunction.congr_simp : ∀ {α : Type u_1} (E : Type u_2) {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E],
  MeasureTheory.Lp.boundedContinuousFunction E p μ = MeasureTheory.Lp.boundedContinuousFunction E p μ
-- Std.Sync.Broadcast
Std.Broadcast.instReprError : Repr Std.Broadcast.Error
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumProdDistrib_symm_apply : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (a : X × Z ⊕ Y × Z),
  Homeomorph.sumProdDistrib.symm a = (Equiv.sumProdDistrib X Y Z).symm a
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.center_toSubmonoid : ∀ (G : Type u_1) [inst : Group G], (Subgroup.center G).toSubmonoid = Submonoid.center G
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.fromAffine_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [inst_1 : Nontrivial R],
  WeierstrassCurve.Projective.Point.fromAffine 0 = 0
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onBoundedFormula_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') (a : L.BoundedFormula α n),
  φ.onBoundedFormula a = φ.toLHom.onBoundedFormula a
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.GrothendieckTopology.OneHypercover.isStronglySheafFor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  {E : J.OneHypercover X} {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)},
  CategoryTheory.Presieve.IsSheaf J F → E.IsStronglySheafFor F
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.splitter : (motive : ZMod 8 → Sort u_1) →
  (a : ZMod 8) →
    (Unit → motive 0) →
      (Unit → motive 2) →
        (Unit → motive 4) →
          (Unit → motive 6) → (Unit → motive 1) → (Unit → motive 7) → (Unit → motive 3) → (Unit → motive 5) → motive a
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a left homology data is preserved by a functor `F`, this functor
preserves the kernel of `S.g : S.X₂ ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [h.IsPreservedBy F],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F
-- Mathlib.Computability.Primrec.Basic
Primrec.decode : ∀ {α : Type u_1} [inst : Primcodable α], Primrec Encodable.decode
-- Mathlib.Logic.Equiv.Fintype
Equiv.toCompl.congr_simp : ∀ {α : Type u_1} {p q : α → Prop} [inst : Finite ↑{x | p x}] (e e_1 : ↑{x | p x} ≃ ↑{x | q x}),
  e = e_1 → e.toCompl = e_1.toCompl
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Construct a model with corners over `ℝ` from a continuous partial equiv with convex range.  -/
ModelWithCorners.ofConvexRange : {E : Type u_4} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_5} →
        [inst_2 : TopologicalSpace H] →
          (φ : PartialEquiv H E) →
            φ.source = Set.univ →
              Convex ℝ φ.target →
                Continuous ↑φ → Continuous ↑φ.symm → (interior φ.target).Nonempty → ModelWithCorners ℝ E H
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.equivMapOfInjective.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) (f : M →ₙ* N)
  (hf : Function.Injective ⇑f), S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := ⋯ }
-- Mathlib.Order.Directed
IsMin.not_isMax' : ∀ {β : Type u_2} [inst : PartialOrder β] [Nontrivial β] [IsDirectedOrder β] {b : β}, IsMin b → ¬IsMax b
-- Std.Time.DateTime
/-- Getter for the `Month` inside of a `DateTime`
 -/
Std.Time.DateTime.month : Std.Time.DateTime → Std.Time.Month.Ordinal
-- Mathlib.RingTheory.TensorProduct.IsBaseChangePi
/-- Base change for direct sums.  -/
IsBaseChange.directSum : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {ι : Type u_3}
  {N : ι → Type u_4} [inst_3 : (i : ι) → AddCommMonoid (N i)] [inst_4 : (i : ι) → Module R (N i)] {P : ι → Type u_5}
  [inst_5 : (i : ι) → AddCommMonoid (P i)] [inst_6 : (i : ι) → Module R (P i)] [inst_7 : (i : ι) → Module S (P i)]
  [inst_8 : ∀ (i : ι), IsScalarTower R S (P i)] {ε : (i : ι) → N i →ₗ[R] P i},
  (∀ (i : ι), IsBaseChange S (ε i)) → IsBaseChange S (DirectSum.lmap ε)
-- Init.Data.String.Basic
String.Pos.toSlice_le : ∀ {s : String} {p q : s.Pos}, p.toSlice ≤ q.toSlice ↔ p ≤ q
-- Mathlib.Computability.Partrec
Partrec.bind : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α →. β} {g : α → β →. σ}, Partrec f → Partrec₂ g → Partrec fun a => (f a).bind (g a)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddEquiv.toAddSemigrpIso_hom : ∀ {X Y : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y] (e : X ≃+ Y),
  e.toAddSemigrpIso.hom = AddSemigrp.ofHom e.toAddHom
-- Mathlib.Topology.Separation.CompletelyRegular
T4Space.instT35Space : ∀ {X : Type u} [inst : TopologicalSpace X] [T4Space X], T35Space X
-- Batteries.Classes.Order
Std.LawfulLTCmp.mk : ∀ {α : Type u_1} [inst : LT α] {cmp : α → α → Ordering} [toOrientedCmp : Std.OrientedCmp cmp],
  (∀ {x y : α}, cmp x y = Ordering.lt ↔ x < y) → Std.LawfulLTCmp cmp
-- Init.Data.String.Lemmas.Order
String.Pos.ofSliceFrom_ne_startPos : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos},
  p ≠ (s.sliceFrom p₀).startPos → String.Pos.ofSliceFrom p ≠ s.startPos
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- Build a `BialgEquiv` from an isomorphism in the category
`HopfAlgCat R`.  -/
CategoryTheory.Iso.toHopfAlgEquiv : {R : Type u} → [inst : CommRing R] → {X Y : HopfAlgCat R} → (X ≅ Y) → X.carrier ≃ₐc[R] Y.carrier
-- Mathlib.Data.Fin.Tuple.Basic
/-- `Fin.find p h` satisfies `p`.  -/
Fin.find_spec : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ k, p k), p (Fin.find p h)
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.coe_mulRight : ∀ {G : Type u_5} [inst : Group G] (a : G), ⇑(Equiv.mulRight a) = fun x => x * a
-- Mathlib.Algebra.Group.Units.Hom
/-- **Alias** of `IsUnit.of_map`. -/
isUnit_of_map_unit : ∀ {R : Type u_2} {S : Type u_3} {F : Type u_5} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : FunLike F R S] (f : F)
  [IsLocalHom f] (a : R), IsUnit (f a) → IsUnit a
-- Mathlib.Algebra.Ring.Defs
NonUnitalRing.toNonUnitalSemiring : {α : Type u_1} → [self : NonUnitalRing α] → NonUnitalSemiring α
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.hexagon_forward_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.MonoidalCategoryStruct.associator X Y Z ≪≫
      β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ≪≫
        CategoryTheory.MonoidalCategoryStruct.associator Y Z X =
    CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫
      CategoryTheory.MonoidalCategoryStruct.associator Y X Z ≪≫
        CategoryTheory.MonoidalCategory.whiskerLeftIso Y (β_ X Z)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v).size = if k ∈ m then m.size else m.size + 1
-- Lean.Meta.Basic
/-- Create a free variable `x` with name, binderInfo and type, add it to the context and run in `k`.
Then revert the context.  -/
Lean.Meta.withLocalDecl : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        Lean.Name →
          Lean.BinderInfo → Lean.Expr → (Lean.Expr → n α) → optParam Lean.LocalDeclKind Lean.LocalDeclKind.default → n α
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.of_coe : ∀ (R : Type u) [inst : Ring R] (X : ModuleCat R), ModuleCat.of R ↑X = X
-- Mathlib.Algebra.Prime.Defs
/-- **Alias** of `Prime.not_isUnit`. -/
Prime.not_unit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ¬IsUnit p
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_add : ∀ (a b : UInt32), (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 4294967296
-- Init.Data.AC
Lean.Data.AC.mergeIdem.eq_1 : Lean.Data.AC.mergeIdem [] = []
-- Mathlib.Logic.Embedding.Basic
/-- The equivalence `one ↪ α` with `α`, for `Unique one`.  -/
Function.Embedding.oneEmbeddingEquiv : {one : Type u_1} → {α : Type u_2} → [Unique one] → (one ↪ α) ≃ α
-- Mathlib.Algebra.Order.UpperLower
LowerSet.addCommSemigroup : {α : Type u_1} →
  [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddCommSemigroup (LowerSet α)