mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- If an additive monoid `M` continuously acts on an R₁ topological space `X`,
`g` is an element of `M` such that its integer multiples are dense in `M`,
and `μ` is a finite inner regular measure on `X` which is ergodic with respect to the action of `M`,
then the vector addition of `g` is an ergodic map.  -/
ergodic_vadd_of_denseRange_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [ContinuousNeg G] {X : Type u_2}
  [inst_3 : TopologicalSpace X] [R1Space X] [inst_5 : MeasurableSpace X] [BorelSpace X] [inst_7 : AddAction G X]
  [ContinuousVAdd G X] {g : G},
  (DenseRange fun x => x • g) →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd G X μ],
      Ergodic (fun x => g +ᵥ x) μ
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.foralls : Lean.Option Bool
-- Mathlib.RingTheory.LinearDisjoint
/-- Images of two `R`-algebras `A` and `B` in `A ⊗[R] B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.include_range : ∀ (R : Type u) [inst : CommSemiring R] (A : Type v) [inst_1 : Semiring A] (B : Type w) [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  Algebra.TensorProduct.includeLeft.range.LinearDisjoint Algebra.TensorProduct.includeRight.range
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.instRespectsIsoSchemeTargetAffineLocallyOfToProperty : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso],
  (AlgebraicGeometry.targetAffineLocally P).RespectsIso
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.toEquiv_inj : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {e₁ e₂ : AddConstEquiv G H a b},
  e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_inv : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]), x⁻¹.valuation = -x.valuation
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` and `g` are absolutely continuous on `uIcc a b`, then `f * g` is absolutely continuous
on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.mul : ∀ {a b : ℝ} {f g : ℝ → ℝ},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (f * g) a b
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℂ_one : Complex.Gammaℂ 1 = 1 / ↑Real.pi
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.prob_compl_lt_one_sub_of_lt_prob : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ] {p : ENNReal}, p < μ s → MeasurableSet s → μ sᶜ < 1 - p
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- `biprodComparison' F X Y` is a split mono.  -/
CategoryTheory.Functor.splitMonoBiprodComparison' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              (X Y : C) →
                [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
                  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] →
                    [F.PreservesZeroMorphisms] → CategoryTheory.SplitMono (F.biprodComparison' X Y)
-- Init.Data.UInt.Basic
/-- Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
 -/
UInt32.lt : UInt32 → UInt32 → Prop
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.instAlgebra : (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] → Algebra R' (TrivSqZeroExt R' M)
-- Mathlib.Algebra.Homology.Embedding.Restriction
ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : e.IsRelIff]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C], (e.restrictionFunctor C).PreservesZeroMorphisms
-- Lean.Elab.Tactic.Rewrite
_private.Lean.Elab.Tactic.Rewrite.0.Lean.Elab.Tactic.withRWRulesSeq.go : (Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit) →
  Bool → Lean.Syntax → Lean.Name → Lean.MessageData → List Lean.Name → Lean.Elab.Tactic.TacticM Unit
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.keyAtIdxD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → α → Sort u_3) (x : ℕ) (fallback : α)
  (h_1 : (x : ℕ) → (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf x fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (n : ℕ) → (fallback : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, x, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => h_1 x fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback => h_2 size k v l r n fallback) =
    h_1 x fallback
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.nndist_eq : ∀ {α : Type u_3} {β : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x y : α),
  nndist (h x) (h y) = nndist x y
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injective_iff_subsingleton_ext_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  [inst_2 : CategoryTheory.HasExt C],
  CategoryTheory.Injective X ↔ ∀ ⦃Y : C⦄, Subsingleton (CategoryTheory.Abelian.Ext Y X 1)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.alter₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  {h : 0 < m.buckets.size} {a : α} {f : Option (β a) → Option (β a)} (a_1 : m.WF),
  Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- A term `x : A` satisfies the 0-boundary condition if there exists a finsupp
`∑ aᵢ·gᵢ : G →₀ A` such that `∑ gᵢ⁻¹ • aᵢ - aᵢ = x`.  -/
groupHomology.IsBoundary₀ : (G : Type u_1) → {A : Type u_2} → [Inv G] → [AddCommGroup A] → [SMul G A] → A → Prop
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_cos : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ], IntervalIntegrable Real.cos μ a b
-- Lean.Elab.Tactic.Simp
Lean.Meta.DSimp.ConfigWithOptions.mk : Lean.Meta.DSimp.Config → Lean.Options → Lean.Meta.DSimp.ConfigWithOptions
-- Init.Data.Nat.Lemmas
Nat.pow_div : ∀ {x m n : ℕ}, n ≤ m → 0 < x → x ^ m / x ^ n = x ^ (m - n)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.map_appLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : Opposite.op U' ⟶ Opposite.op U) {Z : CommRingCat}
  (h : X.presheaf.obj (Opposite.op V) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U' V ⋯) h
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- The underlying type.  -/
CommHopfAlgCat.X : {R : Type u} → [inst : CommRing R] → CommHopfAlgCat R → Type v
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsMinor.subset : ∀ {α : Type u_1} {M N : Matroid α}, N ≤m M → N.E ⊆ M.E
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_last_comp_δ_last : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (self.h (Fin.last n)) (Y.δ (Fin.last (n + 1))) = f.app (Opposite.op { len := n })
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj),
  (Bundle.Pretrivialization.codExtend hs nonempty e).target = Prod.map Subtype.val id '' e.target
-- Mathlib.FieldTheory.Minpoly.Field
/-- The minimal polynomial (over `K`) of `σ : Gal(L/K)` is `X ^ (orderOf σ) - 1`.  -/
minpoly_algHom_toLinearMap : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CommRing L] [IsDomain L] [inst_3 : Algebra K L]
  (σ : L →ₐ[K] L), IsOfFinOrder σ → minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.instMembership : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Membership α (Std.Internal.IndexMultiMap α β)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.isZero_of_subsingleton : ∀ {R : Type u} [inst : Ring R] (M : ModuleCat R) [Subsingleton ↑M], CategoryTheory.Limits.IsZero M
