mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_comp : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {ι₁ : Type u_5} {ι₂ : Type u_6} {ι₃ : Type u_7}
  [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃]
  [inst_4 : Module R M₁] [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : Fintype ι₁] [inst_8 : Fintype ι₂]
  [inst_9 : Finite ι₃] [inst_10 : DecidableEq ι₁] [inst_11 : DecidableEq ι₂] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (b₃ : Module.Basis ι₃ R M₃) (g : M₂ →ₗ[R] M₃) (f : M₁ →ₗ[R] M₂) (i : ι₃),
  LinearMap.toMvPolynomial b₁ b₃ (g ∘ₗ f) i =
    (MvPolynomial.bind₁ (LinearMap.toMvPolynomial b₁ b₂ f)) (LinearMap.toMvPolynomial b₂ b₃ g i)
-- Mathlib.RingTheory.IntegralDomain
/-- **Alias** of `isCyclic_of_injective_ringHom`.

---

A finite subgroup of the unit group of an integral domain is cyclic.  -/
isCyclic_of_subgroup_isDomain : ∀ {R : Type u_1} {G : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : Group G] [Finite G] (f : G →* R),
  Function.Injective ⇑f → IsCyclic G
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_ofNat : ∀ (n : ℕ), ISize.ofBitVec (BitVec.ofNat System.Platform.numBits n) = ISize.ofNat n
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- For a non-trivial space, the affine span of a set is `⊤` iff its vector span is `⊤`.  -/
AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial : ∀ (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} [Nontrivial P], affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.map_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} (x : M) (y : ↥S),
  (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩
-- Init.Data.Vector.Lemmas
Vector.size_ne_zero_of_mem : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, a ∈ xs → n ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi : ∀ {θ : Real.Angle}, (2 • θ).toReal = 2 * θ.toReal - 2 * Real.pi ↔ Real.pi / 2 < θ.toReal
-- Mathlib.Data.Finset.Sigma
/-- `s.sigma t` is the finset of dependent pairs `⟨i, a⟩` such that `i ∈ s` and `a ∈ t i`.  -/
Finset.sigma : {ι : Type u_1} → {α : ι → Type u_2} → Finset ι → ((i : ι) → Finset (α i)) → Finset ((i : ι) × α i)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_one : ∀ {d : ℤ}, Zsqrtd.im 1 = 0
-- Init.Data.String.Slice
String.Slice.instInhabitedSplitInclusiveIterator.default : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} →
        {inst : String.Slice.Pattern.ToForwardSearcher pat σ} → String.Slice.SplitInclusiveIterator pat s
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.instIsOrderedRing : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  IsOrderedRing (ArchimedeanClass.FiniteResidueField K)
-- Mathlib.Order.WithBot
WithBot.le_def : ∀ {α : Type u_1} [inst : LE α] {x y : WithBot α}, x ≤ y ↔ x = ⊥ ∨ ∃ a b, a ≤ b ∧ x = ↑a ∧ y = ↑b
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- A square of squares between left adjoints can be composed by iterating vertical and horizontal
composition.
 -/
CategoryTheory.Bicategory.leftAdjointSquare.comp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d e f x y z : B} →
      {g₁ : a ⟶ d} →
        {h₁ : b ⟶ e} →
          {k₁ : c ⟶ f} →
            {g₂ : d ⟶ x} →
              {h₂ : e ⟶ y} →
                {k₂ : f ⟶ z} →
                  {l₁ : a ⟶ b} →
                    {l₂ : b ⟶ c} →
                      {l₃ : d ⟶ e} →
                        {l₄ : e ⟶ f} →
                          {l₅ : x ⟶ y} →
                            {l₆ : y ⟶ z} →
                              (CategoryTheory.CategoryStruct.comp g₁ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁) →
                                (CategoryTheory.CategoryStruct.comp h₁ l₄ ⟶ CategoryTheory.CategoryStruct.comp l₂ k₁) →
                                  (CategoryTheory.CategoryStruct.comp g₂ l₅ ⟶
                                      CategoryTheory.CategoryStruct.comp l₃ h₂) →
                                    (CategoryTheory.CategoryStruct.comp h₂ l₆ ⟶
                                        CategoryTheory.CategoryStruct.comp l₄ k₂) →
                                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g₁ g₂)
                                          (CategoryTheory.CategoryStruct.comp l₅ l₆) ⟶
                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp l₁ l₂)
                                          (CategoryTheory.CategoryStruct.comp k₁ k₂))
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.Slow.instDecidableEMem : {α : Type u_1} →
  {cmp : α → α → Ordering} → {x : α} → [DecidableEq α] → {t : RBTree.RBSet α cmp} → Decidable (RBTree.RBSet.EMem x t)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges_biUnion_right : ∀ {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)]
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq β] (s : Finset α) (t : Finset ι) (f : ι → Finset β),
  Rel.interedges r s (t.biUnion f) = t.biUnion fun b => Rel.interedges r s (f b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.Equation.map : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {S : Type s} [inst_1 : CommRing S] (f : R →+* S)
  {P : Fin 3 → R}, W'.Equation P → (W'.map f).Equation (⇑f ∘ P)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instMulOneClass.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : MulOneClass R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R],
  BoundedContinuousFunction.instMulOneClass =
    { toOne := BoundedContinuousFunction.instOne, toMul := BoundedContinuousFunction.instMul, one_mul := ⋯,
      mul_one := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : ↥(Subgroup.center (Matrix.SpecialLinearGroup n R))),
  ↑↑A = (Matrix.scalar n) ↑↑(Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity A)
