mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_eq_nnrpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (a : A),
  CFC.sqrt a = a ^ (1 / 2)
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P], P.InnerRegularWRT IsCompact IsClosed
-- Mathlib.Algebra.Category.Grp.Basic
/-- The forgetful functor from additive groups to additive monoids is fully faithful.  -/
AddGrpCat.fullyFaihtfulForget₂ToAddMonCat : (CategoryTheory.forget₂ AddGrpCat AddMonCat).FullyFaithful
-- Init.Data.Slice.Basic
Std.Slice.Self.eq : ∀ {α : Type u} {β : outParam (Type u)} [self : Std.Slice.Self α β], α = β
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
StarOrderedRing.nonneg_iff_quasispectrum_nonneg : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R A p]
  [NonnegSpectrumClass R A] (a : A),
  autoParam (p a) StarOrderedRing.nonneg_iff_quasispectrum_nonneg._auto_1 → (0 ≤ a ↔ ∀ x ∈ quasispectrum R a, 0 ≤ x)
-- Lean.Data.RArray
Lean.RArray.size.eq_def : ∀ {α : Type u} (x : Lean.RArray α),
  x.size =
    match x with
    | Lean.RArray.leaf a => 1
    | Lean.RArray.branch a l r => l.size + r.size
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_binomial_subset : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (k m : ℕ) (x y : R),
  (SkewPolynomial.C x * SkewPolynomial.X ^ k + SkewPolynomial.C y * SkewPolynomial.X ^ m).support ⊆ {k, m}
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_whiskerLeft_hom_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h k : c ⟶ d} (η : h ≅ k),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η.hom))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η.inv)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A skeleton and an open cell of a higher dimension are disjoint.  -/
Topology.RelCWComplex.disjoint_skeletonLT_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {m : ℕ} {j : Topology.RelCWComplex.cell C m},
  n ≤ ↑m → Disjoint (↑(Topology.RelCWComplex.skeletonLT C n)) (Topology.RelCWComplex.openCell m j)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.id_app : ∀ (X : SSet) (n : SimplexCategoryᵒᵖ),
  (CategoryTheory.CategoryStruct.id X).app n = CategoryTheory.CategoryStruct.id (X.obj n)
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.List.HashesTo.hash_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List ((a : α) × β a)} {i size : ℕ},
  Std.DHashMap.Internal.List.HashesTo l i size →
    ∀ (h : 0 < size), ∀ p ∈ l, (↑(Std.DHashMap.Internal.mkIdx size h (hash p.fst))).toNat = i
-- Mathlib.Topology.UniformSpace.HeineCantor
/-- Heine-Cantor: a continuous function on a compact uniform space is uniformly
continuous.  -/
CompactSpace.uniformContinuous_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] [CompactSpace α] {f : α → β},
  Continuous f → UniformContinuous f
-- Mathlib.Tactic.Linarith.Preprocessing
/-- If `e` is of the form `((n : ℕ) : C)`, `isNatCoe e` returns `⟨n, C⟩`.  -/
Mathlib.Tactic.Linarith.isNatCoe : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Lean.Elab.ConfigEval.Commands
/-- `def_eval_config_item f binders* for struct` defines a `ConfigEval.EvalConfigItem struct` structure named `f`
parameterized by the given binders. This structure contains a setter for updating a configuration
object of type `struct`.

The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr`
instances to support evaluation of configuration options for structure fields.
The syntax supports `public`/`private` modifiers. It also supports `scoped`/`local`, which apply
to any derived instances.

The `EvalConfigItem struct` structure can be customized with a `where` clause.
The possible items of the `where` clause are:
- `omit f1, f2, f3` disables generating setters for fields `f1`, `f2`, and `f3` of `struct`
- `option key := fun cfg item => ...` adds a configuration option named `key` with the given
expression as its handler. The handler is only called when the key is an exact match.
The provided value is in `item.value`. Such a handler implies `omit key`.
- `option key* := fun cfg item => ...` adds configuration options with `key` as a proper prefix.
The most-specific `*` handler is called if no handlers for exact matches apply.
 -/
Lean.Elab.ConfigEval.defEvalConfigItemCmd : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_one : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], ↑1 = 1
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFinitePresentation : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.LocallyOfFinitePresentation
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasStrictDerivAt_add_const_iff`. -/
HasStrictDerivAt.add_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => f x + c) f' x
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- If `f` is a morphism of `Arrow V` such that `f.right` is an isomorphism, then the image of `f`
in the right Freyd category is an epimorphism.  -/
CategoryTheory.Preadditive.RightFreyd.epi_of_isIso_right : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} (f : u ⟶ v) [CategoryTheory.IsIso (CategoryTheory.Arrow.Hom.right f)],
  CategoryTheory.Epi ((CategoryTheory.Preadditive.RightFreyd.quotient V).map f)
