mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.map_comp : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {S : Type u_4}
  {T : Type u_5} [inst_3 : CommRing S] [inst_4 : CommRing T] (f : R →+* S) (g : S →+* T),
  Matrix.ProjGenLinGroup.map (g.comp f) = (Matrix.ProjGenLinGroup.map g).comp (Matrix.ProjGenLinGroup.map f)
-- Lean.Elab.DocString
/-- An expander for code blocks in docstrings.
 -/
Lean.Doc.DocCodeBlockExpander : Type
-- Mathlib.Order.SuccPred.Limit
Order.isPredLimitRecOn_of_isPredLimit : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  (isMax : (a : α) → IsMax a → motive a) (pred : (a : α) → ¬IsMin a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → motive a) (hb : Order.IsPredLimit b),
  Order.isPredLimitRecOn b isMax pred isPredLimit = isPredLimit b hb
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_submatrix_le : ∀ {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [inst : Semiring R] (A : Matrix m n R)
  (r : m₀ → m) (c : n₀ → n), (A.submatrix r c).eRank ≤ A.eRank
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_eq_of_eq : ∀ {a b : UInt32}, a = b → a.toBitVec = b.toBitVec
-- Mathlib.Data.EReal.Basic
EReal.coe_ne_top : ∀ (x : ℝ), ↑x ≠ ⊤
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheafCoconeOfSpecializes_ι_app : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C] {y : ↑X}
  (h : p₀ ⤳ y) (U : (TopologicalSpace.OpenNhds y)ᵒᵖ),
  (skyscraperPresheafCoconeOfSpecializes p₀ A h).ι.app U = CategoryTheory.eqToHom ⋯
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.mono_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb μb' : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb →
    μb.AbsolutelyContinuous μb' → MeasureTheory.Measure.QuasiMeasurePreserving f μa μb'
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.thinSkeletonPartialOrder : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [Quiver.IsThin C] → PartialOrder (CategoryTheory.ThinSkeleton C)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Cofix.dest_corec : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (g : α → F α) (x : α),
  (QPF.Cofix.corec g x).dest = QPF.Cofix.corec g <$> g x
-- Init.WF
WellFounded.apply : ∀ {α : Sort u} {r : α → α → Prop}, WellFounded r → ∀ (a : α), Acc r a
-- Mathlib.CategoryTheory.Opposites
/-- `Functor.leftOp` sends identity functors to the canonical isomorphism `unopUnop`.  -/
CategoryTheory.Functor.leftOpId : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (CategoryTheory.Functor.id Cᵒᵖ).leftOp ≅ CategoryTheory.unopUnop C
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprGrobnerConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Grind.GrobnerConfig
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.probReal_compl_eq_one_sub : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → μ.real sᶜ = 1 - μ.real s
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.add_assoc : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F ((x.add y).add z) (x.add (y.add z))
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.instSmallQuot : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] [Small.{w, u} J], Small.{w, max u w} (AddCommGrpCat.Colimits.Quot F)
-- Mathlib.Topology.Compactness.Compact
not_compactSpace_iff : ∀ {X : Type u} [inst : TopologicalSpace X], ¬CompactSpace X ↔ NoncompactSpace X
-- Init.Data.Bool
Bool.eq_true_imp_eq_false : ∀ {b : Bool}, b = true → b = false ↔ b = false
-- Init.Data.BitVec.Basic
/-- Signed division for bitvectors using the SMT-LIB using the
[SMT-LIB convention](http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml),
where division by zero returns `BitVector.allOnes n`.

Specifically, `x.smtSDiv 0 = if x >= 0 then -1 else 1`

SMT-LIB name: `bvsdiv`.
 -/
BitVec.smtSDiv : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.scalarRestriction_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.MonObj A] [inst_5 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsMonHom f] (M : D) [inst_7 : CategoryTheory.ModObj B M],
  CategoryTheory.ModObj.smul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M)
      CategoryTheory.ModObj.smul
-- Mathlib.NumberTheory.Padics.PadicNumbers
_private.Mathlib.NumberTheory.Padics.PadicNumbers.0.Padic.div_nat_pos : ∀ (n : ℕ), 0 < 1 / (↑n + 1)
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsFinite f],
  AlgebraicGeometry.IsFinite (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.cast_addConst : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.addConst B) = ↑(A + B).card / ↑A.card
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.instDecidableRelAdjAddCayleyOfDecidableEqOfDecidablePredMemSet : {M : Type u_1} →
  (s : Set M) →
    [inst : AddGroup M] → [DecidableEq M] → [DecidablePred fun x => x ∈ s] → DecidableRel (SimpleGraph.addCayley s).Adj
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_update_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) [inst_5 : DecidableEq ι]
  (m : ι → M) (i : ι), f (Function.update m i 0) = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_inter_subset : ∀ {α : Type u_2} [inst : Add α] {s t₁ t₂ : Set α}, s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)
