mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.DirectSum.Module
/-- The map constructed using the universal property gives back the original maps when
restricted to each component.  -/
DirectSum.toModule_lof : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] {N : Type u₁} [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] {φ : (i : ι) → M i →ₗ[R] N} (i : ι) (x : M i),
  (DirectSum.toModule R ι N φ) ((DirectSum.lof R ι M i) x) = (φ i) x
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
/-- Unexpander for `μ⁻[f|m]` notation.  -/
MeasureTheory.condLExpUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Group.Irreducible.Defs
Irreducible.mk : ∀ {M : Type u_1} [inst : Monoid M] {p : M}, ¬IsUnit p → (∀ ⦃a b : M⦄, p = a * b → IsUnit a ∨ IsUnit b) → Irreducible p
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.toSpanSingleton_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x y : M),
  LinearMap.toSpanSingleton R M (x + y) = LinearMap.toSpanSingleton R M x + LinearMap.toSpanSingleton R M y
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piLTLim_symm_apply : ∀ {ι : Type u_6} [inst : LinearOrder ι] {X : ι → Type u_7} {i : ι} (hi : Order.IsSuccPrelimit i)
  {f : ↑(InverseSystem.limit InverseSystem.piLTProj i)} (k : ↑(Set.Iio i)) {l : ↑(Set.Iio i)} (hl : ↑l < ↑k),
  (InverseSystem.piLTLim hi).symm f l = ↑f k ⟨↑l, hl⟩
-- Mathlib.Computability.RE
ComputablePred.computable_iff_re_compl_re : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [DecidablePred p],
  ComputablePred p ↔ REPred p ∧ REPred fun a => ¬p a
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {w x : C} {y z : D} (f : w ⟶ x) (g : y ⟶ z) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight w g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z)
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x g)
        h)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opowAux.eq_3 : ∀ (e a0 a : ONote) (x k : ℕ), (x = 0 → False) → e.opowAux a0 a k.succ x = (e + a0.mulNat k).scale a + e.opowAux a0 a k x
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).counitIso =
    TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinearMapRight'_one : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} [inst_1 : Fintype m] [inst_2 : DecidableEq m],
  Matrix.toLinearMapRight' 1 = LinearMap.id
-- Mathlib.Order.Completion
DedekindCut.instDenselyOrdered : ∀ {α : Type u_1} [inst : LinearOrder α] [DenselyOrdered α], DenselyOrdered (DedekindCut α)
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
with Haar measure, let `1 < p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
Then the `Lᵖ'` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
the Fréchet derivative of `u`.

This is the version where the codomain of `u` is a finite-dimensional normed space.
 -/
MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_4} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure] [inst_8 : FiniteDimensional ℝ F] {u : E → F},
  ContDiff ℝ 1 u →
    HasCompactSupport u →
      ∀ {p p' : NNReal},
        1 ≤ p →
          0 < Module.finrank ℝ E →
            (↑p')⁻¹ = ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹ →
              MeasureTheory.eLpNorm u (↑p') μ ≤
                ↑(MeasureTheory.SNormLESNormFDerivOfEqConst F μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.cofan_inj_epi_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂)
  [inst_1 : CategoryTheory.Epi p.unop] {Z : C} (h : X.obj Δ₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ₁).inj A) (CategoryTheory.CategoryStruct.comp (X.map p) h) =
    CategoryTheory.CategoryStruct.comp ((s.cofan Δ₂).inj (A.epiComp p)) h
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_sub : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddGroup γ] [inst_3 : IsTopologicalAddGroup γ] (f g : α →ₘ[μ] γ), ↑(f - g) =ᵐ[μ] ↑f - ↑g
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₁'_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₁'.f = S.L₀.g
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.uliftFunctor_obj : ∀ (X : Type u), CategoryTheory.uliftFunctor.{v, u}.obj X = ULift.{v, u} X
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 1 = f₂
-- Lean.Meta.Basic
/-- Incremental reuse primitive: if `reusableResult?` is `none`, runs `act` and returns its result
together with the saved monadic state after `act` including the heartbeats used by it. If
`reusableResult?` on the other hand is `some (a, state)`, restores full `state` including heartbeats
used and returns `(a, state)`.

The intention is for steps that support incremental reuse to initially pass `none` as
`reusableResult?` and store the result and state in a snapshot. In a further run, if reuse is
possible, `reusableResult?` should be set to the previous result and state, ensuring that the state
after running `withRestoreOrSaveFull` is identical in both runs. Note however that necessarily this
is only an approximation in the case of heartbeats as heartbeats used by `withRestoreOrSaveFull`
itself after calling `act` as well as by reuse-handling code such as the one supplying
`reusableResult?` are not accounted for.
 -/
Lean.Meta.withRestoreOrSaveFull : {α : Type} → Option (α × Lean.Meta.SavedState) → Lean.MetaM α → Lean.MetaM (α × Lean.Meta.SavedState)
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The adjoint is maximal in the sense that it contains every formal adjoint.  -/
LinearPMap.IsFormalAdjoint.le_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  {S : F →ₗ.[𝕜] E} [inst_5 : CompleteSpace E], Dense ↑T.domain → T.IsFormalAdjoint S → S ≤ T.adjoint
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.Hom.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₂} D] →
      {F : C → D} →
        {P : CategoryTheory.MorphismProperty D} →
          [inst_1 : P.IsMultiplicative] →
            {X Y : CategoryTheory.InducedWideCategory D F P} → (hom : F X ⟶ F Y) → P hom → X.Hom Y
