mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Lemmas
List.map_coe_finRange_eq_range : ∀ {n : ℕ}, List.map (fun x => ↑x) (List.finRange n) = List.range n
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.utf8Size_assemble₄ : ∀ {w x y z : UInt8} {c : Char}, ByteArray.utf8DecodeChar?.assemble₄ w x y z = some c → c.utf8Size = 4
-- Std.Net.Addr
/-- Gets address information about the network interfaces on the system, including disabled ones and
multiple addresses for each interface.
 -/
Std.Net.interfaceAddresses : IO (Array Std.Net.InterfaceAddress)
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.norm_le_mul' : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F} {K : NNReal},
  LipschitzWith K f → f 1 = 1 → ∀ (x : E), ‖f x‖ ≤ ↑K * ‖x‖
-- Mathlib.Algebra.Field.Defs
NNRat.smulDivisionSemiring : {K : Type u_1} → [DivisionSemiring K] → SMul ℚ≥0 K
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, t.WF → (k ∈ Std.TreeMap.Raw.map f t ↔ k ∈ t)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in `opow`  -/
ONote.opowAux2 : ONote → ONote × ℕ → ONote
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasRightHomology]
  [inst_3 : S₂.HasRightHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) h₂.rightHomologyIso.hom =
    CategoryTheory.CategoryStruct.comp h₁.rightHomologyIso.hom γ.φH
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.ghostComponent_zero_verschiebungFun : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R),
  (WittVector.ghostComponent 0) x.verschiebungFun = 0
-- Mathlib.Data.Finset.Pi
Finset.piCongrLeft_comp_restrict : ∀ {ι : Type u_2} {π : ι → Type u_3} {s : Finset ι},
  ⇑(Equiv.piCongrLeft (fun i => π ↑i) s.equivToSet) ∘ s.restrict = (↑s).domRestrict
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.le_inf_support_pow : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : SemilatticeInf T] [inst_1 : OrderTop T] [inst_2 : Semiring R]
  [inst_3 : AddMonoid A] [inst_4 : AddMonoid T] [AddLeftMono T] [AddRightMono T] {degt : A → T},
  0 ≤ degt 0 →
    (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
      ∀ (n : ℕ) (f : AddMonoidAlgebra R A), n • f.coeff.support.inf degt ≤ (f ^ n).coeff.support.inf degt
-- Std.Do.SPred.SPred
Std.Do.SPred.not_cons : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {P : Std.Do.SPred (σ :: σs)}, spred(¬P) s = spred(¬P s)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_ofLinearIsometry_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap ∘ₛₗ g = LinearMap.id)
  (h₂ : g ∘ₛₗ f.toLinearMap = LinearMap.id), ⇑(LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂).symm = ⇑g
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- If `m s ≠ 0`, then for some point `x ∈ s` and any `t ∈ 𝓝[s] x` we have `0 < m t`.  -/
MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  [inst_2 : TopologicalSpace α] [SecondCountableTopology α] {s : Set α},
  μ s ≠ 0 → ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, 0 < μ t
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.liftingLocalizedFunctor : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {D₁ : Type u₄} →
      {D₂ : Type u₅} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁] →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] →
                {W₁ : CategoryTheory.MorphismProperty C₁} →
                  {W₂ : CategoryTheory.MorphismProperty C₂} →
                    (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        [inst_4 : L₁.IsLocalization W₁] →
                          (L₂ : CategoryTheory.Functor C₂ D₂) →
                            [inst_5 : L₂.IsLocalization W₂] →
                              CategoryTheory.Localization.Lifting L₁ W₁ (Φ.functor.comp L₂) (Φ.localizedFunctor L₁ L₂)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.dirichletUnitTheorem.logSpace.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.dirichletUnitTheorem.logSpace K = NumberField.Units.dirichletUnitTheorem.logSpace K
-- Init.Data.Dyadic.Basic
Dyadic.instIntCast : IntCast Dyadic
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap.eq_1 : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] {X Y : C₁} (f : L₁.obj X ⟶ L₁.obj Y),
  Φ.homMap L₁ L₂ f =
    (((CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).symm.app X).homCongr
        ((CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).symm.app Y))
      ((Φ.localizedFunctor L₁ L₂).map f)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.toPrenexImpRight : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormula α n}, ψ.IsQF → φ.toPrenexImpRight ψ = φ.imp ψ
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.sum_lt : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : Finset α},
  s.Nonempty → (∀ i ∈ s, padicNorm p (F i) < t) → padicNorm p (∑ i ∈ s, F i) < t
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.faceι.eq_1 : ∀ {n : ℕ} (i : Fin (n + 1)), SSet.boundary.faceι i = SSet.Subcomplex.homOfLE ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk'.injEq : ∀ {X : SSet} {A : X.Subcomplex} (toN : X.N) (notMem : toN.simplex ∉ A.obj (Opposite.op { len := toN.dim }))
  (toN_1 : X.N) (notMem_1 : toN_1.simplex ∉ A.obj (Opposite.op { len := toN_1.dim })),
  ({ toN := toN, notMem := notMem } = { toN := toN_1, notMem := notMem_1 }) = (toN = toN_1)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.freeObj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (F : CategoryTheory.Functor Cᵒᵖ (Type u)) {X Y : Cᵒᵖ} (f : X ⟶ Y),
  (PresheafOfModules.freeObj F).map f =
    ModuleCat.freeDesc (TypeCat.ofHom fun x => ModuleCat.freeMk ((CategoryTheory.ConcreteCategory.hom (F.map f)) x))
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace : ∀ {X Y : AlgebraicGeometry.Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥Y] (f g : X ⟶ Y),
  CompactSpace ↥(CategoryTheory.Limits.equalizer f g)