-- Mathlib.Algebra.Group.Conj
conj_injective : ∀ {α : Type u} [inst : Group α] {x : α}, Function.Injective fun g => x * g * x⁻¹
-- Mathlib.Topology.Algebra.Group.Basic
instContinuousInvMulOpposite : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Inv α] [ContinuousInv α], ContinuousInv αᵐᵒᵖ
-- Mathlib.Topology.Category.Profinite.EffectiveEpi
Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus : profiniteToCompHaus.EffectivelyEnough
-- Mathlib.RingTheory.Radical.NatInt
Int.radical_natAbs_eq_radical : ∀ {z : ℤ}, ↑(UniqueFactorizationMonoid.radical z.natAbs) = UniqueFactorizationMonoid.radical z
-- Mathlib.Computability.Primrec.Basic
Primrec.list_findIdx₁ : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → β → Bool},
  Primrec₂ p → ∀ (l : List β), Primrec fun a => List.findIdx (p a) l
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
GaloisConnection.l_csSup_of_directedOn : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α]
  [inst_1 : ConditionallyCompletePartialOrderSup β] {l : α → β} {u : β → α},
  GaloisConnection l u →
    ∀ {s : Set α}, DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → l (sSup s) = ⨆ x, l ↑x
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_iInf_map_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f →
    ∀ {ι : Sort u_9} (S : ι → Submodule R M), Submodule.comap f (⨅ i, Submodule.map f (S i)) = iInf S
-- Init.Data.SInt.Lemmas
Int64.mul_succ : ∀ {a b : Int64}, a * (b + 1) = a * b + a
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_up : ∀ {α : Type u_1} [inst : MeasurableSpace α], Measurable ULift.up
-- Mathlib.Data.Set.Function
Set.InjOn.preimage_image_inter : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β}, Set.InjOn f s → s₁ ⊆ s → f ⁻¹' f '' s₁ ∩ s = s₁
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_ge_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {l : Filter β}
  {u : β → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l fun x => -u x) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] (K : CochainComplex C₁ ℤ),
  F.mapDerivedCategoryFactorsh.hom.app ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).obj K) =
    CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map ((DerivedCategory.quotientCompQhIso C₁).hom.app K))
      (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app K)
        (CategoryTheory.CategoryStruct.comp
          ((DerivedCategory.quotientCompQhIso C₂).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K))
          (DerivedCategory.Qh.map ((F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).inv.app K))))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.termℍₒ : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.homEquiv_def : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G),
  (CategoryTheory.ihom.adjunction A).homEquiv B C = A.tensorHomEquiv B C
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Queue : Type
-- Lean.Meta.WHNF
Lean.Meta.project? : Lean.Expr → ℕ → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.symm_mulRight : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (u : ↥(unitary A)),
  (Unitary.mulRight R u).symm = Unitary.mulRight R (star u)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk'_surjective : ∀ {X : SSet} (s : X.N), ∃ t, ∃ (ht : t.simplex ∈ X.nonDegenerate t.dim), s = { toS := t, nonDegenerate := ht }
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.Substructure.toElementarySubstructure_toSubstructure : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.Substructure M)
  (htv :
    ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (a : M),
      φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)),
  ↑(S.toElementarySubstructure htv) = S
