mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.mk : Option Lean.Name →
  Lean.Options →
    List Lean.OpenDecl →
      Lean.Elab.MacroStack → Bool → List Lean.Name → Array Lean.Elab.Term.FixedTermElabRef → Lean.Elab.Term.SavedContext
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.uIoc a b = Set.Ioc a b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_of_isSome_maxKey?_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α}, (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey?.isSome = true → t.maxKey?.isSome = true
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.getVert_eq_start_iff_of_not_nil : ∀ {V : Type u} {G : SimpleGraph V} {u w : V} {i : ℕ} {p : G.Walk u w}, p.IsPath → ¬p.Nil → (p.getVert i = u ↔ i = 0)
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.associator_hom_congr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y z t : B} {f f' : x ⟶ y} {g g' : y ⟶ z} {h h' : z ⟶ t}
  (ef : f = f') (eg : g = g') (eh : h = h'),
  (CategoryTheory.Bicategory.associator f g h).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g' h').hom
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.Logic.Function.Basic
/-- Extension of a function `g : α → γ` along a function `f : α → β`.

For every `a : α`, `f a` is sent to `g a`. `f` might not be surjective, so we use an auxiliary
function `j : β → γ` by sending `b : β` not in the range of `f` to `j b`. If you do not care about
the behavior outside the range, `j` can be used as a junk value by setting it to be `0` or
`Classical.arbitrary` (assuming `γ` is nonempty).

This definition is mathematically meaningful only when `f a₁ = f a₂ → g a₁ = g a₂` (spelled
`g.FactorsThrough f`). In particular this holds if `f` is injective.

A typical use case is extending a function from a subtype to the entire type. If you wish to extend
`g : {b : β // p b} → γ` to a function `β → γ`, you should use `Function.extend Subtype.val g j`.  -/
Function.extend : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → (α → β) → (α → γ) → (β → γ) → β → γ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.zero_trim : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {n : MeasurableSpace α} (hle : m ≤ n), MeasureTheory.VectorMeasure.trim 0 hle = 0
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.abToCycles_apply_coe : ∀ (S : CategoryTheory.ShortComplex Ab) (x : ↑S.X₁), ↑(S.abToCycles x) = (CategoryTheory.ConcreteCategory.hom S.f) x
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.isCentralScalar : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] {R : Type u_10}
  [inst_6 : Monoid R] [inst_7 : DistribMulAction R V2] [inst_8 : SMulCommClass k R V2]
  [inst_9 : DistribMulAction Rᵐᵒᵖ V2] [inst_10 : IsCentralScalar R V2], IsCentralScalar R (P1 →ᵃ[k] V2)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on a compact set `s` and `f 0 = 0` and `a : X → A` is
continuous on `t : Set X`, and `0 ≤ a x` and has quasispectrum contained in `s` for all `x ∈ t`,
then `fun x ↦ cfcₙ f (a x)` is continuous on `t`.  -/
ContinuousOn.cfcₙ_nnreal' : ∀ {X : Type u_1} {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_12 : TopologicalSpace X] {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A} {t : Set X},
      ContinuousOn a t →
        (∀ x ∈ t, quasispectrum NNReal (a x) ⊆ s) →
          (∀ x ∈ t, 0 ≤ a x) →
            autoParam (ContinuousOn f s) ContinuousOn.cfcₙ_nnreal'._auto_1 →
              autoParam (f 0 = 0) ContinuousOn.cfcₙ_nnreal'._auto_3 → ContinuousOn (fun x => cfcₙ f (a x)) t
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.instHasTerminalOfOrderTop : ∀ {C : Type u} [inst : Preorder C] [OrderTop C], CategoryTheory.Limits.HasTerminal C
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_singleton : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) {δ : ℝ}, 0 ≤ δ → Metric.cthickening δ {x} = Metric.closedBall x δ
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- A property of objects is a monoidal closed if it is closed under taking internal homs
 -/
CategoryTheory.ObjectProperty.IsMonoidalClosed : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.ObjectProperty C → [CategoryTheory.MonoidalClosed C] → Prop
-- Mathlib.Tactic.IntervalCases
/-- `interval_cases n` searches for upper and lower bounds on a variable `n`,
and if bounds are found,
splits into separate cases for each possible value of `n`.

As an example, in
```
example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 := by
  interval_cases n
  all_goals simp
```
after `interval_cases n`, the goals are `3 = 3 ∨ 3 = 4` and `4 = 3 ∨ 4 = 4`.