-- Mathlib.Logic.Equiv.Fin.Rotate
Fin.snoc_eq_cons_rotate : ∀ {n : ℕ} {α : Type u_1} (v : Fin n → α) (a : α), Fin.snoc v a = fun i => Fin.cons a v ((finRotate (n + 1)) i)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_self : ∀ (x : ℕ), x ||| x = x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
/-- Transfers the embedding of `x ↦ (x)ᵥ` of the number field `K` into its infinite adele
ring to the mixed embedding `x ↦ (φᵢ(x))ᵢ` of `K` into the space `ℝ ^ r₁ × ℂ ^ r₂`, where
`(r₁, r₂)` is the signature of `K` and `φᵢ` are the complex embeddings of `K`.  -/
NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp : ∀ (K : Type u_1) [inst : Field K] {x : K},
  (NumberField.mixedEmbedding K) x =
    (NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace K) ((algebraMap K (NumberField.InfiniteAdeleRing K)) x)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.decode_encode : ∀ {α : Type u} {inst : LE α} {inst_1 : LT α} {β : outParam (Type v)} {inst_2 : LE β} {inst_3 : LT β}
  {inst_4 : Std.PRange.UpwardEnumerable β} {inst_5 : Std.PRange.LawfulUpwardEnumerable β}
  {inst_6 : Std.PRange.LawfulUpwardEnumerableLE β} {inst_7 : Std.PRange.LawfulUpwardEnumerableLT β}
  [self : HasModel✝ α β] {x : α}, HasModel.decode✝ (HasModel.encode✝ x) = x
-- Mathlib.Topology.Sober
genericPoints.eq_1 : ∀ (α : Type u_1) [inst : TopologicalSpace α], genericPoints α = {x | closure {x} ∈ irreducibleComponents α}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Const.insertMany t l).getKey! k = t.getKey! k
-- Mathlib.RepresentationTheory.Coinduced
Rep.instIsRightAdjointCoindFunctor : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H),
  (Rep.coindFunctor k φ).IsRightAdjoint
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSum.match_1.splitter : {n m : ℕ} →
  (motive : Fin n ⊕ Fin m → Sort u_1) →
    (x : Fin n ⊕ Fin m) → ((x : Fin n) → motive (Sum.inl x)) → ((x : Fin m) → motive (Sum.inr x)) → motive x
-- Mathlib.LinearAlgebra.Orientation
/-- `some_basis` gives a basis with the required orientation.  -/
Orientation.someBasis_orientation : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : Nonempty ι]
  [inst_7 : DecidableEq ι] [inst_8 : FiniteDimensional R M] (x : Orientation R M ι)
  (h : Fintype.card ι = Module.finrank R M), (x.someBasis h).orientation = x
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.opEquivalence_inverse : CategoryTheory.RelCat.opEquivalence.inverse = CategoryTheory.RelCat.unopFunctor
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.RawView.mk.inj : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {tree : Std.DTreeMap.Internal.Impl α β} {k_1 : α} {v_1 : β k_1}
  {tree_1 : Std.DTreeMap.Internal.Impl α β},
  { k := k, v := v, tree := tree } = { k := k_1, v := v_1, tree := tree_1 } → k = k_1 ∧ v ≍ v_1 ∧ tree = tree_1
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.support_restriction : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), p.restriction.support = p.support
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.volume_face_mul : ∀ {n : ℕ} (i : Fin (n + 1)) (I : BoxIntegral.Box (Fin (n + 1))),
  (∏ j, ((I.face i).upper j - (I.face i).lower j)) * (I.upper i - I.lower i) = ∏ j, (I.upper j - I.lower j)