-- Mathlib.Order.Heyting.Basic
compl_anti : ∀ {α : Type u_2} [inst : HeytingAlgebra α], Antitone compl
-- Lean.Data.Lsp.CodeActions
/-- Parameters for a [CodeActionRequest](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_codeAction).  -/
Lean.Lsp.CodeActionParams : Type
-- Mathlib.Data.Set.Operations
Set.Subtype.range_coind : ∀ {α : Type u} {β : Type v} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)),
  Set.range (Subtype.coind f h) = Subtype.val ⁻¹' Set.range f
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqHost.beq : Std.Http.URI.Host → Std.Http.URI.Host → Bool
-- Mathlib.Topology.UnitInterval
unitInterval.lt_one_iff_ne_one : ∀ {x : ↑unitInterval}, x < 1 ↔ x ≠ 1
-- Mathlib.CategoryTheory.Monoidal.Action.End
/-- A monoidal functor `F : C ⥤ D ⥤ D` can be thought of as a right action
of `C` on `D`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) →
            [F.Monoidal] → CategoryTheory.MonoidalCategory.MonoidalRightAction C D
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.ninePointCircle_eq_circumsphere_medial : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.ninePointCircle = s.medial.circumsphere
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.pointwise_smul_le_pointwise_smul_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : AddMonoid A] [inst_1 : Group G] [inst_2 : DistribMulAction G A] {a : G}
  {S T : AddSubmonoid A}, a • S ≤ a • T ↔ S ≤ T
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.prop_ihom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : CategoryTheory.MonoidalClosed C] [P.IsMonoidalClosed] {X Y : C},
  P X → P Y → P (X ⟹ Y)
-- Lean.Elab.Tactic.Omega.Core
/-- The facts which give an upper bound on the target variable,
and the coefficient of the target variable in each.
 -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.upperBounds : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → List (Lean.Elab.Tactic.Omega.Fact × ℤ)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id_assoc : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id._auto_3) {Z : C}
  (h_1 :
    X'.E (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃) (CategoryTheory.homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv
      (CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) h_1) =
    h_1
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_comm : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [inst : CommMagma α], A.hadamard B = B.hadamard A
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
MeasureTheory.volume_sum_rpow_lt : ∀ (ι : Type u_1) [inst : Fintype ι] [Nonempty ι] {p : ℝ},
  1 ≤ p →
    ∀ (r : ℝ),
      MeasureTheory.volume {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} =
        ENNReal.ofReal r ^ Fintype.card ι *
          ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))
-- Mathlib.Condensed.Basic
/-- Condensed sets (types) with the appropriate universe levels, i.e. `Type (u + 1)`-valued
sheaves on `CompHaus.{u}`.
 -/
