mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Tactic.Config
/-- `declare_config_elab_legacy elabName TypeName` declares a function `elabName : Syntax → TacticM TypeName`
that elaborates a tactic configuration.
The tactic configuration can be from `Lean.Parser.Tactic.optConfig` or `Lean.Parser.Tactic.config`,
and these can also be wrapped in null nodes (for example, from `(config)?`).

The elaborator responds to the current recovery state.

For defining elaborators for commands, use `declare_command_config_elab`.

This command has been deprecated since 2026-05-14. Use `declare_config_elab` instead.
 -/
Lean.Elab.Tactic.configElab : Lean.ParserDescr
-- Mathlib.Order.Bounded
Set.unbounded_ge_inter_not_ge : ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeInf α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 ≥ x2) (s ∩ {b | ¬a ≤ b}) ↔ Set.Unbounded (fun x1 x2 => x1 ≥ x2) s
-- Mathlib.CategoryTheory.LiftingProperties.Over
CategoryTheory.CommSq.HasLift.over : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X₁ X₂ X₃ X₄ : CategoryTheory.Over S} {t : X₁ ⟶ X₂}
  {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} {sq : CategoryTheory.CommSq t l r b} [⋯.HasLift], sq.HasLift
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- The set of finite `ℝ≥0∞` numbers is homeomorphic to `ℝ≥0`.  -/
ENNReal.ltTopHomeomorphNNReal : ↑{a | a < ⊤} ≃ₜ NNReal
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.IsAffineMap.map_convexCombPair : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] [inst_4 : Convexity.ConvexSpace R N]
  {f : M → N},
  Convexity.IsAffineMap R f →
    ∀ {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : M),
      f (Convexity.convexCombPair s t hs ht h x y) = Convexity.convexCombPair s t hs ht h (f x) (f y)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesColimit_iff_of_iso_diagram : ∀ {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₁ K₂ : CategoryTheory.Functor J C}
  (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂),
  CategoryTheory.Limits.PreservesColimit K₁ F ↔ CategoryTheory.Limits.PreservesColimit K₂ F
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_right_as : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (X : P.I), (P.toCostructuredArrow.obj X).right.as = PUnit.unit
-- Lean.Meta.Sym.ReplaceS
/-- Similar to `replace_fn` in the kernel, but assumes input is maximally shared, and ensures
output is also maximally shared.
 -/
Lean.Meta.Sym.replaceS' : Lean.Expr →
  (Lean.Expr → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM (Option Lean.Expr)) →
    Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_strictMono : StrictMono Cardinal.lift.{u_2, u_1}
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial.congr_simp : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ b₁_1 : Module.Basis ι₁ R M₁),
  b₁ = b₁_1 →
    ∀ (b₂ b₂_1 : Module.Basis ι₂ R M₂),
      b₂ = b₂_1 →
        ∀ (f f_1 : M₁ →ₗ[R] M₂),
          f = f_1 →
            ∀ (i i_1 : ι₂), i = i_1 → LinearMap.toMvPolynomial b₁ b₂ f i = LinearMap.toMvPolynomial b₁_1 b₂_1 f_1 i_1
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instSupSet : {α : Type u_1} → SupSet (MeasureTheory.OuterMeasure α)
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.Clause.eval_relabel : ∀ {α : Type u_1} {β : Type u_2} {r : α → β} {a : β → Bool} {c : Std.Sat.CNF.Clause α},
  Std.Sat.CNF.Clause.eval a (Std.Sat.CNF.Clause.relabel r c) = Std.Sat.CNF.Clause.eval (a ∘ r) c
