mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Try.Collect
_private.Lean.Meta.Tactic.Try.Collect.0.Lean.Meta.Try.Collector.main.go : Lean.MVarId → StateRefT' IO.RealWorld Lean.Meta.Try.Collector.Cache Lean.Meta.Try.Collector.M Unit
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram.hasForget : CategoryTheory.ConcreteCategory LightDiagram fun X Y => C(↑X.toProfinite.toTop, ↑Y.toProfinite.toTop)
-- Lean.Elab.Tactic.Induction
/-- Generalize targets in `fun_induction` and `fun_cases`. Should behave like `elabCasesTargets` with
no targets annotated with `h : _`.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.generalizeTargets : Array Lean.Expr → Lean.Elab.Tactic.TacticM (Array Lean.Expr)
-- Init.System.IO
/-- Mutable reference cells that contain values of type `α`. These cells can read from and mutated in
the `IO` monad.
 -/
IO.Ref : Type → Type
-- Aesop.Search.Expansion.Simp
/-- Add all `let` hypotheses in the local context as `simp` theorems.

Background: by default, in the goal `x : _ := v ⊢ P[x]`, `simp` does not
substitute `x` by `v` in the target. The `simp` option `zetaDelta` can be used
to make `simp` perform this substitution, but we don't want to set it because
then Aesop `simp` would diverge from default `simp`, so we would have to adjust
the `aesop?` output as well. Instead, we add `let` hypotheses explicitly. This
way, `simp?` picks them up as well.

See lean4#3520.
 -/
Aesop.addLetDeclsToSimpTheorems : Lean.Meta.Simp.Context → Lean.MetaM Lean.Meta.Simp.Context
-- Init.Prelude
Nat.le_of_succ_le_succ : ∀ {n m : ℕ}, n.succ ≤ m.succ → n ≤ m
-- Lean.Parser.Types
Lean.Parser.ParserCache : Type
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.insertManyIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (l : ρ),
  m.insertManyIfNew l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have r := ⟨(↑r).insertIfNew a b, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insertIfNew a b)) →
              P m → P m' } :=
        __s
      pure r).run
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xz_sub : ∀ {a : ℕ} (a1 : 1 < a) {m n : ℕ},
  n ≤ m → Pell.xz a1 (m - n) = Pell.xz a1 m * Pell.xz a1 n - ↑(Pell.d✝ a1) * Pell.yz a1 m * Pell.yz a1 n