CondensedSet : Type (u + 2)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The cocone associated to a pushout is a colimit cone.  -/
CategoryTheory.Limits.pushout.isColimit : {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] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushout.cocone f g)
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A topological space is σ-compact iff there exists a countable collection of compact
subspaces that cover the entire space.  -/
SigmaCompactSpace_iff_exists_compact_covering : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  SigmaCompactSpace X ↔ ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = Set.univ
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- The identity function is locally Lipschitz.  -/
LocallyLipschitz.id : ∀ {α : Type u} [inst : PseudoEMetricSpace α], LocallyLipschitz id
-- Mathlib.Order.SetDissipate
Set.dissipate.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] (s : α → Set β) (x : α), Set.dissipate s x = ⋂ y, ⋂ (_ : y ≤ x), s y
-- Mathlib.Order.BoundedOrder.Basic
/-- A subtype remains a bounded order if the property holds at `⊥` and `⊤`.  -/
Subtype.boundedOrder : {α : Type u} → {p : α → Prop} → [inst : LE α] → [inst_1 : BoundedOrder α] → p ⊥ → p ⊤ → BoundedOrder (Subtype p)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- `toPrincipalIdeal R K x` sends `x ≠ 0 : K` to the fractional `R`-ideal generated by `x`  -/
toPrincipalIdeal : (R : Type u_3) →
  (K : Type u_4) →
    [inst : CommRing R] →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] → [IsFractionRing R K] → Kˣ →* (FractionalIdeal (nonZeroDivisors R) K)ˣ
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.coe_iSup_of_directed : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] {S : ι → AddSubsemigroup M},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.trans_div : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f g : β → α}, Multipliable g L → Multipliable (fun b => f b / g b) L → Multipliable f L
-- Lean.Data.KVMap
/-- Erase an entry from the map  -/
Lean.KVMap.erase : Lean.KVMap → Lean.Name → Lean.KVMap
-- Init.Data.BitVec.Bitblast
BitVec.getElem_umod : ∀ {w i : ℕ} {n d : BitVec w} (hi : i < w),
  (n % d)[i] = if d = 0#w then n[i] else (BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w)).r[i]
