mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of `Left.mul_lt_mul_of_nonneg`.

---

Assumes left strict covariance.  -/
mul_lt_mul'' : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c d : α} [inst_1 : Preorder α] [PosMulStrictMono α] [MulPosMono α],
  a < b → c < d → 0 ≤ a → 0 ≤ c → a * c < b * d
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The source of the coequalizer diagram for `f`.  -/
CategoryTheory.IsRegularEpi.W : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.IsRegularEpi f] → C
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Sequential characterization of lower hemicontinuity**:
If `f : α → Set β` is lower hemicontinuous at `x₀`, `y₀ ∈ f x₀`, `𝓝 y₀` is countably generated, and
`x : ℕ → α` tends to `x₀`, then there is a companion sequence `y : ℕ → β` that tends to `y₀` with
`y n ∈ f (x n)` for all sufficiently large `n`.

This is a partial converse of `LowerHemicontinuousAt.of_sequences`.  -/
LowerHemicontinuousAt.exists_seq_tendsto : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x₀ : α},
  LowerHemicontinuousAt f x₀ →
    ∀ {x : ℕ → α},
      Filter.Tendsto x Filter.atTop (nhds x₀) →
        ∀ {y₀ : β},
          y₀ ∈ f x₀ →
            ∀ [(nhds y₀).IsCountablyGenerated],
              ∃ y, (∀ᶠ (n : ℕ) in Filter.atTop, y n ∈ f (x n)) ∧ Filter.Tendsto y Filter.atTop (nhds y₀)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instAlgebraSubtypeAdicCompletionPolynomialRatFuncIdealXMemValuationSubringAdicCompletionIntegers : (K : Type u_2) →
  [inst : Field K] →
    Algebra K ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K))
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Surjective.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.Surjective (CategoryTheory.CategoryStruct.comp f g)], AlgebraicGeometry.Surjective g
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.map_mk : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (val neg : M)
  (val_neg : val + neg = 0) (neg_val : neg + val = 0),
  (AddUnits.map f) { val := val, neg := neg, val_neg := val_neg, neg_val := neg_val } =
    { val := f val, neg := f neg, val_neg := ⋯, neg_val := ⋯ }
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_Iio : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (q : ℚ),
  Rat.cast ⁻¹' Set.Iio ↑q = Set.Iio q
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.braiding_hom_apply : ∀ {X Y : TopCat} {x : ↑X} {y : ↑Y}, (CategoryTheory.ConcreteCategory.hom (β_ X Y).hom) (x, y) = (y, x)
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.isZero_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject] (i : α),
  CategoryTheory.Limits.IsZero (K.X i) →
    (∀ (j : α), c.Rel j i → CategoryTheory.Limits.IsZero (K.X j)) → CategoryTheory.Limits.IsZero (K.pathObject.X i)
-- Mathlib.Data.Part
Part.get_mem : ∀ {α : Type u_1} {o : Part α} (h : o.Dom), o.get h ∈ o
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.liftEquivOfComm_symm_apply_coe : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {A : Type u_2} [inst_5 : Semiring A] [inst_6 : Algebra R' A]
  (a : TrivSqZeroExt R' M →ₐ[R'] A),
  ↑(TrivSqZeroExt.liftEquivOfComm.symm a) = a.toLinearMap ∘ₗ TrivSqZeroExt.inrHom R' M