-- Init.Data.Option.Lemmas
Option.instIdempotentOpOr : ∀ {α : Type u_1}, Std.IdempotentOp Option.or
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_neg_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.covariance X (-Y) μ = -ProbabilityTheory.covariance X Y μ
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.zero_notMem_iff : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  0 ∉ spectrum R a ↔ IsUnit a
-- Init.Prelude
instMonadWithReaderOfOfMonadFunctor : {ρ : Type u} → {m n : Type u → Type v} → [MonadFunctor m n] → [MonadWithReaderOf ρ m] → MonadWithReaderOf ρ n
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.rightRel_r_eq_rightCosetEquivalence : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), ⇑(QuotientGroup.rightRel s) = RightCosetEquivalence ↑s
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_eq_iff_natDegree_eq : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p ≠ 0 → (p.degree = ↑n ↔ p.natDegree = n)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] [inst_4 : HasDerivedCategory C]
  [inst_5 : HasDerivedCategory D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact)
  (F : CategoryTheory.Functor C D) [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] {Z : DerivedCategory D}
  (h :
    (CategoryTheory.shiftFunctor (DerivedCategory D) 1).obj
        (F.mapDerivedCategory.obj ((DerivedCategory.singleFunctor C 0).obj S.X₁)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShiftedHom.map hS.singleδ F.mapDerivedCategory) h =
    CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₃)
      (CategoryTheory.CategoryStruct.comp ⋯.singleδ
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₁))
          h))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constMaxEntry?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.maxEntry? t₁ = Std.DTreeMap.Raw.Const.maxEntry? t₂
-- Lean.Elab.Syntax
Lean.Elab.Term.elabParserName? : Lean.Ident → Lean.Elab.TermElabM (Option Lean.Parser.ParserResolution)
-- Mathlib.RingTheory.Etale.Basic
Algebra.etale_iff : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.Etale R A ↔
    autoParam (Algebra.FormallyEtale R A) Algebra.Etale.formallyEtale._autoParam ∧
      autoParam (Algebra.FinitePresentation R A) Algebra.Etale.finitePresentation._autoParam
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D),
  (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).inverse =
    CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.le_rearrange : ∀ {α : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b : α}, a - b ≤ 0 → a ≤ b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BinaryBiconeMorphism.winl_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B)
  {Z : C} (h : B.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp A.inl (CategoryTheory.CategoryStruct.comp self.hom h) =
    CategoryTheory.CategoryStruct.comp B.inl h
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- At `0` the Gamma function is undefined; by convention we assign it the value `0`.  -/
Complex.Gamma_zero : Complex.Gamma 0 = 0
-- Mathlib.Data.Prod.Lex
Prod.Lex.instWellFoundedRelationLexOfWellFoundedLT : {α : Type u_1} →
  {β : Type u_2} →
    [inst : LT α] → [inst_1 : LT β] → [WellFoundedLT α] → [WellFoundedLT β] → WellFoundedRelation (Lex (α × β))
-- Lean.Elab.DeclNameGen
/-- Adds all prefixes of `ns` as seen constants.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.visitNamespace : Lean.Name → Lean.Elab.Command.NameGen.MkNameM✝ Unit
-- Mathlib.Order.OrderDual
OrderDual.ofDual_lt_ofDual : ∀ {α : Type u_1} [inst : LT α] {a b : αᵒᵈ}, OrderDual.ofDual a < OrderDual.ofDual b ↔ b < a
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Small.limitCone_pt_ext_iff : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : Small.{u, max u v} ↑F.sections] {x y : (CategoryTheory.Limits.Types.Small.limitCone F).pt},
  x = y ↔ (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y
-- Mathlib.Data.Fintype.Quotient
Quotient.finLiftOn_mk : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  {β : Sort u_3} (a : (i : ι) → α i), (Quotient.finLiftOn fun x => ⟦a x⟧) = fun f x => f a
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.exists_mem_support_of_mem_support_prod : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {l : List (Equiv.Perm α)} {x : α},
  x ∈ l.prod.support → ∃ f ∈ l, x ∈ f.support
-- Mathlib.Logic.Basic
or_iff_not_and_not : ∀ {a b : Prop}, a ∨ b ↔ ¬(¬a ∧ ¬b)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCallsParams.mk.sizeOf_spec : ∀ (item : Lean.Lsp.CallHierarchyItem), sizeOf { item := item } = 1 + sizeOf item
-- Mathlib.Algebra.Ring.Shrink
Shrink.instNonAssocRing : {α : Type u_1} → [inst : Small.{v, u_1} α] → [NonAssocRing α] → NonAssocRing (Shrink.{v, u_1} α)
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- notation for p-padic rationals  -/
«termℚ_[_]» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- A function `f : ℂⁿ → E` is integrable on the generalized torus if the function
`f ∘ torusMap c R θ` is integrable on `Icc (0 : ℝⁿ) (fun _ ↦ 2 * π)`.  -/
TorusIntegrable : {n : ℕ} → {E : Type u_1} → [NormedAddCommGroup E] → ((Fin n → ℂ) → E) → (Fin n → ℂ) → (Fin n → ℝ) → Prop
-- Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian
/-- Every object in a cartesian category has commutative comonoid structure.  -/
CategoryTheory.CartesianCopyDiscard.instIsCommComonObjOfCartesian : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C), CategoryTheory.IsCommComonObj X
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_id_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.CategoryStruct.id Y)) h =
    h
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α}, k ∉ m₁ → Std.ExtDHashMap.Const.get! (m₁ ∩ m₂) k = default
-- Mathlib.CategoryTheory.InducedCategory
/-- The induced functor `inducedFunctor F : InducedCategory D F ⥤ D` is fully faithful.  -/
CategoryTheory.fullyFaithfulInducedFunctor : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v, u₂} D] → (F : C → D) → (CategoryTheory.inducedFunctor F).FullyFaithful
-- Init.GetElem
_private.Init.GetElem.0.GetElem?.match_1.splitter : (elem : outParam (Type u_1)) →
  (motive : Option elem → Sort u_2) →
    (x : Option elem) → ((e : elem) → motive (some e)) → (Unit → motive none) → motive x
