mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedId.eq_1 : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁],
  CategoryTheory.Enriched.FunctorCategory.enrichedId V F₁ =
    (CategoryTheory.Enriched.FunctorCategory.homEquiv V) (CategoryTheory.CategoryStruct.id F₁)
-- Mathlib.Analysis.Normed.Group.Constructions
pi_nnnorm_le_iff : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i}
  {r : NNReal}, ‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r
-- Mathlib.ModelTheory.ElementaryMaps
/-- The **Tarski-Vaught test** for elementarity of an embedding.  -/
FirstOrder.Language.Embedding.isElementary_of_exists : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N),
  (∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
      φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))) →
    ∀ {n : ℕ} (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x
-- Init.Data.UInt.Basic
instComplementUSize : Complement USize
-- Init.Core
PLift.up.injEq : ∀ {α : Sort u} (down down_1 : α), ({ down := down } = { down := down_1 }) = (down = down_1)
-- Mathlib.Algebra.Order.Hom.Basic
/-- `SubmultiplicativeHomClass F α β` states that `F` is a type of submultiplicative morphisms.  -/
SubmultiplicativeHomClass : (F : Type u_7) →
  (α : outParam (Type u_8)) → (β : outParam (Type u_9)) → [Mul α] → [Mul β] → [LE β] → [FunLike F α β] → Prop
-- Init.Data.Dyadic.Basic
Dyadic.mul_comm : ∀ (x y : Dyadic), x * y = y * x
-- Mathlib.Data.Set.Lattice
Set.mem_iUnion₂ : ∀ {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} {x : γ} {s : (i : ι) → κ i → Set γ},
  x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instAddLeftCancelSemigroup : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddLeftCancelSemigroup α] → AddLeftCancelSemigroup (Matrix m n α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryGE?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryGE? t₁ k = Std.DTreeMap.Raw.Const.getEntryGE? t₂ k
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValue?.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : List ((_ : α) × β) → Sort u_3) (k : α) (v : β) (l : List ((_ : α) × β))
  (h_1 : Unit → motive []) (h_2 : (k : α) → (v : β) → (l : List ((_ : α) × β)) → motive (⟨k, v⟩ :: l)),
  (match ⟨k, v⟩ :: l with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_2 k v l
-- Mathlib.Order.WithBot
WithBot.forall : ∀ {α : Type u_1} {p : WithBot α → Prop}, (∀ (x : WithBot α), p x) ↔ p ⊥ ∧ ∀ (x : α), p ↑x
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- Given `Φ : SuccStruct C` and an element `j : J` in a well-ordered type,
this is the unique element in `Φ.Iteration j`.  -/
CategoryTheory.SmallObject.SuccStruct.iter : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] → (j : J) → Φ.Iteration j
-- Lean.Util.LeanOptions
/-- Options that are used by Lean as if they were passed using `-D`.  -/
Lean.LeanOptions : Type
-- Mathlib.Algebra.Order.SuccPred.TypeTags
Order.succ_ofMul : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : SuccOrder X] (x : X),
  Order.succ (Additive.ofMul x) = Additive.ofMul (Order.succ x)
-- Mathlib.Analysis.Fourier.Notation
FourierModule.mk.inj : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} {inst : Add E} {inst_1 : Add F} {inst_2 : SMul R E}
  {inst_3 : SMul R F} {toFourierTransform : FourierTransform E F}
  {fourier_add :
    ∀ (f g : E), FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g}
  {fourier_smul : ∀ (r : R) (f : E), FourierTransform.fourier (r • f) = r • FourierTransform.fourier f}
  {toFourierTransform_1 : FourierTransform E F}
  {fourier_add_1 :
    ∀ (f g : E), FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g}
  {fourier_smul_1 : ∀ (r : R) (f : E), FourierTransform.fourier (r • f) = r • FourierTransform.fourier f},
  { toFourierTransform := toFourierTransform, fourier_add := fourier_add, fourier_smul := fourier_smul } =
      { toFourierTransform := toFourierTransform_1, fourier_add := fourier_add_1, fourier_smul := fourier_smul_1 } →
    toFourierTransform = toFourierTransform_1
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₁.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  HomologicalComplex.cylinder.ι₁ K =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (HomologicalComplex.homotopyCofiber.inr
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K)))
-- Init.System.IO
IO.TaskState.ofNat_ctorIdx : ∀ (x : IO.TaskState), IO.TaskState.ofNat x.ctorIdx = x
-- Mathlib.Analysis.Calculus.Deriv.ZPow
iter_deriv_inv_linear : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (k : ℕ) (c d : 𝕜),
  (deriv^[k] fun x => (c * x + d)⁻¹) = fun x => (-1) ^ k * ↑k.factorial * c ^ k * (c * x + d) ^ (-1 - ↑k)