-- Aesop.Search.Queue
Aesop.FIFOQueue.pos : Aesop.FIFOQueue → ℕ
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [inst_4 : CategoryTheory.Category.{v_7, u_7} E]
  (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂)
  {X Y : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)} (f : X ⟶ Y) (X_1 : C₁) (X_2 : C₂),
  (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).map f).app X_1).app X_2 =
    (f.app (F₁.obj X_1)).app (F₂.obj X_2)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y)
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x : X),
  ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).inv.app
            X_1).snd.app
      x =
    CategoryTheory.CategoryStruct.id (ψ.right.obj (X_1.snd.obj (U.obj x)))
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_loops_union_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.closure (M.loops ∪ X) = M.closure X
-- Mathlib.RingTheory.Localization.FractionRing
/-- The image of `IsFractionRing.lift` is the subfield generated by `s`, if the image
of the ring hom is the subring generated by `s`.  -/
IsFractionRing.lift_fieldRange_eq_of_range_eq : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g) {s : Set L},
  g.range = Subring.closure s → (IsFractionRing.lift hg).fieldRange = Subfield.closure s
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_containsThenInsertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t htb).2.impl.toListModel.Perm
      (Std.Internal.List.insertEntryIfNew k v t.toListModel)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inv_hom_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : F.I₀), CategoryTheory.CategoryStruct.comp (e.inv.h₀ i) (e.hom.h₀ (e.inv.s₀ i)) = CategoryTheory.eqToHom ⋯
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.generalizeTelescopeAux : {α : Type} →
  (Array Lean.Expr → Lean.MetaM α) → Array Lean.Meta.GeneralizeTelescope.Entry → ℕ → Array Lean.Expr → Lean.MetaM α
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_toReal : ∀ {a : EReal}, a ≠ ⊤ → a ≠ ⊥ → Filter.Tendsto EReal.toReal (nhds a) (nhds a.toReal)
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.prodMk_right : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α × β → γ}, UniformContinuous f → ∀ (a : α), UniformContinuous fun b => f (a, b)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : CategoryTheory.SplitEpi f},
  x = y ↔ x.section_ = y.section_
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_inv : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → Group (f i)] (i : I) (x : f i),
  Pi.mulSingle i x⁻¹ = (Pi.mulSingle i x)⁻¹
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instInvolutiveStar : {α : Type u_3} →
  {E : α → Type u_4} →
    {p : ENNReal} →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : (i : α) → StarAddMonoid (E i)] → [∀ (i : α), NormedStarGroup (E i)] → InvolutiveStar ↥(lp E p)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.IsCoreflexivePair.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B} (s : B ⟶ A),
  CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A →
    CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A → CategoryTheory.IsCoreflexivePair f g
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.sup_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (F G : CategoryTheory.SubmonoidFunctor M) (x : C), (SemilatticeSup.sup F G).obj x = F.obj x ⊔ G.obj x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Dist.ext_iff : ∀ {α : Type u_3} {x y : Dist α}, x = y ↔ dist = dist
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.pullbackHom_map : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : W ⟶ X)
  [inst_2 : ∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] (i : 𝒰.toPreZeroHypercover.1),
  CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (𝒰.f i) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) f
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.isFiniteMeasure_restrict_Ioc : ∀ (x y : ℝ), MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ioc x y))
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.toFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                CategoryTheory.LaxBraidedFunctor C D → CategoryTheory.Functor C D
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0.inj : ∀ {k : ℕ} {c₁ c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k_1 : ℕ}
  {c₁_1 c₂_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr},
  Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0 k c₁ c₂ =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0 k_1 c₁_1 c₂_1 →
    k = k_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mem_inf : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {p p' : NonUnitalSubsemiring R} {x : R}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Init.Data.Array.MapIdx
List.mapFinIdxM.go.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (as : List α)
  (f : (i : ℕ) → α → i < as.length → m β) (bs : List α) (acc : Array β) (a : bs.length + acc.size = as.length),
  List.mapFinIdxM.go as f bs acc a =
    match bs, acc, a with
    | [], acc, h => pure acc.toList
    | a :: as_1, acc, h => do
      let __do_lift ← f acc.size a ⋯
      List.mapFinIdxM.go as f as_1 (acc.push __do_lift) ⋯
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoal.range : Lean.Lsp.PlainTermGoal → Lean.Lsp.Range
-- Mathlib.Algebra.Group.WithOne.Basic
AddEquiv.withZeroCongr_symm : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), e.withZeroCongr.symm = e.symm.withZeroCongr
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_inl : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Submonoid M),
  Submonoid.map (MonoidHom.inl M N) s = s.prod ⊥
