mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.vComp_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.LaxTrans F G) (θ : CategoryTheory.Lax.LaxTrans G H)
  (a : B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapId a))
      (η.vCompNaturality θ (CategoryTheory.CategoryStruct.id a)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (η.vCompApp θ a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (η.vCompApp θ a)).inv
        (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.vCompApp θ a)))
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
/-- If `ι` is a `Fintype`, `κ i` is a family of types indexed by `ι` and `M i` is a family
of modules indexed by `ι`, then the tensor product of the family `κ i →₀ M i` is linearly
equivalent to `∏ i, κ i →₀ ⨂[R] i, M i`.
 -/
PiTensorProduct.ofFinsuppEquiv : {R : Type u_1} →
  {ι : Type u_2} →
    {κ : ι → Type u_3} →
      {M : ι → Type u_4} →
        [inst : CommSemiring R] →
          [Fintype ι] →
            [DecidableEq ι] →
              [(i : ι) → DecidableEq (κ i)] →
                [inst_4 : (i : ι) → AddCommMonoid (M i)] →
                  [inst_5 : (i : ι) → Module R (M i)] →
                    [(i : ι) → DecidableEq (M i)] →
                      (PiTensorProduct R fun i => κ i →₀ M i) ≃ₗ[R] ((i : ι) → κ i) →₀ PiTensorProduct R fun i => M i
-- Init.Data.Array.Count
Array.count_erase_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) (xs : Array α), Array.count a (xs.erase a) = Array.count a xs - 1
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_kronecker : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix m m α) (B : Matrix n n α),
  (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹
-- Mathlib.Data.Set.Subsingleton
ExistsUnique.setSubsingleton : ∀ {α : Type u_1} {p : α → Prop}, ExistsUnique p → {x | p x}.Subsingleton
-- Init.Data.String.Basic
/-- Given a slice `s` and a position on `s`, obtain the corresponding position on `s.copy.`  -/
String.Slice.Pos.copy : {s : String.Slice} → s.Pos → s.copy.Pos
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.dist_eq : ∀ {α : Type u_3} {β : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x y : α),
  dist (h x) (h y) = dist x y
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.one_lt_card_iff_ne_bot : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Finite ↥H], 1 < Nat.card ↥H ↔ H ≠ ⊥
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.intro.sizeOf_spec : sizeOf Lean.Meta.Grind.AttrKind.intro = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_eq_some_get!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} [inst_2 : Inhabited (β a)], t.contains a = true → t.get? a = some (t.get! a)
-- Mathlib.Data.List.Sort
List.sortedLT_iff_nodup_and_sortedLE : ∀ {α : Type u_1} {l : List α} [inst : PartialOrder α], l.SortedLT ↔ l.Nodup ∧ l.SortedLE
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.instTotallySeparatedSpaceOfDiscreteTopology : ∀ (X : Type u_3) [inst : TopologicalSpace X] [DiscreteTopology X], TotallySeparatedSpace (OnePoint X)
-- Lean.Data.SSet
Lean.SSet.toList : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SSet α → List α
-- Mathlib.GroupTheory.CoprodI
Monoid.instCoprodI : {ι : Type u_1} → (M : ι → Type u_2) → [inst : (i : ι) → Monoid (M i)] → Monoid (Monoid.CoprodI M)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.degBound.eq_2 : ∀ (k : ℕ) (D : ℕ → ℕ) (n : ℕ),
  ChevalleyThm.MvPolynomialC.degBound k D n.succ =
    ChevalleyThm.MvPolynomialC.numBound k D (n + 1) ^ ChevalleyThm.MvPolynomialC.numBound k D (n + 1) *
      ChevalleyThm.MvPolynomialC.degBound k D n
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.centerCharacteristic : ∀ {G : Type u_1} [inst : AddGroup G], (AddSubgroup.center G).Characteristic
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.empty.sizeOf_spec : sizeOf LeanSearchClient.LoogleResult.empty = 1
-- Mathlib.Order.DirSupClosed
DirSupInacc.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α),
  DirSupInacc s =
    ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.containsKey.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : List ((a : α) × β a)),
  Std.Internal.List.containsKey a x =
    match x with
    | [] => false
    | ⟨k, snd⟩ :: l => k == a || Std.Internal.List.containsKey a l