You can also explicitly specify a lower and upper bound to use,
as `interval_cases using hl, hu`.
The hypotheses should be in the form `hl : a ≤ n` and `hu : n < b`,
in which case `interval_cases` calls `fin_cases` on the resulting fact `n ∈ Set.Ico a b`.

You can specify a name `h` for the new hypothesis,
as `interval_cases h : n` or `interval_cases h : n using hl, hu`.
 -/
Mathlib.Tactic.intervalCases : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- A primitivity criterion  -/
SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} [Finite α],
  MulAction.IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s) →
    ∀ {g : M},
      s ∪ g • s ≠ ⊤ →
        MulAction.IsPreprimitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup M (s ∩ g • s))
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.id_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (X : B), (CategoryTheory.StrictPseudofunctor.id B).obj X = X
-- Mathlib.Topology.CompactOpen
ContinuousMap.hasBasis_nhds : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)),
  (nhds f).HasBasis
    (fun S => S.Finite ∧ ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ Set.MapsTo (⇑f) K U) fun x =>
    ⋂ KU ∈ x, {g | Set.MapsTo (⇑g) KU.1 KU.2}
-- Mathlib.Algebra.Group.Subgroup.Defs
HasMemOrNegMem.mem_or_neg_mem : ∀ {S : Type u_3} {G : Type u_4} {inst : Neg G} {inst_1 : SetLike S G} (s : S) [self : HasMemOrNegMem s] (a : G),
  a ∈ s ∨ -a ∈ s
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.smul : ∀ {α : Type u_1} {𝕜 : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7}
  [inst : SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} [inst_1 : SeminormedAddGroup 𝕜] [inst_2 : DistribSMul 𝕜 β]
  [IsBoundedSMul 𝕜 β],
  MeasureTheory.DominatedFinMeasAdditive μ T C →
    ∀ (c : 𝕜), MeasureTheory.DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal core of a subgroup `H` is the largest normal subgroup of `G` contained in `H`,
as shown by `Subgroup.normalCore_eq_iSup`.  -/
Subgroup.normalCore : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G
-- Mathlib.Order.CompleteLattice.PiLex
_private.Mathlib.Order.CompleteLattice.PiLex.0.Pi.Lex.isLUB_sSup : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun i => α i) i))}, IsLUB s (sSup s)
-- Mathlib.Algebra.Ring.Defs
/-- The canonical homomorphism `ℤ → R` for negative values is just the negation of the values
of the canonical homomorphism `ℕ → R`.  -/
Ring.intCast_negSucc : ∀ {R : Type u} [self : Ring R] (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitor_tensor_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom)
        h)
-- Init.Data.Array.MinMax
Array.min?_singleton_append : ∀ {α : Type u_1} {x : α} [inst : Min α] [Std.Associative min] {xs : Array α},
  (#[x] ++ xs).min? = some (xs.min?.elim x (min x))
-- Lean.MetavarContext
Lean.MetavarContext.getDelayedMVarAssignmentExp : Lean.MetavarContext → Lean.MVarId → Option Lean.DelayedMetavarAssignment
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.IsLocallyFull.mk : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D},
  (∀ {U V : C} (f : G.obj U ⟶ G.obj V), CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) ∈ K (G.obj U)) →
    G.IsLocallyFull K
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuous_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuous f ↔
    ∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_appTop : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens),
  AlgebraicGeometry.Scheme.Hom.appTop (f ∣_ U) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ⊤))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)
-- Mathlib.Data.Nat.Log
Nat.log.go.match_3.congr_eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (x x_1 : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (b fuel : ℕ) → motive b fuel.succ)
  (x_2 : ℕ),
  x = x_2 →
    x_1 = 0 →
      (match x, x_1 with
        | x, 0 => h_1 x
        | b, fuel.succ => h_2 b fuel) ≍
        h_1 x_2
