mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- To check that `η = traj κ a` it is enough to show that the restriction of `η` to variables `≤ b`
is `partialTraj κ a b`.  -/
ProbabilityTheory.Kernel.eq_traj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ}
  (η : ProbabilityTheory.Kernel ((i : ↥(Finset.Iic a)) → X ↑i) ((n : ℕ) → X n)),
  (∀ (b : ℕ), η.map (Preorder.frestrictLe b) = ProbabilityTheory.Kernel.partialTraj κ a b) →
    η = ProbabilityTheory.Kernel.traj κ a
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
_private.Std.Data.Iterators.Lemmas.Equivalence.Basic.0.Std.quotOfQuot.congr_simp : ∀ {α : Sort u_1} {R S : α → α → Prop} (h : ∀ (a b : α), R a b → S a b) (a a_1 : Quot R),
  a = a_1 → Std.quotOfQuot✝ h a = Std.quotOfQuot✝ h a_1
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- The adjunction `L ⊣ comonadicRightAdjoint L` given by `[ComonadicLeftAdjoint L]`.  -/
CategoryTheory.comonadicAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.ComonadicLeftAdjoint L] → L ⊣ CategoryTheory.comonadicRightAdjoint L
-- Mathlib.Data.Set.Lattice
Set.biInter_subset_biInter_left : ∀ {α : Type u_1} {β : Type u_2} {s s' : Set α} {t : α → Set β}, s' ⊆ s → ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.reciprocalFactors_one : DihedralGroup.reciprocalFactors 1 = []
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_singleton : ∀ {M : Type u_1} [inst : Zero M] (x : M) [inst_1 : DecidablePred fun x_1 => [x].getD x_1 0 ≠ 0],
  [x].toFinsupp = fun₀ | 0 => x
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (I : Type v) →
        [ℐ : CategoryTheory.SmallCategory I] →
          [hI : CategoryTheory.IsFiltered I] →
            (F : CategoryTheory.Functor I C) →
              (ι : F.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A) →
                CategoryTheory.Limits.IsColimit { pt := A, ι := ι } → CategoryTheory.Limits.IndObjectPresentation A
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
/-- Preprocess the goal to pass it to `Linarith.SimplexAlgorithm.findPositiveVector`.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.preprocess : (matType : ℕ → ℕ → Type) →
  [Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    (hyps : List Mathlib.Tactic.Linarith.Comp) → (maxVar : ℕ) → matType (maxVar + 1) hyps.length × List ℕ
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.orElse_OptionT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  (x : OptionT m α) (h : Unit → OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp x post (EPost.Cons.mk✝ (Std.Internal.Do.wp (h ()) post epost) epost.tail) ⦄ OrElse.orElse x h ⦃
    post; epost ⦄
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_toSubalgebra : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (s : Set A),
  (StarAlgebra.adjoin R s).toSubalgebra = Algebra.adjoin R (s ∪ star s)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_add_pure : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α] (a b : α),
  NonemptyInterval.pure a + NonemptyInterval.pure b = NonemptyInterval.pure (a + b)
-- Init.Data.Fin.Lemmas
Fin.sub_def : ∀ {n : ℕ} (a b : Fin n), a - b = ⟨(n - ↑b + ↑a) % n, ⋯⟩
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_erase_le_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → ∀ {fallback : α}, (cmp ((t.erase k).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true
-- Mathlib.GroupTheory.Coprod.Basic
/-- The minimal additive congruence relation `c` on `FreeAddMonoid (M ⊕ N)`
such that `FreeAddMonoid.of ∘ Sum.inl` and `FreeAddMonoid.of ∘ Sum.inr`
are additive monoid homomorphisms to the quotient by `c`.  -/
AddMonoid.coprodCon : (M : Type u_1) → (N : Type u_2) → [AddZeroClass M] → [AddZeroClass N] → AddCon (FreeAddMonoid (M ⊕ N))
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.restrictScalarsHom_apply : ∀ (R : Type u) {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A] (f : A ≃ₐ[S] A),
  (AlgEquiv.restrictScalarsHom R) f = AlgEquiv.restrictScalars R f
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.mul : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i}
  [inst_2 : (i : ι) → Mul (β i)] [∀ (i : ι), ContinuousMul (β i)],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyAdapted f v → MeasureTheory.StronglyAdapted f (u * v)
-- Mathlib.Order.BooleanAlgebra.Defs
/-- For any `a`, `b`, `(a ⊓ b) ⊓ (a / b) = ⊥`  -/
GeneralizedBooleanAlgebra.inf_inf_sdiff : ∀ {α : Type u} [self : GeneralizedBooleanAlgebra α] (a b : α), a ⊓ b ⊓ a \ b = ⊥
-- Mathlib.Topology.Sober
QuasiSober.sober : ∀ {α : Type u_3} {inst : TopologicalSpace α} [self : QuasiSober α] {S : Set α},
  IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Define a `Kernel α γ` from a `Kernel α (β × γ)` by taking the map of the second projection.
We use `mapOfMeasurable` for better defeqs.  -/
ProbabilityTheory.Kernel.snd : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} → ProbabilityTheory.Kernel α (β × γ) → ProbabilityTheory.Kernel α γ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.coe_toSubsemigroup_symm_apply : ∀ {A : Type u_5} [inst : Add A] (S : Subsemigroup (Multiplicative A)),
  ↑((RelIso.symm AddSubsemigroup.toSubsemigroup) S) = ⇑Multiplicative.ofAdd ⁻¹' ↑S
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Ric.toList_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Std.Rxc.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Ric α}, r.iter.toList = r.toList
-- Std.Net.Addr
Std.Net.MACAddr.mk.injEq : ∀ (octets octets_1 : Vector UInt8 6), ({ octets := octets } = { octets := octets_1 }) = (octets = octets_1)
-- Init.Data.Array.Lemmas
Array.ugetElem_eq_getElem : ∀ {α : Type u_1} {xs : Array α} {i : USize} (h : i.toNat < xs.size), xs[i] = xs[i.toNat]
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropEndWhile_eq_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String}, s.endsWith pat = false → s.dropEndWhile pat = s.toSlice
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Dep.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (D : Set α), M.Dep D = (¬M.Indep D ∧ D ⊆ M.E)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instPNatPowAssoc : PNatPowAssoc Complex.UnitDisc
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
/-- Summand in the sum to be bounded (`ℤ` version).  -/
HurwitzKernelBounds.f_int : ℕ → ℝ → ℝ → ℤ → ℝ
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.comp_id : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : CocompactMap α β),
  f.comp (CocompactMap.id α) = f
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
continuousAt_clog : ∀ {x : ℂ}, x ∈ Complex.slitPlane → ContinuousAt Complex.log x
-- Mathlib.Algebra.Algebra.Spectrum.Pi
isQuasiregular_prod_iff : ∀ {A : Type u_2} {B : Type u_3} [inst : NonUnitalSemiring A] [inst_1 : NonUnitalSemiring B] (a : A) (b : B),
  IsQuasiregular (a, b) ↔ IsQuasiregular a ∧ IsQuasiregular b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.cone_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g), h.cone.snd = snd
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The identity morphism of a short complex.  -/
CategoryTheory.ShortComplex.Hom.id : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → S.Hom S
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_curry_symm : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (V : Type u_9)
  (V₂ : Type u_10), ⇑(LinearEquiv.curry R M V V₂).symm = Function.uncurry
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsPathGraph3Compl.not_adj_fst : ∀ {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α}, G.IsPathGraph3Compl v w₁ w₂ → ¬G.Adj v w₁
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk_empty : ∀ {α : Type u_2} [inst : TopologicalSpace α], { carrier := ∅, is_open' := ⋯ } = ⊥
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual.eq_1 : ∀ {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),
  b.toDual = (b.constr ℕ) fun v => (b.constr ℕ) fun w => if w = v then 1 else 0
-- Mathlib.Logic.Nonempty
Nonempty.exists : ∀ {α : Sort u_3} {p : Nonempty α → Prop}, (∃ (h : Nonempty α), p h) ↔ ∃ a, p ⋯
-- Aesop.Stats.Basic
Aesop.ForwardStateStats.ruleStateStats : Aesop.ForwardStateStats → Array Aesop.ForwardRuleStateStats
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instT0Space : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)]
  [∀ (i : ι), T0Space (R i)], T0Space (RestrictedProduct (fun i => R i) (fun i => A i) 𝓕)