-- Mathlib.Analysis.Normed.Module.Basic
instNormedAddCommGroupRestrictScalars : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} → {E : Type u_3} → [I : NormedAddCommGroup E] → NormedAddCommGroup (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `Fin n ⥤ Fin (n + 1)` which sends `i` to `i.castSucc`.  -/
Fin.castSuccFunctor : (n : ℕ) → CategoryTheory.Functor (Fin n) (Fin (n + 1))
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResultCore.subgoal.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (numNewEqs : ℕ),
  sizeOf (Lean.Meta.InjectionResultCore.subgoal mvarId numNewEqs) = 1 + sizeOf mvarId + sizeOf numNewEqs
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- This is a more convenient formulation to show that a `CokernelCofork` of the form
`CokernelCofork.ofπ p _` is a colimit cocone when we know that `p` is an epimorphism.  -/
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y Q : C} →
        {f : X ⟶ Y} →
          (p : Y ⟶ Q) →
            (w : CategoryTheory.CategoryStruct.comp f p = 0) →
              ({A : C} →
                  (k : Y ⟶ A) →
                    CategoryTheory.CategoryStruct.comp f k = 0 → { l // CategoryTheory.CategoryStruct.comp p l = k }) →
                [hp : CategoryTheory.Epi p] →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p w)
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.eventualRange_eq_range_precomp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j k : J}
  (f : i ⟶ j) (g : j ⟶ k),
  F.eventualRange k = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map g)) →
    F.eventualRange k =
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp f g)))
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def'_norm_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (e : Int.Internal.Linear.Expr) (ePoly ePoly' p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_def'_norm_cert x e ePoly ePoly' p =
    (ePoly.beq' e.norm).and' (p.beq' (Int.Internal.Linear.Poly.add (-1) x ePoly'))
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- Type synonym for a preorder equipped with the upper set topology.  -/
Topology.WithUpperSet : Type u_4 → Type u_4
-- Mathlib.Topology.Bases
TopologicalSpace.SecondCountableTopology.to_firstCountableTopology : ∀ (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α], FirstCountableTopology α
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.rank_pow_quot : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [hfp : NeZero (p.ramificationIdx' P)] [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime],
  P ≠ ⊥ →
    ∀ i ≤ p.ramificationIdx' P,
      Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ i)) =
        (p.ramificationIdx' P - i) • Module.rank (R ⧸ p) (S ⧸ P)
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.mk.sizeOf_spec : ∀ (declName oldArg : Lean.Name) (newArg? : Option Lean.Name) (text? since? : Option String),
  sizeOf { declName := declName, oldArg := oldArg, newArg? := newArg?, text? := text?, since? := since? } =
    1 + sizeOf declName + sizeOf oldArg + sizeOf newArg? + sizeOf text? + sizeOf since?
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- If `β` is finite, then `unconditional β` is the only summation filter `L` on `β` satisfying
`L.LeAtTop` and `L.NeBot`.  -/
SummationFilter.eq_unconditional_of_finite : ∀ {β : Type u_4} [Finite β] (L : SummationFilter β) [L.LeAtTop] [L.NeBot], L = SummationFilter.unconditional β
-- Mathlib.Analysis.Calculus.FDeriv.Defs
hasStrictFDerivAt_iff_isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x ↔ (fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.inductionOn : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {motive : Std.ExtDTreeMap α β cmp → Prop}
  (t : Std.ExtDTreeMap α β cmp), (∀ (a : Std.DTreeMap α β cmp), motive (Std.ExtDTreeMap.mk a)) → motive t
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate : ∀ {ι : Type u_1} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal}
  {r : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I}, l.MemBaseSet I c r π → π.IsSubordinate r
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.toAlternatingMap_alternatizeUncurryFin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F),
  (ContinuousAlternatingMap.alternatizeUncurryFin f).toAlternatingMap =
    AlternatingMap.alternatizeUncurryFin (ContinuousAlternatingMap.toAlternatingMapLinear ∘ₗ ↑f)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.right_unitality_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.OplaxMonoidal] (X : C) {Z : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv h =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.η F)) h))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