-- Mathlib.Order.Directed
directedOn_range : ∀ {α : Type u_1} {ι : Sort u_3} {r : α → α → Prop} {f : ι → α}, DirectedOn r (Set.range f) ↔ Directed r f
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.abs_rpow_le_exp_log_mul : ∀ (x y : ℝ), |x ^ y| ≤ Real.exp (Real.log x * y)
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.closure_sdiff_eq_self`. -/
Matroid.closure_diff_eq_self : ∀ {α : Type u_2} {M : Matroid α} {X Y : Set α}, Y ⊆ M.closure (X \ Y) → M.closure (X \ Y) = M.closure X
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.Indep.indicator_indepFun : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {m : MeasurableSpace Ω} {M : Type u_10}
  {𝓧 : Type u_11} [inst : Zero M] [inst_1 : MeasurableSpace M] (c : M) {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω} {X : Ω → 𝓧},
  MeasurableSet A →
    ProbabilityTheory.Indep m (MeasurableSpace.comap X m𝓧) μ → ProbabilityTheory.IndepFun (A.indicator fun x => c) X μ
-- Std.Sync.Broadcast
/-- Index where the next message will be written in the circular buffer.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.write : {α : Type} → (self : Std.Bounded.State✝ α) → Fin ↑(Std.Bounded.State.capacity✝ self)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_reflectsLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃}
  [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.ReflectsLimit K F] [CategoryTheory.Limits.ReflectsLimit (K.comp F) G],
  CategoryTheory.Limits.ReflectsLimit K (F.comp G)
-- Mathlib.Algebra.Category.Ring.Basic
/-- Build a `RingEquiv` from an isomorphism in the category `RingCat`.  -/
CategoryTheory.Iso.ringCatIsoToRingEquiv : {R S : RingCat} → (R ≅ S) → ↑R ≃+* ↑S
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.FullyFaithful.homNatIso'_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X X_1 : C),
  (hF.homNatIso' X).inv.app X_1 = (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.inv
-- Lean.Elab.PreDefinition.WF.Preprocess
/-- `match (wfParam x) with con y => alt[y] ==> match x with con y => alt[wfParam y]  -/
Lean.Elab.WF.paramMatcher : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Normed.Module.Bases
/-- Biorthogonality.  -/
GeneralSchauderBasis.ortho : ∀ {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {L : SummationFilter β} (self : GeneralSchauderBasis β 𝕜 X L) (i j : β),
  (self.coord i) (↑self j) = Pi.single j 1 i
-- Mathlib.Logic.Equiv.Basic
Equiv.coe_piCongr_symm : ∀ {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (h₁ a)),
  ⇑(h₁.piCongr h₂).symm = fun f a => (h₂ a).symm (f (h₁ a))
-- Std.Data.ExtTreeMap.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate fails.  -/
Std.ExtTreeMap.any : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → (α → β → Bool) → Bool
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_eq_none : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α}, m.contains a = false → m.get? a = none
-- Mathlib.Algebra.Order.Field.Basic
one_lt_div_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → (1 < a / b ↔ a < b)
-- Mathlib.Order.Basic
LE.le.lt_iff_ne' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a → (b < a ↔ a ≠ b)
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.add_subst : ∀ {α : Type u_1} [inst : Ring α] {n e1 e2 t1 t2 : α}, n * e1 = t1 → n * e2 = t2 → n * (e1 + e2) = t1 + t2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyGE?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKeyGE? k = t₂.getKeyGE? k
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Complex.sin_eq_tsum' : ∀ (z : ℂ), Complex.sin z = ∑' (n : ℕ), (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1).factorial / Complex.I
-- Lean.Elab.DocString
/-- A provider of suggestions for code elements.
 -/
Lean.Doc.CodeSuggester : Type
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.funMap_sumInl : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M]
  [inst_1 : (L.sum L').Structure M] [FirstOrder.Language.LHom.sumInl.IsExpansionOn M] {n : ℕ} {f : L.Functions n}
  {x : Fin n → M}, FirstOrder.Language.Structure.funMap (Sum.inl f) x = FirstOrder.Language.Structure.funMap f x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n),
  (-γ).rightShift a n' hn' = -γ.rightShift a n' hn'
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernelRelations_G : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁), (pres₂.cokernelRelations data).G = pres₂.G
-- Mathlib.Analysis.InnerProductSpace.Continuous
ContinuousAt.inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {α : Type u_4} [inst_3 : TopologicalSpace α] {f g : α → E} {x : α},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun t => inner 𝕜 (f t) (g t)) x
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.strongEpi_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} [CategoryTheory.StrongEpiCategory C] (f : P ⟶ Q)
  [CategoryTheory.Epi f], CategoryTheory.StrongEpi f
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.one_comul_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : C) [inst_3 : CategoryTheory.BimonObj M] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one) h)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.Agree.brecOn : ∀ {F : PFunctor.{uA, uB}}
  {motive :
    {n : ℕ} →
      (a : PFunctor.Approx.CofixA F n) → (a_1 : PFunctor.Approx.CofixA F (n + 1)) → PFunctor.Approx.Agree a a_1 → Prop}
  {n : ℕ} {a : PFunctor.Approx.CofixA F n} {a_1 : PFunctor.Approx.CofixA F (n + 1)} (t : PFunctor.Approx.Agree a a_1),
  (∀ {n : ℕ} (a : PFunctor.Approx.CofixA F n) (a_2 : PFunctor.Approx.CofixA F (n + 1))
      (t : PFunctor.Approx.Agree a a_2), PFunctor.Approx.Agree.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ι_functorMapTgt_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  (i : I) (t : A i ⟶ X) (b : B i ⟶ S)
  (w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b) (b' : B i ⟶ T)
  (hb' : CategoryTheory.CategoryStruct.comp b (CategoryTheory.Arrow.Hom.right τ) = b') (t' : A i ⟶ Y)
  (ht' : CategoryTheory.CategoryStruct.comp t (CategoryTheory.Arrow.Hom.left τ) = t') {Z : C}
  (h : ∐ CategoryTheory.SmallObject.functorObjTgtFamily f πY ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πX)
        { i := i, t := t, b := b, w := w })
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapTgt f τ) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πY)
        { i := i, t := t', b := b', w := ⋯ })
      h