-- Mathlib.RingTheory.Extension.Generators
/-- A hom between two families of generators gives
an algebra homomorphism between the polynomial rings.  -/
Algebra.Generators.Hom.toAlgHom : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {P : Algebra.Generators R S ι} →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst_3 : CommRing R'] →
                      [inst_4 : CommRing S'] →
                        [inst_5 : Algebra R' S'] →
                          {P' : Algebra.Generators R' S' ι'} →
                            [inst_6 : Algebra R R'] → [inst_7 : Algebra S S'] → P.Hom P' → P.Ring →ₐ[R] P'.Ring
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSMul' : {α : Type u} →
  {β : Type v} →
    {𝕜 : Type u_1} →
      [inst : NormedField 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : SeminormedAddCommGroup β] →
            [NormedSpace 𝕜 β] → SMul (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- `-2` is a square modulo an odd prime `p` iff `p` is congruent to `1` or `3` mod `8`.  -/
ZMod.exists_sq_eq_neg_two_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], p ≠ 2 → (IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
ContinuousMap.HomotopyEquiv.simplyConnectedSpace_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : ContinuousMap.HomotopyEquiv X Y), SimplyConnectedSpace X ↔ SimplyConnectedSpace Y
-- Mathlib.Computability.TuringMachine.Tape
/-- The "inclusive" right side of the tape, including both `right` and `head`.  -/
Turing.Tape.right₀ : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.Tape Γ → Turing.ListBlank Γ
-- Mathlib.Algebra.Order.Group.Cone
PartialOrder.mkOfGroupCone.eq_1 : ∀ {S : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : SetLike S G] (C : S) [inst_2 : GroupConeClass S G],
  PartialOrder.mkOfGroupCone C =
    { le := fun a b => b / a ∈ C, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- The full subcategory consisting of `t`-bounded above objects.  -/
CategoryTheory.Triangulated.TStructure.minus : {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] →
              CategoryTheory.Triangulated.TStructure C → CategoryTheory.ObjectProperty C
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.leftInverse_u_l : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisCoinsertion l u), Function.LeftInverse u l
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instLieRingModule : (R : Type u_1) →
  (L : Type u_2) →
    (M : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → LieRingModule L (LieDerivation R L M)
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.ParseResult.error.inj : ∀ {α ι : Type} {pos : ι} {err : Std.Internal.Parsec.Error} {pos_1 : ι} {err_1 : Std.Internal.Parsec.Error},
  Std.Internal.Parsec.ParseResult.error pos err = Std.Internal.Parsec.ParseResult.error pos_1 err_1 →
    pos = pos_1 ∧ err = err_1
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_sdiff_Ioo_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a < b → Finset.Ioc a b \ Finset.Ioo a b = {b}
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α], IsPiSystem (Set.range Set.Ioi)
-- Init.Prelude
instHOrOfOrOp : {α : Type u_1} → [OrOp α] → HOr α α α
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.eraseMin.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (size : ℕ) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size Ordnode.nil x r))
  (h_3 :
    (size sz : ℕ) →
      (l' : Ordnode α) →
        (y : α) →
          (r' : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size (Ordnode.node sz l' y r') x r)),
  (match Ordnode.nil with
    | Ordnode.nil => h_1 ()
    | Ordnode.node size Ordnode.nil x r => h_2 size x r
    | Ordnode.node size (Ordnode.node sz l' y r') x r => h_3 size sz l' y r' x r) =
    h_1 ()
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Composition of continuous linear maps, as a linear map. Compare `LinearMap.lcomp`.  -/
ContinuousLinearMap.lcomp : {R : Type u_1} →
  {U : Type u_2} →
    {V : Type u_3} →
      (W : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid U] →
            [inst_2 : Module R U] →
              [inst_3 : TopologicalSpace U] →
                [inst_4 : AddCommMonoid V] →
                  [inst_5 : Module R V] →
                    [inst_6 : TopologicalSpace V] →
                      [inst_7 : AddCommMonoid W] →
                        [inst_8 : Module R W] →
                          [inst_9 : TopologicalSpace W] →
                            [inst_10 : ContinuousAdd W] →
                              [inst_11 : ContinuousConstSMul R W] → (U →L[R] V) → (V →L[R] W) →ₗ[R] U →L[R] W
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.ultrametric_strict : ∀ {α : Type u_3} {S : Type u_4} [inst : LinearOrder S] [inst_1 : AddCommGroup α] (f : α → S),
  IsNonarchimedean f → (∀ (a : α), f a = f (-a)) → ∀ {a b : α}, f a ≠ f b → f (a + b) = max (f a) (f b)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget₂AddMon_obj_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C), CategoryTheory.AddMonObj.zero = CategoryTheory.AddMonObj.zero
-- Aesop.Frontend.Saturate
Aesop.Frontend.addLocalImplications : Aesop.LocalRuleSet → Aesop.ElabM Aesop.LocalRuleSet
-- Init.Data.Vector.Lemmas
Vector.insertIdx!.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ) (x : α),
  xs.insertIdx! i x =
    if x_1 : i ≤ n then xs.insertIdx i x x_1
    else
      have this := { default := xs.push x };
      panicWithPosWithDecl "Init.Data.Vector.Basic" "Vector.insertIdx!" 408 4 "index out of bounds"
-- Init.Data.List.Lemmas
List.map_tail? : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, Option.map (List.map f) l.tail? = (List.map f l).tail?
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
multipliable_nat_add_iff : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (k : ℕ),
  (Multipliable fun n => f (n + k)) ↔ Multipliable f
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.popWhile.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α),
  Array.popWhile p as = if h : as.size > 0 then if p as[as.size - 1] = true then Array.popWhile p as.pop else as else as
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.maxKey! ∈ t
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1NormedAddCommGroup : {R : Type u_3} →
  {M : Type u_4} →
    [inst : NormedRing R] →
      [inst_1 : NormedAddCommGroup M] →
        [inst_2 : Module R M] →
          [inst_3 : Module Rᵐᵒᵖ M] →
            [IsBoundedSMul R M] →
              [IsBoundedSMul Rᵐᵒᵖ M] → [SMulCommClass R Rᵐᵒᵖ M] → NormedAddCommGroup (TrivSqZeroExt R M)
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isSemisimple_neg : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, (-f).IsSemisimple ↔ f.IsSemisimple
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.modifyₘ : {α : Type u} →
  {β : Type v} →
    [BEq α] →
      [Hashable α] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → (β → β) → Std.DHashMap.Internal.Raw₀ α fun x => β
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.const.eq_def : ∀ (basis : Tactic.ComputeAsymptotics.Basis) (c : ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis c =
    match basis with
    | [] => Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal c
    | basis_hd :: basis_tl =>
      Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl c) fun x => c
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instLawfulBEqMon : LawfulBEq Lean.Grind.CommRing.Mon
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {i j : Fin (n + 1)},
      i ≠ j →
        ∀ {r : ℝ},
          r ∈ Set.Icc 0 1 →
            SignType.sign ((s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) r)) =
              SignType.sign ((s.signedInfDist j) (s.excenter signs))