-- Lean.Server.CodeActions.Basic
Lean.Server.CodeAction.getFileSource! : Lean.Lsp.CodeAction → Lean.Lsp.DocumentUri
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.HoldsForLocalizationAway`
if `P` holds for each localization map `R →+* Rᵣ`.  -/
RingHom.HoldsForLocalizationAway : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with negation.  -/
InnerProductSpace.laplacian_neg : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F},
  Laplacian.laplacian (-f) = -Laplacian.laplacian f
-- Mathlib.Order.WithBot
WithTop.trichotomous.gt : ∀ {α : Type u_1} [inst : Preorder α] [Std.Trichotomous fun x1 x2 => x1 > x2], Std.Trichotomous fun x1 x2 => x1 > x2
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 7 → (Int8.ofNat n).toNatClampNeg = n
-- Mathlib.Order.Category.PartOrd
PartOrd.instConcreteCategoryOrderHomCarrier : CategoryTheory.ConcreteCategory PartOrd fun x1 x2 => ↑x1 →o ↑x2
-- Mathlib.Analysis.Normed.Group.Defs
GroupNorm.toNormedCommGroup.eq_1 : ∀ {E : Type u_5} [inst : CommGroup E] (f : GroupNorm E),
  f.toNormedCommGroup =
    { toNorm := f.toNormedGroup.toNorm, toGroup := f.toNormedGroup.toGroup, mul_comm := ⋯,
      toMetricSpace := f.toNormedGroup.toMetricSpace, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.isEquivalencePreservesLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : CategoryTheory.Functor D C) [E.IsEquivalence],
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_aestronglyMeasurable : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν → ∀ᵐ (ω' : Ω') ∂ν, MeasureTheory.AEStronglyMeasurable X (κ ω')
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_left_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).left.as = PUnit.unit
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of the power of a function is the power of the trailing coefficient.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℤ} {f : 𝕜 → 𝕜},
  MeromorphicAt f x → meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.shrinkFunctorIsoFunctor_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (X_1 : Cᵒᵖ),
  S.shrinkFunctorIsoFunctor.inv.app X_1 = (CategoryTheory.shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.inv
-- Mathlib.Algebra.GroupWithZero.WithZero
MulEquiv.withZero_apply_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : Group β] (e : α ≃* β) (a : WithZero β),
  (MulEquiv.withZero e).symm a = (WithZero.map' ↑e.symm) a
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.coe_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M),
  ↑(AddSubmonoid.map f S) = ⇑f '' ↑S
-- Init.NotationExtra
/-- Step-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 -/
Lean.convCalc_ : Lean.ParserDescr
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.zmodeq_ofDigits_digits : ∀ (b b' : ℕ) (c : ℤ), ↑b' ≡ c [ZMOD ↑b] → ∀ (n : ℕ), ↑n ≡ Nat.ofDigits c (b'.digits n) [ZMOD ↑b]
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
image_comap_zeroLocus_eq_zeroLocus_comap : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f →
    ∀ (I : Ideal S), PrimeSpectrum.comap f '' PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)
-- Mathlib.Analysis.Convolution
MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd' : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd G] [MeasurableNeg G] {x : G},
  MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun t => x - t) μ) →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun t => (L (f (x - t))) (g t)) μ
-- Mathlib.Order.Monotone.Defs
instDecidableAntitoneOfForallForallForallLe : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → {f : α → β} → [i : Decidable (∀ (a b : α), a ≤ b → f b ≤ f a)] → Decidable (Antitone f)
-- Mathlib.Computability.Partrec
Partrec.of_eq : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α →. σ},
  Partrec f → (∀ (n : α), f n = g n) → Partrec g
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPNatLit : Lean.Options → Bool
-- Mathlib.Tactic.ComputeDegree
/-- `miscomputedDegree? deg false_goals` takes as input
* an `Expr`ession `deg`, representing the degree of a polynomial
  (i.e. an `Expr`ession of inferred type either `ℕ` or `WithBot ℕ`);
* a list of `MVarId`s `false_goals`.

Although inconsequential for this function, the list of goals `false_goals` reduces to `False`
if `norm_num`med.
`miscomputedDegree?` extracts error information from goals of the form
* `a ≠ b`, assuming it comes from `⊢ coeff_of_given_degree ≠ 0` —
  reducing to `False` means that the coefficient that was supposed to vanish, does not;
* `a ≤ b`, assuming it comes from `⊢ degree_of_subterm ≤ degree_of_polynomial` —
  reducing to `False` means that there is a term of degree that is apparently too large;
* `a = b`, assuming it comes from `⊢ computed_degree ≤ given_degree` —
  reducing to `False` means that there is a term of degree that is apparently too large.

The cases `a ≠ b` and `a = b` are not a perfect match with the top coefficient:
reducing to `False` is not exactly correlated with a coefficient being non-zero.
It does mean that `compute_degree` reduced the initial goal to an unprovable state
(unless there was already a contradiction in the initial hypotheses!), but it is indicative that
there may be some problem.
 -/
Mathlib.Tactic.ComputeDegree.miscomputedDegree? : Lean.Expr → List Lean.Expr → List Lean.MessageData
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `MonoidHom.pi`.

---

A family of monoid homomorphisms `f a : γ →* β a` defines a monoid homomorphism
`Pi.monoidHom f : γ →* Π a, β a` given by `Pi.monoidHom f x b = f b x`.  -/
Pi.monoidHom : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → MulOneClass (f i)] →
      {γ : Type w} → [inst_1 : MulOneClass γ] → ((i : I) → γ →* f i) → γ →* (i : I) → f i
-- Mathlib.Algebra.Order.Hom.Ring
/-- See Note [custom simps projection]  -/
OrderRingIso.Simps.symm_apply : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Mul α] →
      [inst_1 : Add α] → [inst_2 : LE α] → [inst_3 : Mul β] → [inst_4 : Add β] → [inst_5 : LE β] → α ≃+*o β → β → α
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Build the `apply` discrimination tree?  -/
Mathlib.Tactic.ClickSuggestions.Choice.app : Mathlib.Tactic.ClickSuggestions.Choice → Bool
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- The projection onto the quotient is a cokernel in the categorical sense.  -/
ModuleCat.cokernelIsColimit : {R : Type u} →
  [inst : Ring R] → {M N : ModuleCat R} → (f : M ⟶ N) → CategoryTheory.Limits.IsColimit (ModuleCat.cokernelCocone f)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- For an integer `n`, The equivalence between the elements of `integerSet K` of norm `n`
and the product of the set of nonzero principal ideals of `K` of norm `n` and the torsion of `K`.  -/
NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (n : ℕ) →
        { a // NumberField.mixedEmbedding.norm ↑a = ↑n } ≃
          { I // Submodule.IsPrincipal ↑I ∧ Ideal.absNorm ↑I = n } × ↥(NumberField.Units.torsion K)
-- Mathlib.Testing.Plausible.Functions
/-- Map a `TotalFunction` to one whose default value is zero so that it represents a `Finsupp`.  -/
Plausible.TotalFunction.zeroDefault : {α : Type u} → {β : Type v} → [Zero β] → Plausible.TotalFunction α β → Plausible.TotalFunction α β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey? = some k
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.commute_monodromyPerm_toPermFiber : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {g : G} {x : X}
  {γ : FundamentalGroup X x}, Commute ((⋯.monodromyPerm x) γ) ((⋯.toPermFiber x) g)
-- Lean.Level
Lean.Level.succ.inj : ∀ {a a_1 : Lean.Level}, a.succ = a_1.succ → a = a_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- 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_15.eq_3 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (distance : ℕ) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.rotateRight distance with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_3 distance
-- Batteries.Tactic.Congr
/-- If `closePost := true`, it will try again on goals on which `congr` failed to make progress
with default transparency.  -/
Batteries.Tactic.Congr.Config.closePost : Batteries.Tactic.Congr.Config → Bool
-- Init.Prelude
/-- The `<*` operator is overloaded using `seqLeft`.

When thinking about `f` as potential side effects, `<*` evaluates first the left and then the right
argument for their side effects, discarding the value of the right argument and returning the value
of the left argument.

For most applications, `Applicative` or `Monad` should be used rather than `SeqLeft` itself.
 -/
SeqLeft : (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrRight.eq_1 : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N₁]
  [inst_2 : AddCommMonoid N₂] (e : N₁ ≃+ N₂),
  e.addMonoidHomCongrRight = { toEquiv := e.addMonoidHomCongrRightEquiv, map_add' := ⋯ }
-- Mathlib.NumberTheory.RamificationInertia.Ramification
_private.Mathlib.NumberTheory.RamificationInertia.Ramification.0.Ideal.termF : Lean.ParserDescr
-- Mathlib.Algebra.Notation.Prod
Prod.sub_def : ∀ {G : Type u_8} {H : Type u_9} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), a - b = (a.1 - b.1, a.2 - b.2)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.textEdits? : Lean.Lsp.InlayHint → Option (Array Lean.Lsp.TextEdit)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instWeaklyLocallyCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [WeaklyLocallyCompactSpace M], WeaklyLocallyCompactSpace Mᵈᵐᵃ
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- Build a `BialgEquiv` from an isomorphism in the category
`BialgCat R`.  -/
CategoryTheory.Iso.toBialgEquiv : {R : Type u} → [inst : CommRing R] → {X Y : BialgCat R} → (X ≅ Y) → X.carrier ≃ₐc[R] Y.carrier
-- Mathlib.Data.Finset.Card
Finset.card_union_le : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).card ≤ s.card + t.card
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WindowClientCapabilities.mk.inj : ∀ {showDocument? showDocument?_1 : Option Lean.Lsp.ShowDocumentClientCapabilities},
  { showDocument? := showDocument? } = { showDocument? := showDocument?_1 } → showDocument? = showDocument?_1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- (General) non-primitive corecursor for `Seq α` that allows using a friendly operation in the
tail of the corecursive definition.  -/
Tactic.ComputeAsymptotics.Seq.gcorec : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      (β → Option (α × γ × β)) →
        (op : γ → Stream'.Seq α → Stream'.Seq α) →
          [Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass op] → β → Stream'.Seq α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- The open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace  -/
UpperHalfPlane.termℍ : Lean.ParserDescr
-- Mathlib.RingTheory.Algebraic.Pi
polynomial_smul_apply' : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : SMul S T] (p : Polynomial R) (f : S → T) (x : S), (p • f) x = (Polynomial.aeval x) p • f x
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.mul_continuousOn : ∀ {X : Type u_1} {R : Type u_8} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] [inst_5 : NormedRing R]
  [SecondCountableTopologyEither X R] {f g : X → R} {s : Set X},
  MeasureTheory.LocallyIntegrableOn f s μ →
    ContinuousOn g s → IsLocallyClosed s → MeasureTheory.LocallyIntegrableOn (fun x => f x * g x) s μ
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq.eq_1 : ∀ (a b : Lean.Grind.AC.Var), Lean.Grind.AC.instBEqSeq.beq (Lean.Grind.AC.Seq.var a) (Lean.Grind.AC.Seq.var b) = (a == b)
-- Mathlib.Tactic.Translate.Core
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.elabRename.elabRule : Lean.Name →
  Array Lean.Name →
    Lean.NameMap Lean.Name → Lean.TSyntax `Mathlib.Tactic.Translate.renameRule → Lean.MetaM (Lean.NameMap Lean.Name)
-- Mathlib.RingTheory.MvPolynomial.Basic
/-- The submodule of polynomials that are sum of monomials in the set `s`.  -/
MvPolynomial.restrictSupport : {σ : Type u} → (R : Type v) → [inst : CommSemiring R] → Set (σ →₀ ℕ) → Submodule R (MvPolynomial σ R)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instAddCommGroup : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → AddCommGroup (ContDiffMapSupportedIn E F n K)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_insert_le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.minKey? = some km → (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.Algebra.AlgebraicCard
Algebraic.cardinalMk_le_mul : ∀ (R A : Type u) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing A] [IsDomain A] [inst_4 : Algebra R A]
  [Module.IsTorsionFree R A], Cardinal.mk { x // IsAlgebraic R x } ≤ Cardinal.mk (Polynomial R) * Cardinal.aleph0
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.leftOp_inverse_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ Dᵒᵖ) {X Y : D} (f : X ⟶ Y), e.leftOp.inverse.map f = (e.inverse.map f.op).op
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Construct the expression for an atomic 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.WhiskerRight.of : Mathlib.Tactic.BicategoryLike.Atom → Mathlib.Tactic.BicategoryLike.WhiskerRight