-- Mathlib.RingTheory.MvPowerSeries.Derivative
_private.Mathlib.RingTheory.MvPowerSeries.Derivative.0.MvPowerSeries.pderivFun_coe_mul_coe : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} (f g : MvPolynomial σ R),
  MvPowerSeries.pderivFun i (↑f * ↑g) = ↑f * ↑((MvPolynomial.pderiv i) g) + ↑g * ↑((MvPolynomial.pderiv i) f)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.integral_gaussianReal_eq_integral_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : ℝ} {v : NNReal} {f : ℝ → E},
  v ≠ 0 → ∫ (x : ℝ), f x ∂ProbabilityTheory.gaussianReal μ v = ∫ (x : ℝ), ProbabilityTheory.gaussianPDFReal μ v x • f x
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetsResponse.widgets : Lean.Widget.GetWidgetsResponse → Array Lean.Widget.PanelWidgetInstance
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coeMonoidHom`. -/
ModularForm.coeHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : MulOne F] → [inst_2 : MulOneClass β] → [IsOneApply F α β] → [IsMulApply F α β] → F →* α → β
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.head.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : List α) → x ≠ [] → Sort u_2) (a : α) (tail : List α) (x : a :: tail ≠ [])
  (h_1 : (a : α) → (tail : List α) → (x : a :: tail ≠ []) → motive (a :: tail) x),
  (match a :: tail, x with
    | a :: tail, x => h_1 a tail x) =
    h_1 a tail x
-- Lean.Parser.Basic
/-- The position prior to the failing parser  -/
Lean.Parser.RecoveryContext.initialPos : Lean.Parser.RecoveryContext → String.Pos.Raw
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square with `0 : 0 ⟶ 0` on the right and `𝟙 X` on the left is a pullback square.  -/
CategoryTheory.IsPullback.zero_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.IsPullback 0 (CategoryTheory.CategoryStruct.id X) 0 0
-- Mathlib.Data.Multiset.Count
Multiset.count_eq_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a : α}, Multiset.count a s = 0 ↔ a ∉ s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
one_lt_pow_iff : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ}, n ≠ 0 → (1 < x ^ n ↔ 1 < x)
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.StrictMono.liftRingHom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S) {a : ℕ → ℕ}
  (ha : StrictMono a) (f : (n : ℕ) → R →+* S ⧸ I ^ a n)
  (hf : ∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) [inst_2 : IsAdicComplete I S],
  IsAdicComplete.StrictMono.liftRingHom I ha f hf =
    IsAdicComplete.liftRingHom I (fun n => (Ideal.Quotient.factorPow I ⋯).comp (f n)) ⋯
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.instMkMor₂BicategoryM : Mathlib.Tactic.BicategoryLike.MkMor₂ Mathlib.Tactic.Bicategory.BicategoryM
-- Init.Data.Slice.List.Lemmas
List.mkSlice_rcc_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1
-- Mathlib.CategoryTheory.Shift.Basic
/-- `shift` is monoidal  -/
CategoryTheory.HasShift.shiftMonoidal : {C : Type u} →
  {A : Type u_2} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {inst_1 : AddMonoid A} → [self : CategoryTheory.HasShift C A] → CategoryTheory.HasShift.shift.Monoidal
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.fg_of_fg_map : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B),
  Function.Injective ⇑f → (Subalgebra.map f S).FG → S.FG
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_apply_apply : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α), e.symm (e x) = x
-- Aesop.Search.Expansion.Norm
Aesop.normalizeGoalMVar : Lean.MVarId → Aesop.UnorderedArraySet Lean.MVarId → Aesop.NormM Aesop.NormSeqResult
-- Mathlib.Analysis.SpecificLimits.Normed
dist_partial_sum_le_of_le_geometric : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {r C : ℝ} {f : ℕ → α},
  (∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) →
    ∀ (n : ℕ), dist (∑ i ∈ Finset.range n, f i) (∑ i ∈ Finset.range (n + 1), f i) ≤ C * r ^ n
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ},
  0 ≤ p → ∀ {f g : α → ENNReal}, AEMeasurable f μ → ∫⁻ (a : α), f a ^ p ∂μ = 0 → ∫⁻ (a : α), (f * g) a ∂μ = 0
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_inf_of_antitone : ∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} [inst_1 : Preorder ι] [IsCodirectedOrder ι] {f g : ι → α},
  Antitone f → Antitone g → ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i
-- Init.Core
Thunk.sizeOf_eq : ∀ {α : Type u_1} [inst : SizeOf α] (a : Thunk α), sizeOf a = 1 + sizeOf a.get
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofAlgHom_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂)
  (h₂ : g.comp f = AlgHom.id R A₁) (a : A₁), (AlgEquiv.ofAlgHom f g h₁ h₂) a = f a
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredElemCarrierObjPartOrdEmbIsCardinalFilteredWithTopValSetPropSetWithTop : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular] (S : Subtype (J.PropSetWithTop κ')), CategoryTheory.IsCardinalFiltered (↑↑S) κ
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The Lie algebra of an additive Lie group, i.e., its tangent space at zero. We use
the word `AddGroupLieAlgebra` instead of `LieAlgebra` as the latter is taken as a generic class.  -/
AddGroupLieAlgebra : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                (G : Type u_4) → [inst : TopologicalSpace G] → [ChartedSpace H G] → [AddGroup G] → Type u_3
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α] [CompleteSpace α],
  Topology.IsClosedEmbedding TopologicalSpace.NonemptyCompacts.toCloseds
-- Mathlib.Data.Set.Function
Set.injOn_id : ∀ {α : Type u_1} (s : Set α), Set.InjOn id s
-- Std.Time.Date.Unit.Day
Std.Time.Day.instDecidableLeOrdinal : {x y : Std.Time.Day.Ordinal} → Decidable (x ≤ y)
-- Mathlib.Algebra.Ring.Invertible
/-- Multiplying an additive unit from the right produces another additive unit.  -/
AddUnits.mulRight : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → AddUnits R → R → AddUnits R
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instOneHom : (G H : GrpCat) → One (G ⟶ H)
-- Mathlib.Algebra.GradedMulAction
/-- The graded version of `Monoid.toMulAction`.  -/
GradedMonoid.GMonoid.toGMulAction : {ιA : Type u_1} →
  (A : ιA → Type u_4) → [inst : AddMonoid ιA] → [inst_1 : GradedMonoid.GMonoid A] → GradedMonoid.GMulAction A A
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.instHasLimitOppositeDiscreteOpFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [CategoryTheory.Limits.HasCoproduct Z], CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor Z).op
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.exists_forall_norm_le : ∀ {α : Type u_1} {F : Type u_5} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup F]
  (f : MeasureTheory.SimpleFunc α F), ∃ C, ∀ (x : α), ‖f x‖ ≤ C
-- Mathlib.Data.ENat.Pow
ENat.epow_eq_zero_iff : ∀ {x y : ℕ∞}, x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.ext_iff : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] {f : R →+* S} {M : ModuleCat R}
  {g g' : ↑((ModuleCat.coextendScalars f).obj M)},
  g = g' ↔ (ModuleCat.CoextendScalars.equiv f M) g = (ModuleCat.CoextendScalars.equiv f M) g'