fderiv_csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → fderiv ℂ (fun x => Complex.sin (f x)) x = Complex.cos (f x) • fderiv ℂ f x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelp.mk.inj : ∀ {signatures : Array Lean.Lsp.SignatureInformation} {activeSignature? activeParameter? : Option ℕ}
  {signatures_1 : Array Lean.Lsp.SignatureInformation} {activeSignature?_1 activeParameter?_1 : Option ℕ},
  { signatures := signatures, activeSignature? := activeSignature?, activeParameter? := activeParameter? } =
      { signatures := signatures_1, activeSignature? := activeSignature?_1, activeParameter? := activeParameter?_1 } →
    signatures = signatures_1 ∧ activeSignature? = activeSignature?_1 ∧ activeParameter? = activeParameter?_1
-- Mathlib.Data.Int.Cast.Defs
AddCommGroupWithOne.toAddCommMonoidWithOne : {R : Type u} → [self : AddCommGroupWithOne R] → AddCommMonoidWithOne R
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- A 2-cell in `CatEnrichedOrdinary C` has a corresponding "base" 2-cell in `CatEnriched C`.  -/
CategoryTheory.CatEnrichedOrdinary.Hom.base : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {X Y : CategoryTheory.CatEnrichedOrdinary C} →
        {f g : X ⟶ Y} →
          (f ⟶ g) → (CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- Let `f : β → α` be a multipliable function and let `b ∈ β` be an index.
Lemma `tprod_eq_mul_tprod_ite` writes `∏ n, f n` as `f b` times the product of the
remaining terms.  -/
Multipliable.tprod_eq_mul_tprod_ite : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  [T2Space α] [inst_4 : DecidableEq β],
  Multipliable f → ∀ (b : β), ∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n
-- Init.Data.List.MapIdx
List.length_mapIdx_go : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {l : List α} {acc : Array β},
  (List.mapIdx.go f l acc).length = l.length + acc.size
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_linearCombination_left : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (f : ι →₀ R) (i : ι),
  (b.toDual ((Finsupp.linearCombination R ⇑b) f)) (b i) = f i
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_lt_fib_succ : ∀ {n : ℕ}, 2 ≤ n → Nat.fib n < Nat.fib (n + 1)
-- Mathlib.Tactic.NormNum.Core
/-- A `Methods` implementation which calls `norm_num`.  -/
Mathlib.Meta.NormNum.methods : optParam Bool true → Lean.Meta.Simp.Methods
-- Batteries.Data.Float.Basic
/-- The floating point value "not a number", used to represent erroneous numerical computations
such as `0 / 0`. Using `nan` in any float operation will return `nan`, and all comparisons
involving `nan` return `false`, including in particular `nan == nan`.
 -/
Float.nan : Float
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.minpoly_gen : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  minpoly F (IntermediateField.AdjoinSimple.gen F α) = minpoly F α
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivLM.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (n k : ℕ∞) {K : TopologicalSpace.Compacts E},
  ContDiffMapSupportedIn.fderivLM 𝕜 n k =
    { toFun := fun f => if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0, map_add' := ⋯,
      map_smul' := ⋯ }
-- Init.Data.Vector.Extract
Vector.extract_push : ∀ {n : ℕ} {α : Type u_1} {xs : Vector α n} {b : α} {start stop : ℕ},
  (xs.push b).extract start stop =
    if h₁ : stop ≤ n then Vector.cast ⋯ (xs.extract start stop)
    else if h₂ : start ≤ n then Vector.cast ⋯ ((xs.extract start).push b) else Vector.cast ⋯ #v[]
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Ioc_sdiff_Ioi`. -/
Set.Ioc_diff_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a b \ Set.Ioi c = Set.Ioc a (min b c)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_inter_ground_eq : ∀ {α : Type u_1} (M : Matroid α) (D : Set α), M.delete (D ∩ M.E) = M.delete D
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.underlyingIso_top_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C},
  (CategoryTheory.Subobject.underlyingIso (CategoryTheory.CategoryStruct.id B)).hom = ⊤.arrow
-- Mathlib.Order.Heyting.Basic
IsCompl.hnot_eq : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, IsCompl a b → ￢a = b
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Equiv.toHom_range : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.toHom.range = ⊤
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.productive_congr : ∀ {α : Type u} {s t : Stream'.WSeq α}, s ~ʷ t → (s.Productive ↔ t.Productive)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
/-- We say that a morphism `f : X ⟶ Y` is locally quasi finite if `Γ(Y, U) ⟶ Γ(X, V)` is
quasi-finite (in the mathlib sense) for every pair of affine opens that `f` maps one into the other.

Note that this does not require `f` to be quasi-compact nor locally of finite type.

Being locally quasi-finite implies that `f` has discrete fibers
(via `f.isDiscrete_preimage_singleton`).
The converse holds under various scenarios:

- `locallyQuasiFinite_iff_isDiscrete_preimage_singleton`:
  If `f` is quasi-compact, this is equivalent to `f ⁻¹ {x}` being `κ(x)`-finite for all `x`.
- `locallyQuasiFinite_iff_isDiscrete_preimage_singleton`:
  If `f` is locally of finite type, this is equivalent to `f` having discrete fibers.
- `locallyQuasiFinite_iff_finite_preimage_singleton`:
  If `f` is of finite type, this is equivalent to `f` having finite fibers.
 -/
AlgebraicGeometry.LocallyQuasiFinite : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Init.Data.String.Defs
/-- The proof that `offset` is valid for the string slice `s`.  -/
String.Slice.Pos.isValidForSlice : ∀ {s : String.Slice} (self : s.Pos), String.Pos.Raw.IsValidForSlice s self.offset
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.natCast_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, (↑n).comp p = ↑n
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheckSite.decl.injEq : ∀ (name name_1 : Lean.Name),
  (Lean.Doc.DeferredCheckSite.decl name = Lean.Doc.DeferredCheckSite.decl name_1) = (name = name_1)
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.isClopen_closedBall`.

---

For any valuation `v` compatible with the valuative relation on `R`, the closed `r`-ball
around zero `{x | v.restrict x ≤ r}` is clopen in the valuative topology.  -/
IsValuativeTopology.isClopen_closedBall : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  {r : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, r ≠ 0 → IsClopen {x | v.restrict x ≤ r}
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for the `positivity` tactic: `Nat.cast` is always non-negative,
and positive when its input is.  -/
Mathlib.Meta.Positivity.evalNatCast : Mathlib.Meta.Positivity.PositivityExt
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.instInhabitedTerminationMeasure : Inhabited Lean.Elab.TerminationMeasure
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumCongr_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13} [inst_8 : TopologicalSpace M']
  [inst_9 : ChartedSpace H M'] {N : Type u_15} [inst_10 : TopologicalSpace N] [inst_11 : ChartedSpace H N]
  {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [inst_12 : TopologicalSpace N'] [inst_13 : ChartedSpace H N']
  (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n), ⇑(φ.sumCongr ψ) = Sum.map ⇑φ ⇑ψ
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj.hasMap : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : 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_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃],
  ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj
        X₃).HasMap
    r
-- Mathlib.Tactic.ModCases
/-- Proves an expression of the form `OnModCases n a b p` where `n` and `b` are raw nat literals
and `b ≤ n`. Returns the list of subgoals `?gi : a ≡ i [MOD n] → p`.
 -/
Mathlib.Tactic.ModCases.NatMod.proveOnModCases : {u : Lean.Level} →
  (n a b : Q(ℕ)) →
    (p : Q(Sort u)) → Lean.MetaM (Q(Mathlib.Tactic.ModCases.NatMod.OnModCases «$n» «$a» «$b» «$p») × List Lean.MVarId)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.mk.inj : ∀
  {trueExpr falseExpr natZExpr btrueExpr bfalseExpr ordEqExpr intExpr trueExpr_1 falseExpr_1 natZExpr_1 btrueExpr_1
    bfalseExpr_1 ordEqExpr_1 intExpr_1 : Lean.Expr},
  { trueExpr := trueExpr, falseExpr := falseExpr, natZExpr := natZExpr, btrueExpr := btrueExpr,
        bfalseExpr := bfalseExpr, ordEqExpr := ordEqExpr, intExpr := intExpr } =
      { trueExpr := trueExpr_1, falseExpr := falseExpr_1, natZExpr := natZExpr_1, btrueExpr := btrueExpr_1,
        bfalseExpr := bfalseExpr_1, ordEqExpr := ordEqExpr_1, intExpr := intExpr_1 } →
    trueExpr = trueExpr_1 ∧
      falseExpr = falseExpr_1 ∧
        natZExpr = natZExpr_1 ∧
          btrueExpr = btrueExpr_1 ∧ bfalseExpr = bfalseExpr_1 ∧ ordEqExpr = ordEqExpr_1 ∧ intExpr = intExpr_1