-- Mathlib.Algebra.Exact.Basic
Function.Surjective.comp_exact_iff_exact : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {P : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P]
  [inst_5 : Module R M] [inst_6 : Module R M'] [inst_7 : Module R N] [inst_8 : Module R P] {f : M →ₗ[R] N}
  {g : N →ₗ[R] P} {p : M' →ₗ[R] M}, Function.Surjective ⇑p → (Function.Exact ⇑(f ∘ₗ p) ⇑g ↔ Function.Exact ⇑f ⇑g)
-- Mathlib.MeasureTheory.Function.UnifTight
/-- A sequence of functions `f` is uniformly tight in `L^p` if for all `ε > 0`, there
exists some measurable set `s` with finite measure such that the Lp-norm of
`f i` restricted to `sᶜ` is smaller than `ε` for all `i`.  -/
MeasureTheory.UnifTight : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} →
      [NormedAddCommGroup β] → {x : MeasurableSpace α} → (ι → α → β) → ENNReal → MeasureTheory.Measure α → Prop
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.coe_apply_complex : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {i j : Fin 2}, ↑(↑↑(ModularGroup.coe g) i j) = ↑(↑g i j)
-- Mathlib.Analysis.Analytic.IteratedFDeriv
Function.Embedding.equivOfFiniteSelfEmbedding.eq_1 : ∀ {α : Type u_1} [inst : Finite α] (e : α ↪ α), e.equivOfFiniteSelfEmbedding = Equiv.ofBijective ⇑e ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} [inst : Inhabited β] {f : Option β → Option β},
      (t.alter k f)[k']! = if cmp k k' = Ordering.eq then (f t[k]?).get! else t[k']!
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_eq_div_rnDeriv_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.rnDeriv ν =ᵐ[ν] fun x => μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C} (h : CategoryTheory.Limits.pushout g f ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g f) h
-- Mathlib.Data.Set.Function
Set.RightInvOn.extendDomain : ∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} [inst : DecidablePred p] {f : α ≃ Subtype p} {g₁ g₂ : Equiv.Perm α}
  {t : Set α},
  Set.RightInvOn (⇑g₁) (⇑g₂) t → Set.RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.homOfLE_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (hle : N₁ ≤ N₂),
  CategoryTheory.CategoryStruct.comp (PresheafOfModules.Submodule.homOfLE hle) N₂.ι = N₁.ι
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.measurable_condExpKernel : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : Set Ω},
  MeasurableSet s → Measurable fun ω => ((ProbabilityTheory.condExpKernel μ m) ω) s
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.mk : {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) →
                autoParam (∀ (n : ℤ), (le n).IsClosedUnderIsomorphisms)
                    CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam →
                  autoParam (∀ (n : ℤ), (ge n).IsClosedUnderIsomorphisms)
                      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam →
                    (∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le n X → le n' ((CategoryTheory.shiftFunctor C a).obj X)) →
                      (∀ (n a n' : ℤ),
                          a + n' = n → ∀ (X : C), ge n X → ge n' ((CategoryTheory.shiftFunctor C a).obj X)) →
                        (∀ ⦃X Y : C⦄ (f : X ⟶ Y), le 0 X → ge 1 Y → f = 0) →
                          le 0 ≤ le 1 →
                            ge 1 ≤ ge 0 →
                              (∀ (A : C),
                                  ∃ X Y,
                                    ∃ (_ : le 0 X) (_ : ge 1 Y),
                                      ∃ f g h,
                                        CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
                                          CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                CategoryTheory.Triangulated.TStructure C
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : SizeOf R] (order : ℕ) (coeffs : Fin order → R),
  sizeOf { order := order, coeffs := coeffs } = 1 + sizeOf order
-- Init.Grind.Ring.Field
Lean.Grind.Field.mk : {α : Type u} →
  [toCommRing : Lean.Grind.CommRing α] →
    [toInv : Inv α] →
      [toDiv : Div α] →
        [zpow : HPow α ℤ α] →
          (∀ (a b : α), a / b = a * b⁻¹) →
            0 ≠ 1 →
              0⁻¹ = 0 →
                (∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1) →
                  (∀ (a : α), a ^ 0 = 1) →
                    (∀ (a : α) (n : ℕ), a ^ (↑n + 1) = a ^ ↑n * a) →
                      (∀ (a : α) (n : ℤ), a ^ (-n) = (a ^ n)⁻¹) → Lean.Grind.Field α
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- `Function.extend s f 0` as a bundled hom.  -/
Function.ExtendByZero.hom : {ι : Type u_1} → {η : Type v} → (R : Type w) → (ι → η) → [inst : AddZeroClass R] → (ι → R) →+ η → R
-- Lean.Parser.Extra
_private.Lean.Parser.Basic.0.Lean.Parser.addQuotDepth.formatter : ℤ → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instSub : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] → [IsTopologicalAddGroup N] → Sub (M [⋀^ι]→L[R] N)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_inv_lt_iff_of_neg : ∀ {x y z : ℝ}, 0 < x → 0 < y → z < 0 → (x ^ z⁻¹ < y ↔ y ^ z < x)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.prop_inverseImage_iff : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (X : C), P.inverseImage F X ↔ P (F.obj X)
-- Init.Data.Range.Polymorphic.SInt
Int64.lt.eq_1 : ∀ (a b : Int64), a.lt b = (a.toBitVec.slt b.toBitVec = true)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The set of lifts of an element `x` of `⨂[R] i, s i` in `FreeAddMonoid (R × Π i, s i)`.  -/
PiTensorProduct.lifts : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            (PiTensorProduct R fun i => s i) → Set (FreeAddMonoid (R × ((i : ι) → s i)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insert!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insert! k v t).minKey? = some k
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_singleton : ∀ {α : Type u_1} [inst : EDist α] {x : α}, {x}.infsep = 0
-- Lean.MetavarContext
Lean.MetavarKind.syntheticOpaque.sizeOf_spec : sizeOf Lean.MetavarKind.syntheticOpaque = 1
-- Std.Http.Data.Headers.Basic
/-- Parses a comma-separated list of transfer codings from a header value, validating chunked placement.
 -/
Std.Http.Header.TransferEncoding.parse : Std.Http.Header.Value → Option Std.Http.Header.TransferEncoding
-- Mathlib.Analysis.Calculus.FDeriv.Const
tsupport_fderiv_subset : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F}, tsupport (fderiv 𝕜 f) ⊆ tsupport f
-- Mathlib.Data.List.Nodup
List.get_bijective_iff : ∀ {α : Type u} {l : List α} [inst : BEq α] [LawfulBEq α], Function.Bijective l.get ↔ ∀ (a : α), List.count a l = 1
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.sumInl.eq_1 : ∀ {n : Type u_1} (p : Type u_2) {R : Type u₂} (t : Matrix.TransvectionStruct n R),
  Matrix.TransvectionStruct.sumInl p t = { i := Sum.inl t.i, j := Sum.inl t.j, hij := ⋯, c := t.c }
-- Mathlib.Algebra.Notation.Prod
Prod.instDiv.eq_1 : ∀ {G : Type u_8} {H : Type u_9} [inst : Div G] [inst_1 : Div H],
  Prod.instDiv = { div := fun p q => (p.1 / q.1, p.2 / q.2) }
-- Mathlib.FieldTheory.Fixed
FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield : ∀ (M : Type u) [inst : Monoid M] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F],
  SMulCommClass M (↥(FixedPoints.subfield M F)) F
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- The function has compact support .  -/
CompactlySupportedContinuousMap.hasCompactSupport' : ∀ {α : Type u_5} {β : Type u_6} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (self : CompactlySupportedContinuousMap α β), HasCompactSupport self.toFun
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.zero_eq_ofENat : ∀ {m : ℕ∞}, 0 = ↑m ↔ m = 0
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Internal.AssocList.toList_iter : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Internal.AssocList α β}, l.iter.toList = l.toList
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.replace.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → α → α → Sort u_2) (a : α) (as : List α) (b c : α)
  (h_1 : (x x_1 : α) → motive [] x x_1) (h_2 : (a : α) → (as : List α) → (b c : α) → motive (a :: as) b c),
  (match a :: as, b, c with
    | [], x, x_1 => h_1 x x_1
    | a :: as, b, c => h_2 a as b c) =
    h_2 a as b c
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If there exists a nonzero `s ∈ S` such that `n ∣ s`, then `IsCyclotomicExtension S A B`
implies `IsCyclotomicExtension (S ∪ {n}) A B`.  -/
IsCyclotomicExtension.of_union_of_dvd : ∀ {n : ℕ} [NeZero n] {S : Set ℕ} (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B],
  (∃ s ∈ S, s ≠ 0 ∧ n ∣ s) → ∀ [H : IsCyclotomicExtension S A B], IsCyclotomicExtension (S ∪ {n}) A B
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_X : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).X i =
    CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.addHaarMeasure_closure_self : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G},
  (MeasureTheory.Measure.addHaarMeasure K₀) (closure ↑K₀) = 1
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
_private.Std.Data.Iterators.Lemmas.Equivalence.StepCongr.0.Std.IterM.Equiv.step_eq.aux_subtypeMk_congr : ∀ {α : Type u} {P Q R : α → Prop} {h₁ : ∀ (a : α), P a → R a} {h₂ : ∀ (a : α), Q a → R a},
  P = Q → (fun a ha => ⟨a, ⋯⟩) ≍ fun a ha => ⟨a, ⋯⟩