-- Mathlib.Algebra.DirectSum.Basic
/-- The canonical isomorphism of a finite direct sum of additive commutative monoids
and the corresponding finite product.  -/
DirectSum.addEquivProd : {ι : Type u_1} →
  [Fintype ι] → (G : ι → Type u_2) → [inst : (i : ι) → AddCommMonoid (G i)] → DirectSum ι G ≃+ ((i : ι) → G i)
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.killComplFun_mul : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} (p q : MvPowerSeries τ R),
  MvPowerSeries.killComplFun e (p * q) = MvPowerSeries.killComplFun e p * MvPowerSeries.killComplFun e q
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_list_sum : ∀ {R : Type u} [inst : Semiring R] (l : List (Polynomial R)) (n : ℕ),
  l.sum.coeff n = (List.map (⇑(Polynomial.lcoeff R n)) l).sum
-- Mathlib.Data.Finset.Sups
Finset.filter_sups_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : DecidableLE α] (s t : Finset α) (a : α),
  {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}
-- Mathlib.Tactic.CategoryTheory.CategoryStar
/-- The syntax `Category* C` creates a new distinct implicit universe parameter `v`, placed
just before any parameters appearing in `C` and its type, and elaborates to `Category.{v} C`.
 -/
Mathlib.Tactic.CategoryStar.«termCategory*__» : Lean.ParserDescr
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.getType : Lean.IR.LocalContext → Lean.IR.VarId → Option Lean.IR.IRType
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionDisabled.mk.inj : ∀ {reason reason_1 : String}, { reason := reason } = { reason := reason_1 } → reason = reason_1
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.instFaithfulSMul : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u_4) [inst_1 : CommRing A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  FaithfulSMul R (FractionRing A)
-- Mathlib.RingTheory.RingHom.Surjective
/-- A surjective ring homomorphism `R →+* S` induces a surjective homomorphism `R_{f⁻¹(P)} →+* S_P`
for every prime ideal `P` of `S`.  -/
RingHom.surjective_localRingHom_of_surjective : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f →
    ∀ (P : Ideal S) [inst_2 : P.IsPrime], Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.flippingIso_inv_toFunctor_obj_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) {X Y : C} (f : X ⟶ Y) (j : D),
  ((CategoryTheory.flippingIso.inv.toFunctor.obj F).map f).app j = (F.obj j).map f
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The opcycles of the short complex `shortComplex` at `E^{n₁}(f₁, f₂, f₃)`
identifies to `opZ^{n₁}(f₂, f₃)`.  -/
CategoryTheory.Abelian.SpectralObject.opcyclesIso : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesIso._auto_1) →
                        (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesIso._auto_3) →
                          (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles ≅ X.opcycles f₂ f₃ n₁
-- Mathlib.Data.List.Sigma
List.kunion.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (x : List (Sigma β)), [].kunion x = x
-- Std.Data.ExtHashMap.Basic
/-- Creates a hash map from an array of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.ExtHashMap.unitOfArray : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Std.ExtHashMap α Unit
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.zeroX_subst_zeroX : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R), PowerSeries.subst F.zeroX F.zeroX = F.zeroX
-- Mathlib.FieldTheory.Normal.Defs
AlgEquiv.restrictNormal_trans : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} {K₃ : Type u_5} [inst_1 : Field K₁]
  [inst_2 : Field K₂] [inst_3 : Field K₃] [inst_4 : Algebra F K₁] [inst_5 : Algebra F K₂] [inst_6 : Algebra F K₃]
  (χ : K₁ ≃ₐ[F] K₂) (ω : K₂ ≃ₐ[F] K₃) (E : Type u_6) [inst_7 : Field E] [inst_8 : Algebra F E] [inst_9 : Algebra E K₁]
  [inst_10 : Algebra E K₂] [inst_11 : Algebra E K₃] [inst_12 : IsScalarTower F E K₁] [inst_13 : IsScalarTower F E K₂]
  [inst_14 : IsScalarTower F E K₃] [inst_15 : Normal F E],
  (χ.trans ω).restrictNormal E = (χ.restrictNormal E).trans (ω.restrictNormal E)