-- Mathlib.CategoryTheory.Action.Monoidal
/-- An oplax monoidal functor induces an oplax monoidal functor between
the categories of `G`-actions within those categories.  -/
CategoryTheory.Functor.instOplaxMonoidalActionMapAction : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        {W : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_2, u_3} W] →
            [inst_3 : CategoryTheory.MonoidalCategory V] →
              [inst_4 : CategoryTheory.MonoidalCategory W] →
                (F : CategoryTheory.Functor V W) → [F.OplaxMonoidal] → (F.mapAction G).OplaxMonoidal
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- The `PushoutObjObj` structure given by the pushout of the colimits API.  -/
CategoryTheory.Functor.PushoutObjObj.ofHasPushout : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              {X₁ Y₁ : C₁} →
                (f₁ : X₁ ⟶ Y₁) →
                  {X₂ Y₂ : C₂} →
                    (f₂ : X₂ ⟶ Y₂) →
                      [CategoryTheory.Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] → F.PushoutObjObj f₁ f₂
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.ofList_eq_insertMany_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α}, Std.HashSet.Raw.ofList l = ∅.insertMany l
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.forIn'_eq_forIn'_rco : ∀ {α : Type u} {r : Std.Rio α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α] [inst_3 : Std.PRange.Least? α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_8 : Std.Rxo.IsAlwaysFinite α] [inst_9 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w}
  [inst_10 : Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.PRange.UpwardEnumerable.least...r.upper) init fun a ha acc => f a ⋯ acc
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.of_mul_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Semigroup α] [MulLeftMono α] {a b : α},
  MulLECancellable (a * b) → MulLECancellable b
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyonedaType_obj_map : ∀ (X : Type uᵒᵖ) {X_1 Y : CommGrpCat} (f : X_1 ⟶ Y),
  (CommGrpCat.coyonedaType.obj X).map f =
    CommGrpCat.ofHom (MonoidHom.pi fun i => (CommGrpCat.Hom.hom f).comp (Pi.evalMonoidHom (fun a => ↑X_1) i))
-- Mathlib.CategoryTheory.Localization.Linear
CategoryTheory.Localization.instLinearLocalizationQ : ∀ (R : Type w) [inst : Ring R] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  [inst_2 : CategoryTheory.Preadditive C] (W : CategoryTheory.MorphismProperty C) [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.Preadditive W.Localization] [inst_5 : W.Q.Additive], CategoryTheory.Functor.Linear R W.Q
-- Lean.Parser.Types
Lean.Parser.ParserCacheKey : Type
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one.eq_1 : ∀ {α : Type u_2} [inst : One α], Finset.one = { one := {1} }
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.distribMulAction : {S : Type u_2} →
  {R : Type u} →
    {M : Type v} →
      [inst : Monoid S] →
        [inst_1 : AddMonoid R] →
          [inst_2 : AddMonoid M] →
            [DistribMulAction S R] → [DistribMulAction S M] → DistribMulAction S (TrivSqZeroExt R M)
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- If an equivalence `E : C ≌ D` is compatible with shifts, so is `E.symm`.
 -/