-- Mathlib.Topology.Category.TopCat.Opens
/-- The inclusion of the top open subset (i.e. the whole space) is an isomorphism.
 -/
TopologicalSpace.Opens.inclusionTopIso : (X : TopCat) → (TopologicalSpace.Opens.toTopCat X).obj ⊤ ≅ X
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau.mk : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    (basic free : Array ℕ) → matType basic.size free.size → Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.congr : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f g : E →L[R] F}, f.HasLeftInverse → g = f → g.HasLeftInverse
-- Mathlib.Data.TypeVec
TypeVec.ofSubtype.eq_def : ∀ {n : ℕ} {α : TypeVec.{u} n} (p : α.Arrow (TypeVec.repeat n Prop)) (x : Fin2 n) (x_1 : TypeVec.Subtype_ p x),
  TypeVec.ofSubtype p x x_1 =
    match n, α, p, x, x_1 with
    | .(n + 1), α, p, i.fs, x => TypeVec.ofSubtype (TypeVec.dropFun p) i x
    | .(n + 1), α, p, Fin2.fz, x => x
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYoneda.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.uliftYoneda.{w, v₁, u₁} =
    CategoryTheory.yoneda.comp
      ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type v₁) (Type (max w v₁))).obj CategoryTheory.uliftFunctor.{w, v₁})
-- Aesop.Forward.State
Aesop.RawHyp.patSubst.injEq : ∀ (subst subst_1 : Aesop.Substitution),
  (Aesop.RawHyp.patSubst subst = Aesop.RawHyp.patSubst subst_1) = (subst = subst_1)
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHom : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G], ↑(LocallyFiniteOrder.orderAddMonoidHom G) = LocallyFiniteOrder.addMonoidHom G
-- Mathlib.Data.Finset.Card
Finset.card_le_card_of_injective : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : ↥s → ↥t}, Function.Injective f → s.card ≤ t.card
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.whiskeringRight_obj_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ᵣ E) {X Y : C ⥤ᵣ D} (f : X ⟶ Y),
  ((CategoryTheory.RightExactFunctor.whiskeringRight C D E).obj F).map f =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.leftRel_eq : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), ⇑(QuotientAddGroup.leftRel s) = fun x y => -x + y ∈ s
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instAddCommSemigroup : {m : Type u_1} →
  {n : Type u_2} →
    {α : m → n → Type v} → [(i : m) → (j : n) → AddCommSemigroup (α i j)] → AddCommSemigroup (DMatrix m n α)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileChangeType.Created.sizeOf_spec : sizeOf Lean.Lsp.FileChangeType.Created = 1
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInvEquiv_mul : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv),
  ↑((S.leftInvEquiv hS) x) * ↑x = 1
-- Std.Async.Timer
/-- If:
- `s` is still running the timer restarts counting from now and completes after `duration`
  milliseconds.
- `s` is not yet or not anymore running this is a no-op.
 -/
Std.Async.Sleep.reset : Std.Async.Sleep → Std.Async.Async Unit
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_right_inj : ∀ {x : NNReal} {y z : ℝ}, x ≠ 0 → x ≠ 1 → (x ^ y = x ^ z ↔ y = z)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.swap_mulVec : ∀ {R : Type u_1} {n : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n) (a : n → R),
  (Matrix.swap R i j).mulVec a = a ∘ ⇑(Equiv.swap i j)