-- Init.Data.BitVec.Bitblast
BitVec.eq_iff_eq_of_inv : ∀ {α : Sort u_1} {w : ℕ} (f : α → BitVec w) (g : BitVec w → α),
  (∀ (x : α), g (f x) = x) → ∀ (x y : α), x = y ↔ f x = f y
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.ofHom_Y' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y) [inst_1 : W.ContainsIdentities], (CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).Y' = Y
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_inv : ∀ (x : ℝ), √x⁻¹ = (√x)⁻¹
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.autCongr_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₁ ≃ₐ[R] A₁),
  ϕ.autCongr ψ = ϕ.symm.trans (ψ.trans ϕ)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Suppose `a : X → Set A` is a continuous family of nonnegative elements.
Suppose further that `s : X → Set ℝ≥0` is a family of compact sets such that `s x₀` contains the
spectrum of `a x` for all sufficiently close `x`. If `f : ℝ≥0 → ℝ≥0` is continuous on each `s x`,
then `fun x ↦ cfc f (a x)` is continuous.  -/
Continuous.cfc_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_10 : TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A},
  Continuous a →
    (∀ (x : X), IsCompact (s x)) →
      (∀ (x₀ : X), ∀ᶠ (x : X) in nhds x₀, spectrum NNReal (a x) ⊆ s x₀) →
        autoParam (∀ (x : X), ContinuousOn f (s x)) Continuous.cfc_nnreal._auto_1 →
          autoParam (∀ (x : X), 0 ≤ a x) Continuous.cfc_nnreal._auto_3 → Continuous fun x => cfc f (a x)
-- Mathlib.Topology.Algebra.Group.Pointwise
singleton_add_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) {b : α},
  s ∈ nhds b → {a} + s ∈ nhds (a + b)
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
panicking if no such element exists.
 -/
Std.TreeSet.Raw.getLT! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet.Raw α cmp → α → α
-- Mathlib.GroupTheory.Sylow
Sylow.eq_top_of_zero : ∀ {G : Type u_1} [inst : Group G] (H : Sylow 0 G), ↑H = ⊤
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minEntry?_cons.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → (Unit → motive none) → ((w : (a : α) × β a) → motive (some w)) → motive x
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_eq_zero_of_forall_eq_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  (∀ x ∈ t, f x = 0) → ∫ᵛ (x : X) in t, f x ∂[B; μ] = 0
-- Mathlib.Control.Bitraversable.Instances
/-- The bitraverse function for `bicompr`.  -/
Bicompr.bitraverse : {t : Type u → Type u → Type u} →
  [Bitraversable t] →
    (F : Type u → Type u) →
      [Traversable F] →
        {m : Type u → Type u} →
          [Applicative m] →
            {α β α' β' : Type u} → (α → m β) → (α' → m β') → Function.bicompr F t α α' → m (Function.bicompr F t β β')
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instSetLike : {M : Type u_1} → [inst : Mul M] → SetLike (Subsemigroup M) M
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₀.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.L₀X₂ToP
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) h) =
    CategoryTheory.CategoryStruct.comp S.L₀.g h