CategoryTheory.Equivalence.CommShift.instSymm : ∀ {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] (E : C ≌ D) (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : E.functor.CommShift A]
  [inst_6 : E.inverse.CommShift A] [E.CommShift A], E.symm.CommShift A
-- Mathlib.Algebra.Group.Nat.Even
Nat.div_two_mul_two_of_even : ∀ {n : ℕ}, Even n → n / 2 * 2 = n
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Basic.0.Array.MergeSort.Internal.merge.go.induct_unfolding : ∀ {α : Type u_1} (le : α → α → Bool)
  (motive : (xs ys : Subarray α) → 0 < Std.Slice.size xs → 0 < Std.Slice.size ys → Array α → Array α → Prop),
  (∀ (xs ys : Subarray α) (hxs : 0 < Std.Slice.size xs) (hys : 0 < Std.Slice.size ys) (acc : Array α),
      have x := xs[0];
      have y := ys[0];
      le x y = true →
        ∀ (h : 1 < Std.Slice.size xs),
          motive (xs.drop 1) ys ⋯ hys (acc.push x)
              (Array.MergeSort.Internal.merge.go✝ le (xs.drop 1) ys ⋯ hys (acc.push x)) →
            motive xs ys hxs hys acc (Array.MergeSort.Internal.merge.go✝ le (xs.drop 1) ys ⋯ hys (acc.push x))) →
    (∀ (xs ys : Subarray α) (hxs : 0 < Std.Slice.size xs) (hys : 0 < Std.Slice.size ys) (acc : Array α),
        have x := xs[0];
        have y := ys[0];
        le x y = true →
          ¬1 < Std.Slice.size xs →
            motive xs ys hxs hys acc (Std.Slice.foldl (fun acc y => acc.push y) (acc.push x) ys)) →
      (∀ (xs ys : Subarray α) (hxs : 0 < Std.Slice.size xs) (hys : 0 < Std.Slice.size ys) (acc : Array α),
          have x := xs[0];
          have y := ys[0];
          ¬le x y = true →
            ∀ (h : 1 < Std.Slice.size ys),
              motive xs (ys.drop 1) hxs ⋯ (acc.push y)
                  (Array.MergeSort.Internal.merge.go✝ le xs (ys.drop 1) hxs ⋯ (acc.push y)) →
                motive xs ys hxs hys acc (Array.MergeSort.Internal.merge.go✝ le xs (ys.drop 1) hxs ⋯ (acc.push y))) →
        (∀ (xs ys : Subarray α) (hxs : 0 < Std.Slice.size xs) (hys : 0 < Std.Slice.size ys) (acc : Array α),
            have x := xs[0];
            have y := ys[0];
            ¬le x y = true →
              ¬1 < Std.Slice.size ys →
                motive xs ys hxs hys acc (Std.Slice.foldl (fun acc x => acc.push x) (acc.push y) xs)) →
          ∀ (xs ys : Subarray α) (hxs : 0 < Std.Slice.size xs) (hys : 0 < Std.Slice.size ys) (acc : Array α),
            motive xs ys hxs hys acc (Array.MergeSort.Internal.merge.go✝ le xs ys hxs hys acc)
-- Mathlib.Order.Filter.Basic
Filter.principal_eq_iff_eq : ∀ {α : Type u} {s t : Set α}, Filter.principal s = Filter.principal t ↔ s = t
-- Init.Data.String.Basic
String.head_data : ∀ {b : String} {h : b.toList ≠ []}, b.toList.head h = b.toByteArray.utf8DecodeChar 0 ⋯
-- Mathlib.Algebra.Quandle
ShelfHom.inhabited : (S : Type u_4) → [inst : Shelf S] → Inhabited (ShelfHom S S)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.infinite_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, (-s).Infinite ↔ s.Infinite
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- The resolution maps intertwine the lift of a morphism and that morphism.  -/
CategoryTheory.ProjectiveResolution.lift_commutes : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z)
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q) Q.π =
    CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_emod_left : ∀ (a b : ℤ), a * b % b = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- One subspace is less than or equal to another if and only if all its points are in the second