-- Batteries.Data.List.Lemmas
List.insertP.loop.eq_def : ∀ {α : Type u_1} (p : α → Bool) (a : α) (a_1 a_2 : List α),
  List.insertP.loop p a a_1 a_2 =
    match a_1, a_2 with
    | [], r => (a :: r).reverseAux []
    | b :: l, r => bif p b then (a :: r).reverseAux (b :: l) else List.insertP.loop p a l (b :: r)
-- Init.Data.BitVec.Lemmas
BitVec.intMax_add_one : ∀ {w : ℕ}, BitVec.intMax w + 1#w = BitVec.intMin w
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value_Ioi : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot],
      l₁ ≤ Filter.principal s →
        l₂ ≤ Filter.principal s →
          ∀ {f : X → α},
            ContinuousOn f s →
              ∀ {v : α}, Filter.Tendsto f l₁ (nhds v) → Filter.Tendsto f l₂ Filter.atTop → Set.Ioi v ⊆ f '' s
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
uliftZMultiplesHom_symm_apply : ∀ (G : Type u) [inst : AddGroup G] (a : ULift.{u, 0} ℤ →+ G), (uliftZMultiplesHom G).symm a = a (AddEquiv.ulift.symm 1)
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.mk_of_charts : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (equiv : E ≃L[𝕜] E'' × F) (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
  x ∈ domChart.source →
    f x ∈ codChart.source →
      domChart ∈ IsManifold.maximalAtlas I n M →
        codChart ∈ IsManifold.maximalAtlas J n N →
          domChart.source ⊆ f ⁻¹' codChart.source →
            Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv)
                (domChart.extend I).target →
              Manifold.IsSubmersionAtOfComplement F I J n f x
-- Init.Data.Fin.Lemmas
Fin.rev_eq : ∀ {n a : ℕ} (i : Fin (n + 1)) (h : n = a + ↑i), i.rev = ⟨a, ⋯⟩
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Product of elements of a subsemiring of a `CommSemiring` indexed by a `Finset` is in the
`Subsemiring`.  -/
Subsemiring.prod_mem : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Subsemiring R) {ι : Type u_2} {t : Finset ι} {f : ι → R},
  (∀ c ∈ t, f c ∈ s) → ∏ i ∈ t, f i ∈ s
-- Mathlib.RingTheory.RingHom.Bijective
RingHom.Bijective.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k)[k]? = none
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.withConstants_funMap_sumInr : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] (α : Type u_1)
  [inst_1 : (FirstOrder.Language.constantsOn α).Structure M] {a : α} {x : Fin 0 → M},
  FirstOrder.Language.Structure.funMap (Sum.inr a) x = ↑(L.con a)
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.card_algHom_of_finrank_dvd : ∀ {F : Type u_3} {K : Type u_4} {L : Type u_5} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [inst_3 : Field L] [inst_4 : Algebra F L] [Finite L] [inst_6 : Finite K],
  Module.finrank F K ∣ Module.finrank F L → Fintype.card (K →ₐ[F] L) = Module.finrank F K
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPSeries_hasSum : ∀ (L : PeriodPair) (z x : ℂ),
  (∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖) →
    HasSum (fun i => (L.weierstrassPSeries x).coeff i * (z - x) ^ i) (L.weierstrassP z)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.map_cochainsFunctor_shortExact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
  X.ShortExact → (X.map (groupCohomology.cochainsFunctor k G)).ShortExact
-- Init.Data.Random
/-- Returns a standard number generator.  -/
mkStdGen : optParam ℕ 0 → StdGen
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.liftR_map : ∀ {n : ℕ} {α β : TypeVec.{u_1} n} {F' : TypeVec.{u_1} n → Type u} [inst : MvFunctor F'] [LawfulMvFunctor F']
  (R : (β.prod β).Arrow (TypeVec.repeat n Prop)) (x : F' α) (f g : α.Arrow β) (h : α.Arrow (TypeVec.Subtype_ R)),
  TypeVec.comp (TypeVec.subtypeVal R) h = TypeVec.comp (TypeVec.prod.map f g) TypeVec.prod.diag →
    MvFunctor.LiftR' R (MvFunctor.map f x) (MvFunctor.map g x)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_11 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_11 f k