-- Mathlib.Logic.Function.Iterate
Pi.map_iterate : ∀ {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → α i → α i) (n : ℕ), (Pi.map f)^[n] = Pi.map fun i => (f i)^[n]
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.hom_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (β : Y ≅ X),
  α.hom = β.inv ↔ β.hom = α.inv
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldlM (fun d a x => f d a) init t = List.foldlM f init t.keys
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.prod.diag.match_1.splitter : (motive : (x : ℕ) → (x_1 : TypeVec.{u_1} x) → (x : Fin2 x) → x_1 x → Sort u_2) →
  (x : ℕ) →
    (x_1 : TypeVec.{u_1} x) →
      (x_2 : Fin2 x) →
        (x_3 : x_1 x_2) →
          ((n : ℕ) → (α : TypeVec.{u_1} n.succ) → (a : Fin2 n) → (x : α a.fs) → motive n.succ α a.fs x) →
            ((n : ℕ) → (x : TypeVec.{u_1} n.succ) → (x_4 : x Fin2.fz) → motive n.succ x Fin2.fz x_4) →
              motive x x_1 x_2 x_3
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.homMk_id : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) (S : 𝒮) (a : 𝒳)
  [inst_2 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) (CategoryTheory.CategoryStruct.id a)],
  CategoryTheory.Functor.Fiber.homMk p S (CategoryTheory.CategoryStruct.id a) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.Fiber.mk ⋯)
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDidOpenTextDocumentParams : Lean.Lsp.FileSource Lean.Lsp.DidOpenTextDocumentParams
-- Mathlib.Algebra.WithConv
WithConv.addEquiv_apply : ∀ (A : Type u_2) [inst : AddMonoid A] (self : WithConv A), (WithConv.addEquiv A) self = self.ofConv
-- Mathlib.Data.Multiset.Defs
/-- decidable equality for functions whose domain is bounded by multisets  -/
Multiset.decidableEqPiMultiset : {α : Type u_1} →
  {m : Multiset α} → {β : α → Type u_3} → [(a : α) → DecidableEq (β a)] → DecidableEq ((a : α) → a ∈ m → β a)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_mem_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, a ∈ m.insert k → (k == a) = false → a ∈ m
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.instDecidableEqValue.decEq : (x x_1 : Fin.Value✝) → Decidable (x = x_1)
-- Mathlib.Order.Cover
Eq.wcovBy : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b → a ⩿ b
-- Lean.Util.LeanOptions
Lean.LeanOptions.ofArray : Array Lean.LeanOption → Lean.LeanOptions
-- Mathlib.Order.Defs.Unbundled
UpperSet.mk.inj : ∀ {α : Type u_1} {inst : LE α} {carrier : Set α} {upper' : IsUpperSet carrier} {carrier_1 : Set α}
  {upper'_1 : IsUpperSet carrier_1},
  { carrier := carrier, upper' := upper' } = { carrier := carrier_1, upper' := upper'_1 } → carrier = carrier_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.snd_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [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] [inst_6 : AddTorsor V2 P2], AffineMap.snd.linear = LinearMap.snd k V1 V2
-- Init.Data.List.ToArray
List.zipWithMAux_toArray_succ' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u} {m : Type u → Type v} [inst : Monad m] (as : List α) (bs : List β)
  (f : α → β → m γ) (i : ℕ) (xs : Array γ),
  as.toArray.zipWithMAux bs.toArray f (i + 1) xs =
    (List.drop (i + 1) as).toArray.zipWithMAux (List.drop (i + 1) bs).toArray f 0 xs
-- Mathlib.Analysis.Calculus.BumpFunction.Convolution
/-- Special case of `ContDiffBump.convolution_tendsto_right` where `g` is continuous,
and the limit is taken only in the first function.  -/
ContDiffBump.convolution_tendsto_right_of_continuous : ∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace ℝ G]
  [CompleteSpace E'] [BorelSpace G] [inst_7 : FiniteDimensional ℝ G] [μ.IsAddHaarMeasure] {ι : Type u_1}
  {φ : ι → ContDiffBump 0} {l : Filter ι},
  Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
    Continuous g →
      ∀ (x₀ : G),
        Filter.Tendsto (fun i => MeasureTheory.convolution ((φ i).normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) l
          (nhds (g x₀))
-- Mathlib.Topology.LocallyConstant.Basic
/-- If α is finite, this constructs a locally constant function to `α → β` given a
family of locally constant functions with values in β indexed by α.  -/
LocallyConstant.unflip : {X : Type u_5} →
  {α : Type u_6} →
    {β : Type u_7} → [Finite α] → [inst : TopologicalSpace X] → (α → LocallyConstant X β) → LocallyConstant X (α → β)
-- Std.Time.Internal.UnitVal
/-- Adds two `UnitVal` values of the same ratio.
 -/
Std.Time.Internal.UnitVal.add : {α : ℚ} → Std.Time.Internal.UnitVal α → Std.Time.Internal.UnitVal α → Std.Time.Internal.UnitVal α
-- Init.Data.BitVec.Bitblast
BitVec.extractAndExtendAux.eq_1 : ∀ {w : ℕ} (k len : ℕ) (x : BitVec w) (acc : BitVec (k * len)) (hle : k ≤ w),
  BitVec.extractAndExtendAux k len x acc hle =
    match hwi : w - k with
    | 0 => BitVec.cast ⋯ acc
    | n'.succ =>
      have acc' := BitVec.extractAndExtendBit k len x ++ acc;
      BitVec.extractAndExtendAux (k + 1) len x (BitVec.cast ⋯ acc') ⋯
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.instIsCompleteAbs : CauSeq.IsComplete ℝ abs
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.equivPair_smul_same : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M),
  (Monoid.CoprodI.Word.equivPair i) (Monoid.CoprodI.of m • w) =
    { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := ((Monoid.CoprodI.Word.equivPair i) w).tail,
      fstIdx_ne := ⋯ }
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `f` is circle integrable and `g` is continuous on the circle `sphere c |R|`, then `f • g` is
circle integrable.
 -/
CircleIntegrable.smul_continuousOn : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → 𝕜} {g : ℂ → F},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (f • g) c R
-- Init.Prelude
/-- The list of macro scopes.  -/
Lean.MacroScopesView.scopes : Lean.MacroScopesView → List Lean.MacroScope
-- Mathlib.Topology.Order.OrderClosed
upperBounds_closure : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] (s : Set α),
  upperBounds (closure s) = upperBounds s
-- Mathlib.Data.String.Defs
/-- Construct the string consisting of `n` copies of the character `c`.  -/
String.replicate : ℕ → Char → String
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_eq_prime_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)], addOrderOf x = p ↔ p • x = 0 ∧ x ≠ 0
-- Mathlib.LinearAlgebra.Matrix.Defs
Set.matrix_eq_pi : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {S : Set α},
  S.matrix = ⇑Matrix.of.symm ⁻¹' Set.univ.pi fun x => Set.univ.pi fun x => S
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The map from `Ext X Y n` to a `ShiftedHom` type in the *constructed* derived
category given by `HasDerivedCategory.standard`: this definition is introduced
only in order to prove properties of the abelian group structure on `Ext`-groups.
Do not use this definition: use the more general `hom` instead.  -/
CategoryTheory.Abelian.Ext.hom' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          {n : ℕ} →
            CategoryTheory.Abelian.Ext X Y n →
              CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X)
                ((DerivedCategory.singleFunctor C 0).obj Y) ↑n
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiable_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'], MDiff Prod.fst
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ},
  f ∈ 𝒜 m →
    0 < m →
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f))
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatchThe : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α : Type u} {x : m α} {h : ε → m α}
  {Q : Std.Do.PostCond α ps} [inst : MonadExceptOf ε m] [inst_1 : Std.Do.WP m ps],
  (Std.Do.wp (tryCatchThe ε x h)).apply Q = (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.one_lt_prod_iff_of_one_le : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : PartialOrder N] {f : ι → N} {s : Finset ι}
  [MulLeftMono N], (∀ x ∈ s, 1 ≤ f x) → (1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x)