-- Mathlib.Logic.Small.Basic
small_orderDual : ∀ {α : Type u_1} [h : Small.{v, u_1} α], Small.{v, u_1} αᵒᵈ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.dropUntil.eq_def : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v w : V} (x : G.Walk v w) (x_1 : V) (x_2 : x_1 ∈ x.support),
  x.dropUntil x_1 x_2 =
    match w, x, x_1, x_2 with
    | .(v), SimpleGraph.Walk.nil, u, h => ⋯.mpr SimpleGraph.Walk.nil
    | w, SimpleGraph.Walk.cons r p, u, h =>
      if hx : v = u then
        Eq.ndrec (motive := fun u => u ∈ (SimpleGraph.Walk.cons r p).support → G.Walk u w)
          (fun h => SimpleGraph.Walk.cons r p) hx h
      else p.dropUntil u ⋯
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.semilatticeSup.eq_1 : ∀ {E : Type u_3} [inst : Group E], GroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.inter_mem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {s t : Set ((i : ι) → α i)},
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α → s ∩ t ∈ MeasureTheory.measurableCylinders α
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.iff_of_mulEquiv : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_4} [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] {H : Type u_5} [inst_5 : Group H]
  [inst_6 : MulSemiringAction H B] (e : H ≃* G),
  (∀ (h : H) (x : B), e h • x = h • x) → (IsGaloisGroup H A B ↔ IsGaloisGroup G A B)
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identification `unmop X ⊗ - = unmop (mop - ⊗ X)` as a natural isomorphism.  -/
CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : Cᴹᵒᵖ) →
        CategoryTheory.MonoidalCategory.tensorLeft X.unmop ≅
          (CategoryTheory.mopFunctor C).comp
            ((CategoryTheory.MonoidalCategory.tensorRight X).comp (CategoryTheory.unmopFunctor C))
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
/-- The relation used to construct colimits in types for `J : SingleObj G ⥤ Type u` is
equivalent to the `MulAction.orbitRel` equivalence relation on `J.obj (SingleObj.star G)`.  -/
CategoryTheory.Limits.SingleObj.colimitTypeRel_iff_orbitRel : ∀ {G : Type v} [inst : Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u))
  (x y : J.obj (CategoryTheory.SingleObj.star G)),
  J.ColimitTypeRel ⟨CategoryTheory.SingleObj.star G, x⟩ ⟨CategoryTheory.SingleObj.star G, y⟩ ↔
    (MulAction.orbitRel G (J.obj (CategoryTheory.SingleObj.star G))) x y
-- Mathlib.Algebra.Field.Defs
/-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

Do not use this lemma directly. Use `NNRat.smul_def` instead.  -/
DivisionRing.nnqsmul_def : ∀ {K : Type u_2} [self : DivisionRing K] (q : ℚ≥0) (a : K), DivisionRing.nnqsmul q a = ↑q * a
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasProduct_of_hasBiproduct : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} [CategoryTheory.Limits.HasBiproduct F],
  CategoryTheory.Limits.HasProduct F
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioo_succ : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioo a.succ b.succ, f i = ∑ i ∈ Finset.Ioo a b, f i.succ
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of `Order.not_isPredLimit_of_isPredArchimedean`. -/
Order.not_isPredLimit : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α], ¬Order.IsPredLimit a
-- Mathlib.Algebra.Order.Field.Basic
min_div_div_right : ∀ {α : Type u_4} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {c : α},
  0 ≤ c → ∀ (a b : α), min (a / c) (b / c) = min a b / c