-- Std.Async.Basic
/-- Runs all computations concurrently and returns the result of the first one to finish.
All other results are lost, and the tasks are not cancelled, so they'll continue their execution
until the end.
 -/
Std.Async.Async.raceAll : {c : Type u_1} →
  {α : Type} →
    [ForM Std.Async.Async c (Std.Async.Async α)] → c → optParam Task.Priority Task.Priority.default → Std.Async.Async α
-- Lean.Data.Lsp.Window
Lean.Lsp.instFromJsonMessageActionItem.fromJson : Lean.Json → Except String Lean.Lsp.MessageActionItem
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withBotCongr_toAddHom : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), ↑e.withBotCongr = (↑e).withBotMap
-- Mathlib.Data.Multiset.MapFold
Multiset.erase_attach_map : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] (s : Multiset α) (f : α → β) (x : { x // x ∈ s }),
  Multiset.map (fun j => f ↑j) (s.attach.erase x) = Multiset.map f (s.erase ↑x)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.ofAlgEquiv_toPresentation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (e : S ≃ₐ[R] T), (P.ofAlgEquiv e).toPresentation = P.ofAlgEquiv e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] [Std.LawfulEqOrd α]
  {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit}, t₁.WF → t₂.WF → (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁.Equiv t₂
-- Init.Data.Iterators.Combinators.Monadic.Append
/-- The internal state of the `IterM.append` iterator combinator.
 -/
Std.Iterators.Types.Append : Type w → Type w → (Type w → Type w') → Type w → Type w
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.toListRev_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β},
  (array.iterM m).toListRev = pure array.toListRev
-- Mathlib.Data.Nat.Choose.Lucas
/-- **Lucas's Theorem**: For primes `p`, `choose n k` is congruent to the product of
`choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p)` over `i` modulo `p`.  -/
Choose.choose_modEq_prod_range_choose_nat : ∀ {n k p : ℕ} [Fact (Nat.Prime p)] {a : ℕ},
  n < p ^ a → k < p ^ a → n.choose k ≡ ∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]
-- Mathlib.Algebra.DirectSum.Decomposition
/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
a module to a direct sum of components.  -/
DirectSum.decomposeLinearEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : DecidableEq ι] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              (ℳ : ι → Submodule R M) → [DirectSum.Decomposition ℳ] → M ≃ₗ[R] DirectSum ι fun i => ↥(ℳ i)
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_eq_iInter_cthickening' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ},
  ∀ s ⊆ Set.Ioi δ,
    (∀ (ε : ℝ), δ < ε → (s ∩ Set.Ioc δ ε).Nonempty) →
      ∀ (E : Set α), Metric.cthickening δ E = ⋂ ε ∈ s, Metric.cthickening ε E
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeIdeal_ne_one : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I : Ideal R}, ↑I ≠ 1 ↔ I ≠ 1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `mul_inv_le_iff₀` for a version with multiplication on the other side.  -/
mul_inv_le_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (b * c⁻¹ ≤ a ↔ b ≤ c * a)
-- Mathlib.Algebra.Module.Injective
Module.Baer.instSemilatticeInfExtensionOf : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) → (f : M →ₗ[R] Q) → SemilatticeInf (Module.Baer.ExtensionOf i f)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Prod.instMeasurableSingletonClass : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α]
  [MeasurableSingletonClass β], MeasurableSingletonClass (α × β)