-- Init.Data.Iterators.Basic
/-- This type is a wrapper around `IterM` so that it becomes a useful termination measure for
recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.finitelyManySteps`.
 -/
Std.IterM.TerminationMeasures.Finite : (α : Type w) → (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → Type w
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Coercion to a function as an `AddMonoidHom`. Similar to `AddMonoidHom.coeFn`.  -/
ContinuousMap.coeFnAddMonoidHom : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddMonoid β] → [inst_3 : ContinuousAdd β] → C(α, β) →+ α → β
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_prod_of_discrete_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} {x : α × β},
  ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 => f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1
-- Init.Data.SInt.Lemmas
Int8.ofNat_div : ∀ {a b : ℕ}, a < 2 ^ 7 → b < 2 ^ 7 → Int8.ofNat (a / b) = Int8.ofNat a / Int8.ofNat b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_7 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (len w start : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w)
  (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match len, Std.Tactic.BVDecide.BVExpr.extract start len expr with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_7 len w start expr
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.sub_closure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s : Set G},
  IsOpen s → ∀ (t : Set G), s - closure t = s - t
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.inr_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.map f g) =
    CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.map_id : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j},
  Ring.DirectLimit.map (fun x => RingHom.id (G x)) ⋯ = RingHom.id (Ring.DirectLimit G fun x x_1 h => ⇑(f x x_1 h))
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.mk.injEq : ∀ {α : Type} (values : Std.Queue α) (consumers : Std.Queue (Std.CloseableChannel.Consumer✝ α)) (closed : Bool)
  (values_1 : Std.Queue α) (consumers_1 : Std.Queue (Std.CloseableChannel.Consumer✝ α)) (closed_1 : Bool),
  ({ values := values, consumers := consumers, closed := closed } =
      { values := values_1, consumers := consumers_1, closed := closed_1 }) =
    (values = values_1 ∧ consumers = consumers_1 ∧ closed = closed_1)
-- Batteries.Classes.Order
Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] [inst_2 : DecidableLT α] [DecidableLE α] [inst_4 : DecidableEq α],
  (∀ (x : α), ¬x < x) →
    (∀ {x y z : α}, x < y → y < z → x < z) →
      (∀ {x y : α}, ¬x < y ↔ y ≤ x) →
        (∀ {x y : α}, x ≤ y → y ≤ x → x = y) → Std.LawfulCmp fun x1 x2 => compareOfLessAndEq x1 x2
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.isEmpty = true → m.getKey! a = default
-- Mathlib.Computability.Primrec.Basic
Primrec.sumInr : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec Sum.inr
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.map_mod : ∀ {R : Type u} {k : Type y} [inst : Field R] {p q : Polynomial R} [inst_1 : Field k] (f : R →+* k),
  Polynomial.map f (p % q) = Polynomial.map f p % Polynomial.map f q
-- Mathlib.GroupTheory.OrderOfElement
/-- This is the same as `IsOfFinAddOrder.addOrderOf_pos` but with one fewer explicit
assumption since this is automatic in case of a finite cancellative additive monoid.  -/
addOrderOf_pos : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [Finite G] (x : G), 0 < addOrderOf x
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.whisker_unit : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  (t : CategoryTheory.Bicategory.LeftExtension f g) {x : B} (h : c ⟶ x),
  (t.whisker h).unit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight t.unit h)
      (CategoryTheory.Bicategory.associator f t.extension h).hom
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.toEquiv_toHomeomorph : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  h.toHomeomorph.toEquiv = h.toEquiv
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux2.match_1.splitter : {α : Type u_1} →
  (motive : α ⊕ List (Computation α) → Sort u_2) →
    (o : α ⊕ List (Computation α)) →
      ((a : α) → motive (Sum.inl a)) → ((ls : List (Computation α)) → motive (Sum.inr ls)) → motive o
-- Mathlib.Data.Set.Card
Set.encard_singleton_inter : ∀ {α : Type u_1} (s : Set α) (x : α), ({x} ∩ s).encard ≤ 1
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.exists_away : ∀ (R : Type u_4) (S : Type u_5) {inst : CommSemiring R} {inst_1 : CommSemiring S} {inst_2 : Algebra R S}
  [self : Algebra.IsStandardOpenImmersion R S], ∃ r, IsLocalization.Away r S
-- Mathlib.GroupTheory.Commutator.Finite
instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet : ∀ {G : Type u_1} [inst : Group G] [Finite ↑(commutatorSet G)],
  Finite ↑(commutatorSet ↥(closureCommutatorRepresentatives G))
-- Init.Data.Int.DivMod.Lemmas
Int.mul_le_mul_left_of_neg : ∀ {a b c : ℤ}, a < 0 → (a * b ≤ a * c ↔ c ≤ b)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.openCell.eq_1 : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.openCell n i = ↑(Topology.RelCWComplex.map n i) '' Metric.ball 0 1