subspace.  -/
AffineSubspace.le_def' : ∀ {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₁ s₂ : AffineSubspace k P), s₁ ≤ s₂ ↔ ∀ p ∈ s₁, p ∈ s₂
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_diagonal_diagonal : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {m : Type u_10} {n : Type u_11} [inst : Zero α] [inst_1 : Zero β]
  [inst_2 : Zero γ] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] (f : α → β → γ),
  (∀ (b : β), f 0 b = 0) →
    (∀ (a : α), f a 0 = 0) →
      ∀ (a : m → α) (b : n → β),
        Matrix.kroneckerMap f (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun mn => f (a mn.1) (b mn.2)
-- Mathlib.Tactic.NormNum.IsCoprime
Mathlib.Meta.NormNum.int_not_isCoprime_helper : ∀ (x y : ℤ) (d : ℕ), x.gcd y = d → d.beq 1 = false → ¬IsCoprime x y
-- Mathlib.Data.Set.Countable
Set.Countable.prod : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β}, s.Countable → t.Countable → (s ×ˢ t).Countable
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_succ_top : ∀ {M : Type u_3} [inst : AddCommMonoid M] {a b : ℕ},
  a ≤ b → ∀ (f : ℕ → M), ∑ k ∈ Finset.Ico a (b + 1), f k = ∑ k ∈ Finset.Ico a b, f k + f b
-- Mathlib.Data.Vector.Basic
/-- Apply a monadic function to each component of a vector,
returning a vector inside the monad.  -/
List.Vector.mmap : {m : Type u → Type u_6} →
  [Monad m] → {α : Type u_7} → {β : Type u} → (α → m β) → {n : ℕ} → List.Vector α n → m (List.Vector β n)
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.all_one_of_le_one_le_of_prod_eq_one : ∀ {α : Type u_4} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {s : Multiset α},
  (∀ x ∈ s, 1 ≤ x) → s.prod = 1 → ∀ x ∈ s, x = 1
-- Mathlib.Logic.Unique
Unique.ext_iff : ∀ {α : Sort u} {x y : Unique α}, x = y ↔ default = default
-- Mathlib.Tactic.TFAE
/-- `tfae_finish` closes goals of the form `TFAE [P₁, P₂, ...]` once a sufficient collection
of hypotheses of the form `Pᵢ → Pⱼ` or `Pᵢ ↔ Pⱼ` have been introduced to the local context.

`tfae_have` can be used to conveniently introduce these hypotheses; see `tfae_have`.

Example:
```lean4
example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry /- proof of P → Q -/
  tfae_have 2 → 1 := sorry /- proof of Q → P -/
  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
  tfae_finish
```
 -/
Mathlib.Tactic.TFAE.tfaeFinish : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Volume.Measure
EuclideanSpace.euclideanHausdorffMeasure_eq_volume : ∀ (d : ℕ), MeasureTheory.Measure.euclideanHausdorffMeasure d = MeasureTheory.volume
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.diff.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (l₁ : List α) (a : α) (l₂ : List α)
  (h_1 : (l : List α) → motive l []) (h_2 : (l₁ : List α) → (a : α) → (l₂ : List α) → motive l₁ (a :: l₂)),
  (match l₁, a :: l₂ with
    | l, [] => h_1 l
    | l₁, a :: l₂ => h_2 l₁ a l₂) =
    h_2 l₁ a l₂
-- Init.Control.Lawful.MonadAttach.Lemmas
WeaklyLawfulMonadAttach.attach_bind_val : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] {x : m α} {f : α → m β},
  (do
      let a ← MonadAttach.attach x
      f ↑a) =
    x >>= f