-- Batteries.Data.List.Lemmas
List.foldlIdx_eq_foldl_zipIdx : ∀ {α : Type u_1} {xs : List α} {α_1 : Type u_2} {f : ℕ → α_1 → α → α_1} {i : α_1} {s : ℕ},
  List.foldlIdx f i xs s = List.foldl (fun b ab => f ab.2 b ab.1) i (xs.zipIdx s)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_natAbs : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.C R ↑n.natAbs = Polynomial.Chebyshev.C R n
-- Mathlib.Tactic.Simproc.VecPerm
/-- Given a list `l` of elements of type `α` and a list `perm` of indices (as natural numbers), outputs
the list whose `i`th entry is `l[perm[i]]`.
In the case where `perm ~ [0, ..., l.length-1]`, this is just computing the permutation of `l`
represented by `perm`.
 -/
_private.Mathlib.Tactic.Simproc.VecPerm.0.Mathlib.Tactic.FinVec.permArray : {α : Type u_1} → [Inhabited α] → Array α → Array ℕ → Array α
-- Mathlib.Algebra.CharP.Defs
CharP.eq : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] {p q : ℕ}, CharP R p → CharP R q → p = q
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The carrier of `H ⊔ N` is just `↑H + ↑N` (pointwise set addition)
when `N` is normal.  -/
AddSubgroup.add_normal : ∀ {G : Type u_2} [inst : AddGroup G] (H N : AddSubgroup G) [hN : N.Normal], ↑(H ⊔ N) = ↑H + ↑N
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry : Type
-- Std.Data.String.ToNat
String.Slice.toNat?_congr : ∀ {s t : String.Slice}, s.copy = t.copy → s.toNat? = t.toNat?
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_diff_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Cofan.eq_of_inj_apply_eq_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {i₁ i₂ : C}
  (y₁ : F i₁) (y₂ : F i₂),
  (CategoryTheory.ConcreteCategory.hom (c.inj i₁)) y₁ = (CategoryTheory.ConcreteCategory.hom (c.inj i₂)) y₂ → i₁ = i₂
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_neg : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ↑↑(-f) =ᵐ[μ] -↑↑f
-- Init.Data.Range.Polymorphic.IntLemmas
Int.length_toList_roo : ∀ {a b : ℤ}, (a<...b).toList.length = (b - a - 1).toNat
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instCompleteSemilatticeInf.eq_1 : ∀ (M : Type u_1) [inst : MulOneClass M],
  SaturatedSubmonoid.instCompleteSemilatticeInf M =
    { toPartialOrder := SaturatedSubmonoid.instPartialOrder, toInfSet := SaturatedSubmonoid.instInfSet M,
      isGLB_sInf := ⋯ }
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.effectiveEpi_of_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.ReflectsEffectiveEpis] {X Y : C}
  (f : X ⟶ Y), CategoryTheory.EffectiveEpi (F.map f) → CategoryTheory.EffectiveEpi f