-- Mathlib.Order.LatticeIntervals
/-- `Icc a b` is a `BoundedOrder` whenever `a ≤ b`.  -/
Set.Icc.instBoundedOrderElemOfFactLe : {α : Type u_1} → {a b : α} → [inst : Preorder α] → [Fact (a ≤ b)] → BoundedOrder ↑(Set.Icc a b)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A cyclic group is always commutative. This is not an `instance` because often we have
a better proof of `AddCommGroup`.  -/
IsAddCyclic.addCommGroup : {α : Type u_1} → [inst : AddGroup α] → [IsAddCyclic α] → AddCommGroup α
-- Mathlib.Data.List.Sort
/-- Variant of `pairwise_mergeSort` using relation typeclasses.  -/
List.pairwise_mergeSort' : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [Std.Total r] [IsTrans α r] (l : List α),
  List.Pairwise r (l.mergeSort fun x1 x2 => decide (r x1 x2))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get a ⋯
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.restrict_restrict : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (g : G) (t : Set α), (μ.restrict t).restrict (g +ᵥ s) = μ.restrict ((g +ᵥ s) ∩ t)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.sInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : Set (CategoryTheory.MorphismProperty C)},
  (∀ W' ∈ W, W'.RespectsIso) → (sInf W).RespectsIso
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanlMFast : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {α : Type u_3} → [Monad m] → (β → α → m β) → β → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m (Array β)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with sums.  -/
Real.circleAverage_fun_sum : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {c : ℂ} {R : ℝ} {ι : Type u_4} {s : Finset ι}
  {f : ι → ℂ → E},
  (∀ i ∈ s, CircleIntegrable (f i) c R) →
    Real.circleAverage (fun z => ∑ i ∈ s, f i z) c R = ∑ i ∈ s, Real.circleAverage (f i) c R
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
_private.Lean.Meta.Tactic.Grind.EMatchTheoremPtr.0.Lean.Meta.Grind.isSameEMatchTheoremPtr.unsafe_1 : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatchTheorem → Bool
-- Mathlib.Order.Filter.Pointwise
IsUnit.smul_tendsto_smul_iff : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Monoid γ] [inst_1 : MulAction γ β] {m : α → β} {c : γ}
  {f : Filter α} {g : Filter β}, IsUnit c → (Filter.Tendsto (c • m) f (c • g) ↔ Filter.Tendsto m f g)
-- Init.Data.Float.Model.Float
Float.Model.instMul : Mul Float.Model
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_ric_eq_zero_iff : ∀ {n i : ℕ}, (*...=n).toList[i]! = 0 ↔ n < i ∨ i = 0
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.mk.injEq : ∀ (nonOverlapping : Array Lean.Server.FileWorker.AbsoluteLspSemanticToken)
  (current? : Option Lean.Server.FileWorker.AbsoluteLspSemanticToken)
  (surrounding : List Lean.Server.FileWorker.AbsoluteLspSemanticToken)
  (nonOverlapping_1 : Array Lean.Server.FileWorker.AbsoluteLspSemanticToken)
  (current?_1 : Option Lean.Server.FileWorker.AbsoluteLspSemanticToken)
  (surrounding_1 : List Lean.Server.FileWorker.AbsoluteLspSemanticToken),
  ({ nonOverlapping := nonOverlapping, current? := current?, surrounding := surrounding } =
      { nonOverlapping := nonOverlapping_1, current? := current?_1, surrounding := surrounding_1 }) =
    (nonOverlapping = nonOverlapping_1 ∧ current? = current?_1 ∧ surrounding = surrounding_1)
-- Lean.MetavarContext
/-- Set the kind of an fvar. If the given metavariable is not declared or the
given fvar doesn't exist in its context, the `MetavarContext` is returned
unchanged.
 -/
Lean.MetavarContext.setFVarKind : Lean.MetavarContext → Lean.MVarId → Lean.FVarId → Lean.LocalDeclKind → Lean.MetavarContext
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isDetecting_bot_of_isGroupoid : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsGroupoid C], ⊥.IsDetecting
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PushoutCocone.unop_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g), c.unop.pt = Opposite.unop c.pt
-- Mathlib.Topology.Constructions
continuous_sigma_map : ∀ {ι : Type u_5} {κ : Type u_6} {σ : ι → Type u_7} {τ : κ → Type u_8} [inst : (i : ι) → TopologicalSpace (σ i)]
  [inst_1 : (k : κ) → TopologicalSpace (τ k)] {f₁ : ι → κ} {f₂ : (i : ι) → σ i → τ (f₁ i)},
  Continuous (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Continuous (f₂ i)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
cfcHom_eq_of_isStarNormal : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : A) [ha : IsStarNormal a],
  cfcHom ha = (StarAlgebra.elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)