-- Mathlib.RingTheory.PowerSeries.NoZeroDivisors
/-- The variable of the power series ring over an integral domain is irreducible.  -/
PowerSeries.X_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R], Irreducible PowerSeries.X
-- Mathlib.Order.Hom.Basic
/-- A preorder which embeds into a well-founded preorder is itself well-founded.  -/
OrderEmbedding.wellFoundedLT : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [WellFoundedLT β] (f : α ↪o β),
  WellFoundedLT α
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk'_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictPseudofunctorCore B C) {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g),
  (CategoryTheory.StrictPseudofunctor.mk' S).map₂ a_1 = S.map₂ a_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α}, Std.DHashMap.Internal.Raw₀.Const.get? m a = m.get? a
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.trans_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant A] (P P' : HomotopicalAlgebra.Cylinder A) [inst_3 : P'.IsGood],
  (P.trans P').π = CategoryTheory.Limits.pushout.desc P.π P'.π ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.apply_eq_true_of_lt_skipPrefixWhile_bool : ∀ {p : Char → Bool} {s : String} {pos : s.Pos} (h : pos < s.skipPrefixWhile p), p (pos.get ⋯) = true
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.submodule_map_reverse_eq_comap : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)),
  Submodule.map CliffordAlgebra.reverse p = Submodule.comap CliffordAlgebra.reverse p
-- Std.Time.Date.Unit.Month
Std.Time.Month.instAddOffset : Add Std.Time.Month.Offset
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.orbitProdStabilizerEquivGroup.eq_1 : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (b : X),
  MulAction.orbitProdStabilizerEquivGroup G b =
    ((MulAction.orbitEquivQuotientStabilizer G b).prodCongr (Equiv.refl ↥(MulAction.stabilizer G b))).trans
      Subgroup.groupEquivQuotientProdSubgroup.symm
-- Mathlib.Topology.Order.OrderClosed
instOrderClosedTopologyProd : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β], OrderClosedTopology (α × β)
-- Mathlib.MeasureTheory.Group.AEStabilizer
AddAction.aestabilizer.eq_1 : ∀ (G : Type u_1) {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α),
  AddAction.aestabilizer G μ s = { carrier := {g | g +ᵥ s =ᵐ[μ] s}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }