mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- An isomorphism is an open immersion.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (H : X ≅ Y),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion H.hom
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.idemFst_add_idemSnd : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] {p : ENNReal},
  WithLp.idemFst + WithLp.idemSnd = 1
-- Mathlib.NumberTheory.Ostrowski
Rat.AbsoluteValue.padic_le_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (n : ℤ), (Rat.AbsoluteValue.padic p) ↑n ≤ 1
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- **Suslin's Theorem**: in a Hausdorff topological space, an analytic set with an analytic
complement is measurable.  -/
MeasureTheory.AnalyticSet.measurableSet_of_compl : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] [inst_2 : MeasurableSpace α] [OpensMeasurableSpace α]
  {s : Set α}, MeasureTheory.AnalyticSet s → MeasureTheory.AnalyticSet sᶜ → MeasurableSet s
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_eq : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → F'}
  [inst_3 : CompleteSpace F'] (hf : MeasureTheory.Integrable f μ),
  MeasureTheory.condExpL1 hm μ f = (MeasureTheory.condExpL1CLM F' hm μ) (MeasureTheory.Integrable.toL1 f hf)
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Submodule.AssociatePrimes.mem_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {I : Ideal R}, I ∈ N.associatedPrimes ↔ N.IsAssociatedPrime I
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instCartesianMonoidalCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Grp.instCartesianMonoidalCategory =
    { toMonoidalCategory := CategoryTheory.Grp.instMonoidalCategory,
      isTerminalTensorUnit :=
        CategoryTheory.Limits.IsTerminal.ofUniqueHom
          (fun G => CategoryTheory.Grp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.toUnit G.toMon)) ⋯,
      fst := fun G H => CategoryTheory.Grp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.fst G.toMon H.toMon),
      snd := fun G H => CategoryTheory.Grp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.snd G.toMon H.toMon),
      fst_def := ⋯, snd_def := ⋯,
      tensorProductIsBinaryProduct := fun G H =>
        CategoryTheory.Limits.BinaryFan.IsLimit.mk
          (CategoryTheory.Limits.BinaryFan.mk
            (CategoryTheory.Grp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.fst G.toMon H.toMon))
            (CategoryTheory.Grp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.snd G.toMon H.toMon)))
          (fun {T} f g => { hom := CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom }) ⋯ ⋯ ⋯ }
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f pf x r → HasFPowerSeriesOnBall (-f) (-pf) x r
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.instNontrivialDual : ∀ (K : Type uK) {V : Type uV} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V] [Nontrivial V], Nontrivial (Module.Dual K V)
-- Mathlib.Topology.PartialHomeomorph.Basic
Set.partialHomeomorphSubtypeCoe_target : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X) (hs : Nonempty ↑s),
  (s.partialHomeomorphSubtypeCoe hs).target = s
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.isUnit_add_one : ∀ {R : Type u_1} [inst : Ring R] {r : R}, IsNilpotent r → IsUnit (r + 1)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.not_rev : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool},
  FreeAddGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
-- Init.Data.UInt.Lemmas
UInt16.toNat_mod_uSizeSize : ∀ (n : UInt16), n.toNat % USize.size = n.toNat
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.List.toArrayAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (xs : Array α) (h_1 : (xs : Array α) → motive [] xs)
  (h_2 : (a : α) → (as : List α) → (xs : Array α) → motive (a :: as) xs),
  (match [], xs with
    | [], xs => h_1 xs
    | a :: as, xs => h_2 a as xs) =
    h_1 xs
-- Mathlib.GroupTheory.Perm.List
List.formPerm_rotate : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (n : ℕ), (l.rotate n).formPerm = l.formPerm
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The operation `of` is natural.  -/
CategoryTheory.FreeGroupoid.ofCompMapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        (F : CategoryTheory.Functor C D) →
          (CategoryTheory.FreeGroupoid.of C).comp (CategoryTheory.FreeGroupoid.map F) ≅
            F.comp (CategoryTheory.FreeGroupoid.of D)
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_toReal_le : ∀ {a : ENNReal}, ENNReal.ofReal a.toReal ≤ a
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_sub : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : SubNegZeroMonoid α] (d₁ d₂ : n → α),
  Matrix.diagonal d₁ - Matrix.diagonal d₂ = Matrix.diagonal fun i => d₁ i - d₂ i
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- Pushforwards of submodules along a `LinearEquiv` have the same dimension.  -/
LinearEquiv.rank_map_eq : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (f : M ≃ₗ[R] M₁) (p : Submodule R M),
  Module.rank R ↥(Submodule.map (↑f) p) = Module.rank R ↥p
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
MonoidAlgebra.instHopfAlgebraStruct.eq_1 : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (G : Type u_3)
  [inst_3 : Group G],
  MonoidAlgebra.instHopfAlgebraStruct R A G =
    { toBialgebra := MonoidAlgebra.instBialgebra R A G,
      antipode :=
        ((Finsupp.lsum R) fun g => MonoidAlgebra.lsingle g⁻¹ ∘ₗ HopfAlgebraStruct.antipode R) ∘ₗ
          ↑(MonoidAlgebra.coeffLinearEquiv R) }
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasure : ∀ {Ω : Type u_1} [inst : PseudoMetricSpace Ω] [inst_1 : MeasurableSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  [TopologicalSpace.SeparableSpace Ω], Continuous MeasureTheory.LevyProkhorov.ofMeasure
-- Mathlib.CategoryTheory.Shift.Opposite
/-- Given a `CommShift` structure on `F`, this is the corresponding `CommShift` structure on
`OppositeShift.functor F` (for the naive shifts on the opposite categories).
 -/
CategoryTheory.Functor.commShiftOp : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (A : Type u_3) →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift C A] →
              [inst_4 : CategoryTheory.HasShift D A] →
                (F : CategoryTheory.Functor C D) →
                  [F.CommShift A] → (CategoryTheory.OppositeShift.functor A F).CommShift A
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point.0.termX : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_alter_eq_add_one : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∉ m → (f (Std.ExtDHashMap.Const.get? m k)).isSome = true → (Std.ExtDHashMap.Const.alter m k f).size = m.size + 1
-- Init.Data.String.Modify
/-- Given a valid position in a string, obtain the corresponding position after modifying a character
in that string, provided that the position was before the changed position.  -/
String.Pos.toModifyOfLE : {s : String} → (q p : s.Pos) → (f : Char → Char) → (hp : p ≠ s.endPos) → q ≤ p → (p.modify f hp).Pos
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Raw.filterMap f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Raw.Const.get t x ⋯)).isSome).getD fallback
-- Lean.MetavarContext
/-- Return the local declaration of the free variable `x` in `xs` with the smallest index  -/
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.getLocalDeclWithSmallestIdx : Lean.LocalContext → Array Lean.Expr → Lean.LocalDecl
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.ArrayStxBuilder.mkNode : Lean.Elab.Term.Quotation.ArrayStxBuilder → Lean.SyntaxNodeKind → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Order.SuccPred.WithBot
/-- Not to be confused with `WithTop.orderPred_top`, which is about `Order.pred`.  -/
WithTop.pred_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α], ⊤.pred = ⊤
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toOplax_toPrelaxFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C), F.toOplax.toPrelaxFunctor = F.toPrelaxFunctor
-- Mathlib.Analysis.InnerProductSpace.Coalgebra
/-- A finite-dimensional inner product space with an algebra structure induces
a coalgebra, where comultiplication is given by the adjoint of multiplication
and the counit is given by the adjoint of the algebra map.

This is implemented by providing a linear equivalence between the inner product
space and an algebra.

See note [reducible non-instances].  -/
InnerProductSpace.coalgebraOfAlgebra : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          [FiniteDimensional 𝕜 E] →
            {A : Type u_3} →
              [inst_4 : Ring A] →
                [inst_5 : Module 𝕜 A] → [SMulCommClass 𝕜 A A] → [IsScalarTower 𝕜 A A] → (E ≃ₗ[𝕜] A) → Coalgebra 𝕜 E
-- Mathlib.Data.NNReal.Defs
Real.coe_nnabs : ∀ (x : ℝ), ↑(Real.nnabs x) = |x|
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.ExtendScalars.bracket_tmul : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] (s t : A) (x : L) (y : M),
  ⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ[R] ⁅x, y⁆
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformation.mk.sizeOf_spec : ∀ (label : Lean.Lsp.ParameterInformationLabel) (documentation? : Option Lean.Lsp.MarkupContent),
  sizeOf { label := label, documentation? := documentation? } = 1 + sizeOf label + sizeOf documentation?
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioi_zero : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M), ∑ i > 0, f i = ∑ j, f j.succ
-- Mathlib.Algebra.Ring.Defs
CommRing.toCommSemiring : {α : Type u} → [s : CommRing α] → CommSemiring α
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_le_lineMap_iff_of_lt' : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r r' : k},
  a < b → ((AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b) r' ↔ r ≤ r')
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- Check that `e` is definitionally equal to `𝟙_ C`.  -/
Mathlib.Tactic.Monoidal.id₁? : Lean.Expr → Mathlib.Tactic.Monoidal.MonoidalM (Option Mathlib.Tactic.BicategoryLike.Obj)
-- Mathlib.Order.RelIso.Basic
RelHom.id_comp : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s), (RelHom.id s).comp f = f
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_eq_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.dedup = 0 ↔ s = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (i : J.L) {Z : C} (h : d.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) h) =
    CategoryTheory.CategoryStruct.comp (I.fst i) (CategoryTheory.CategoryStruct.comp (d.inj (J.fst i)) h)
-- Init.Data.Rat.Lemmas
Rat.zpow_natCast : ∀ (q : ℚ) (n : ℕ), q ^ ↑n = q ^ n
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNat' : ∀ {n : ℕ}, (UInt32.ofNat n).toNat = n % 2 ^ 32
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.mk.inj : ∀ {α : Type} {producers : Std.Queue (IO.Promise Bool)}
  {consumers : Std.Queue (Std.CloseableChannel.Bounded.Consumer✝ α)} {capacity : ℕ}
  {buf : Vector (IO.Ref (Option α)) capacity} {bufCount sendIdx : ℕ} {hsend : sendIdx < capacity} {recvIdx : ℕ}
  {hrecv : recvIdx < capacity} {closed : Bool} {producers_1 : Std.Queue (IO.Promise Bool)}
  {consumers_1 : Std.Queue (Std.CloseableChannel.Bounded.Consumer✝ α)} {capacity_1 : ℕ}
  {buf_1 : Vector (IO.Ref (Option α)) capacity_1} {bufCount_1 sendIdx_1 : ℕ} {hsend_1 : sendIdx_1 < capacity_1}
  {recvIdx_1 : ℕ} {hrecv_1 : recvIdx_1 < capacity_1} {closed_1 : Bool},
  { producers := producers, consumers := consumers, capacity := capacity, buf := buf, bufCount := bufCount,
        sendIdx := sendIdx, hsend := hsend, recvIdx := recvIdx, hrecv := hrecv, closed := closed } =
      { producers := producers_1, consumers := consumers_1, capacity := capacity_1, buf := buf_1,
        bufCount := bufCount_1, sendIdx := sendIdx_1, hsend := hsend_1, recvIdx := recvIdx_1, hrecv := hrecv_1,
        closed := closed_1 } →
    producers = producers_1 ∧
      consumers = consumers_1 ∧
        capacity = capacity_1 ∧
          buf ≍ buf_1 ∧ bufCount = bufCount_1 ∧ sendIdx = sendIdx_1 ∧ recvIdx = recvIdx_1 ∧ closed = closed_1
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
/-- Each element of `GL(2, ℝ)⁺` defines a map of `C ^ n` manifolds `ℍ → ℍ`.  -/
UpperHalfPlane.contMDiff_smul : ∀ {n : WithTop ℕ∞} {g : GL (Fin 2) ℝ},
  0 < ↑(Matrix.GeneralLinearGroup.det g) →
    ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun τ => g • τ
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_inf : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M), ↑(N ⊓ N') = ↑N ∩ ↑N'
-- Init.PropLemmas
not_or : ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬q
-- Mathlib.AlgebraicGeometry.EllipticCurve.LFunction
/-- The local polynomial associated to a Weierstrass curve `W` over a nonarchimedean local field.
In the case of good reduction it is given by `1 - a T + q T ^ 2` where `q` is the cardinality of the
residue field `κ` and `a = q + 1 - |W(κ)|`. Note that `q` (and also `|W(κ)|`) is defined via
`Nat.card`, so `q` has junk value `0` when the residue field is infinite.  -/
WeierstrassCurve.localPolynomial : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} →
          [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → Polynomial ℤ
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The `m`-simplices of the `n`-th standard simplex are
the monotone maps from `Fin (m+1)` to `Fin (n+1)`.  -/
SSet.stdSimplex.asOrderHom : {n : ℕ} →
  {m : SimplexCategoryᵒᵖ} → (SSet.stdSimplex.obj { len := n }).obj m → Fin ((Opposite.unop m).len + 1) →o Fin (n + 1)
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.degree_list_sum_le : ∀ {S : Type u_1} [inst : Semiring S] (l : List (Polynomial S)), l.sum.degree ≤ (List.map Polynomial.natDegree l).maximum
-- Mathlib.Topology.Order.NhdsSet
/-- **Alias** of the reverse direction of `Ioi_mem_nhdsSet_Ici_iff`. -/
Ioi_mem_nhdsSet_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  a < b → Set.Ioi a ∈ nhdsSet (Set.Ici b)
-- Mathlib.Data.Fin.Tuple.Basic
/-- Recurse on an `n+1`-tuple by splitting it its initial `n`-tuple and its last element.  -/
Fin.snocCases : {n : ℕ} →
  {α : Fin (n + 1) → Sort u_1} →
    {motive : ((i : Fin n.succ) → α i) → Sort u_2} →
      ((xs : (i : Fin n) → α i.castSucc) → (x : α (Fin.last n)) → motive (Fin.snoc xs x)) →
        (x : (i : Fin n.succ) → α i) → motive x
-- Mathlib.Probability.Distributions.Pareto
/-- The Pareto pdf is positive for all reals `>= t`.  -/
ProbabilityTheory.paretoPDFReal_pos : ∀ {t r x : ℝ}, 0 < t → 0 < r → t ≤ x → 0 < ProbabilityTheory.paretoPDFReal t r x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toList_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  {f : α → β → Option γ},
  Std.DTreeMap.Const.toList (Std.DTreeMap.filterMap (fun k v => f k v) t) =
    List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DTreeMap.Const.toList t)
-- Mathlib.Topology.Order.OrderClosed
PredOrder.nhdsGE_eq_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] [PredOrder α] (a : α),
  nhdsWithin a (Set.Ici a) = nhds a
-- Batteries.Data.List.Lemmas
List.idxOfNth_eq_idxOfNth_iff : ∀ {α : Type u_1} {x : α} {n m : ℕ} [inst : BEq α] {xs : List α},
  List.idxOfNth x xs n = List.idxOfNth x xs m ↔ (List.count x xs ≤ m ∨ n ≤ m) ∧ (List.count x xs ≤ n ∨ m ≤ n)
-- Mathlib.Data.Fin.Tuple.Basic
/-- `cons` and `snoc` commute. We state this lemma in a non-dependent setting, as otherwise it
would involve a cast to convince Lean that the two types are equal, making it harder to use.  -/
Fin.cons_snoc_eq_snoc_cons : ∀ {n : ℕ} {β : Sort u_2} (a : β) (q : Fin n → β) (b : β), Fin.cons a (Fin.snoc q b) = Fin.snoc (Fin.cons a q) b
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCancelCommMonoid : {α : Type u_1} → [CancelCommMonoid α] → CancelCommMonoid αᵐᵒᵖ
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_insert_one : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Algebra.adjoin R (insert 1 s) = Algebra.adjoin R s
-- Init.Data.Nat.ToString
Nat.toDigits_of_lt_base : ∀ {b n : ℕ}, n < b → b.toDigits n = [n.digitChar]
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.derivative_U_eval_one : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ),
  3 * Polynomial.eval 1 (Polynomial.derivative (Polynomial.Chebyshev.U R n)) = (↑n + 2) * (↑n + 1) * ↑n