-- Mathlib.Topology.NhdsSet
nhdsSet_neBot_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {s : Set α}, (nhdsSet s).NeBot ↔ s.Nonempty
-- Mathlib.Data.Finset.Lattice.Union
Finset.sup_eq_biUnion : ∀ {α : Type u_7} {β : Type u_8} [inst : DecidableEq β] (s : Finset α) (t : α → Finset β), s.sup t = s.biUnion t
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [h : Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.insert k).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grind.quot : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The natural transformation `t.truncLE n ⟶ 𝟭 C` when `t` is a t-structure
on a category `C` and `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.truncLEι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) → (n : ℤ) → t.truncLE n ⟶ CategoryTheory.Functor.id C
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β] [BorelSpace β] [μ.Regular] (f : α ≃ₜ β),
  (MeasureTheory.Measure.map (⇑f) μ).Regular
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.instInhabitedState : Inhabited Lean.Meta.Grind.Arith.Cutsat.State
-- Mathlib.Algebra.Homology.Homotopy
/-- the sum of two homotopies is a homotopy between the sum of the respective morphisms.  -/
Homotopy.add : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            {f₁ g₁ f₂ g₂ : C ⟶ D} → Homotopy f₁ g₁ → Homotopy f₂ g₂ → Homotopy (f₁ + f₂) (g₁ + g₂)
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
/-- The growth condition that the function `g` must satisfy for the Akra-Bazzi theorem to apply.
It roughly states that `c₁ g(n) ≤ g(u) ≤ c₂ g(n)`, for `u` between `b * n` and `n`, for any
constant `b ∈ (0, 1)`.  -/
AkraBazziRecurrence.GrowsPolynomially : (ℝ → ℝ) → Prop
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.USize.beq_eq_decide_eq : ∀ {a b : USize}, (a == b) = decide (a = b)
-- Mathlib.Order.Hom.Basic
/-- To show that `f : α → β`, `g : β → α` make up an order isomorphism of linear orders,
it suffices to prove `cmp a (g b) = cmp (f a) b`.  -/
OrderIso.ofCmpEqCmp : {α : Type u_6} →
  {β : Type u_7} →
    [inst : LinearOrder α] →
      [inst_1 : LinearOrder β] → (f : α → β) → (g : β → α) → (∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b) → α ≃o β
-- Mathlib.Data.Sym.Sym2
Sym2.ext_iff : ∀ {α : Type u_1} {p q : Sym2 α}, p = q ↔ ∀ (x : α), x ∈ p ↔ x ∈ q
-- Mathlib.Algebra.Module.Presentation.DirectSum
/-- The obvious presentation of the module `ι →₀ N` that is deduced from a presentation
of the module `N`.  -/
Module.Presentation.finsupp : {A : Type u} →
  [inst : Ring A] →
    {N : Type v} →
      [inst_1 : AddCommGroup N] →
        [inst_2 : Module A N] →
          Module.Presentation A N → (ι : Type w) → [DecidableEq ι] → [DecidableEq N] → Module.Presentation A (ι →₀ N)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_inv_le_iff : ∀ {x y : ENNReal} {z : ℝ}, 0 < z → (x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z)
-- Mathlib.Algebra.Ring.SumsOfSquares
NonUnitalSubsemiring.sumSq.eq_1 : ∀ (T : Type u_2) [inst : NonUnitalCommSemiring T],
  NonUnitalSubsemiring.sumSq T = (Subsemigroup.square T).nonUnitalSubsemiringClosure
-- Mathlib.Data.Sym.Basic
Sym.coe_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (s : Sym α n) (f : α → β), ↑(Sym.map f s) = Multiset.map f ↑s
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of an `AddMonoid` inherits a scalar multiplication.  -/
AddSubmonoidClass.instNSMul : {M : Type u_5} →
  [inst : AddMonoid M] → {A : Type u_4} → [inst_1 : SetLike A M] → [AddSubmonoidClass A M] → (S : A) → SMul ℕ ↥S
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.nnnorm_smul_const : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] {R : Type u_4} {β : Type u_5}
  [inst_2 : SeminormedAddCommGroup β] [inst_3 : SeminormedRing R] [inst_4 : Module R β] [inst_5 : NormSMulClass R β]
  (f : C(α, R)) (b : β), ‖f • ContinuousMap.const α b‖₊ = ‖f‖₊ * ‖b‖₊
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.PInfty_comp_πSummand_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n)
      (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n }))) =
    s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n }))
-- Aesop.Tree.Data
Aesop.NormalizationState.notNormal : Aesop.NormalizationState
-- Mathlib.Probability.Independence.Kernel.Indep
/-- The measurable space structures generated by independent pi-systems are independent.  -/
ProbabilityTheory.Kernel.iIndepSets.iIndep : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} (m : ι → MeasurableSpace Ω),
  (∀ (i : ι), m i ≤ _mΩ) →
    ∀ (π : ι → Set (Set Ω)),
      (∀ (n : ι), IsPiSystem (π n)) →
        (∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) →
          ProbabilityTheory.Kernel.iIndepSets π κ μ → ProbabilityTheory.Kernel.iIndep m κ μ
-- Init.SizeOf
Lean.Macro.Exception.error.sizeOf_spec : ∀ (a : Lean.Syntax) (a_1 : String), sizeOf (Lean.Macro.Exception.error a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.of_right_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Y X B A : C} (p : X ⟶ Y) (i : A ⟶ B)
  [CategoryTheory.IsIso p], CategoryTheory.HasLiftingProperty i p
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_injective_iff : ∀ {a₁ a₂ : Complex.UnitClosedDisc}, a₁ = a₂ ↔ ↑a₁ = ↑a₂
-- Mathlib.Algebra.Group.Finsupp
Finsupp.coe_nsmul : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] (n : ℕ) (f : ι →₀ M), ⇑(n • f) = n • ⇑f
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balanceR_eq_balance' : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Balanced →
    r.Balanced →
      l.Sized →
        r.Sized →
          ((∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨
              ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r') →
            l.balanceR x r = l.balance' x r
-- Mathlib.Computability.Reduce
manyOneReducible_refl : ∀ {α : Type u_1} [inst : Primcodable α] (p : α → Prop), p ≤₀ p
-- Init.Data.Option.Lemmas
Option.filter_or_filter : ∀ {α : Type u_1} {o o' : Option α} {f : α → Bool},
  Option.filter f (o.or (Option.filter f o')) = Option.filter f (o.or o')
-- Mathlib.Algebra.Free
/-- The embedding `α → FreeAddSemigroup α`.  -/
FreeAddSemigroup.of : {α : Type u} → α → FreeAddSemigroup α
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.insertIdx.loop.eq_def : ∀ {α : Type u} (i : ℕ) (as : Array α) (j : Fin as.size),
  Array.insertIdx.loop✝ i as j =
    if i < ↑j then
      let j' := ⟨↑j - 1, ⋯⟩;
      let as_1 := as.swap ↑j' ↑j ⋯ ⋯;
      Array.insertIdx.loop✝ i as_1 ⟨↑j', ⋯⟩
    else as
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.

`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
iteration.