-- Std.Http.Data.Status
/-- 500 Internal Server Error
 -/
Std.Http.Status.internalServerError : Std.Http.Status
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
/-- Any nonzero vector can be mapped by a continuous linear map to a nonzero scalar.  -/
SeparatingDual.exists_ne_zero' : ∀ {R : Type u_1} {V : Type u_2} {inst : Ring R} {inst_1 : AddCommGroup V} {inst_2 : TopologicalSpace V}
  {inst_3 : TopologicalSpace R} {inst_4 : Module R V} [self : SeparatingDual R V] (x : V), x ≠ 0 → ∃ f, f x ≠ 0
-- Mathlib.Order.Minimal
setOfPred_minimal_subset : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), {x | Minimal (fun x => x ∈ s) x} ⊆ s
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.roots_C_mul_X_sub_C : ∀ {R : Type u} {a : R} [inst : Field R] (b : R),
  a ≠ 0 → (Polynomial.C a * Polynomial.X - Polynomial.C b).roots = {a⁻¹ * b}
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∩ m₂).getKey? k = if k ∈ m₂ then m₁.getKey? k else none
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_div_cancel : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → b * a / b = a
-- Std.Do.PostCond
/-- Conjunction of exception assertions is defined as pointwise conjunction of the assertions for each
potential exception.
 -/
Std.Do.«term_∧ₑ_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Contraction
transpose_dualTensorHom : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.Dual R M) (m : M),
  Module.Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m)) =
    (dualTensorHom R (Module.Dual R M) (Module.Dual R M)) ((Module.Dual.eval R M) m ⊗ₜ[R] f)
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffWithinAt.mono_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E],
  UniqueDiffWithinAt 𝕜 s x → s ⊆ closure t → UniqueDiffWithinAt 𝕜 t x
-- Mathlib.Tactic.IntervalCases
/-- `intervalCases` proves goal `g` by splitting into cases for each integer between the given bounds.

Parameters:
* `g`: the goal, which can have any type `⊢ tgt` (it works in both proofs and programs)
* `e`: the scrutinee, the expression we are proving is bounded between integers
* `e'`: a version of `e` used for error messages. (This is used by the `interval_cases` frontend
  tactic because it uses a fresh variable for `e`, so it is more helpful to show the
  pre-generalized expression in error messages.)
* `lbs`: A list of candidate lower bound expressions.
  The tactic will automatically pick the best lower bound it can find from the list.
* `ubs`: A list of candidate upper bound expressions.
  The tactic will automatically pick the best upper bound it can find from the list.
* `mustUseBounds`: If true, the tactic will fail if it is unable to parse any of the
  given `ubs` or `lbs` into bounds. If false (the default), these will be silently skipped
  and an error message is only produced if we could not find any bounds (including those supplied
  by the type itself, e.g. if we are working over `Nat` or `Fin n`).

Returns an array of `IntervalCasesSubgoal`, one per subgoal. A subgoal has the following fields:
* `rhs`: the numeral expression for this case
* `value`: the integral value of `rhs`
* `goal`: the subgoal of type `⊢ e = rhs → tgt`

Note that this tactic does not perform any substitution or introduction steps -
all subgoals are in the same context as `goal` itself.
 -/
Mathlib.Tactic.IntervalCases.intervalCases : Lean.MVarId →
  Lean.Expr →
    Lean.Expr →
      Array Lean.Expr →
        Array Lean.Expr → optParam Bool false → Lean.MetaM (Array Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal)