-- Mathlib.SetTheory.Ordinal.Notation
ONote.sub_nfBelow : ∀ {o₁ o₂ : ONote} {b : Ordinal.{0}}, o₁.NFBelow b → o₂.NF → (o₁ - o₂).NFBelow b
-- Mathlib.CategoryTheory.Limits.Cones
/-- Eta rule for cones.  -/
CategoryTheory.Limits.Cone.eta : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → (c : CategoryTheory.Limits.Cone F) → c ≅ { pt := c.pt, π := c.π }
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.comp_smul : ∀ {k : Type u} {G : Type v} [inst : CommSemiring k] [inst_1 : Monoid G] {M N O : Rep.{u_1, u, v} k G} (f : M ⟶ N)
  (r : k) (g : N ⟶ O), CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roc : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toArray[i]! = if i < (n - m).toNat then m + 1 + ↑i else 0
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqvAux.eq_def : ∀ {α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) (x : ℕ) (x_1 : x ≤ xs.size),
  xs.isEqvAux ys hsz p x x_1 =
    match x, x_1 with
    | 0, x => true
    | i.succ, h => p xs[i] ys[i] && xs.isEqvAux ys hsz p i ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.isoMk_inv : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  {Q : CategoryTheory.MorphismProperty C} [inst_2 : Q.IsMultiplicative] {F : CategoryTheory.Functor C D} {X : D}
  {A B : P.CostructuredArrow Q F X} (f : A.left ≅ B.left) (hf : Q f.hom) (hf' : Q f.inv)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f.hom) B.hom = A.hom)
      CategoryTheory.MorphismProperty.CostructuredArrow.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.CostructuredArrow.isoMk f hf hf' w).inv =
    CategoryTheory.MorphismProperty.CostructuredArrow.homMk f.inv hf' ⋯
-- Mathlib.Topology.Constructions
tendsto_subtype_rng : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_5} {p : X → Prop} {l : Filter Y} {f : Y → Subtype p}
  {x : Subtype p}, Filter.Tendsto f l (nhds x) ↔ Filter.Tendsto (fun x => ↑(f x)) l (nhds ↑x)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.comp_onTerm : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {L'' : FirstOrder.Language} (φ : L' →ᴸ L'')
  (ψ : L →ᴸ L'), (φ.comp ψ).onTerm = φ.onTerm ∘ ψ.onTerm
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt32HOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_of_le_one_right' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulLeftMono α] {a b : α}, b ≤ 1 → a * b ≤ a
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α), (a ::ₘ s).card = s.card + 1
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
/-- A morphism `f : X ⟶ Y` is quasi-finite at `x : X`
if the stalk map `𝒪_{X, x} ⟶ 𝒪_{Y, f x}` is quasi-finite.  -/
AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → ↥X → Prop
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrKey.mk.injEq : ∀ (relName head : Lean.Name) (arity : ℕ) (relName_1 head_1 : Lean.Name) (arity_1 : ℕ),
  ({ relName := relName, head := head, arity := arity } = { relName := relName_1, head := head_1, arity := arity_1 }) =
    (relName = relName_1 ∧ head = head_1 ∧ arity = arity_1)
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → Filter.map (↑e) (nhds x) = nhds (↑e x)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.mk.inj : ∀ {carrier : Type u} {str : Semigroup carrier} {carrier_1 : Type u} {str_1 : Semigroup carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Init.Data.BitVec.Bitblast
BitVec.cpopLayer.eq_def : ∀ {len w iterNum : ℕ} (oldLayer : BitVec (len * w)) (newLayer : BitVec (iterNum * w)) (hold : 2 * (iterNum - 1) < len),
  oldLayer.cpopLayer newLayer hold =
    if hlen : len - iterNum * 2 = 0 then
      have this := ⋯;
      BitVec.cast ⋯ newLayer
    else
      have op1 := BitVec.extractLsb' (2 * iterNum * w) w oldLayer;
      have op2 := BitVec.extractLsb' ((2 * iterNum + 1) * w) w oldLayer;
      have newLayer' := op1 + op2 ++ newLayer;
      have hcast := ⋯;
      oldLayer.cpopLayer (BitVec.cast hcast newLayer') ⋯