-- Lean.Data.Lsp.Extra
Lean.Lsp.HighlightMatchesOptions.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Finset.prod_ite_zero : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] {p : ι → Prop} [inst_1 : DecidablePred p] {f : ι → M₀}
  {s : Finset ι}, (∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0
-- Lean.Parser.Term
Lean.Parser.Term.ellipsis.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Monoid
continuous_pow : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [ContinuousMul M] (n : ℕ), Continuous fun a => a ^ n
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_const_smul : ∀ {α : Type u_1} {f : α → ENNReal} {R : Type u_4} [inst : SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (a : R),
  ∑' (i : α), a • f i = a • ∑' (i : α), f i
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instInhabited : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → Inhabited (MonoidAlgebra R M)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {f : β → β} {hc : k ∈ t.modify k f}, (t.modify k f)[k] = f t[k]
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Edge.mk.injEq : ∀ (src dst : ℕ) (proof : Lean.Expr) (src_1 dst_1 : ℕ) (proof_1 : Lean.Expr),
  ({ src := src, dst := dst, proof := proof } = { src := src_1, dst := dst_1, proof := proof_1 }) =
    (src = src_1 ∧ dst = dst_1 ∧ proof = proof_1)
-- Mathlib.Data.Fin.SuccPred
finCongr_apply_mk : ∀ {n m : ℕ} (h : m = n) (k : ℕ) (hk : k < m), (finCongr h) ⟨k, hk⟩ = ⟨k, ⋯⟩
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.one_def : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : AddCommMonoidWithOne A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoidWithOne B] [inst_4 : Module R B], 1 = 1 ⊗ₜ[R] 1
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.Context.mk : Option ℕ → Aesop.ForwardHypData → Aesop.RuleTac.ForwardM.Context
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.eraseIdx.eq_1 : ∀ {α : Type u} (xs : Array α) (i : ℕ) (h : i < xs.size),
  xs.eraseIdx i h =
    if h' : i + 1 < xs.size then
      let xs' := xs.swap (i + 1) i h' h;
      xs'.eraseIdx (i + 1) ⋯
    else xs.pop
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.injective : ∀ {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 : E →L[R] F}, f.HasLeftInverse → Function.Injective ⇑f
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_neg_pi_div_two_iff : ∀ {z : ℂ}, z.arg = -(Real.pi / 2) ↔ z.re = 0 ∧ z.im < 0
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality : ∀ {R S : CommRingCat} (f : R ⟶ S),
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.Scheme.ΓSpecIso S).inv =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
      (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f))
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.unipotentLower_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₂ ⟶ X₁),
  (CategoryTheory.Biprod.unipotentLower r).inv =
    CategoryTheory.Biprod.ofComponents (CategoryTheory.CategoryStruct.id X₁) 0 (-r)
      (CategoryTheory.CategoryStruct.id X₂)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.toCircle_neg : ∀ {T : ℝ} (x : AddCircle T), (-x).toCircle = x.toCircle⁻¹
-- Mathlib.Data.Finset.Sort
/-- `sort s` constructs a sorted list from the unordered set `s`.
(Uses merge sort algorithm.)  -/
Finset.sort : {α : Type u_1} →
  Finset α →
    (r : autoParam (α → α → Prop) Finset.sort._auto_1) →
      [DecidableRel r] → [IsTrans α r] → [Std.Antisymm r] → [Std.Total r] → List α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