-- Mathlib.Data.UInt
UInt16.toFin_injective : Function.Injective UInt16.toFin
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k fallback = fallback
-- Mathlib.Algebra.Polynomial.Homogenize
/-- Given a polynomial `p : R[X]`, this is the vector `![p₀, p₁]` of homogeneous bivariate
polynomials of degree `p.natDegree` such that `p(x) = p₀(x,1)/p₁(x,1)` and `p₁` is a monomial.  -/
Polynomial.toTupleMvPolynomial : {R : Type u_1} → [inst : CommSemiring R] → Polynomial R → Fin 2 → MvPolynomial (Fin 2) R
-- Mathlib.Data.Int.Bitwise
/-- `lor` takes two integers and returns their bitwise `or`  -/
Int.lor : ℤ → ℤ → ℤ
-- Init.Conv
/-- `delta id1 id2 ...` unfolds all occurrences of `id1`, `id2`, ... in the target.
Like the `delta` tactic, this ignores any definitional equations and uses
primitive delta-reduction instead, which may result in leaking implementation details.
Users should prefer `unfold` for unfolding definitions.  -/
Lean.Parser.Tactic.Conv.delta : Lean.ParserDescr
-- Init.Data.UInt.Bitwise
UInt64.shiftLeft_or : ∀ {a b c : UInt64}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Mathlib.NumberTheory.Divisors
/-- See also `Nat.mem_properDivisors`.  -/
Nat.mem_properDivisors_iff_exists : ∀ {m n : ℕ}, n ≠ 0 → (m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k)
-- Init.Data.Array.Lemmas
Array.flatMap_toList : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → List β},
  List.flatMap f xs.toList = (Array.flatMap (fun a => (f a).toArray) xs).toList
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swap_map_toFun : ∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), (Bipointed.swap.map f).toFun a = f.toFun a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.map_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) CategoryTheory.Limits.biprod.fst =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f
-- Mathlib.Order.CompleteLattice.Basic
biInf_const : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {a : α} {s : Set β}, s.Nonempty → ⨅ i ∈ s, a = a
-- Mathlib.Algebra.Group.Shrink
Shrink.instCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : CommMonoid α],
  Shrink.instCommMonoid = (equivShrink α).symm.commMonoid
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  P.isoModSerre f ↔ P.monoModSerre f
-- Mathlib.Order.Disjoint
Codisjoint.sup_left' : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α} (c : α),
  Codisjoint a b → Codisjoint (c ⊔ a) b
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.mulEquiv_def : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsFreeGroup G], IsFreeGroup.mulEquiv G = ⋯.some.repr.symm
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).getKey? a = if cmp k a = Ordering.eq then none else t.getKey? a
-- Mathlib.Tactic.Simps.Basic
/-- An Expression used by simps for the projection. It must be definitionally equal to an original
projection (or a composition of multiple projections).
These Expressions can contain the universe parameters specified in the first argument of
`structureExt`.  -/
Simps.ProjectionData.expr : Simps.ProjectionData → Lean.Expr
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLiftEquiv_symm_apply : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : IsIntegralClosure B₂ A L₂] [inst_22 : Algebra.IsAlgebraic K L] [inst_23 : Algebra.IsAlgebraic K L₂]
  (σ : B ≃ₐ[A] B₂), ⇑(galLiftEquiv K L L₂ σ).symm = ⇑(galLift K L₂ L ↑σ.symm)
-- Std.Time.Format.DateFormat
/-- PM string (e.g., "PM").  -/
Std.Time.DayPeriodSymbols.pm : Std.Time.DayPeriodSymbols → String
-- Mathlib.FieldTheory.Fixed
FixedBy.subfield_mem_iff : ∀ {M : Type u} [inst : Monoid M] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F] (m : M) (x : F),
  x ∈ FixedBy.subfield F m ↔ m • x = x
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.powerSeriesRingEquiv_coe_apply : ∀ (K : Type u_2) [inst : Field K] (f : PowerSeries K),
  ↑((LaurentSeries.powerSeriesRingEquiv K) f) =
    (LaurentSeries.LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f)
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Return whether `kabstract` uniquely finds pattern `p` in `e` at position `targetPos`.  -/
Mathlib.Tactic.ClickSuggestions.kabstractFindsPositions : Lean.Expr → Lean.Expr → Lean.SubExpr.Pos → Lean.MetaM Bool