This function is deprecated. Instead of `it.allowNontermination.findM?`, use `it.findM?`.

Example:
```lean example
#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
 -/
Std.IterM.Partial.findM? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → Std.IterM.Partial m β → (β → m (ULift.{w, 0} Bool)) → m (Option β)
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.instInhabitedGCongrKey : Inhabited Mathlib.Tactic.GCongr.GCongrKey
-- Mathlib.Data.Int.Cast.Defs
/-- The canonical homomorphism `ℤ → R` agrees with the one from `ℕ → R` on `ℕ`.  -/
AddCommGroupWithOne.intCast_ofNat : ∀ {R : Type u} [self : AddCommGroupWithOne R] (n : ℕ), IntCast.intCast ↑n = ↑n
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaEquiv_symm_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C}
  (f : X ⟶ Y) {P : CategoryTheory.Functor C (Type w)} (t : P.obj X),
  CategoryTheory.shrinkCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (P.map f)) t) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyoneda.{w, v, u}.map f.op)
      (CategoryTheory.shrinkCoyonedaEquiv.symm t)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_comp_add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (c : 𝕜),
  iteratedDerivWithin n (fun z => f (z + c)) s = fun x => iteratedDerivWithin n f (c +ᵥ s) (x + c)
-- Std.Data.DTreeMap.Lemmas
/-- Implementation detail of the tree map  -/
Std.DTreeMap.isSetoid : (α : Type u) →
  (β : α → Type v) → (cmp : autoParam (α → α → Ordering) Std.DTreeMap.isSetoid._auto_1) → Setoid (Std.DTreeMap α β cmp)
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_mod_of_dvd : ∀ (a b : UInt32), b.toNat ∣ 65536 → (a % b).toUInt16 = a.toUInt16 % b.toUInt16
-- Init.Data.String.Defs
String.Slice.mk.injEq : ∀ (str : String) (startInclusive endExclusive : str.Pos)
  (startInclusive_le_endExclusive : startInclusive ≤ endExclusive) (str_1 : String)
  (startInclusive_1 endExclusive_1 : str_1.Pos) (startInclusive_le_endExclusive_1 : startInclusive_1 ≤ endExclusive_1),
  ({ str := str, startInclusive := startInclusive, endExclusive := endExclusive,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive } =
      { str := str_1, startInclusive := startInclusive_1, endExclusive := endExclusive_1,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive_1 }) =
    (str = str_1 ∧ startInclusive ≍ startInclusive_1 ∧ endExclusive ≍ endExclusive_1)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.setImportAll : Lean.ParseImports.Parser
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.smul_orbit_subset : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] (m : M) (a : α),
  m • MulAction.orbit M a ⊆ MulAction.orbit M a
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The 1-morphism `h` commutes with the left Kan extension `f⁺ g`.  -/
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : a ⟶ c) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
            {x : B} →
              (h : c ⟶ x) →
                [inst_2 : CategoryTheory.Bicategory.Lan.CommuteWith f g h] →
                  CategoryTheory.Bicategory.lan f (CategoryTheory.CategoryStruct.comp g h) ≅
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lan f g) h
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSliceData : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The quotient `G ⧸ N` of a complete first countable uniform group `G` by a normal subgroup
is itself complete. In contrast to `QuotientGroup.completeSpace_right'`, in this version `G` is
already equipped with a uniform structure.
[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Even though `G` is equipped with a uniform structure, the quotient `G ⧸ N` does not inherit a
uniform structure, so it is still provided manually via `IsTopologicalGroup.rightUniformSpace`.
In the most common use cases, this coincides (definitionally) with the uniform structure on the
quotient obtained via other means.  -/
QuotientGroup.completeSpace_right : ∀ (G : Type u_1) [inst : Group G] [us : UniformSpace G] [inst_1 : IsRightUniformGroup G] [FirstCountableTopology G]
  (N : Subgroup G) [inst_3 : N.Normal] [hG : CompleteSpace G], CompleteSpace (G ⧸ N)
-- Mathlib.GroupTheory.Coset.Defs
Subgroup.quotientEquivOfEq_mk : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h : s = t) (a : α), (Subgroup.quotientEquivOfEq h) ↑a = ↑a
-- Mathlib.Analysis.Normed.Group.Basic
enorm_le_iff_norm_le : ∀ {E : Type u_5} {F : Type u_6} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {x : E} {y : F},
  ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖
-- Mathlib.Algebra.Category.ModuleCat.Abelian
ModuleCat.forget_reflectsLimitsOfSize : ∀ {R : Type u} [inst : Ring R],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{v, v, max v w, max v w, max (max u (v + 1)) (w + 1), max (v + 1) (w + 1)}
    (CategoryTheory.forget (ModuleCat R))
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_closure_pos_iff_notMem_closure`. -/
EMetric.infEdist_closure_pos_iff_notMem_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {E : Set α}, 0 < Metric.infEDist x (closure E) ↔ x ∉ closure E
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc : ∀ (R : CommRingCat) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec ((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).inv)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec R).toSpecΓ h) =
    h
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.skippingBinders.loop.visitLambda : {α : Type} →
  ℕ →
    Array Lean.Name →
      (Array Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM α) →
        ℕ → Array Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.continuousAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F}, HasGradientAt f f' x → ContinuousAt f x