trichotomy_of_mul_eq_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] {a b c d : α} [MulLeftStrictMono α] [MulRightStrictMono α],
  a * b = c * d → a = c ∧ b = d ∨ a < c ∨ b < d
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} [inst_1 : SizeOf C]
  (lift : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I)
  (lift_fac :
    autoParam
      (∀ (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (lift F') F'.m = F.m)
      CategoryTheory.Limits.IsImage.lift_fac._autoParam),
  sizeOf { lift := lift, lift_fac := lift_fac } = 1
-- Mathlib.Data.Set.Image
Set.compl_image : ∀ {α : Type u_1}, Set.image compl = Set.preimage compl
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β},
  Std.DTreeMap.Internal.Impl.empty.Equiv t ↔ t.isEmpty = true
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An `OrderMonoidHom` can be made to an `OrderHom` between their `MulArchimedeanOrder`.  -/
MulArchimedeanOrder.orderHom : {M : Type u_2} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        {N : Type u_3} →
          [inst_3 : CommGroup N] →
            [inst_4 : LinearOrder N] →
              [inst_5 : IsOrderedMonoid N] → (M →*o N) → MulArchimedeanOrder M →o MulArchimedeanOrder N
-- Mathlib.GroupTheory.Complement
/-- Given two subgroups `H' ⊆ H`, there exists a transversal to `H'` inside `H`  -/
AddSubgroup.exists_right_transversal_of_le : ∀ {G : Type u_1} [inst : AddGroup G] {H' H : AddSubgroup G},
  H' ≤ H → ∃ S, ↑H' + S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Given a continuous linear map from `M p` to the space of continuous multilinear maps
in `n` variables `M 0`, ..., `M n` with `M p` removed,
returns a continuous multilinear map in all `n + 1` variables.  -/
ContinuousLinearMap.uncurryMid : {𝕜 : Type u} →
  {n : ℕ} →
    {Ei : Fin n.succ → Type wEi} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  (p : Fin (n + 1)) → (Ei p →L[𝕜] Ei (p.succAbove i) [×n]→L[𝕜] G) → ContinuousMultilinearMap 𝕜 Ei G
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_mul_add_tmod : ∀ (m k : ℤ), m.tdiv k * k + m.tmod k = m
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_eq_zero_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, a / b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.pow_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) (n : ℕ) (m : M), (f ^ n) m = (⇑f)^[n] m
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.isoSum_inv_app_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor (A ⊕ B) C) (b : B),
  F.isoSum.inv.app (Sum.inr b) = CategoryTheory.CategoryStruct.id (F.obj (Sum.inr b))
-- Mathlib.Topology.DiscreteQuotient
/-- Map a discrete quotient along a continuous map.  -/
DiscreteQuotient.map : {X : Type u_2} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {A : DiscreteQuotient X} →
          {B : DiscreteQuotient Y} →
            (f : C(X, Y)) → DiscreteQuotient.LEComap f A B → Quotient A.toSetoid → Quotient B.toSetoid
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioc_sub_one_left_eq_Icc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α),
  Set.Ioc (a - 1) b = Set.Icc a b
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_comp_codRestrict`. -/
Set.restrict_comp_codRestrict : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → β} {b : Set α} (h : ∀ (x : ι), f x ∈ b),
  b.domRestrict g ∘ Set.codRestrict f b h = g ∘ f
-- Mathlib.Data.Set.Prod
Set.pi_univ : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι), (s.pi fun i => Set.univ) = Set.univ
-- Init.Data.UInt.Lemmas
UInt16.ofInt_neg_one : UInt16.ofInt (-1) = -1
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.mapEmbedding_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') (u v : V),
  Function.Injective (SimpleGraph.Path.mapEmbedding f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGet_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} (hk : k ∈ t₁),
  Std.DTreeMap.Internal.Impl.Const.get t₁ k hk = Std.DTreeMap.Internal.Impl.Const.get t₂ k ⋯
-- Init.Data.UInt.Lemmas
USize.not_le : ∀ {a b : USize}, ¬a ≤ b ↔ b < a
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_eraseKey_of_key_ne : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] {a : α} {l : List ((a : α) × β a)} (p : (a : α) × β a),
  p.fst ≠ a → (p ∈ Std.Internal.List.eraseKey a l ↔ p ∈ l)