-- Mathlib.Algebra.Quaternion
Quaternion.imI_smul : ∀ {S : Type u_1} {R : Type u_3} [inst : CommRing R] (a : Quaternion R) [inst_1 : SMul S R] (s : S),
  (s • a).imI = s • a.imI
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : Option β → Option β},
  (t.alter k f).getKey! k = if (f t[k]?).isSome = true then k else default
-- Init.Data.Nat.Dvd
Nat.mul_div_assoc : ∀ {k n : ℕ} (m : ℕ), k ∣ n → m * n / k = m * (n / k)
-- Mathlib.Logic.Nontrivial.Basic
Function.nontrivial : ∀ {α : Type u_1} {β : Type u_2} [h : Nonempty α] [Nontrivial β], Nontrivial (α → β)
-- Mathlib.ModelTheory.Algebra.Field.Basic
/-- An indexing type to name each of the field axioms. The theory
of fields is defined as the range of a function `FieldAxiom ->
Language.ring.Sentence`  -/
FirstOrder.Field.FieldAxiom : Type
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.supports_run : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) {k : K}
  (s : Turing.TM2to1.StAct K Γ σ k) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.SupportsStmt S (Turing.TM2to1.stRun s q) ↔ Turing.TM2.SupportsStmt S q
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- A set of generators of a free group, chosen arbitrarily  -/
IsFreeGroup.Generators : (G : Type u_1) → [inst : Group G] → [IsFreeGroup G] → Type u_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.inv : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p₁ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.mul_cert p₁ (-1) p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.mem_next : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] {j : ι}
  {k' : ι'}, c'.Rel (e.f j) k' → ∃ k, e.f k = k'
-- Std.Data.Internal.List.Associative
Std.Internal.List.keys_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.keys (Std.Internal.List.eraseKey k l) = (Std.Internal.List.keys l).erase k
-- Std.Time.Internal.Bounded
/-- Creates a new `Bounded` Integer.
 -/
Std.Time.Internal.Bounded.mk : {lo hi : ℤ} → {rel : ℤ → ℤ → Prop} → (val : ℤ) → rel lo val ∧ rel val hi → Std.Time.Internal.Bounded rel lo hi