-- Init.Data.SInt.Basic
/-- Negates 16-bit signed integers. Usually accessed via the `-` prefix operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.neg : Int16 → Int16
-- Mathlib.Algebra.Group.Hom.Defs
/-- Composition of `MulHom`s as a `MulHom`.  -/
MulHom.comp : {M : Type u_4} →
  {N : Type u_5} →
    {P : Type u_6} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  (CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₂ = g
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- An auxiliary cocone used in the lemma `pointwiseRightKanExtension_lift_app`  -/
CategoryTheory.Functor.structuredArrowMapCone : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                (G : CategoryTheory.Functor D H) →
                  (L.comp G ⟶ F) →
                    (Y : D) → CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj Y L).comp F)
-- Init.Prelude
Lean.Macro.instInhabitedMethods.default : Lean.Macro.Methods
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β},
  ContinuousWithinAt g t (f x) → ContinuousWithinAt f s x → Set.MapsTo f s t → ContinuousWithinAt (g ∘ f) s x
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The predicate on ordinals which we prove by induction, see `GoodProducts.P0`,
`GoodProducts.Plimit` and `GoodProducts.linearIndependentAux` in the section `Induction` below
 -/
Profinite.NobelingProof.P : (I : Type u) → [inst : LinearOrder I] → [WellFoundedLT I] → Ordinal.{u} → Prop
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.mk.sizeOf_spec : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : optParam (Set M) Set.univ} [inst_5 : SizeOf ι] [inst_6 : SizeOf E]
  [inst_7 : SizeOf H] [inst_8 : SizeOf M] [inst_9 : (a : M) → SizeOf (s a)]
  (toFun : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)
  (locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)) (nonneg' : ∀ (i : ι) (x : M), 0 ≤ (toFun i) x)
  (sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1) (sum_le_one' : ∀ (x : M), ∑ᶠ (i : ι), (toFun i) x ≤ 1),
  sizeOf
      { toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', sum_eq_one' := sum_eq_one',
        sum_le_one' := sum_le_one' } =
    1
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
_private.Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation.0.MeasureTheory.VectorMeasure.bound.eq_1 : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  (μ : MeasureTheory.VectorMeasure X E), μ.bound = (μ.semivariation Set.univ).toNNReal
-- Mathlib.Data.Part
Part.union_get_eq : ∀ {α : Type u_1} [inst : Union α] (a b : Part α) (hab : (a ∪ b).Dom), (a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯
-- Mathlib.RingTheory.LocalRing.Quotient
IsLocalRing.finrank_quotient_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [Module.Finite R S] [Module.Free R S],
  Module.finrank (R ⧸ IsLocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)) =
    Module.finrank R S
-- Mathlib.Topology.Homotopy.Equiv
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousMap.HomotopyEquiv.Simps.symm_apply : {X : Type u} →
  {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → ContinuousMap.HomotopyEquiv X Y → Y → X
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- If a short complex `S` is such that `S.f = 0` and that the kernel of `S.g` is preserved
by a functor `F`, then `F` preserves the left homology of `S`.  -/
CategoryTheory.Functor.preservesLeftHomology_of_zero_f : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C),
  S.f = 0 →
    ∀ [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F], F.PreservesLeftHomologyOf S